NWN Group question

solve.py

import z3

# num trinkets = t
# num girls = x

"""
https://imgur.com/a/i9x75EX
The number of trinkets (T) divides evenly by the number of girls (G) and the number of families, which is G-2 (because there are two pairs of sisters, essentially eliminating two girls from the count). Since T is a multiple of G, let's say that T = k*G, where k is some counting number. The number of trinkets per family (T/[G-2]) is five more than the number of trinkets per girl (T/G). In other words,
T/G + 5 = T/(G-2)
Substituting in T = kG and solving for G gives
G = 2 + 2k/5

"""
s = z3.Optimize()
t = z3.Int('t') # total trinkets
x = z3.Int('x') # total girls

s.add(x > 4)
s.add(x < 10)

s.add(t > 0)
s.add(t/x + 5 == t/(x-2))

s.add(t%x == 0)
s.add(t%(x-1) == 0)
s.add()

assert s.check() == z3.sat
m = s.model()
print(m)

# trick is each FAMILY is 1

# answer is t//(x-1) trinkets per girl, x-1 girls