(DEFINE-PRIMITIVE-ROLE R1) (DEFINE-PRIMITIVE-ATTRIBUTE R2) (DEFINE-PRIMITIVE-ROLE R3 :PARENTS R15) (DEFINE-PRIMITIVE-ATTRIBUTE R4) (DEFINE-PRIMITIVE-ATTRIBUTE R5) (DEFINE-PRIMITIVE-ROLE R6 :PARENTS R15) (DEFINE-PRIMITIVE-ROLE R7 :PARENTS R15) (DEFINE-PRIMITIVE-ATTRIBUTE R8) (DEFINE-PRIMITIVE-ROLE R9 :PARENTS R15) (DEFINE-PRIMITIVE-ROLE R10) (DEFINE-PRIMITIVE-ATTRIBUTE R11) (DEFINE-PRIMITIVE-ROLE R12 :PARENTS R15) (DEFINE-PRIMITIVE-ROLE R13) (DEFINE-PRIMITIVE-ROLE R14 :PARENTS R15) (DEFINE-PRIMITIVE-ROLE R15) (DEFINE-PRIMITIVE-ATTRIBUTE R16) (DEFINE-PRIMITIVE-ROLE R17) (DEFINE-PRIMITIVE-ROLE R18 :PARENTS R15) (DEFINE-PRIMITIVE-ROLE R19 :PARENTS R15) (DEFINE-PRIMITIVE-ROLE R20) (DEFINE-PRIMITIVE-ATTRIBUTE R21) (DEFINE-PRIMITIVE-ROLE R22 :PARENTS R15) (DEFINE-PRIMITIVE-ROLE R23) (DEFINE-PRIMITIVE-ROLE R24) (DEFINE-PRIMITIVE-ATTRIBUTE R25 :PARENTS R15) (DEFINE-PRIMITIVE-ROLE R26 :PARENTS R15) (DEFINE-PRIMITIVE-ATTRIBUTE R27) (DEFINE-PRIMITIVE-ROLE R28 :PARENTS R15) (DEFINE-PRIMITIVE-ROLE R29) (DEFINE-PRIMITIVE-ROLE R30 :PARENTS R15) (IMPLIES *TOP* (ALL R26 C4)) (IMPLIES *TOP* (ALL R16 C5)) (IMPLIES *TOP* (ALL R12 C6)) (IMPLIES *TOP* (ALL R4 C37)) (IMPLIES *TOP* (ALL R9 C60)) (IMPLIES *TOP* (ALL R25 C7)) (IMPLIES *TOP* (ALL R7 C58)) (IMPLIES *TOP* (ALL R28 C10)) (IMPLIES *TOP* (ALL R11 C37)) (IMPLIES *TOP* (ALL R22 C55)) (IMPLIES *TOP* (ALL R8 C37)) (IMPLIES *TOP* (ALL R18 C18)) (IMPLIES *TOP* (ALL R14 C19)) (IMPLIES *TOP* (ALL R5 C37)) (IMPLIES *TOP* (ALL R2 C37)) (IMPLIES *TOP* (ALL R27 C38)) (IMPLIES *TOP* (ALL R19 C95)) (IMPLIES *TOP* (ALL R30 C57)) (IMPLIES *TOP* (ALL R6 C54)) (IMPLIES *TOP* (ALL R3 C34)) (DEFINE-CONCEPT C4 (OR C66 C67)) (DEFINE-CONCEPT C5 (OR C63 C62)) (DEFINE-CONCEPT C6 (OR C68 C69)) (DEFINE-CONCEPT C7 (AND (OR C70 C71) (OR (OR (OR (OR C72 C73) C74) C75) C76))) (DEFINE-CONCEPT C8 (AND C70 (OR (OR C74 C75) C76))) (DEFINE-CONCEPT C9 (AND (ALL R29 C10) (SOME R1 C77))) (DEFINE-CONCEPT C10 (SOME R15 C78)) (DEFINE-CONCEPT C11 (AND C10 C79)) (DEFINE-CONCEPT C12 (AND C10 C80)) (DEFINE-CONCEPT C13 (AND C10 C81)) (IMPLIES C14 (AND (ALL R29 C19) (SOME R1 C17))) (IMPLIES (AND (ALL R29 C19) (SOME R1 C17)) C14) (IMPLIES C14 (AND (SOME R1 C17) (SOME R24 C36))) (IMPLIES (AND (SOME R1 C17) (SOME R24 C36)) C14) (DEFINE-CONCEPT C15 (AND (AND C14 (SOME R23 C19)) (ALL R1 C82))) (DEFINE-CONCEPT C16 (AND (AND C14 (SOME R17 C19)) (ALL R1 C83))) (DEFINE-CONCEPT C17 (OR C82 C83)) (DEFINE-CONCEPT C18 (OR C84 C85)) (IMPLIES C18 (AND (AND (AT-LEAST 1 R27) (AT-LEAST 1 R8)) (AT-LEAST 1 R2))) (DEFINE-CONCEPT C19 (OR (OR (OR (OR (OR (OR C20 C86) C21) C87) C88) C89) C23)) (DEFINE-CONCEPT C20 (OR (OR C90 C91) C92)) (DEFINE-CONCEPT C21 (EXACTLY 1 R30)) (DEFINE-CONCEPT C22 (AT-LEAST 2 R30)) (DEFINE-CONCEPT C23 (SOME R5 C93)) (DEFINE-CONCEPT C24 (SOME R5 C40)) (DEFINE-CONCEPT C25 (AND (SOME R2 C40) (SOME R8 C40))) (DEFINE-CONCEPT C26 (AND (SOME R2 C41) (SOME R8 C41))) (DEFINE-CONCEPT C27 (OR C25 C26)) (DEFINE-CONCEPT C28 (AND (SOME R27 C39) (SOME R8 C94))) (DEFINE-CONCEPT C29 (AND C95 (SOME R10 C96))) (DEFINE-CONCEPT C30 (AND C95 (SOME R10 C97))) (DEFINE-CONCEPT C31 (AND C95 (SOME R10 C98))) (DEFINE-CONCEPT C32 (AND C29 (SOME R20 C19))) (DEFINE-CONCEPT C33 (AND C30 (SOME R17 C19))) (DEFINE-CONCEPT C34 (OR C65 C64)) (DEFINE-CONCEPT C35 (OR C99 C100)) (DEFINE-CONCEPT C36 (SOME R13 C35)) (DEFINE-CONCEPT C37 (OR (OR (OR (OR C101 C102) C103) C94) C93)) (DEFINE-CONCEPT C38 (OR (OR (OR (OR C104 C105) C106) C107) C108)) (DEFINE-CONCEPT C39 (OR C105 C106)) (DEFINE-CONCEPT C40 (OR C101 C102)) (DEFINE-CONCEPT C41 (OR C94 C93)) (DEFINE-CONCEPT C42 (OR C109 C110)) (DEFINE-CONCEPT C43 (AND C45 (SOME R15 C100))) (DEFINE-CONCEPT C44 (AND C45 (SOME R15 C35))) (DEFINE-CONCEPT C45 (AND (AND (AND (AND (AND (AND (AND (AND (SOME R15 C15) (SOME R15 C16)) (AT-LEAST 2 R12)) (AT-LEAST 1 R28)) (SOME R15 C9)) (SOME R15 C32)) (SOME R15 C33)) (ALL R18 (OR (AND (AT-LEAST 2 R19) (ALL R19 C31)) (AND (AT-LEAST 1 R19) (ALL R19 C29))))) (ALL R22 (AND (AT-LEAST 2 R19) (ALL R19 C31))))) (IMPLIES C46 (NOT (OR (OR (OR (OR (OR C61 C54) C9) C17) C100) C59))) (DEFINE-CONCEPT C47 (AND (AND (AND (AND (AND (AND (AND (AND (AND (AND (AT-LEAST 1 R3) (AT-LEAST 1 R28)) (AT-LEAST 1 R7)) (AT-LEAST 2 R22)) (AT-LEAST 1 R14)) (AT-LEAST 1 R9)) (AT-LEAST 2 R18)) (AT-MOST 3 R18)) (SOME R18 C84)) (SOME R18 C85)) (SOME R26 C66))) (DEFINE-CONCEPT C48 (AND (AND (AND (AND C47 (NOT C45)) (ALL R15 C46)) (ALL R18 C27)) (ALL R25 C8))) (IMPLIES (AND (AND (AND (AND (AND (AND (AND C48 (ALL R14 C24)) (ALL R18 C25)) (AT-LEAST 2 R12)) (ALL R12 C68)) (ALL R28 C13)) (AT-LEAST 1 R25)) (SOME R21 C42)) C49) (IMPLIES C49 (OR C48 C2)) (DEFINE-CONCEPT C50 (SOME R5 C41)) (DEFINE-CONCEPT C51 (AND (AND (AND (AND (AND (AND (AND C48 (ALL R14 C50)) (ALL R28 C12)) (ALL R18 C26)) (AT-LEAST 2 R12)) (ALL R12 C68)) (AT-LEAST 1 R25)) (SOME R21 C109))) (DEFINE-CONCEPT C52 (AND (AND (AND (AND C48 (ALL R18 C28)) (AT-MOST 0 R25)) (SOME R12 C69)) (SOME R12 C68))) (DEFINE-CONCEPT C3 (AND (AND C48 (AT-MOST 0 R25)) (SOME R26 C62))) (DEFINE-CONCEPT C2 (AND (AND (AND (AND (AND C47 C45) (SOME R15 C61)) (SOME R26 C63)) (SOME R3 (ALL R21 (OR C109 C110)))) (SOME R25 (OR (OR C74 C75) C76)))) (IMPLIES (AND (AND (AND (AND C2 (SOME R14 (ALL R5 (OR C102 C101)))) (SOME R18 (ALL R2 (OR C102 C101)))) (SOME R18 (ALL R8 (OR C102 C101)))) (SOME R28 C13)) C49) (DEFINE-CONCEPT C1 (AND (AND (AND (AND C2 (SOME R14 (ALL R5 (OR C103 C94)))) (SOME R18 (ALL R2 (OR (OR C103 C94) C93)))) (SOME R18 (ALL R8 (OR (OR C103 C94) C93)))) (SOME R28 C12))) (DEFINE-CONCEPT C53 (AND (AND (AND (AND (AND (AND (AND (AND (AND C47 C45) (SOME R12 C69)) (SOME R16 C63)) (SOME R15 C61)) (SOME R28 C11)) (ALL R25 (OR (OR C72 C73) C74))) (SOME R3 (ALL R4 C94))) (SOME R5 (NOT C101))) (AT-LEAST 2 R18))) (IMPLIES C54 (NOT (OR C7 C4 C55 C56 C17 C9 C57 C10 C34 C58 C59 C18 C60 C19 C61 C62 C63 C6 C47))) (IMPLIES C7 (NOT (OR C54 C4 C55 C56 C17 C9 C57 C10 C34 C58 C59 C18 C60 C19 C61 C62 C63 C6 C47))) (IMPLIES C4 (NOT (OR C54 C7 C55 C56 C17 C9 C57 C10 C34 C58 C59 C18 C60 C19 C61 C62 C63 C6 C47))) (IMPLIES C55 (NOT (OR C54 C7 C4 C56 C17 C9 C57 C10 C34 C58 C59 C18 C60 C19 C61 C62 C63 C6 C47))) (IMPLIES C56 (NOT (OR C54 C7 C4 C55 C17 C9 C57 C10 C34 C58 C59 C18 C60 C19 C61 C62 C63 C6 C47))) (IMPLIES C17 (NOT (OR C54 C7 C4 C55 C56 C9 C57 C10 C34 C58 C59 C18 C60 C19 C61 C62 C63 C6 C47))) (IMPLIES C9 (NOT (OR C54 C7 C4 C55 C56 C17 C57 C10 C34 C58 C59 C18 C60 C19 C61 C62 C63 C6 C47))) (IMPLIES C57 (NOT (OR C54 C7 C4 C55 C56 C17 C9 C10 C34 C58 C59 C18 C60 C19 C61 C62 C63 C6 C47))) (IMPLIES C10 (NOT (OR C54 C7 C4 C55 C56 C17 C9 C57 C34 C58 C59 C18 C60 C19 C61 C62 C63 C6 C47))) (IMPLIES C34 (NOT (OR C54 C7 C4 C55 C56 C17 C9 C57 C10 C58 C59 C18 C60 C19 C61 C62 C63 C6 C47))) (IMPLIES C58 (NOT (OR C54 C7 C4 C55 C56 C17 C9 C57 C10 C34 C59 C18 C60 C19 C61 C62 C63 C6 C47))) (IMPLIES C59 (NOT (OR C54 C7 C4 C55 C56 C17 C9 C57 C10 C34 C58 C18 C60 C19 C61 C62 C63 C6 C47))) (IMPLIES C18 (NOT (OR C54 C7 C4 C55 C56 C17 C9 C57 C10 C34 C58 C59 C60 C19 C61 C62 C63 C6 C47))) (IMPLIES C60 (NOT (OR C54 C7 C4 C55 C56 C17 C9 C57 C10 C34 C58 C59 C18 C19 C61 C62 C63 C6 C47))) (IMPLIES C19 (NOT (OR C54 C7 C4 C55 C56 C17 C9 C57 C10 C34 C58 C59 C18 C60 C61 C62 C63 C6 C47))) (IMPLIES C61 (NOT (OR C54 C7 C4 C55 C56 C17 C9 C57 C10 C34 C58 C59 C18 C60 C19 C62 C63 C6 C47))) (IMPLIES C62 (NOT (OR C54 C7 C4 C55 C56 C17 C9 C57 C10 C34 C58 C59 C18 C60 C19 C61 C63 C6 C47))) (IMPLIES C63 (NOT (OR C54 C7 C4 C55 C56 C17 C9 C57 C10 C34 C58 C59 C18 C60 C19 C61 C62 C6 C47))) (IMPLIES C6 (NOT (OR C54 C7 C4 C55 C56 C17 C9 C57 C10 C34 C58 C59 C18 C60 C19 C61 C62 C63 C47))) (IMPLIES C47 (NOT (OR C54 C7 C4 C55 C56 C17 C9 C57 C10 C34 C58 C59 C18 C60 C19 C61 C62 C63 C6))) (IMPLIES C64 (NOT (OR C65))) (IMPLIES C65 (NOT (OR C64)))