WebSPASS Input Form

There is a detailed description of the syntax and SPASS options available. You can also try the File Upload Form. Last but not least, there is a FAQ.

begin_problem(Pelletier54). list_of_descriptions. name({*Pelletier's Problem No. 54*}). author({*Christoph Weidenbach*}). status(unsatisfiable). description({*Problem taken in revised form from the "Pelletier Collection", Journal of Automated Reasoning, Vol. 2, No. 2, pages 191-216*}). end_of_list. list_of_symbols. predicates[(F,2)]. end_of_list. list_of_formulae(axioms). formula(forall([U],exists([V],forall([W],equiv(F(W,V),equal(W,U)))))). end_of_list. list_of_formulae(conjectures). formula(not(exists([U],forall([V],equiv(F(V,U),forall([W],implies(F(V,W),exists([X],and(F(X,W),not(exists([Y],and(F(Y,W),F(Y,X))))))))))))). end_of_list. % this is a comment. We like comments ;-) list_of_settings(SPASS). {* set_flag(PGiven,1). set_flag(PProblem,0). *} end_of_list. end_problem.

To submit this form, please press this button:

To reset this form to its initial setting, please press this button: