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