slow_nsatz.v

(** Most of the ~ 10 minutes in this file are spent reifying the goal. *)
Require Export Coq.nsatz.Nsatz Coq.setoid_ring.Ring_tac Coq.QArith.QArith.
Open Scope Q_scope.

Notation "2" := (1+1).
Notation "3" := (1+1+1).

Notation goal0 := (forall
  x1 y1 x2 y2 x3 y3 a b : Q,
  y1^2-x1^3-a*x1-b == 0 ->
  y2^2-x2^3-a*x2-b == 0 ->
  y3^2-x3^3-a*x3-b == 0->
  ((2 * x2 + x3) * (y3 - y2)) ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
  2 * ((2 * x2 + x3) * (y3 - y2)) * ((2 * x2 + x3) * (y3 - y2)) * (x3 - x2) * (x3 - x2) * (x3 - x2) *
  (x3 - x2) * x2 * x3 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) *
  (x2 - x1) +
  2 * ((2 * x2 + x3) * (y3 - y2)) * ((2 * x2 + x3) * (y3 - y2)) * (x3 - x2) * (x3 - x2) * (x3 - x2) *
  (x3 - x2) * x2 * x1 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) *
  (x2 - x1) -
  2 * ((2 * x2 + x3) * (y3 - y2)) * ((2 * x2 + x3) * (y3 - y2)) * (x3 - x2) * (x3 - x2) * (x3 - x2) *
  (x3 - x2) * x2 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) *
  (y2 - y1) +
  ((2 * x2 + x3) * (y3 - y2)) ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x3 * x3 * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
  2 * ((2 * x2 + x3) * (y3 - y2)) * ((2 * x2 + x3) * (y3 - y2)) * (x3 - x2) * (x3 - x2) * (x3 - x2) *
  (x3 - x2) * x3 * x1 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) *
  (x2 - x1) -
  2 * ((2 * x2 + x3) * (y3 - y2)) * ((2 * x2 + x3) * (y3 - y2)) * (x3 - x2) * (x3 - x2) * (x3 - x2) *
  (x3 - x2) * x3 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) *
  (y2 - y1) +
  ((2 * x2 + x3) * (y3 - y2)) ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x1 * x1 * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  2 * ((2 * x2 + x3) * (y3 - y2)) * ((2 * x2 + x3) * (y3 - y2)) * (x3 - x2) * (x3 - x2) * (x3 - x2) *
  (x3 - x2) * x1 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) *
  (y2 - y1) +
  ((2 * x2 + x3) * (y3 - y2)) ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x2 - x1) *
  (x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) -
  2 * ((2 * x2 + x3) * (y3 - y2)) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y2 * x2 *
  x2 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  2 ^ 2 * ((2 * x2 + x3) * (y3 - y2)) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y2 *
  x2 * x3 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  2 ^ 2 * ((2 * x2 + x3) * (y3 - y2)) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y2 *
  x2 * x1 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
  2 ^ 2 * ((2 * x2 + x3) * (y3 - y2)) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y2 *
  x2 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) -
  2 * ((2 * x2 + x3) * (y3 - y2)) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y2 * x3 *
  x3 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  2 ^ 2 * ((2 * x2 + x3) * (y3 - y2)) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y2 *
  x3 * x1 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
  2 ^ 2 * ((2 * x2 + x3) * (y3 - y2)) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y2 *
  x3 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) -
  2 * ((2 * x2 + x3) * (y3 - y2)) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y2 * x1 *
  x1 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
  2 ^ 2 * ((2 * x2 + x3) * (y3 - y2)) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y2 *
  x1 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) -
  2 * ((2 * x2 + x3) * (y3 - y2)) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y2 *
  (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) -
  2 * ((2 * x2 + x3) * (y3 - y2)) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 * x2 *
  x2 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  2 ^ 2 * ((2 * x2 + x3) * (y3 - y2)) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 *
  x2 * x3 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  2 ^ 2 * ((2 * x2 + x3) * (y3 - y2)) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 *
  x2 * x1 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
  2 ^ 2 * ((2 * x2 + x3) * (y3 - y2)) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 *
  x2 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) -
  2 * ((2 * x2 + x3) * (y3 - y2)) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 * x3 *
  x3 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  2 ^ 2 * ((2 * x2 + x3) * (y3 - y2)) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 *
  x3 * x1 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
  2 ^ 2 * ((2 * x2 + x3) * (y3 - y2)) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 *
  x3 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) -
  2 * ((2 * x2 + x3) * (y3 - y2)) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 * x1 *
  x1 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
  2 ^ 2 * ((2 * x2 + x3) * (y3 - y2)) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 *
  x1 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) -
  2 * ((2 * x2 + x3) * (y3 - y2)) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 *
  (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) -
  2 * ((2 * x2 + x3) * (y3 - y2)) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x2 * x2 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  2 ^ 2 * ((2 * x2 + x3) * (y3 - y2)) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x2 *
  x3 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  2 ^ 2 * ((2 * x2 + x3) * (y3 - y2)) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x2 *
  x1 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
  2 ^ 2 * ((2 * x2 + x3) * (y3 - y2)) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x2 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) -
  2 * ((2 * x2 + x3) * (y3 - y2)) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x3 * x3 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  2 ^ 2 * ((2 * x2 + x3) * (y3 - y2)) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x3 *
  x1 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
  2 ^ 2 * ((2 * x2 + x3) * (y3 - y2)) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x3 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) -
  2 * ((2 * x2 + x3) * (y3 - y2)) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x1 * x1 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
  2 ^ 2 * ((2 * x2 + x3) * (y3 - y2)) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x1 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) -
  2 * ((2 * x2 + x3) * (y3 - y2)) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) *
  (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) +
  (x3 - x2) ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y2 * y2 * x2 * x2 * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
  2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y2 * y2 * x2 * x3 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
  2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y2 * y2 * x2 * x1 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y2 * y2 * x2 * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
  (x3 - x2) ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y2 * y2 * x3 * x3 * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
  2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y2 * y2 * x3 * x1 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y2 * y2 * x3 * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
  (x3 - x2) ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y2 * y2 * x1 * x1 * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y2 * y2 * x1 * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
  (x3 - x2) ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y2 * y2 * (x2 - x1) * (x2 - x1) *
  (y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) +
  2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y2 * y1 * x2 * x2 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
  2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y2 * y1 * x2 * x3 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
  2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y2 * y1 * x2 * x1 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y2 * y1 * x2 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
  2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y2 * y1 * x3 * x3 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
  2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y2 * y1 * x3 * x1 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y2 * y1 * x3 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
  2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y2 * y1 * x1 * x1 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y2 * y1 * x1 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
  2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y2 * y1 * (x2 - x1) *
  (x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) +
  (x3 - x2) ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 * y1 * x2 * x2 * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
  2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 * y1 * x2 * x3 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
  2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 * y1 * x2 * x1 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 * y1 * x2 * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
  (x3 - x2) ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 * y1 * x3 * x3 * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
  2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 * y1 * x3 * x1 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 * y1 * x3 * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
  (x3 - x2) ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 * y1 * x1 * x1 * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 * y1 * x1 * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
  (x3 - x2) ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 * y1 * (x2 - x1) * (x2 - x1) *
  (y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) +
  (x3 - x2) ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 * x2 * x2 * x2 * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
  (1 + 2 ^ 2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 * x2 *
  x2 * x3 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
  3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 * x2 * x2 * x1 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 * x2 * x2 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
  2 * (1 + 2 ^ 2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 * x2 *
  x3 * x3 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
  2 * (2 * 3) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 * x2 *
  x3 * x1 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  2 ^ 3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 * x2 * x3 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
  2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 * x2 * x1 * x1 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 * x2 * x1 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
  (x3 - x2) ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 * x2 * (x2 - x1) * (x2 - x1) *
  (y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) +
  2 * (1 + 2 ^ 2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 * x3 *
  x3 * x3 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
  2 * (1 + 2 ^ 3) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 * x3 *
  x3 * x1 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  2 * (2 * 3) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 * x3 *
  x3 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
  2 * 3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 * x3 * x1 * x1 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  2 * (2 * 3) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 * x3 *
  x1 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
  3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 * x3 * (x2 - x1) *
  (x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) -
  2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 * x1 * x1 * x1 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
  (x3 - x2) ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 * x1 * (x2 - x1) * (x2 - x1) *
  (y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) +
  (1 + 2 ^ 2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x3 * x3 *
  x3 * x3 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
  2 * (2 * 3) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x3 * x3 *
  x3 * x1 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  2 ^ 3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x3 * x3 * x3 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
  2 * 3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x3 * x3 * x1 * x1 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  2 * (2 * 3) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x3 * x3 *
  x1 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
  3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x3 * x3 * (x2 - x1) *
  (x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) -
  2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x3 * x1 * x1 * x1 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
  2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x3 * x1 * (x2 - x1) *
  (x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) -
  3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x1 * x1 * x1 * x1 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
  2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x1 * x1 * x1 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) -
  (x3 - x2) ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x1 * x1 * (x2 - x1) * (x2 - x1) *
  (y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) +
  (x3 - x2) ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x3 * x3 * x3 * x3 * x3 * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
  3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x3 * x3 * x3 * x3 * x1 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x3 * x3 * x3 * x3 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
  2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x3 * x3 * x3 * x1 * x1 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x3 * x3 * x3 * x1 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
  (x3 - x2) ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x3 * x3 * x3 * (x2 - x1) * (x2 - x1) *
  (y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) -
  2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x3 * x3 * x1 * x1 * x1 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
  (x3 - x2) ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x3 * x3 * x1 * (x2 - x1) * (x2 - x1) *
  (y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) -
  3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x3 * x1 * x1 * x1 * x1 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
  2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x3 * x1 * x1 * x1 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) -
  (x3 - x2) ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x3 * x1 * x1 * (x2 - x1) * (x2 - x1) *
  (y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) -
  (x3 - x2) ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x1 * x1 * x1 * x1 * x1 * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
  2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x1 * x1 * x1 * x1 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) -
  (x3 - x2) ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x1 * x1 * x1 * (x2 - x1) * (x2 - x1) *
  (y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) -
  3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x2 * x2 * x2 * x2 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  2 * (2 * 3) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x2 * x2 * x2 *
  x3 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  2 ^ 3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x2 * x2 * x2 * x1 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
  2 * 3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x2 * x2 * x2 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) -
  2 * (1 + 2 ^ 3) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x2 * x2 * x3 *
  x3 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  2 * (2 * (2 * 3)) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x2 * x2 *
  x3 * x1 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
  2 * (1 + 2 ^ 3) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x2 * x2 * x3 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) -
  2 * 3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x2 * x2 * x1 * x1 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
  2 * (1 + 2 ^ 2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x2 * x2 * x1 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) -
  3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x2 * x2 * (x2 - x1) *
  (x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) -
  2 * (2 * 3) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x2 * x3 * x3 *
  x3 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  2 * (2 * (2 * 3)) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x2 * x3 *
  x3 * x1 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
  2 * (1 + 2 ^ 3) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x2 * x3 * x3 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) -
  2 * (2 * 3) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x2 * x3 * x1 *
  x1 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
  2 * (2 * (1 + 2 ^ 2)) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x2 *
  x3 * x1 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) -
  2 * 3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x2 * x3 * (x2 - x1) *
  (x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) +
  2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x2 * x1 * x1 * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) -
  2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x2 * x1 * (x2 - x1) *
  (x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) -
  3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x3 * x3 * x3 * x3 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  2 ^ 3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x3 * x3 * x3 * x1 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
  2 * 3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x3 * x3 * x3 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) -
  2 * 3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x3 * x3 * x1 * x1 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
  2 * (1 + 2 ^ 2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x3 * x3 * x1 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) -
  3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x3 * x3 * (x2 - x1) *
  (x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) +
  2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x3 * x1 * x1 * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) -
  2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x3 * x1 * (x2 - x1) *
  (x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) +
  (x3 - x2) ^ 2 * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x1 * x1 * x1 * x1 * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x1 * x1 * x1 * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
  (x3 - x2) ^ 2 * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x1 * x1 * (x2 - x1) * (x2 - x1) *
  (y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) +
  2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * y2 * x2 * x2 * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
  2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * y2 * x2 * x3 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
  2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * y2 * x2 * x1 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * y2 * x2 * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
  2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * y2 * x3 * x3 * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
  2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * y2 * x3 * x1 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * y2 * x3 * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
  2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * y2 * x1 * x1 * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * y2 * x1 * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
  2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * y2 * (x2 - x1) * (x2 - x1) *
  (y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) +
  2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * y1 * x2 * x2 * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
  2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * y1 * x2 * x3 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
  2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * y1 * x2 * x1 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * y1 * x2 * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
  2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * y1 * x3 * x3 * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
  2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * y1 * x3 * x1 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * y1 * x3 * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
  2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * y1 * x1 * x1 * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * y1 * x1 * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
  2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * y1 * (x2 - x1) * (x2 - x1) *
  (y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) +
  3 * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x2 * x2 * x2 * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
  (1 + 2 ^ 3) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x2 * x2 * x3 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
  (1 + 2 * 3) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x2 * x2 * x1 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  2 * 3 * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x2 * x2 * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
  (1 + 2 ^ 3) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x2 * x3 * x3 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
  2 * (1 + 2 * 3) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x2 * x3 * x1 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  2 * (2 * 3) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x2 * x3 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
  (1 + 2 ^ 2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x2 * x1 * x1 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  2 ^ 3 * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x2 * x1 * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
  3 * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x2 * (x2 - x1) * (x2 - x1) *
  (y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) +
  3 * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x3 * x3 * x3 * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
  (1 + 2 * 3) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x3 * x3 * x1 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  2 * 3 * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x3 * x3 * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
  (1 + 2 ^ 2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x3 * x1 * x1 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  2 ^ 3 * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x3 * x1 * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
  3 * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x3 * (x2 - x1) * (x2 - x1) *
  (y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) +
  (x3 - x2) ^ 2 * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x1 * x1 * x1 * (x2 - x1) * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  2 * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x1 * x1 * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
  (x3 - x2) ^ 2 * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x1 * (x2 - x1) * (x2 - x1) * (y2 - y1) *
  (y2 - y1) * (y2 - y1) * (y2 - y1)
  ==
  (x3 - x2) ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 * y1 * x2 * x2 * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
  2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 * y1 * x2 * x3 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
  2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 * y1 * x2 * x1 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
  (x3 - x2) ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 * y1 * x3 * x3 * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
  2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 * y1 * x3 * x1 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
  (x3 - x2) ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 * y1 * x1 * x1 * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
  2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 * x2 * x2 * y3 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 * x2 * x2 *
  ((2 * x1 + x2) * (y2 - y1)) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) *
  (x2 - x1) +
  2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 * x2 * x2 * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) +
  2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 * x2 * x3 * y3 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 * x2 * x3 *
  ((2 * x1 + x2) * (y2 - y1)) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) *
  (x2 - x1) +
  2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 * x2 * x3 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) +
  2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 * x2 * x1 * y3 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 * x2 * x1 *
  ((2 * x1 + x2) * (y2 - y1)) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) *
  (x2 - x1) +
  2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 * x2 * x1 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) +
  2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 * x3 * x3 * y3 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 * x3 * x3 *
  ((2 * x1 + x2) * (y2 - y1)) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) *
  (x2 - x1) +
  2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 * x3 * x3 * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) +
  2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 * x3 * x1 * y3 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 * x3 * x1 *
  ((2 * x1 + x2) * (y2 - y1)) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) *
  (x2 - x1) +
  2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 * x3 * x1 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) +
  2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 * x1 * x1 * y3 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 * x1 * x1 *
  ((2 * x1 + x2) * (y2 - y1)) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) *
  (x2 - x1) +
  2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * y1 * x1 * x1 * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) +
  (x3 - x2) ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 * x2 * x2 * x2 * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
  3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 * x2 * x2 * x3 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
  (1 + 2 ^ 2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 * x2 *
  x2 * x1 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 * x2 * x2 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
  2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 * x2 * x3 * x3 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
  2 * (2 * 3) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 * x2 *
  x3 * x1 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  2 ^ 3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 * x2 * x3 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
  2 * (1 + 2 ^ 2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 * x2 *
  x1 * x1 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  2 * (2 * 3) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 * x2 *
  x1 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
  3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 * x2 * (x2 - x1) *
  (x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) -
  2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 * x3 * x3 * x3 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
  2 * 3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 * x3 * x3 * x1 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  2 * 3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 * x3 * x3 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
  2 * (1 + 2 ^ 3) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 * x3 *
  x1 * x1 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  2 * (2 * (2 * 3)) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 *
  x3 * x1 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
  (1 + 2 * 3) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 * x3 *
  (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) +
  2 * (1 + 2 ^ 2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 * x1 *
  x1 * x1 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  2 * (1 + 2 ^ 3) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 * x1 *
  x1 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
  (1 + 2 ^ 3) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 * x1 *
  (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) +
  (x3 - x2) ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 * y3 * y3 * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 * y3 *
  ((2 * x1 + x2) * (y2 - y1)) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) *
  (x2 - x1) +
  2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 * y3 * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) +
  (x3 - x2) ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 * ((2 * x1 + x2) * (y2 - y1)) *
  ((2 * x1 + x2) * (y2 - y1)) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x2 *
  ((2 * x1 + x2) * (y2 - y1)) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) *
  (y2 - y1) -
  3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x3 * x3 * x3 * x3 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x3 * x3 * x3 * x1 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
  2 * 3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x3 * x3 * x1 * x1 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  2 * (2 * 3) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x3 * x3 *
  x1 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
  (1 + 2 ^ 2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x3 * x3 *
  (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) +
  2 * (2 * 3) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x3 * x1 *
  x1 * x1 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  2 * (2 * (2 * 3)) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x3 *
  x1 * x1 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
  2 * (1 + 2 * 3) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x3 * x1 *
  (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) +
  2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x3 * y3 * y3 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x3 * y3 *
  ((2 * x1 + x2) * (y2 - y1)) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) *
  (x2 - x1) +
  2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x3 * y3 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) +
  2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x3 *
  ((2 * x1 + x2) * (y2 - y1)) * ((2 * x1 + x2) * (y2 - y1)) * (x2 - x1) * (x2 - x1) *
  (x2 - x1) * (x2 - x1) -
  2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x3 *
  ((2 * x1 + x2) * (y2 - y1)) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) *
  (y2 - y1) +
  (1 + 2 ^ 2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x1 * x1 *
  x1 * x1 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  2 * (2 * 3) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x1 * x1 *
  x1 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
  (1 + 2 ^ 3) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x1 * x1 *
  (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) +
  2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x1 * y3 * y3 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x1 * y3 *
  ((2 * x1 + x2) * (y2 - y1)) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) *
  (x2 - x1) +
  2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x1 * y3 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) +
  2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x1 *
  ((2 * x1 + x2) * (y2 - y1)) * ((2 * x1 + x2) * (y2 - y1)) * (x2 - x1) * (x2 - x1) *
  (x2 - x1) * (x2 - x1) -
  2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x2 * x1 *
  ((2 * x1 + x2) * (y2 - y1)) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) *
  (y2 - y1) -
  (x3 - x2) ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x3 * x3 * x3 * x3 * x3 * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x3 * x3 * x3 * x3 * x1 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
  (x3 - x2) ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x3 * x3 * x3 * x3 * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) -
  2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x3 * x3 * x3 * x1 * x1 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
  (x3 - x2) ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x3 * x3 * x3 * (x2 - x1) * (x2 - x1) *
  (y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) +
  2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x3 * x3 * x1 * x1 * x1 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  2 * 3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x3 * x3 * x1 * x1 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
  (1 + 2 ^ 2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x3 * x3 * x1 *
  (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) +
  (x3 - x2) ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x3 * x3 * y3 * y3 * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x3 * x3 * y3 *
  ((2 * x1 + x2) * (y2 - y1)) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) *
  (x2 - x1) +
  2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x3 * x3 * y3 * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) +
  (x3 - x2) ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x3 * x3 * ((2 * x1 + x2) * (y2 - y1)) *
  ((2 * x1 + x2) * (y2 - y1)) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x3 * x3 *
  ((2 * x1 + x2) * (y2 - y1)) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) *
  (y2 - y1) +
  3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x3 * x1 * x1 * x1 * x1 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  2 ^ 3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x3 * x1 * x1 * x1 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
  (1 + 2 * 3) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x3 * x1 * x1 *
  (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) +
  2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x3 * x1 * y3 * y3 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x3 * x1 * y3 *
  ((2 * x1 + x2) * (y2 - y1)) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) *
  (x2 - x1) +
  2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x3 * x1 * y3 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) +
  2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x3 * x1 *
  ((2 * x1 + x2) * (y2 - y1)) * ((2 * x1 + x2) * (y2 - y1)) * (x2 - x1) * (x2 - x1) *
  (x2 - x1) * (x2 - x1) -
  2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x3 * x1 *
  ((2 * x1 + x2) * (y2 - y1)) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) *
  (y2 - y1) +
  (x3 - x2) ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x1 * x1 * x1 * x1 * x1 * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x1 * x1 * x1 * x1 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
  3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x1 * x1 * x1 * (x2 - x1) *
  (x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) +
  (x3 - x2) ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x1 * x1 * y3 * y3 * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x1 * x1 * y3 *
  ((2 * x1 + x2) * (y2 - y1)) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) *
  (x2 - x1) +
  2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x1 * x1 * y3 * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) +
  (x3 - x2) ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x1 * x1 * ((2 * x1 + x2) * (y2 - y1)) *
  ((2 * x1 + x2) * (y2 - y1)) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * x1 * x1 *
  ((2 * x1 + x2) * (y2 - y1)) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) *
  (y2 - y1) -
  2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * y1 * y1 * x2 * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * y1 * y1 * x3 * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * y1 * y1 * x1 * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * y1 * x2 * y3 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
  2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * y1 * x2 *
  ((2 * x1 + x2) * (y2 - y1)) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) *
  (x2 - x1) -
  2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * y1 * x2 * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) -
  2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * y1 * x3 * y3 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
  2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * y1 * x3 *
  ((2 * x1 + x2) * (y2 - y1)) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) *
  (x2 - x1) -
  2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * y1 * x3 * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) -
  2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * y1 * x1 * y3 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
  2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * y1 * x1 *
  ((2 * x1 + x2) * (y2 - y1)) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) *
  (x2 - x1) -
  2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * y1 * x1 * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) -
  2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x2 * x2 * x2 * x2 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x2 * x2 * x2 * x3 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  2 ^ 3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x2 * x2 * x2 * x1 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
  2 * 3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x2 * x2 * x2 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) -
  2 * (2 * 3) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x2 * x2 * x3 *
  x1 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
  2 * (1 + 2 ^ 2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x2 * x2 * x3 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) -
  2 * (2 * 3) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x2 * x2 * x1 *
  x1 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
  2 * (1 + 2 ^ 3) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x2 * x2 * x1 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) -
  2 * 3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x2 * x2 * (x2 - x1) *
  (x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) +
  2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x2 * x3 * x3 * x3 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
  2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x2 * x3 * x3 * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) -
  2 * (2 * 3) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x2 * x3 * x1 *
  x1 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
  2 * (2 * (1 + 2 ^ 2)) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x2 *
  x3 * x1 * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) -
  2 ^ 3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x2 * x3 * (x2 - x1) *
  (x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) -
  2 ^ 3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x2 * x1 * x1 * x1 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
  2 * (1 + 2 ^ 3) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x2 * x1 * x1 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) -
  2 * (2 * 3) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x2 * x1 *
  (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) -
  2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x2 * y3 * y3 * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
  2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x2 * y3 *
  ((2 * x1 + x2) * (y2 - y1)) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) *
  (x2 - x1) -
  2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x2 * y3 * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) -
  2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x2 *
  ((2 * x1 + x2) * (y2 - y1)) * ((2 * x1 + x2) * (y2 - y1)) * (x2 - x1) * (x2 - x1) *
  (x2 - x1) * (x2 - x1) +
  2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x2 *
  ((2 * x1 + x2) * (y2 - y1)) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) *
  (y2 - y1) +
  2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x3 * x3 * x3 * x3 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
  2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x3 * x3 * x3 * x1 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x3 * x3 * x3 * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
  2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x3 * x3 * x1 * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) -
  2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x3 * x3 * (x2 - x1) *
  (x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) -
  2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x3 * x1 * x1 * x1 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
  2 * (1 + 2 ^ 2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x3 * x1 * x1 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) -
  2 ^ 3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x3 * x1 * (x2 - x1) *
  (x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) -
  2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x3 * y3 * y3 * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
  2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x3 * y3 *
  ((2 * x1 + x2) * (y2 - y1)) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) *
  (x2 - x1) -
  2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x3 * y3 * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) -
  2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x3 *
  ((2 * x1 + x2) * (y2 - y1)) * ((2 * x1 + x2) * (y2 - y1)) * (x2 - x1) * (x2 - x1) *
  (x2 - x1) * (x2 - x1) +
  2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x3 *
  ((2 * x1 + x2) * (y2 - y1)) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) *
  (y2 - y1) -
  2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x1 * x1 * x1 * x1 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
  2 * 3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x1 * x1 * x1 *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) -
  2 * 3 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x1 * x1 * (x2 - x1) *
  (x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) -
  2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x1 * y3 * y3 * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
  2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x1 * y3 *
  ((2 * x1 + x2) * (y2 - y1)) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) *
  (x2 - x1) -
  2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x1 * y3 * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) -
  2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x1 *
  ((2 * x1 + x2) * (y2 - y1)) * ((2 * x1 + x2) * (y2 - y1)) * (x2 - x1) * (x2 - x1) *
  (x2 - x1) * (x2 - x1) +
  2 ^ 2 * (x3 - x2) * (x3 - x2) * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * x1 *
  ((2 * x1 + x2) * (y2 - y1)) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) *
  (y2 - y1) +
  (x3 - x2) ^ 2 * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * y1 * y1 * (x2 - x1) * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
  2 * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * y1 * y3 * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  2 * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * y1 *
  ((2 * x1 + x2) * (y2 - y1)) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) *
  (x2 - x1) +
  2 * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * y1 * (x2 - x1) * (x2 - x1) *
  (x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) +
  (x3 - x2) ^ 2 * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x2 * x2 * x2 * (x2 - x1) * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
  (x3 - x2) ^ 2 * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x2 * x2 * x3 * (x2 - x1) * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
  3 * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x2 * x2 * x1 * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  3 * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x2 * x2 * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) -
  (x3 - x2) ^ 2 * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x2 * x3 * x3 * (x2 - x1) * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
  2 * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x2 * x3 * x1 * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  2 * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x2 * x3 * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
  3 * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x2 * x1 * x1 * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  2 * 3 * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x2 * x1 * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
  3 * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x2 * (x2 - x1) * (x2 - x1) *
  (y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) -
  (x3 - x2) ^ 2 * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x3 * x3 * x3 * (x2 - x1) * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  (x3 - x2) ^ 2 * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x3 * x3 * x1 * (x2 - x1) * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) +
  (x3 - x2) ^ 2 * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x3 * x3 * (x2 - x1) * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
  (x3 - x2) ^ 2 * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x3 * x1 * x1 * (x2 - x1) * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  2 * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x3 * x1 * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
  (x3 - x2) ^ 2 * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x3 * (x2 - x1) * (x2 - x1) * (y2 - y1) *
  (y2 - y1) * (y2 - y1) * (y2 - y1) +
  (x3 - x2) ^ 2 * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x1 * x1 * x1 * (x2 - x1) * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  3 * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x1 * x1 * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) +
  3 * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * x1 * (x2 - x1) * (x2 - x1) *
  (y2 - y1) * (y2 - y1) * (y2 - y1) * (y2 - y1) +
  (x3 - x2) ^ 2 * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * y3 * y3 * (x2 - x1) * (x2 - x1) *
  (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  2 * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * y3 *
  ((2 * x1 + x2) * (y2 - y1)) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) *
  (x2 - x1) +
  2 * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * y3 * (x2 - x1) * (x2 - x1) *
  (x2 - x1) * (y2 - y1) * (y2 - y1) * (y2 - y1) +
  (x3 - x2) ^ 2 * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * ((2 * x1 + x2) * (y2 - y1)) *
  ((2 * x1 + x2) * (y2 - y1)) * (x2 - x1) * (x2 - x1) * (x2 - x1) * (x2 - x1) -
  2 * (x3 - x2) * (x3 - x2) * (y3 - y2) * (y3 - y2) * (y3 - y2) * (y3 - y2) *
  ((2 * x1 + x2) * (y2 - y1)) * (x2 - x1) * (x2 - x1) * (y2 - y1) * (y2 - y1) *
  (y2 - y1)) (only parsing).
