begin_problem(sample). list_of_descriptions. name({* sample file *}). author({* Firstname, Lastname, Matrikel *}). status(unsatisfiable). description({* Sample file to show the input syntax of SPASS. *}). end_of_list. list_of_symbols. functions[ % put the function definitions here (f,2),(a,0),(b,0) ]. predicates[ % put the predicate definitions here (P,1), (Q,1) ]. end_of_list. list_of_formulae(axioms). % examples formula(forall([x,y], implies( and( P(x), Q(y) ), P(f(x,y)) ) )). formula(forall([x,y], implies( or( P(x), not(Q(y)) ), not(Q(f(x,y))) ) )). formula(and( P(a), not(Q(b)) )). end_of_list. list_of_formulae(conjectures). formula(exists([x,y], implies( or( P(x), not(Q(y)) ), not(Q(f(x,y))) ) )). end_of_list. list_of_settings(SPASS). {* set_flag(DocProof,1). *} end_of_list. end_problem.