(<=> (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))))))
(<=> (Relsent@Ol-User%Kif-Meta ?X)
(Exists (?R ?Tlist)
(And (Or (Relconst@Ol-User%Kif-Meta ?R)
(Funconst@Ol-User%Kif-Meta ?R))
(List ?Tlist)
(>= (Length ?Tlist) 1)
(=> (Item ?T ?Tlist) (Term@Ol-User%Kif-Meta ?T))
(= ?X (Cons ?R ?Tlist)))))
(<=> (Conjunction@Ol-User%Kif-Meta ?X)
(Exists (?Plist)
(And (List ?Plist)
(>= (Length ?Plist) 1)
(=> (Item ?P ?Plist)
(Sentence@Ol-User%Kif-Meta ?P))
(= ?X (Cons 'And ?Plist)))))
(<=> (Disjunction@Ol-User%Kif-Meta ?X)
(Exists (?Plist)
(And (List ?Plist)
(>= (Length ?Plist) 1)
(=> (Item ?P ?Plist)
(Sentence@Ol-User%Kif-Meta ?P))
(= ?X (Cons 'Or ?Plist)))))
(<=> (Implication@Ol-User%Kif-Meta ?X)
(Exists (?Plist)
(And (List ?Plist)
(>= (Length ?Plist) 2)
(=> (Item ?P ?Plist)
(Sentence@Ol-User%Kif-Meta ?P))
(= ?X (Cons '=> ?Plist)))))