Using a sledgehammer to kill a fly

from z3 import *

# Define a boatload of integers
a, b, c, k = Ints('a b c k')
a2, b2, c2, k2 = Ints('a2 b2 c2 k2')

# Ask for a solution directly
solve(And(
    # Ensure positive ints
    a > 0,
    b > 0,
    c > 0,
    k > 0,
    # Our equivalence on squares
    a * a + 5 * k == b * b,
    b * b + 5 * k == c * c,
    # Make sure nothing better exists
    Not(Exists([a2, b2, c2, k2], And(
        b2 < b, # Alternatively change to whatever other conditions you want
        a2 > 0,
        b2 > 0,
        c2 > 0,
        k2 > 0,
        a2 * a2 + 5 * k2 == b2 * b2,
        b2 * b2 + 5 * k2 == c2 * c2
    )))
))