Some silly Z3 scripts I wrote

  from z3 import *
  
  s = Solver()
  s.set("timeout", 600)
  a = Int('a')
  b = Int('b')
  c = Int('c')
  s.add(a > 0)
  s.add(b > 0)
  s.add(c > 0)
  theorem = a ** 3 + b ** 3 != c ** 3
  if s.check(Not(theorem)) == sat:
      print(f"Counterexample: {s.model()}")
  else:
      print("Theorem true")