from z3 import *

x1,x2,x3 = Bool("x1"), Bool("x2"), Bool("x3")

phi = [ Or(Not(x1), Not(x2)), Or(Not(x1), x2),\
  Or(Not(x1), x3), x1, Or(Not(x3), x2)]

solver = Solver()
solver.set(unsat_core=True)


for i,c in enumerate(phi):
  solver.assert_and_track(c, "phi" + str(i)) 

if solver.check() == z3.unsat:
  uc = solver.unsat_core()
  print(uc) # [phi0, phi1, phi3]