(<=> (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 ?Vlist)
(Sentence@Ol-User%Kif-Meta ?P)
(>= (Length ?Vlist) 1)
(=> (Item ?V ?Vlistp)
(Indvar@Ol-User%Kif-Meta ?V))
(= ?X (Listof 'Kappa ?Vlistp ?P))))
(Exists (?Vlist ?Sv ?P)
(And (List ?Vlist)
(Seqvar@Ol-User%Kif-Meta ?Sv)
(Sentence@Ol-User%Kif-Meta ?P)
(=> (Item ?V ?Vlist)
(Indvar@Ol-User%Kif-Meta ?V))
(= ?X
(Listof 'Kappa
(Append ?Vlist (Listof ?Sv))
?P))))
(Exists (?Vlist ?T)
(And (List ?Vlist)
(Term@Ol-User%Kif-Meta ?T)
(>= (Length ?Vlist) 1)
(=> (Item ?V ?Vlistp)
(Indvar@Ol-User%Kif-Meta ?V))
(= ?X (Listof 'Lambda ?Vlistp ?T))))
(Exists (?Vlist ?Sv ?T)
(And (List ?Vlist)
(Seqvar@Ol-User%Kif-Meta ?Sv)
(Sentence@Ol-User%Kif-Meta ?T)
(=> (Item ?V ?Vlist)
(Indvar@Ol-User%Kif-Meta ?V))
(= ?X
(Listof 'Lambda
(Append ?Vlist (Listof ?Sv))
?T))))))