added experimental "remote_z3_atp", Sutcliffe's TPTP-syntax-aware wrapper for Z3 -- allows to do head-to-head comparison of Sledgehammer's ATP translation and of Sascha's SMT translation
Bool = FOL +
types bool 0
arities bool :: term
consts tt,ff :: "bool"
end