(<=> (>= ?X ?Y) (Or (> ?X ?Y) (= ?X ?Y)))
(=> (Nonnegative-Integer ?X) (>= ?X 0)) (=> (Non-Negative-Integer@Kif-Extensions ?X) (>= ?X 0)) (=> (Nth-Domain@Frame-Ontology ?Relation ?N ?Type) (Forall (?Tuple) (=> (Member@Ol-User%Kif-Sets ?Tuple ?Relation) (And (>= (Length@Ol-User%Kif-Lists ?Tuple) ?N) (Instance-Of@Frame-Ontology (Nth@Ol-User%Kif-Lists ?Tuple ?N) ?Type))))) (=> (Minimum-Value-Cardinality@Frame-Ontology ?Instance ?Binary-Relation ?N) (>= (Value-Cardinality@Frame-Ontology ?Instance ?Binary-Relation) ?N)) (=> (Has-At-Least@Ol-User%Slot-Constraint-Sugar ?Instance ?Binary-Relation ?N) (>= (Value-Cardinality@Frame-Ontology ?Instance ?Binary-Relation) ?N))
(<=> (Non-Negative-Integer@Kif-Extensions ?X) (And (Integer ?X) (>= ?X 0))) (<=> (Nth-Domain@Frame-Ontology ?Relation ?N ?Type) (And (Defined@Ol-User%Kif-Extensions (Arity@Frame-Ontology ?Relation)) (Positive-Integer@Ol-User%Kif-Extensions ?N) (Class@Frame-Ontology ?Type) (Forall (?Tuple) (=> (Member@Ol-User%Kif-Sets ?Tuple ?Relation) (And (>= (Length@Ol-User%Kif-Lists ?Tuple) ?N) (Instance-Of@Frame-Ontology (Nth@Ol-User%Kif-Lists ?Tuple ?N) ?Type)))))) (<=> (Minimum-Value-Cardinality@Frame-Ontology ?Instance ?Binary-Relation ?N) (And (Binary-Relation@Ol-User%Kif-Relations ?Binary-Relation) (Nonnegative-Integer ?N) (>= (Value-Cardinality@Frame-Ontology ?Instance ?Binary-Relation) ?N))) (<=> (Minimum-Slot-Cardinality@Frame-Ontology ?Domain-Class ?Relation ?N) (=> (Instance-Of@Frame-Ontology ?Instance ?Domain-Class) (>= (Value-Cardinality@Frame-Ontology ?Instance ?Relation) ?N))) (<=> (Quanterm@Ol-User%Kif-Meta ?X) (Or (Exists (?T ?P) (And (Term@Ol-User%Kif-Meta ?T) (Sentence@Ol-User%Kif-Meta ?P) (= ?X (Listof 'The ?T ?P)))) (Exists (?T ?P) (And (Term@Ol-User%Kif-Meta ?T) (Sentence@Ol-User%Kif-Meta ?P) (= ?X (Listof 'Setofall ?T ?P)))) (Exists (?Vlist ?P) (And (List@Ol-User%Kif-Lists ?Vlist) (Sentence@Ol-User%Kif-Meta ?P) (>= (Length@Ol-User%Kif-Lists ?Vlist) 1) (=> (Item@Ol-User%Kif-Lists ?V ?Vlistp) (Indvar@Ol-User%Kif-Meta ?V)) (= ?X (Listof 'Kappa ?Vlistp ?P)))) (Exists (?Vlist ?Sv ?P) (And (List@Ol-User%Kif-Lists ?Vlist) (Seqvar@Ol-User%Kif-Meta ?Sv) (Sentence@Ol-User%Kif-Meta ?P) (=> (Item@Ol-User%Kif-Lists ?V ?Vlist) (Indvar@Ol-User%Kif-Meta ?V)) (= ?X (Listof 'Kappa (Append@Ol-User%Kif-Lists ?Vlist (Listof ?Sv)) ?P)))) (Exists (?Vlist ?T) (And (List@Ol-User%Kif-Lists ?Vlist) (Term@Ol-User%Kif-Meta ?T) (>= (Length@Ol-User%Kif-Lists ?Vlist) 1) (=> (Item@Ol-User%Kif-Lists ?V ?Vlistp) (Indvar@Ol-User%Kif-Meta ?V)) (= ?X (Listof 'Lambda ?Vlistp ?T)))) (Exists (?Vlist ?Sv ?T) (And (List@Ol-User%Kif-Lists ?Vlist) (Seqvar@Ol-User%Kif-Meta ?Sv) (Sentence@Ol-User%Kif-Meta ?T) (=> (Item@Ol-User%Kif-Lists ?V ?Vlist) (Indvar@Ol-User%Kif-Meta ?V)) (= ?X (Listof 'Lambda (Append@Ol-User%Kif-Lists ?Vlist (Listof ?Sv)) ?T))))))
(>= (Value-Cardinality@Frame-Ontology ?Instance ?Binary-Relation) 1)