theory sTs_1ax
imports Main
begin
nitpick_params [verbose, timeout = 120]

sledgehammer_params [provers = "
  e cvc3 metis smt spass z3 z3_tptp remote_e_sine remote_vampire
", slice=true, verbose=true, isar_proof=true, timeout=120]

declare[[show_brackets=true]]
declare[[show_types=true]]
declare[[show_consts=true]]

typedecl sT

axiomatization
  empty_set::sT and
  inS::"sT => sT => bool" (infixl "\<in>\<^isub>\<sigma>" 55)
  where
  empty_ax:"!(x::sT). ~(x \<in>\<^isub>\<sigma> empty_set)"

theorem --"refute finds a model"
  "~(? x. x \<in>\<^isub>\<sigma> empty_set)"
  nitpick
  refute
  oops

theorem --"metis proves it."
  "~(? x. x \<in>\<^isub>\<sigma> empty_set)"
  by (metis empty_ax)

end