Failed attempt at getting Z3 to spit out the symmetric group of degree 3

z3_s3_failure.py

from z3 import *
  
# create sort
group = DeclareSort('G')

# create function symbols
iden = Function('e', group)
mult = Function('m', group, group, group)
inv = Function('i', group, group)

# declare the group axioms
x, y, z = Consts('x y z', group)
group_axioms = [ ForAll([x, y, z], mult(x, mult(y, z)) == mult(mult(x, y), z)),
        ForAll(x, mult(x, iden()) == x),
        ForAll(x, mult(iden(), x) == x),
        ForAll(x, mult(x, inv(x)) == iden()),
        ForAll(x, mult(inv(x), x) == iden())]

# add non-commutativity as an "axiom", to try to force z3 to produce a non-commutative group like S_3
non_comm = [ Exists([x, y], mult(x, y) != mult(y, x)) ]

s = Solver()
s.add(group_axioms + non_comm)

# run the checker, hopefully finding an instance?
print(s)
print(s.check())
print(s.model()[group])