#!/usr/bin/env python3

from z3 import *
a=Bool('a')
b=Bool('b')

s=Solver()

s.add (Or(And(Not(And(a, b)), Or(a, b)), Or((And(a, b)), Not(Or(a, b)))) != True)

print (s.check())

print (simplify(Or(And(Not(And(a, b)), Or(a, b)), Or((And(a, b)), Not(Or(a, b))))))