Require Export List.
Require Export Setoid.
Require Export BinPos.
Require Export BinList.
Require Export Znumtheory.
Require Export Morphisms Setoid Bool.
Require Export Algebra_syntax.
Require Export Ncring.
Require Export Ncring_initial.
Require Export Ncring_tac.
Require Export Integral_domain.
Require Export DiscrR.
Require Export Coq.nsatz.Nsatz.
Require Export AdmitAxiom.

Ltac start :=
  let p := fresh in
  evar (p : Prop); split; [ | exact p ].
Ltac finish :=
  let p := match reverse goal with H := ?e |- _ => let dummy := constr:(ltac:(is_evar e; exact I)) in H end in
  let p0 := (eval cbv delta [p] in p) in
  clear p; repeat match goal with H : _ |- _ => revert H end;
  let g := match goal with |- ?g => g end in
  unify g p0; admit.

Ltac reduce x :=
  lazymatch x with
  | let n := ?v in ?f => reduce (match v with n => f end)
  | ?v => v
  end.
Ltac get_snd y :=
  let x := (eval cbv delta [y] in y) in
  let x := reduce x in
  lazymatch x with
  | (_, ?p) => exact p
  end.
Definition pre_goal1 : goal0 * Prop.
Proof.
  start.
  intros.
  intros;
  apply (@psos_r1b _ _ _ _ _ _ _ _ _ _ _);
  match goal with |- (@equality ?r _ _ _) =>
                  repeat equalities_to_goal  end.
  finish.
Defined.
Definition goal1 : Prop.
Proof. get_snd pre_goal1. Defined.

(*Goal goal0.
  intros.
  Time try nsatz.
Abort.*)

Module A.
Definition pre_goal1 : goal1 * Prop.
  start.
  cbv delta [goal1].
  intros *.

  Ltac nsatz0 r0 :=
    let radicalmax := constr:(6%N) in
    let info := constr:(1%Z) in
    let lparam := constr:(@nil Q) in
    let lvar := constr:(@nil Q) in
    let nparam := eval compute in (Z.of_nat (List.length lparam)) in
        match goal with
          |- ?g => let lb := lterm_goal g in
                 let k := match lvar with
                          |(@nil _) =>
                           match lparam with
                           |(@nil _) =>
                            let r := constr:(list_reifyl (lterm:=lb)) in r
                           end end in pose k as r0 end.
  Time nsatz0 r0.
  finish.
Defined.

Definition goal1 : Prop.
Proof. get_snd pre_goal1. Defined.
End A.