#!/usr/bin/env python3

from z3 import *

x=Int('x')
y=Int('y')

s=Solver()

exp1=And(Or(x!=7, y!=0), Or(x<6, x>7))
exp2=And(x!=6, x!=7)

s.add(exp1!=exp2)

print (simplify(exp1)) # no luck, the expression doesn't simplified

print (s.check())
#print (s.model())