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