(define x1::int) (assert (and (>= x1 0) (<= x1 2))) (define x2::int) (assert (and (>= x2 3) (<= x2 5))) (define x3::int) (assert (and (>= x3 6) (<= x3 8))) (define x4::int) (assert (and (>= x4 9) (<= x4 13))) (define x5::int) (assert (and (>= x5 14) (<= x5 15))) (define x6::int) (assert (and (>= x6 16) (<= x6 18))) (define x7::int) (assert (and (>= x7 19) (<= x7 24))) (define x8::int) (assert (and (>= x8 25) (<= x8 27))) (define x9::int) (assert (and (>= x9 28) (<= x9 33))) (define x10::int) (assert (and (>= x10 34) (<= x10 38))) (define x11::int) (assert (and (>= x11 39) (<= x11 40))) (define x12::int) (assert (and (>= x12 41) (<= x12 43))) (define x13::int) (assert (and (>= x13 44) (<= x13 53))) (define x14::int) (assert (and (>= x14 54) (<= x14 56))) (define x15::int) (assert (and (>= x15 57) (<= x15 61))) (define x16::int) (assert (and (>= x16 62) (<= x16 63))) (define x17::int) (assert (and (>= x17 64) (<= x17 66))) (define x18::int) (assert (and (>= x18 67) (<= x18 76))) (define x19::int) (assert (and (>= x19 77) (<= x19 84))) (define x20::int) (assert (and (>= x20 85) (<= x20 95))) (define x21::int) (assert (and (>= x21 96) (<= x21 104))) (define x22::int) (assert (and (>= x22 105) (<= x22 106))) (define x23::int) (assert (and (>= x23 107) (<= x23 108))) (define c1::bool (or (/= x18 74) (/= x13 53))) (define c2::bool (or (/= x13 45) (/= x19 77))) (define c3::bool (or (/= x19 83) (/= x21 104))) (define c4::bool (or (/= x19 83) (/= x21 102))) (define c5::bool (or (/= x19 83) (/= x21 103))) (define c6::bool (or (/= x20 89) (/= x20 85))) (define c7::bool (or (/= x19 83) (/= x21 100))) (define c8::bool (or (/= x19 83) (/= x21 101))) (define c9::bool (or (/= x18 74) (/= x13 45))) (define c10::bool (or (/= x19 83) (/= x21 98))) (define c11::bool (or (/= x20 89) (/= x19 79))) (define c12::bool (or (/= x18 74) (/= x13 46))) (define c13::bool (or (/= x19 83) (/= x21 99))) (define c14::bool (or (/= x10 34) (/= x7 24))) (define c15::bool (or (/= x19 84) (/= x21 96))) (define c16::bool (or (/= x20 89) (/= x19 81))) (define c17::bool (or (/= x18 74) (/= x13 47))) (define c18::bool (or (/= x19 81) (/= x20 87))) (define c19::bool (or (/= x18 74) (/= x13 48))) (define c20::bool (or (/= x10 34) (/= x7 22))) (define c21::bool (or (/= x20 89) (/= x19 80))) (define c22::bool (or (/= x19 81) (/= x20 91))) (define c23::bool (or (/= x18 74) (/= x13 52))) (define c24::bool (or (/= x21 101) (/= x20 85))) (define c25::bool (or (/= x20 95) (/= x20 85))) (define c26::bool (or (/= x20 88) (/= x20 85))) (define c27::bool (or (/= x19 82) (/= x21 99))) (define c28::bool (or (/= x19 82) (/= x21 100))) (define c29::bool (or (/= x7 23) (/= x9 33))) (define c30::bool (or (/= x19 82) (/= x21 101))) (define c31::bool (or (/= x20 88) (/= x19 81))) (define c32::bool (or (/= x7 23) (/= x10 34))) (define c33::bool (or (/= x19 82) (/= x21 102))) (define c34::bool (or (/= x20 88) (/= x19 80))) (define c35::bool (or (/= x20 88) (/= x19 79))) (define c36::bool (or (/= x3 7) (/= x2 3))) (define c37::bool (or (/= x13 48) (/= x18 75))) (define c38::bool (or (/= x1 1) (/= x3 8))) (define c39::bool (or (/= x18 72) (/= x13 51))) (define c40::bool (or (/= x18 72) (/= x13 52))) (define c41::bool (or (/= x18 72) (/= x13 53))) (define c42::bool (or (/= x13 48) (/= x18 73))) (define c43::bool (or (/= x13 47) (/= x19 77))) (define c44::bool (or (/= x18 72) (/= x13 48))) (define c45::bool (or (/= x20 91) (/= x19 79))) (define c46::bool (or (/= x19 79) (/= x20 87))) (define c47::bool (or (/= x13 47) (/= x18 75))) (define c48::bool (or (/= x13 47) (/= x18 76))) (define c49::bool (or (/= x13 47) (/= x18 68))) (define c50::bool (or (/= x20 90) (/= x20 85))) (define c51::bool (or (/= x13 47) (/= x18 72))) (define c52::bool (or (/= x13 46) (/= x19 77))) (define c53::bool (or (/= x13 47) (/= x18 73))) (define c54::bool (or (/= x18 73) (/= x13 52))) (define c55::bool (or (/= x13 47) (/= x18 71))) (define c56::bool (or (/= x18 73) (/= x13 51))) (define c57::bool (or (/= x19 80) (/= x20 91))) (define c58::bool (or (/= x19 77) (/= x13 52))) (define c59::bool (or (/= x18 73) (/= x13 49))) (define c60::bool (or (/= x20 90) (/= x19 81))) (define c61::bool (or (/= x20 90) (/= x19 80))) (define c62::bool (or (/= x19 80) (/= x20 87))) (define c63::bool (or (/= x20 90) (/= x19 79))) (define c64::bool (or (/= x19 78) (/= x21 96))) (define c65::bool (or (/= x13 53) (/= x19 77))) (define c66::bool (or (/= x9 29) (/= x7 24))) (define c67::bool (or (/= x13 46) (/= x18 76))) (define c68::bool (or (/= x13 46) (/= x18 75))) (define c69::bool (or (/= x13 46) (/= x18 73))) (define c70::bool (or (/= x9 30) (/= x7 20))) (define c71::bool (or (/= x22 105) (/= x19 79))) (define c72::bool (or (/= x20 85) (/= x20 91))) (define c73::bool (or (/= x22 105) (/= x19 81))) (define c74::bool (or (/= x20 93) (/= x20 85))) (define c75::bool (or (/= x22 105) (/= x19 80))) (define c76::bool (or (/= x9 30) (/= x7 24))) (define c77::bool (or (/= x20 93) (/= x19 79))) (define c78::bool (or (/= x20 93) (/= x19 80))) (define c79::bool (or (/= x20 93) (/= x19 81))) (define c80::bool (or (/= x13 46) (/= x18 72))) (define c81::bool (or (/= x13 46) (/= x18 71))) (define c82::bool (or (/= x20 85) (/= x20 87))) (define c83::bool (or (/= x13 45) (/= x18 76))) (define c84::bool (or (/= x13 45) (/= x18 72))) (define c85::bool (or (/= x13 45) (/= x18 73))) (define c86::bool (or (/= x13 45) (/= x18 75))) (define c87::bool (or (/= x21 97) (/= x19 78))) (define c88::bool (or (/= x21 97) (/= x20 85))) (define c89::bool (or (/= x21 97) (/= x19 84))) (define c90::bool (or (/= x21 97) (/= x19 83))) (define c91::bool (or (/= x21 97) (/= x19 82))) (define c92::bool (or (/= x9 31) (/= x7 20))) (define c93::bool (or (/= x20 92) (/= x19 81))) (define c94::bool (or (/= x20 92) (/= x19 79))) (define c95::bool (or (/= x9 31) (/= x7 24))) (define c96::bool (or (/= x20 92) (/= x19 80))) (define c97::bool (or (/= x14 54) (/= x18 73))) (define c98::bool (or (/= x13 45) (/= x18 71))) (define c99::bool (or (/= x19 78) (/= x21 100))) (define c100::bool (or (/= x19 78) (/= x21 99))) (define c101::bool (or (/= x13 45) (/= x18 69))) (define c102::bool (or (/= x19 78) (/= x21 102))) (define c103::bool (or (/= x19 78) (/= x21 101))) (define c104::bool (or (/= x20 92) (/= x20 85))) (define c105::bool (or (/= x2 3) (/= x3 8))) (define c106::bool (or (/= x19 78) (/= x21 103))) (define c107::bool (or (/= x19 78) (/= x21 104))) (define c108::bool (or (/= x21 98) (/= x19 78))) (define c109::bool (or (/= x21 98) (/= x19 82))) (define c110::bool (or (/= x13 53) (/= x18 73))) (define c111::bool (or (/= x13 51) (/= x19 77))) (define c112::bool (or (/= x13 53) (/= x18 75))) (define c113::bool (or (/= x21 98) (/= x20 85))) (define c114::bool (or (/= x20 95) (/= x19 79))) (define c115::bool (or (/= x20 95) (/= x19 80))) (define c116::bool (or (/= x20 95) (/= x19 81))) (define c117::bool (or (/= x21 103) (/= x19 82))) (define c118::bool (or (/= x7 23) (/= x9 31))) (define c119::bool (or (/= x7 23) (/= x9 29))) (define c120::bool (or (/= x7 23) (/= x9 30))) (define c121::bool (or (/= x21 103) (/= x20 85))) (define c122::bool (or (/= x19 83) (/= x21 96))) (define c123::bool (or (/= x20 85) (/= x21 99))) (define c124::bool (or (/= x18 76) (/= x13 48))) (define c125::bool (or (/= x20 85) (/= x21 100))) (define c126::bool (or (/= x20 85) (/= x21 102))) (define c127::bool (or (/= x13 48) (/= x19 77))) (define c128::bool (or (/= x18 69) (/= x13 47))) (define c129::bool (or (/= x20 94) (/= x19 81))) (define c130::bool (or (/= x20 94) (/= x19 79))) (define c131::bool (or (/= x21 104) (/= x19 82))) (define c132::bool (or (/= x20 94) (/= x19 80))) (define c133::bool (or (/= x20 94) (/= x20 85))) (define c134::bool (or (/= x21 104) (/= x20 85))) (define c135::bool (or (/= x19 84) (/= x21 100))) (define c136::bool (or (/= x19 82) (/= x21 96))) (define c137::bool (or (/= x22 105) (/= x23 107))) (define c138::bool (or (/= x19 84) (/= x21 99))) (define c139::bool (or (/= x19 84) (/= x21 98))) (define c140::bool (or (/= x19 84) (/= x21 104))) (define c141::bool (or (/= x20 86) (/= x19 79))) (define c142::bool (or (/= x19 84) (/= x21 103))) (define c143::bool (or (/= x7 21) (/= x9 31))) (define c144::bool (or (/= x20 86) (/= x19 80))) (define c145::bool (or (/= x19 84) (/= x21 102))) (define c146::bool (or (/= x10 34) (/= x7 21))) (define c147::bool (or (/= x18 72) (/= x14 54))) (define c148::bool (or (/= x20 86) (/= x19 81))) (define c149::bool (or (/= x19 84) (/= x21 101))) (define c150::bool (or (/= x10 34) (/= x7 20))) (define c151::bool (or (/= x20 86) (/= x20 85))) (define c152::bool (or (/= x20 86) (/= x23 107))) (define c153::bool (or (/= x20 93) (/= x21 102))) (define c154::bool (or (/= x20 93) (/= x21 103))) (define c155::bool (or (/= x20 89) (/= x21 101))) (define c156::bool (or (/= x20 89) (/= x21 97))) (define c157::bool (or (/= x20 86) (/= x21 103))) (define c158::bool (or (/= x20 94) (/= x21 103))) (define c159::bool (or (/= x20 91) (/= x21 101))) (define c160::bool (or (/= x20 86) (/= x21 101))) (define c161::bool (or (/= x20 95) (/= x21 101))) (define c162::bool (or (/= x20 92) (/= x23 107))) (define c163::bool (or (/= x20 94) (/= x21 102))) (define c164::bool (or (/= x20 91) (/= x21 97))) (define c165::bool (or (/= x20 88) (/= x21 101))) (define c166::bool (or (/= x20 89) (/= x21 98))) (define c167::bool (or (/= x20 87) (/= x21 97))) (define c168::bool (or (/= x20 89) (/= x21 103))) (define c169::bool (or (/= x20 95) (/= x21 98))) (define c170::bool (or (/= x20 93) (/= x23 107))) (define c171::bool (or (/= x20 90) (/= x21 99))) (define c172::bool (or (/= x20 92) (/= x21 102))) (define c173::bool (or (/= x20 89) (/= x21 100))) (define c174::bool (or (/= x20 94) (/= x21 99))) (define c175::bool (or (/= x20 86) (/= x21 99))) (define c176::bool (or (/= x20 91) (/= x23 107))) (define c177::bool (or (/= x20 92) (/= x21 103))) (define c178::bool (or (/= x20 94) (/= x21 97))) (define c179::bool (or (/= x20 92) (/= x21 98))) (define c180::bool (or (/= x20 94) (/= x23 107))) (define c181::bool (or (/= x20 88) (/= x21 98))) (define c182::bool (or (/= x20 86) (/= x21 102))) (define c183::bool (or (/= x20 86) (/= x21 97))) (define c184::bool (or (/= x19 83) (/= x23 107))) (define c185::bool (or (/= x20 88) (/= x21 97))) (define c186::bool (or (/= x20 91) (/= x21 100))) (define c187::bool (or (/= x20 85) (/= x23 107))) (define c188::bool (or (/= x20 92) (/= x21 99))) (define c189::bool (or (/= x20 87) (/= x21 104))) (define c190::bool (or (/= x20 92) (/= x21 104))) (define c191::bool (or (/= x20 90) (/= x21 97))) (define c192::bool (or (/= x19 84) (/= x23 107))) (define c193::bool (or (/= x20 93) (/= x21 99))) (define c194::bool (or (/= x20 93) (/= x21 100))) (define c195::bool (or (/= x20 90) (/= x21 104))) (define c196::bool (or (/= x19 78) (/= x23 107))) (define c197::bool (or (/= x20 95) (/= x21 104))) (define c198::bool (or (/= x20 90) (/= x21 98))) (define c199::bool (or (/= x20 93) (/= x21 101))) (define c200::bool (or (/= x20 92) (/= x21 101))) (define c201::bool (or (/= x20 88) (/= x23 107))) (define c202::bool (or (/= x20 95) (/= x21 103))) (define c203::bool (or (/= x20 87) (/= x21 101))) (define c204::bool (or (/= x20 90) (/= x21 103))) (define c205::bool (or (/= x20 90) (/= x21 100))) (define c206::bool (or (/= x20 95) (/= x21 97))) (define c207::bool (or (/= x20 87) (/= x21 100))) (define c208::bool (or (/= x20 92) (/= x21 97))) (define c209::bool (or (/= x20 91) (/= x21 98))) (define c210::bool (or (/= x20 95) (/= x23 107))) (define c211::bool (or (/= x20 91) (/= x21 103))) (define c212::bool (or (/= x20 86) (/= x21 104))) (define c213::bool (or (/= x20 94) (/= x21 100))) (define c214::bool (or (/= x20 94) (/= x21 101))) (define c215::bool (or (/= x20 90) (/= x21 101))) (define c216::bool (or (/= x20 94) (/= x21 98))) (define c217::bool (or (/= x20 87) (/= x21 98))) (define c218::bool (or (/= x20 88) (/= x21 99))) (define c219::bool (or (/= x20 89) (/= x23 107))) (define c220::bool (or (/= x20 94) (/= x21 104))) (define c221::bool (or (/= x20 87) (/= x23 107))) (define c222::bool (or (/= x20 91) (/= x21 104))) (define c223::bool (or (/= x20 86) (/= x21 98))) (define c224::bool (or (/= x20 89) (/= x21 102))) (define c225::bool (or (/= x20 93) (/= x21 97))) (define c226::bool (or (/= x20 88) (/= x21 102))) (define c227::bool (or (/= x20 92) (/= x21 100))) (define c228::bool (or (/= x20 90) (/= x21 102))) (define c229::bool (or (/= x20 93) (/= x21 98))) (define c230::bool (or (/= x20 88) (/= x21 100))) (define c231::bool (or (/= x20 91) (/= x21 102))) (define c232::bool (or (/= x20 95) (/= x21 99))) (define c233::bool (or (/= x20 91) (/= x21 99))) (define c234::bool (or (/= x20 90) (/= x23 107))) (define c235::bool (or (/= x20 88) (/= x21 103))) (define c236::bool (or (/= x20 87) (/= x21 103))) (define c237::bool (or (/= x20 87) (/= x21 99))) (define c238::bool (or (/= x20 87) (/= x21 102))) (define c239::bool (or (/= x20 88) (/= x21 104))) (define c240::bool (or (/= x20 86) (/= x21 100))) (define c241::bool (or (/= x20 95) (/= x21 100))) (define c242::bool (or (/= x20 89) (/= x21 104))) (define c243::bool (or (/= x20 93) (/= x21 104))) (define c244::bool (or (/= x20 95) (/= x21 102))) (define c245::bool (or (/= x20 89) (/= x21 99))) (define c246::bool (or (/= x19 82) (/= x23 107))) (assert c1) (assert c2) (assert c3) (assert c4) (assert c5) (assert c6) (assert c7) (assert c8) (assert c9) (assert c10) (assert c11) (assert c12) (assert c13) (assert c14) (assert c15) (assert c16) (assert c17) (assert c18) (assert c19) (assert c20) (assert c21) (assert c22) (assert c23) (assert c24) (assert c25) (assert c26) (assert c27) (assert c28) (assert c29) (assert c30) (assert c31) (assert c32) (assert c33) (assert c34) (assert c35) (assert c36) (assert c37) (assert c38) (assert c39) (assert c40) (assert c41) (assert c42) (assert c43) (assert c44) (assert c45) (assert c46) (assert c47) (assert c48) (assert c49) (assert c50) (assert c51) (assert c52) (assert c53) (assert c54) (assert c55) (assert c56) (assert c57) (assert c58) (assert c59) (assert c60) (assert c61) (assert c62) (assert c63) (assert c64) (assert c65) (assert c66) (assert c67) (assert c68) (assert c69) (assert c70) (assert c71) (assert c72) (assert c73) (assert c74) (assert c75) (assert c76) (assert c77) (assert c78) (assert c79) (assert c80) (assert c81) (assert c82) (assert c83) (assert c84) (assert c85) (assert c86) (assert c87) (assert c88) (assert c89) (assert c90) (assert c91) (assert c92) (assert c93) (assert c94) (assert c95) (assert c96) (assert c97) (assert c98) (assert c99) (assert c100) (assert c101) (assert c102) (assert c103) (assert c104) (assert c105) (assert c106) (assert c107) (assert c108) (assert c109) (assert c110) (assert c111) (assert c112) (assert c113) (assert c114) (assert c115) (assert c116) (assert c117) (assert c118) (assert c119) (assert c120) (assert c121) (assert c122) (assert c123) (assert c124) (assert c125) (assert c126) (assert c127) (assert c128) (assert c129) (assert c130) (assert c131) (assert c132) (assert c133) (assert c134) (assert c135) (assert c136) (assert c137) (assert c138) (assert c139) (assert c140) (assert c141) (assert c142) (assert c143) (assert c144) (assert c145) (assert c146) (assert c147) (assert c148) (assert c149) (assert c150) (assert c151) (assert c152) (assert c153) (assert c154) (assert c155) (assert c156) (assert c157) (assert c158) (assert c159) (assert c160) (assert c161) (assert c162) (assert c163) (assert c164) (assert c165) (assert c166) (assert c167) (assert c168) (assert c169) (assert c170) (assert c171) (assert c172) (assert c173) (assert c174) (assert c175) (assert c176) (assert c177) (assert c178) (assert c179) (assert c180) (assert c181) (assert c182) (assert c183) (assert c184) (assert c185) (assert c186) (assert c187) (assert c188) (assert c189) (assert c190) (assert c191) (assert c192) (assert c193) (assert c194) (assert c195) (assert c196) (assert c197) (assert c198) (assert c199) (assert c200) (assert c201) (assert c202) (assert c203) (assert c204) (assert c205) (assert c206) (assert c207) (assert c208) (assert c209) (assert c210) (assert c211) (assert c212) (assert c213) (assert c214) (assert c215) (assert c216) (assert c217) (assert c218) (assert c219) (assert c220) (assert c221) (assert c222) (assert c223) (assert c224) (assert c225) (assert c226) (assert c227) (assert c228) (assert c229) (assert c230) (assert c231) (assert c232) (assert c233) (assert c234) (assert c235) (assert c236) (assert c237) (assert c238) (assert c239) (assert c240) (assert c241) (assert c242) (assert c243) (assert c244) (assert c245) (assert c246) (check)