set(auto).

formula_list(usable).

-(((all x s(x)) -> (all x t(x))) -> ((exists x -s(x)) | (all x t(x)))).

end_of_list.