(<=> (Pairwise-Disjoint@Ol-User%Kif-Sets @Sets)
(Forall (?S1 ?S2)
(=> (Item ?S1 (Listof @Sets))
(Item ?S2 (Listof @Sets))
(Or (= ?S1 ?S2) (Disjoint@Ol-User%Kif-Sets ?S1 ?S2)))))
(<=> (Composition-Of@Frame-Ontology ?Binary-Relation
?List-Of-Relations)
(And (Binary-Relation@Ol-User%Kif-Relations ?Binary-Relation)
(List ?List-Of-Relations)
(Not (Null ?List-Of-Relations))
(=> (Item ?R ?List-Of-Relations)
(Binary-Relation@Ol-User%Kif-Relations ?R))
(Or (And (Single ?List-Of-Relations)
(= ?Binary-Relation (First ?List-Of-Relations)))
(And (Double ?List-Of-Relations)
(= ?Binary-Relation
(Composition@Ol-User%Kif-Relations
(First (Rest ?List-Of-Relations))
(First ?List-Of-Relations))))
(Exists
(?Left-Sub-Relation)
(And (= ?Binary-Relation
(Composition@Ol-User%Kif-Relations
(Last ?List-Of-Relations)
?Left-Sub-Relation))
(Composition-Of@Frame-Ontology
?Left-Sub-Relation
(Butlast ?List-Of-Relations)))))))
(<=> (Relation-Universe@Frame-Ontology ?Relation)
(And (Relation@Ol-User%Kif-Relations ?Relation)
(Class@Frame-Ontology ?Type-Class)
(Forall (?X)
(<=> (Exists (?Tuple)
(And (Member@Ol-User%Kif-Sets ?Tuple
?Relation)
(Item ?X ?Tuple)))
(Instance-Of@Frame-Ontology ?X ?Type-Class)))))
(<=> (Expression@Ol-User%Kif-Meta ?Expr)
(Or (Word@Ol-User%Kif-Meta ?Expr)
(And (List ?Expr)
(Forall (?Subexpr)
(=> (Item ?Subexpr ?Expr)
(Expression@Ol-User%Kif-Meta ?Subexpr))))))
(<=> (Logterm@Ol-User%Kif-Meta ?X)
(Or (Exists (?P1 ?T1)
(And (Sentence@Ol-User%Kif-Meta ?P1)
(Term@Ol-User%Kif-Meta ?T1)
(= ?X (Listof 'If ?P1 ?T1))))
(Exists (?P1 ?T1 ?T2)
(And (Sentence@Ol-User%Kif-Meta ?P1)
(Term@Ol-User%Kif-Meta ?T1)
(Term@Ol-User%Kif-Meta ?T2)
(= ?X (Listof 'If ?P1 ?T1 ?T2))))
(Exists (?Clist)
(And (List ?Clist)
(=> (Item ?C ?Clist)
(Exists (?P ?T)
(And (Sentence@Ol-User%Kif-Meta ?P)
(Term@Ol-User%Kif-Meta ?T)
(= ?C (Listof ?P ?T)))))
(= ?X (Cons 'Cond ?Clist))))))