(documentationentailsEnglishLanguage "The operator of logical entailment. (entails ?FORMULA1 ?FORMULA2) means that ?FORMULA2 can be derived from ?FORMULA1 by means of the proof theory of SUO-KIF.")
(documentationentailsSpanishLanguage "El operador de consecuencia lógica. (entails ?FORMULA1 ?FORMULA2) significa que se puede derivar ?FORMULA2 de ?FORMULA1 por medio de la teoría de la demostración de SUO-KIF.")