antecedent

(=>     (and         (agreementEffectiveDuring ?AGR ?DATE)         (instance ?TIME ?DATE)         (containsFormula ?AGR ?FORMULA))     (holdsDuring ?TIME ?FORMULA))	Government.kif 738-743	If X is an agreement effective during of Y, Z is an instance of X, and Y contains the formula W, then W holds during Z
(=>     (and         (instance ?CONST             (ConstitutionFn ?COUNTRY))         (instance ?COUNTRY Nation)         (equal ?GOV             (GovernmentFn ?COUNTRY))         (instance             (WhenFn ?GOV) ?CLASS)         (agreementEffectiveDuring ?CONST ?CLASS)         (subProposition ?PART ?CONST)         (containsFormula ?PART ?FORMULA))     (holdsObligation ?GOV ?FORMULA))	Government.kif 745-754	If All of the following hold: (1) X is an instance of the constitution of Y (2) Y is an instance of nation (3) equal Z and the government of Y (4) the time of existence of Z is an instance of W (5) W is an agreement effective during of X (6) V is a sub-proposition of X (7) V contains the formula U, then Z is obliged to perform tasks of type U

Show simplified definition (without tree view)
Show simplified definition (with tree view)