#!/usr/bin/env python3

from z3 import *

s = Solver()

x = Real('x')
Dx = Real('Dx')
y = Real('y')
Dy = Real('Dy')
z = Real('z')
Dz = Real('Dz')
t0 = Real('t0')
eqT0 = t0 >= 0
eq0x = x + Dx * t0 == (185 * t0) + 147847636573416
eq0y = y + Dy * t0 == (49 * t0) + 190826994408605
eq0z = z + Dz * t0 == (219 * t0) + 140130741291716
t1 = Real('t1')
eqT1 = t1 >= 0
eq1x = x + Dx * t1 == (-26 * t1) + 287509258905812
eq1y = y + Dy * t1 == (31 * t1) + 207449079739538
eq1z = z + Dz * t1 == (8 * t1) + 280539021150559
t2 = Real('t2')
eqT2 = t2 >= 0
eq2x = x + Dx * t2 == (-147 * t2) + 390970075767404
eq2y = y + Dy * t2 == (-453 * t2) + 535711685410735
eq2z = z + Dz * t2 == (-149 * t2) + 404166182422876
#solve for x, y, z, Dx, Dy, Dz, t1, t2, t3.


s.add(eqT0,
      eq0x,
      eq0y,
      eq0z,
      eqT1,
      eq1x,
      eq1y,
      eq1z,
      eqT2,
      eq2x,
      eq2y,
eq2z)

if s.check() == sat:
    print("Solution:", s.model())
else:
    print("No solution found")

print(273997500449219 + 463222539161932 + 239756157786030)