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