#!/usr/bin/env python3

from z3 import *

rx, ry, rz = Ints('rx ry rz')
rvx, rvy, rvz = Ints('rvx rvy rvz')
t0, t1, t2 = Ints('t0 t1 t2')
answer = Int('answer')

solve(
    rx + t0 * rvx == 225415405941969 + t0 * 23,
    ry + t0 * rvy == 400648127977931 + t0 * -204,
    rz + t0 * rvz == 79201130433258 + t0 * 617,

    rx + t1 * rvx == 353783687623292 + t1 * -80,
    ry + t1 * rvy == 138575899489956 + t1 * 156,
    rz + t1 * rvz == 318416438572569 + t1 * 21,

    rx + t2 * rvx == 215751176267772 + t2 * -120,
    ry + t2 * rvy == 376619563956940 + t2 * 126,
    rz + t2 * rvz == 230133299986253 + t2 * -352,

    answer == rx + ry + rz,
)