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