# coding: utf-8
from z3 import *

# Create an instance of a z3 solver

solver = None

# Declare needed z3 variables

# Add the needed constraints to check equivalence of the two formulae.

# solver.add(...)


# Check and print the result.

result = solver.check()
print(result)
if result == sat:
    print(solver.model())