begin_problem(Ord). list_of_descriptions. name({*Ord*}). author({*Andreas Abel*}). status(unsatisfiable). description({* Proofs about partial orders. *}). end_of_list. list_of_symbols. predicates[(leq,2),(eq,2),(sup,3)]. end_of_list. list_of_formulae(axioms). % Reflexivity formula(forall([x],leq(x,x))). % Transitivity formula(forall([x,y,z],implies(and(leq(x,y),leq(y,z)),leq(x,z)))). % Equivalence formula(forall([x,y],equiv(and(leq(x,y),leq(y,x)),eq(x,y)))). % Supremum formula(forall([x,y,z], equiv(sup(x,y,z), forall([w],equiv(and(leq(x,w),leq(y,w)),leq(z,w)))))). end_of_list. list_of_formulae(conjectures). % Part 1 formula(forall([x,y,z], implies(eq(x,y), implies(eq(x,z),eq(y,z))))). % Part 2 formula(forall([w,x,y,z], implies(and(sup(x,y,z),sup(x,y,w)),eq(z,w)))). % Part 3 formula(forall([x,y], equiv(leq(x,y), exists([z],and(sup(x,y,z),eq(y,z)))))). end_of_list. end_problem.