(set-info :smt-lib-version 2.6)
(set-logic QF_LIA)
(set-info :source |
Generated by: Martin Bromberger
Generated on: 2018-01-06
Generator: https://www.mpi-inf.mpg.de/fileadmin/inf/rg1/Documents/RandomUnboundedSageScript.tar.gz
Application: This is a satisfiable problem with bounded and unbounded directions and, therefore, a good test for the termination/completeness of branch-and-bound solvers.
Publications: M. Bromberger. A Reduction from Unbounded Linear Mixed Arithmetic Problems into Bounded Problems. (Work in progress.)

The benchmarks in this class were randomly generated by a sagemath script and by way of construction they are all satisfiable.
Target solver: CVC4 Mathsat SPASS-IQ YICES Z3
|)
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
(set-info :category "random")
(set-info :status sat)
(declare-fun x0 () Int)
(declare-fun x1 () Int)
(declare-fun x2 () Int)
(declare-fun x3 () Int)
(declare-fun x4 () Int)
(declare-fun x5 () Int)
(declare-fun x6 () Int)
(declare-fun x7 () Int)
(declare-fun x8 () Int)
(declare-fun x9 () Int)
(declare-fun x10 () Int)
(declare-fun x11 () Int)
(declare-fun x12 () Int)
(declare-fun x13 () Int)
(declare-fun x14 () Int)
(declare-fun x15 () Int)
(declare-fun x16 () Int)
(declare-fun x17 () Int)
(declare-fun x18 () Int)
(declare-fun x19 () Int)
(declare-fun x20 () Int)
(declare-fun x21 () Int)
(declare-fun x22 () Int)
(declare-fun x23 () Int)
(declare-fun x24 () Int)
(declare-fun x25 () Int)
(declare-fun x26 () Int)
(declare-fun x27 () Int)
(declare-fun x28 () Int)
(declare-fun x29 () Int)
(declare-fun x30 () Int)
(declare-fun x31 () Int)
(declare-fun x32 () Int)
(declare-fun x33 () Int)
(declare-fun x34 () Int)
(declare-fun x35 () Int)
(declare-fun x36 () Int)
(declare-fun x37 () Int)
(declare-fun x38 () Int)
(declare-fun x39 () Int)
(declare-fun x40 () Int)
(declare-fun x41 () Int)
(declare-fun x42 () Int)
(declare-fun x43 () Int)
(declare-fun x44 () Int)
(declare-fun x45 () Int)
(declare-fun x46 () Int)
(declare-fun x47 () Int)
(declare-fun x48 () Int)
(declare-fun x49 () Int)
(declare-fun x50 () Int)
(declare-fun x51 () Int)
(declare-fun x52 () Int)
(declare-fun x53 () Int)
(declare-fun x54 () Int)
(declare-fun x55 () Int)
(declare-fun x56 () Int)
(declare-fun x57 () Int)
(declare-fun x58 () Int)
(declare-fun x59 () Int)
(declare-fun x60 () Int)
(declare-fun x61 () Int)
(declare-fun x62 () Int)
(declare-fun x63 () Int)
(declare-fun x64 () Int)
(declare-fun x65 () Int)
(declare-fun x66 () Int)
(declare-fun x67 () Int)
(declare-fun x68 () Int)
(declare-fun x69 () Int)
(declare-fun x70 () Int)
(declare-fun x71 () Int)
(declare-fun x72 () Int)
(declare-fun x73 () Int)
(declare-fun x74 () Int)
(declare-fun x75 () Int)
(declare-fun x76 () Int)
(declare-fun x77 () Int)
(declare-fun x78 () Int)
(declare-fun x79 () Int)
(declare-fun x80 () Int)
(declare-fun x81 () Int)
(declare-fun x82 () Int)
(declare-fun x83 () Int)
(declare-fun x84 () Int)
(declare-fun x85 () Int)
(declare-fun x86 () Int)
(declare-fun x87 () Int)
(declare-fun x88 () Int)
(declare-fun x89 () Int)
(declare-fun x90 () Int)
(declare-fun x91 () Int)
(declare-fun x92 () Int)
(declare-fun x93 () Int)
(declare-fun x94 () Int)
(declare-fun x95 () Int)
(declare-fun x96 () Int)
(declare-fun x97 () Int)
(declare-fun x98 () Int)
(declare-fun x99 () Int)

(assert (and 
(<= 10 (+ (* (- 1) x1) (+ (* (- 1) x5) (+ (* 1 x6) (+ (* 1 x7) (+ (* (- 2) x9) (+ (* 2 x10) (+ (* 2 x11) (+ (* 1 x12) (+ (* 1 x13) (+ (* (- 2) x14) (+ (* (- 2) x15) (+ (* 2 x16) (+ (* 1 x18) (+ (* (- 1) x20) (+ (* 1 x22) (+ (* (- 1) x23) (+ (* (- 2) x24) (+ (* 2 x27) (+ (* 1 x29) (+ (* 1 x31) (+ (* (- 2) x32) (+ (* (- 1) x33) (+ (* 1 x34) (+ (* (- 1) x35) (+ (* 2 x36) (+ (* 1 x38) (+ (* 1 x39) (+ (* (- 2) x42) (+ (* (- 1) x43) (+ (* 2 x44) (+ (* 2 x46) (+ (* 1 x48) (+ (* 1 x51) (+ (* (- 1) x52) (+ (* (- 2) x54) (+ (* 2 x56) (+ (* 1 x57) (+ (* 1 x58) (+ (* 1 x61) (+ (* (- 1) x64) (+ (* (- 2) x65) (+ (* 1 x66) (+ (* 1 x67) (+ (* (- 1) x68) (+ (* 1 x69) (+ (* 2 x70) (+ (* (- 1) x74) (+ (* (- 1) x75) (+ (* 2 x77) (+ (* (- 1) x78) (+ (* 1 x81) (+ (* 2 x83) (+ (* (- 1) x84) (+ (* 1 x86) (+ (* 2 x88) (+ (* (- 1) x89) (+ (* (- 2) x96) (* (- 1) x99) )))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= 8 (+ (* (- 2) x2) (+ (* 1 x3) (+ (* (- 2) x5) (+ (* 2 x6) (+ (* (- 1) x10) (+ (* 1 x13) (+ (* (- 1) x14) (+ (* 2 x15) (+ (* (- 2) x16) (+ (* 1 x17) (+ (* (- 2) x18) (+ (* (- 1) x20) (+ (* 2 x23) (+ (* (- 1) x25) (+ (* 2 x27) (+ (* (- 2) x33) (+ (* 1 x35) (+ (* (- 1) x36) (+ (* 1 x38) (+ (* 1 x39) (+ (* 1 x40) (+ (* 1 x43) (+ (* 2 x44) (+ (* (- 1) x46) (+ (* (- 1) x47) (+ (* 1 x53) (+ (* 2 x54) (+ (* 1 x55) (+ (* 2 x57) (+ (* (- 2) x58) (+ (* (- 2) x61) (+ (* 2 x64) (+ (* 2 x66) (+ (* (- 2) x67) (+ (* 2 x68) (+ (* (- 2) x69) (+ (* 2 x71) (+ (* 2 x72) (+ (* (- 1) x74) (+ (* (- 2) x75) (+ (* 2 x77) (+ (* (- 2) x78) (+ (* (- 1) x79) (+ (* 1 x80) (+ (* 2 x82) (+ (* 1 x83) (+ (* 1 x84) (+ (* (- 1) x89) (+ (* (- 1) x90) (+ (* 1 x91) (+ (* (- 2) x92) (+ (* 1 x94) (+ (* 1 x96) (+ (* 2 x97) (+ (* 1 x98) (* (- 1) x99) )))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= (- 50) (+ (* (- 1) x0) (+ (* 1 x1) (+ (* 1 x2) (+ (* (- 2) x5) (+ (* 2 x6) (+ (* 1 x8) (+ (* 1 x9) (+ (* (- 2) x10) (+ (* (- 2) x13) (+ (* (- 2) x15) (+ (* (- 2) x16) (+ (* (- 2) x17) (+ (* 1 x20) (+ (* 1 x21) (+ (* (- 1) x24) (+ (* (- 1) x25) (+ (* 1 x26) (+ (* (- 1) x30) (+ (* (- 1) x31) (+ (* (- 1) x32) (+ (* 2 x33) (+ (* 2 x34) (+ (* 2 x37) (+ (* 1 x41) (+ (* 1 x43) (+ (* (- 1) x45) (+ (* 2 x49) (+ (* (- 1) x50) (+ (* (- 2) x55) (+ (* 1 x56) (+ (* 2 x57) (+ (* (- 1) x58) (+ (* 1 x61) (+ (* 2 x62) (+ (* 2 x64) (+ (* 2 x65) (+ (* 2 x67) (+ (* 1 x68) (+ (* (- 1) x70) (+ (* (- 1) x71) (+ (* (- 1) x73) (+ (* (- 1) x74) (+ (* 2 x75) (+ (* (- 2) x76) (+ (* 2 x77) (+ (* 1 x78) (+ (* (- 2) x85) (+ (* 1 x86) (+ (* 2 x87) (+ (* 1 x89) (+ (* 1 x91) (+ (* (- 1) x92) (+ (* 2 x93) (+ (* (- 1) x95) (+ (* 2 x97) (+ (* (- 1) x98) (* (- 2) x99) ))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= (- 32) (+ (* 2 x0) (+ (* (- 2) x2) (+ (* 1 x4) (+ (* (- 1) x5) (+ (* (- 2) x6) (+ (* 1 x7) (+ (* (- 2) x8) (+ (* (- 2) x9) (+ (* 2 x10) (+ (* 2 x12) (+ (* (- 1) x14) (+ (* (- 2) x15) (+ (* (- 1) x16) (+ (* 2 x17) (+ (* 2 x18) (+ (* 1 x19) (+ (* 1 x20) (+ (* 2 x21) (+ (* 2 x22) (+ (* 2 x24) (+ (* 1 x25) (+ (* (- 1) x26) (+ (* 2 x27) (+ (* 2 x28) (+ (* 2 x30) (+ (* 1 x34) (+ (* 2 x35) (+ (* (- 2) x36) (+ (* 2 x37) (+ (* (- 2) x38) (+ (* (- 1) x39) (+ (* 2 x42) (+ (* (- 1) x44) (+ (* 2 x45) (+ (* 1 x46) (+ (* (- 2) x47) (+ (* 1 x48) (+ (* (- 2) x49) (+ (* 1 x51) (+ (* (- 2) x52) (+ (* 1 x56) (+ (* (- 2) x58) (+ (* 1 x59) (+ (* (- 2) x61) (+ (* (- 1) x63) (+ (* 2 x64) (+ (* 2 x65) (+ (* 1 x67) (+ (* 1 x69) (+ (* (- 2) x70) (+ (* 2 x74) (+ (* (- 1) x77) (+ (* 1 x78) (+ (* 2 x81) (+ (* (- 1) x82) (+ (* (- 2) x83) (+ (* 1 x85) (+ (* (- 2) x89) (+ (* (- 2) x92) (+ (* 1 x93) (+ (* 1 x94) (+ (* (- 1) x97) (* 1 x99) ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= (- 23) (+ (* (- 2) x1) (+ (* 1 x2) (+ (* (- 2) x3) (+ (* 1 x4) (+ (* (- 2) x5) (+ (* (- 1) x6) (+ (* (- 2) x11) (+ (* 1 x12) (+ (* (- 1) x13) (+ (* 1 x14) (+ (* (- 1) x15) (+ (* 1 x19) (+ (* (- 2) x23) (+ (* (- 1) x24) (+ (* (- 2) x25) (+ (* 2 x26) (+ (* 2 x27) (+ (* (- 1) x28) (+ (* (- 1) x30) (+ (* (- 2) x31) (+ (* (- 2) x40) (+ (* 2 x42) (+ (* 2 x43) (+ (* (- 2) x44) (+ (* 2 x45) (+ (* 1 x46) (+ (* 1 x49) (+ (* 2 x50) (+ (* 1 x51) (+ (* 1 x52) (+ (* 2 x54) (+ (* 1 x55) (+ (* 1 x56) (+ (* 2 x60) (+ (* 2 x61) (+ (* (- 2) x62) (+ (* 1 x63) (+ (* 2 x64) (+ (* 2 x65) (+ (* (- 1) x67) (+ (* 1 x69) (+ (* (- 2) x71) (+ (* 2 x73) (+ (* (- 2) x74) (+ (* (- 2) x75) (+ (* 1 x76) (+ (* (- 1) x79) (+ (* (- 1) x80) (+ (* 1 x81) (+ (* (- 2) x82) (+ (* (- 1) x83) (+ (* 1 x84) (+ (* (- 2) x86) (+ (* 1 x87) (+ (* 2 x88) (+ (* 2 x90) (+ (* (- 1) x95) (+ (* (- 2) x96) (* 2 x97) ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= (- 28) (+ (* (- 1) x0) (+ (* (- 2) x2) (+ (* (- 2) x5) (+ (* (- 1) x8) (+ (* 2 x10) (+ (* (- 2) x12) (+ (* (- 2) x19) (+ (* (- 2) x21) (+ (* 1 x22) (+ (* 2 x23) (+ (* 1 x24) (+ (* 1 x25) (+ (* (- 1) x27) (+ (* (- 2) x28) (+ (* 2 x30) (+ (* 2 x31) (+ (* 2 x34) (+ (* (- 1) x36) (+ (* (- 2) x37) (+ (* (- 1) x39) (+ (* 2 x40) (+ (* (- 1) x41) (+ (* (- 1) x42) (+ (* 2 x44) (+ (* 2 x46) (+ (* (- 1) x47) (+ (* (- 1) x49) (+ (* 2 x52) (+ (* 1 x53) (+ (* 2 x54) (+ (* 1 x55) (+ (* (- 1) x56) (+ (* 2 x59) (+ (* 1 x61) (+ (* (- 2) x62) (+ (* (- 1) x64) (+ (* 1 x65) (+ (* (- 2) x66) (+ (* (- 1) x67) (+ (* 2 x69) (+ (* (- 1) x72) (+ (* 2 x74) (+ (* 1 x75) (+ (* 1 x78) (+ (* 2 x80) (+ (* (- 2) x81) (+ (* 2 x83) (+ (* 2 x84) (+ (* (- 1) x85) (+ (* 2 x87) (+ (* (- 2) x88) (+ (* 2 x92) (+ (* 2 x93) (+ (* 2 x95) (* (- 2) x99) ))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= 18 (+ (* 2 x2) (+ (* (- 1) x10) (+ (* 2 x11) (+ (* (- 2) x12) (+ (* (- 2) x13) (+ (* (- 1) x14) (+ (* (- 1) x17) (+ (* (- 2) x18) (+ (* (- 2) x20) (+ (* (- 1) x22) (+ (* 1 x23) (+ (* 1 x28) (+ (* (- 2) x30) (+ (* 2 x33) (+ (* (- 2) x35) (+ (* (- 2) x37) (+ (* (- 1) x38) (+ (* 2 x39) (+ (* 1 x42) (+ (* (- 2) x43) (+ (* (- 1) x46) (+ (* 2 x47) (+ (* 2 x51) (+ (* (- 2) x53) (+ (* 2 x55) (+ (* (- 2) x56) (+ (* (- 2) x58) (+ (* 2 x61) (+ (* (- 1) x63) (+ (* (- 1) x64) (+ (* 1 x65) (+ (* 2 x66) (+ (* (- 1) x67) (+ (* (- 1) x69) (+ (* 1 x70) (+ (* 2 x71) (+ (* 2 x72) (+ (* (- 2) x74) (+ (* 2 x77) (+ (* 2 x79) (+ (* (- 1) x81) (+ (* (- 1) x83) (+ (* (- 2) x87) (+ (* (- 2) x90) (+ (* 2 x92) (+ (* (- 2) x93) (+ (* (- 1) x94) (+ (* 1 x96) (+ (* 1 x97) (* (- 2) x99) )))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= 8 (+ (* (- 2) x0) (+ (* (- 1) x1) (+ (* 1 x2) (+ (* (- 1) x3) (+ (* 2 x4) (+ (* 2 x5) (+ (* 2 x9) (+ (* 2 x11) (+ (* (- 1) x12) (+ (* 1 x13) (+ (* (- 2) x16) (+ (* (- 2) x17) (+ (* 2 x18) (+ (* 2 x19) (+ (* 1 x20) (+ (* (- 2) x21) (+ (* (- 1) x22) (+ (* 1 x23) (+ (* (- 1) x24) (+ (* 2 x26) (+ (* 1 x27) (+ (* 2 x28) (+ (* 1 x29) (+ (* (- 1) x33) (+ (* 2 x34) (+ (* 2 x35) (+ (* 2 x36) (+ (* (- 1) x37) (+ (* 2 x38) (+ (* 1 x39) (+ (* (- 2) x41) (+ (* 1 x42) (+ (* 1 x44) (+ (* (- 1) x46) (+ (* 1 x48) (+ (* (- 1) x49) (+ (* (- 1) x51) (+ (* (- 1) x52) (+ (* (- 2) x53) (+ (* (- 2) x54) (+ (* 1 x55) (+ (* (- 2) x56) (+ (* (- 2) x57) (+ (* 2 x58) (+ (* (- 2) x60) (+ (* (- 1) x62) (+ (* (- 1) x65) (+ (* (- 1) x67) (+ (* 2 x68) (+ (* 2 x69) (+ (* 1 x70) (+ (* 1 x71) (+ (* 1 x74) (+ (* 2 x77) (+ (* 2 x78) (+ (* 2 x79) (+ (* 2 x82) (+ (* (- 2) x83) (+ (* (- 1) x84) (+ (* 2 x86) (+ (* 2 x87) (+ (* (- 1) x90) (+ (* (- 2) x91) (+ (* (- 1) x92) (+ (* (- 1) x93) (+ (* 2 x94) (+ (* (- 2) x95) (+ (* (- 1) x96) (* (- 1) x97) ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= (- 1) (+ (* 1 x0) (+ (* 2 x1) (+ (* 1 x4) (+ (* (- 1) x5) (+ (* (- 1) x6) (+ (* 1 x7) (+ (* (- 1) x9) (+ (* (- 2) x10) (+ (* (- 2) x12) (+ (* 1 x14) (+ (* (- 2) x15) (+ (* (- 1) x18) (+ (* 1 x19) (+ (* (- 1) x21) (+ (* 1 x24) (+ (* 1 x26) (+ (* 2 x29) (+ (* (- 2) x32) (+ (* 1 x35) (+ (* (- 1) x40) (+ (* 1 x41) (+ (* 1 x42) (+ (* (- 1) x43) (+ (* (- 2) x45) (+ (* 1 x46) (+ (* 2 x47) (+ (* 2 x48) (+ (* (- 1) x54) (+ (* 1 x56) (+ (* 2 x58) (+ (* 1 x59) (+ (* (- 2) x60) (+ (* 2 x61) (+ (* 1 x62) (+ (* 1 x63) (+ (* 2 x66) (+ (* 1 x69) (+ (* (- 1) x71) (+ (* 2 x72) (+ (* (- 1) x73) (+ (* (- 2) x75) (+ (* (- 1) x76) (+ (* 2 x77) (+ (* 2 x80) (+ (* 2 x81) (+ (* (- 2) x83) (+ (* (- 2) x84) (+ (* 2 x85) (+ (* 2 x86) (+ (* (- 2) x87) (+ (* 1 x88) (+ (* (- 2) x89) (+ (* 1 x91) (+ (* (- 1) x94) (+ (* (- 1) x95) (+ (* (- 1) x98) (* (- 2) x99) ))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= 14 (+ (* (- 1) x6) (+ (* 2 x7) (+ (* (- 2) x8) (+ (* (- 1) x9) (+ (* (- 2) x11) (+ (* 1 x12) (+ (* (- 1) x13) (+ (* 1 x14) (+ (* (- 2) x15) (+ (* (- 1) x16) (+ (* (- 1) x17) (+ (* (- 1) x18) (+ (* 2 x20) (+ (* (- 1) x21) (+ (* 1 x25) (+ (* (- 2) x26) (+ (* (- 1) x28) (+ (* (- 2) x29) (+ (* 1 x32) (+ (* 2 x33) (+ (* 1 x34) (+ (* 1 x36) (+ (* 2 x37) (+ (* (- 2) x41) (+ (* 1 x42) (+ (* (- 1) x44) (+ (* (- 2) x45) (+ (* 1 x48) (+ (* 2 x51) (+ (* 2 x52) (+ (* (- 1) x53) (+ (* (- 2) x54) (+ (* (- 2) x55) (+ (* 2 x56) (+ (* (- 1) x57) (+ (* 2 x59) (+ (* (- 1) x60) (+ (* 2 x61) (+ (* 1 x63) (+ (* 2 x65) (+ (* 2 x66) (+ (* (- 1) x68) (+ (* (- 1) x70) (+ (* (- 2) x71) (+ (* (- 2) x73) (+ (* (- 1) x74) (+ (* 2 x76) (+ (* (- 1) x77) (+ (* (- 2) x78) (+ (* (- 2) x79) (+ (* 1 x80) (+ (* (- 1) x81) (+ (* 2 x82) (+ (* 2 x84) (+ (* 1 x88) (+ (* 2 x90) (+ (* (- 1) x91) (+ (* (- 1) x92) (+ (* (- 2) x94) (+ (* (- 1) x96) (* (- 2) x97) ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= 40 (+ (* (- 1) x0) (+ (* 2 x2) (+ (* (- 2) x3) (+ (* (- 2) x4) (+ (* 1 x6) (+ (* (- 2) x8) (+ (* 2 x11) (+ (* 1 x12) (+ (* 2 x15) (+ (* 1 x19) (+ (* (- 2) x20) (+ (* 2 x22) (+ (* (- 2) x23) (+ (* (- 1) x24) (+ (* 2 x25) (+ (* (- 1) x26) (+ (* 1 x29) (+ (* (- 2) x30) (+ (* (- 2) x31) (+ (* 1 x33) (+ (* (- 2) x35) (+ (* (- 2) x40) (+ (* (- 2) x42) (+ (* 1 x43) (+ (* 2 x46) (+ (* (- 2) x50) (+ (* (- 1) x53) (+ (* 2 x54) (+ (* (- 1) x58) (+ (* (- 2) x60) (+ (* 2 x61) (+ (* (- 1) x63) (+ (* (- 1) x65) (+ (* (- 2) x67) (+ (* (- 1) x68) (+ (* (- 2) x69) (+ (* (- 2) x70) (+ (* (- 2) x72) (+ (* 2 x74) (+ (* (- 2) x77) (+ (* (- 2) x79) (+ (* (- 1) x80) (+ (* 2 x81) (+ (* 2 x83) (+ (* (- 1) x84) (+ (* 1 x86) (+ (* 2 x87) (+ (* 2 x89) (+ (* (- 1) x90) (+ (* 2 x91) (+ (* 1 x92) (+ (* (- 1) x93) (+ (* (- 2) x94) (+ (* 2 x97) (* 2 x99) ))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= 1 (+ (* (- 2) x0) (+ (* 2 x1) (+ (* (- 2) x2) (+ (* (- 1) x4) (+ (* 1 x7) (+ (* (- 1) x8) (+ (* 1 x11) (+ (* 1 x13) (+ (* (- 1) x15) (+ (* 2 x17) (+ (* 2 x18) (+ (* 2 x19) (+ (* (- 2) x20) (+ (* 1 x22) (+ (* (- 2) x24) (+ (* (- 1) x26) (+ (* 2 x27) (+ (* 1 x29) (+ (* (- 2) x31) (+ (* (- 1) x32) (+ (* (- 2) x33) (+ (* 2 x34) (+ (* 1 x35) (+ (* 2 x36) (+ (* (- 1) x38) (+ (* 1 x40) (+ (* 2 x41) (+ (* (- 1) x43) (+ (* (- 2) x45) (+ (* (- 1) x47) (+ (* (- 1) x50) (+ (* 2 x51) (+ (* 2 x52) (+ (* 1 x53) (+ (* (- 1) x54) (+ (* (- 1) x55) (+ (* (- 1) x57) (+ (* (- 2) x58) (+ (* 1 x60) (+ (* (- 1) x64) (+ (* (- 2) x65) (+ (* 1 x66) (+ (* (- 1) x68) (+ (* 1 x69) (+ (* (- 2) x71) (+ (* (- 2) x72) (+ (* 1 x73) (+ (* 2 x76) (+ (* 1 x77) (+ (* (- 1) x78) (+ (* 2 x79) (+ (* (- 2) x81) (+ (* (- 1) x83) (+ (* (- 1) x84) (+ (* 2 x86) (+ (* 2 x87) (+ (* 1 x89) (+ (* 1 x91) (* 1 x94) ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= 45 (+ (* (- 1) x0) (+ (* 1 x2) (+ (* (- 2) x4) (+ (* 1 x5) (+ (* 1 x6) (+ (* 2 x7) (+ (* 1 x8) (+ (* (- 1) x11) (+ (* 1 x12) (+ (* (- 2) x13) (+ (* 2 x15) (+ (* 2 x16) (+ (* (- 2) x17) (+ (* 2 x18) (+ (* (- 2) x19) (+ (* 2 x20) (+ (* 2 x22) (+ (* (- 2) x23) (+ (* (- 1) x24) (+ (* (- 1) x25) (+ (* 1 x26) (+ (* 1 x27) (+ (* (- 2) x28) (+ (* 1 x29) (+ (* (- 2) x32) (+ (* (- 2) x33) (+ (* 2 x34) (+ (* (- 2) x35) (+ (* 1 x40) (+ (* (- 1) x42) (+ (* (- 1) x43) (+ (* 2 x44) (+ (* (- 1) x45) (+ (* (- 2) x46) (+ (* 1 x47) (+ (* (- 2) x48) (+ (* (- 2) x50) (+ (* (- 2) x51) (+ (* (- 1) x54) (+ (* (- 2) x55) (+ (* 2 x57) (+ (* 1 x59) (+ (* (- 1) x62) (+ (* (- 2) x67) (+ (* (- 1) x68) (+ (* (- 1) x72) (+ (* (- 2) x74) (+ (* 1 x75) (+ (* (- 2) x76) (+ (* (- 1) x78) (+ (* 1 x82) (+ (* (- 2) x84) (+ (* (- 2) x88) (+ (* (- 2) x89) (+ (* 2 x93) (+ (* 2 x95) (+ (* (- 2) x97) (* (- 1) x98) )))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= (- 25) (+ (* (- 1) x1) (+ (* (- 2) x3) (+ (* (- 2) x7) (+ (* 2 x10) (+ (* 1 x13) (+ (* 2 x14) (+ (* (- 2) x15) (+ (* 1 x16) (+ (* 2 x17) (+ (* (- 2) x18) (+ (* (- 1) x19) (+ (* (- 1) x20) (+ (* 1 x24) (+ (* (- 2) x28) (+ (* (- 1) x29) (+ (* 1 x30) (+ (* (- 1) x32) (+ (* 1 x34) (+ (* 1 x35) (+ (* (- 1) x39) (+ (* 2 x41) (+ (* 1 x42) (+ (* 2 x43) (+ (* 1 x44) (+ (* 1 x45) (+ (* (- 2) x46) (+ (* (- 1) x48) (+ (* 1 x49) (+ (* 1 x51) (+ (* (- 2) x53) (+ (* (- 1) x54) (+ (* (- 2) x55) (+ (* 2 x56) (+ (* 1 x62) (+ (* 1 x69) (+ (* (- 2) x70) (+ (* 1 x71) (+ (* (- 1) x72) (+ (* (- 1) x74) (+ (* 1 x75) (+ (* 2 x78) (+ (* (- 1) x81) (+ (* (- 2) x82) (+ (* (- 1) x83) (+ (* (- 2) x85) (+ (* (- 2) x86) (+ (* 1 x89) (+ (* (- 1) x91) (+ (* (- 1) x92) (+ (* (- 2) x93) (+ (* 1 x95) (+ (* 2 x96) (* 1 x99) ))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= 5 (+ (* 1 x0) (+ (* 1 x1) (+ (* (- 2) x2) (+ (* 1 x3) (+ (* (- 1) x5) (+ (* (- 2) x6) (+ (* (- 1) x8) (+ (* (- 1) x9) (+ (* 1 x10) (+ (* 1 x11) (+ (* 1 x12) (+ (* (- 2) x14) (+ (* 2 x15) (+ (* (- 2) x16) (+ (* (- 2) x18) (+ (* (- 1) x19) (+ (* 2 x22) (+ (* (- 2) x23) (+ (* 1 x24) (+ (* 2 x25) (+ (* 2 x26) (+ (* 1 x27) (+ (* 2 x30) (+ (* (- 2) x31) (+ (* 2 x34) (+ (* 2 x35) (+ (* (- 2) x37) (+ (* (- 1) x38) (+ (* 2 x41) (+ (* (- 1) x42) (+ (* (- 2) x43) (+ (* 1 x45) (+ (* 2 x46) (+ (* 2 x49) (+ (* 2 x50) (+ (* 1 x52) (+ (* 2 x53) (+ (* 2 x54) (+ (* (- 2) x55) (+ (* 1 x56) (+ (* (- 1) x57) (+ (* 1 x58) (+ (* (- 2) x59) (+ (* (- 2) x60) (+ (* (- 2) x62) (+ (* (- 2) x63) (+ (* (- 2) x64) (+ (* 1 x65) (+ (* (- 2) x66) (+ (* (- 1) x68) (+ (* (- 2) x69) (+ (* (- 1) x70) (+ (* (- 1) x71) (+ (* 1 x72) (+ (* 1 x74) (+ (* 1 x76) (+ (* (- 2) x77) (+ (* (- 1) x79) (+ (* (- 2) x82) (+ (* 2 x85) (+ (* (- 2) x87) (+ (* 1 x89) (+ (* 1 x90) (+ (* 1 x91) (+ (* (- 2) x93) (+ (* (- 1) x94) (* 1 x98) ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= (- 5) (+ (* 1 x0) (+ (* (- 1) x1) (+ (* (- 2) x3) (+ (* 2 x4) (+ (* 1 x8) (+ (* 1 x9) (+ (* 1 x10) (+ (* (- 2) x13) (+ (* (- 1) x14) (+ (* (- 1) x15) (+ (* (- 2) x16) (+ (* 2 x17) (+ (* (- 2) x18) (+ (* 2 x21) (+ (* (- 1) x22) (+ (* 2 x26) (+ (* (- 2) x27) (+ (* (- 1) x28) (+ (* 1 x29) (+ (* (- 2) x31) (+ (* (- 1) x33) (+ (* (- 2) x35) (+ (* (- 2) x36) (+ (* (- 2) x37) (+ (* 2 x38) (+ (* 2 x39) (+ (* 1 x40) (+ (* 1 x41) (+ (* 1 x42) (+ (* (- 2) x43) (+ (* (- 1) x46) (+ (* 2 x47) (+ (* 2 x48) (+ (* 1 x50) (+ (* 2 x51) (+ (* 2 x52) (+ (* (- 1) x53) (+ (* 1 x54) (+ (* 2 x57) (+ (* 2 x58) (+ (* 2 x60) (+ (* 2 x62) (+ (* (- 2) x65) (+ (* (- 1) x66) (+ (* (- 1) x67) (+ (* (- 2) x69) (+ (* (- 2) x70) (+ (* 1 x71) (+ (* 2 x73) (+ (* 1 x75) (+ (* 1 x77) (+ (* (- 1) x80) (+ (* (- 1) x81) (+ (* (- 1) x82) (+ (* 2 x86) (+ (* (- 1) x88) (+ (* 2 x89) (+ (* (- 2) x91) (+ (* (- 2) x92) (+ (* 2 x94) (+ (* 2 x95) (+ (* 2 x96) (* (- 2) x98) ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= 10 (+ (* (- 2) x1) (+ (* 1 x2) (+ (* (- 1) x3) (+ (* (- 2) x7) (+ (* 1 x9) (+ (* (- 1) x12) (+ (* (- 2) x14) (+ (* 1 x15) (+ (* 2 x16) (+ (* 1 x20) (+ (* (- 1) x22) (+ (* 1 x23) (+ (* 2 x24) (+ (* (- 1) x26) (+ (* (- 1) x27) (+ (* 1 x30) (+ (* 1 x33) (+ (* 2 x35) (+ (* (- 1) x37) (+ (* (- 2) x38) (+ (* 2 x41) (+ (* (- 1) x42) (+ (* 1 x44) (+ (* 1 x45) (+ (* 1 x46) (+ (* (- 2) x48) (+ (* (- 1) x53) (+ (* (- 1) x55) (+ (* (- 2) x56) (+ (* (- 1) x58) (+ (* (- 1) x59) (+ (* (- 1) x60) (+ (* 2 x61) (+ (* 2 x62) (+ (* (- 1) x63) (+ (* (- 2) x65) (+ (* (- 1) x66) (+ (* 2 x67) (+ (* (- 2) x69) (+ (* 2 x70) (+ (* 2 x71) (+ (* (- 2) x72) (+ (* (- 1) x74) (+ (* 2 x75) (+ (* 2 x76) (+ (* 2 x84) (+ (* 1 x86) (+ (* (- 1) x87) (+ (* (- 2) x88) (+ (* (- 1) x90) (+ (* (- 1) x93) (+ (* (- 1) x95) (+ (* 2 x96) (+ (* (- 2) x98) (* 1 x99) ))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= (- 48) (+ (* 1 x2) (+ (* (- 2) x4) (+ (* 1 x5) (+ (* 2 x7) (+ (* (- 2) x9) (+ (* 2 x10) (+ (* 1 x11) (+ (* (- 2) x12) (+ (* (- 1) x13) (+ (* 2 x14) (+ (* (- 2) x15) (+ (* (- 1) x17) (+ (* 1 x18) (+ (* 2 x19) (+ (* 1 x20) (+ (* 2 x22) (+ (* (- 1) x23) (+ (* 2 x25) (+ (* (- 2) x29) (+ (* (- 1) x31) (+ (* (- 1) x33) (+ (* 1 x34) (+ (* (- 2) x35) (+ (* (- 2) x36) (+ (* 1 x39) (+ (* (- 1) x41) (+ (* 1 x42) (+ (* 1 x44) (+ (* (- 2) x45) (+ (* (- 1) x46) (+ (* 2 x47) (+ (* (- 1) x48) (+ (* (- 2) x49) (+ (* (- 1) x51) (+ (* (- 2) x54) (+ (* 2 x55) (+ (* (- 1) x56) (+ (* (- 2) x59) (+ (* 2 x60) (+ (* (- 2) x63) (+ (* (- 1) x65) (+ (* (- 2) x66) (+ (* 2 x68) (+ (* 1 x69) (+ (* (- 1) x70) (+ (* 1 x71) (+ (* (- 1) x73) (+ (* (- 2) x76) (+ (* (- 1) x77) (+ (* 2 x80) (+ (* 2 x84) (+ (* (- 1) x89) (+ (* 1 x91) (+ (* (- 2) x92) (+ (* 2 x94) (+ (* (- 1) x95) (+ (* (- 2) x98) (* (- 2) x99) )))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= 30 (+ (* (- 2) x0) (+ (* 2 x1) (+ (* 2 x3) (+ (* 1 x5) (+ (* (- 2) x8) (+ (* (- 2) x13) (+ (* (- 2) x14) (+ (* 1 x18) (+ (* 1 x20) (+ (* (- 1) x22) (+ (* 2 x23) (+ (* 2 x24) (+ (* (- 1) x25) (+ (* 2 x26) (+ (* (- 1) x27) (+ (* (- 1) x28) (+ (* (- 1) x31) (+ (* (- 1) x32) (+ (* (- 2) x33) (+ (* 2 x36) (+ (* 1 x38) (+ (* 2 x39) (+ (* (- 1) x40) (+ (* (- 1) x41) (+ (* (- 1) x42) (+ (* (- 1) x43) (+ (* 1 x44) (+ (* (- 1) x45) (+ (* (- 2) x46) (+ (* (- 2) x47) (+ (* 1 x48) (+ (* (- 2) x49) (+ (* (- 1) x52) (+ (* 1 x55) (+ (* (- 1) x56) (+ (* 2 x57) (+ (* (- 1) x58) (+ (* (- 1) x59) (+ (* 1 x60) (+ (* (- 2) x61) (+ (* (- 1) x63) (+ (* (- 1) x66) (+ (* (- 1) x67) (+ (* (- 2) x69) (+ (* (- 1) x70) (+ (* 1 x73) (+ (* 2 x77) (+ (* (- 2) x78) (+ (* 2 x80) (+ (* (- 1) x81) (+ (* (- 1) x82) (+ (* 2 x83) (+ (* (- 2) x84) (+ (* 2 x85) (+ (* 2 x86) (+ (* 1 x87) (+ (* 1 x88) (+ (* (- 1) x91) (+ (* 2 x92) (+ (* 1 x93) (+ (* (- 1) x94) (+ (* 1 x95) (* (- 2) x97) ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= (- 4) (+ (* 2 x0) (+ (* 2 x1) (+ (* (- 2) x2) (+ (* 1 x3) (+ (* (- 1) x4) (+ (* 1 x5) (+ (* (- 1) x11) (+ (* (- 2) x13) (+ (* 2 x14) (+ (* 1 x17) (+ (* (- 1) x18) (+ (* (- 1) x20) (+ (* (- 1) x22) (+ (* (- 2) x25) (+ (* 2 x26) (+ (* (- 1) x29) (+ (* (- 1) x30) (+ (* (- 1) x31) (+ (* 1 x32) (+ (* (- 1) x33) (+ (* (- 2) x34) (+ (* 1 x37) (+ (* (- 1) x38) (+ (* (- 1) x42) (+ (* 1 x44) (+ (* (- 1) x45) (+ (* 2 x47) (+ (* (- 2) x48) (+ (* (- 2) x49) (+ (* 2 x54) (+ (* 1 x55) (+ (* 1 x56) (+ (* (- 1) x57) (+ (* 1 x58) (+ (* 2 x59) (+ (* 2 x61) (+ (* 1 x63) (+ (* (- 1) x64) (+ (* 1 x65) (+ (* (- 2) x66) (+ (* (- 2) x69) (+ (* 1 x71) (+ (* 2 x72) (+ (* (- 1) x74) (+ (* 2 x78) (+ (* 1 x79) (+ (* 1 x82) (+ (* 2 x83) (+ (* 2 x84) (+ (* 2 x88) (+ (* 2 x89) (+ (* (- 2) x91) (+ (* (- 1) x93) (+ (* (- 1) x94) (+ (* 1 x95) (+ (* 2 x97) (* 2 x99) ))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= (- 2) (+ (* (- 1) x1) (+ (* 1 x2) (+ (* 1 x4) (+ (* (- 1) x5) (+ (* 2 x7) (+ (* (- 1) x8) (+ (* (- 2) x11) (+ (* 2 x13) (+ (* 2 x14) (+ (* (- 2) x15) (+ (* (- 1) x16) (+ (* 1 x17) (+ (* 1 x18) (+ (* 1 x19) (+ (* 1 x20) (+ (* (- 2) x21) (+ (* 1 x22) (+ (* 2 x23) (+ (* 1 x24) (+ (* 2 x25) (+ (* (- 1) x30) (+ (* (- 1) x31) (+ (* 1 x32) (+ (* (- 2) x33) (+ (* 2 x34) (+ (* (- 2) x35) (+ (* 2 x36) (+ (* 2 x40) (+ (* 2 x41) (+ (* (- 2) x43) (+ (* (- 2) x44) (+ (* (- 1) x45) (+ (* (- 2) x48) (+ (* 2 x49) (+ (* (- 1) x50) (+ (* 2 x52) (+ (* (- 1) x53) (+ (* (- 2) x54) (+ (* 2 x55) (+ (* (- 1) x57) (+ (* 2 x59) (+ (* 2 x63) (+ (* 2 x64) (+ (* (- 2) x66) (+ (* 2 x67) (+ (* (- 2) x68) (+ (* 1 x69) (+ (* 2 x70) (+ (* 2 x72) (+ (* (- 2) x74) (+ (* 2 x75) (+ (* (- 2) x76) (+ (* 2 x77) (+ (* 2 x80) (+ (* (- 2) x81) (+ (* (- 2) x83) (+ (* 2 x84) (+ (* 2 x86) (+ (* 1 x87) (+ (* 1 x88) (+ (* (- 2) x89) (+ (* 1 x90) (+ (* (- 1) x92) (+ (* (- 2) x93) (+ (* 2 x94) (+ (* 1 x95) (+ (* (- 1) x96) (* (- 2) x97) )))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= (- 7) (+ (* 1 x0) (+ (* (- 2) x1) (+ (* 1 x3) (+ (* (- 1) x4) (+ (* 2 x5) (+ (* (- 1) x6) (+ (* 2 x10) (+ (* (- 1) x11) (+ (* (- 2) x12) (+ (* (- 2) x13) (+ (* 1 x14) (+ (* (- 1) x15) (+ (* (- 1) x16) (+ (* 2 x18) (+ (* (- 1) x21) (+ (* 1 x22) (+ (* 1 x23) (+ (* (- 1) x25) (+ (* (- 2) x27) (+ (* (- 2) x28) (+ (* 2 x29) (+ (* 1 x31) (+ (* (- 1) x32) (+ (* 1 x34) (+ (* (- 1) x36) (+ (* (- 1) x37) (+ (* 1 x39) (+ (* 2 x41) (+ (* 2 x42) (+ (* (- 1) x47) (+ (* 2 x48) (+ (* (- 2) x49) (+ (* (- 1) x50) (+ (* 1 x53) (+ (* 2 x54) (+ (* 1 x56) (+ (* (- 2) x58) (+ (* 2 x62) (+ (* (- 1) x63) (+ (* (- 1) x64) (+ (* (- 1) x65) (+ (* (- 2) x66) (+ (* (- 1) x68) (+ (* 2 x69) (+ (* 1 x70) (+ (* (- 2) x71) (+ (* (- 1) x74) (+ (* (- 1) x76) (+ (* (- 2) x79) (+ (* 1 x80) (+ (* 1 x84) (+ (* 2 x85) (+ (* (- 2) x88) (+ (* 1 x89) (+ (* (- 2) x93) (+ (* (- 2) x96) (+ (* (- 2) x97) (* 2 x98) )))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= 11 (+ (* 2 x0) (+ (* (- 2) x1) (+ (* (- 2) x4) (+ (* (- 2) x5) (+ (* (- 1) x7) (+ (* (- 1) x8) (+ (* 2 x9) (+ (* 2 x13) (+ (* (- 1) x14) (+ (* 1 x15) (+ (* 1 x16) (+ (* (- 2) x18) (+ (* (- 2) x19) (+ (* (- 2) x22) (+ (* (- 2) x24) (+ (* 1 x25) (+ (* (- 1) x26) (+ (* 2 x30) (+ (* (- 1) x32) (+ (* (- 1) x34) (+ (* (- 1) x35) (+ (* (- 1) x37) (+ (* 1 x38) (+ (* (- 1) x39) (+ (* 1 x40) (+ (* (- 1) x42) (+ (* 1 x44) (+ (* (- 2) x48) (+ (* 1 x52) (+ (* (- 2) x53) (+ (* (- 1) x54) (+ (* (- 1) x55) (+ (* 2 x56) (+ (* (- 1) x58) (+ (* (- 1) x59) (+ (* (- 2) x61) (+ (* (- 2) x64) (+ (* (- 2) x66) (+ (* (- 1) x67) (+ (* (- 2) x68) (+ (* 2 x69) (+ (* 2 x72) (+ (* 2 x74) (+ (* 2 x75) (+ (* 1 x77) (+ (* (- 2) x78) (+ (* (- 2) x79) (+ (* 2 x81) (+ (* (- 1) x82) (+ (* (- 2) x86) (+ (* (- 2) x87) (+ (* (- 1) x90) (+ (* (- 2) x92) (+ (* (- 2) x93) (+ (* (- 1) x95) (+ (* (- 1) x96) (+ (* 1 x97) (+ (* (- 2) x98) (* (- 2) x99) ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= 34 (+ (* 1 x1) (+ (* 1 x2) (+ (* (- 2) x4) (+ (* (- 1) x5) (+ (* (- 1) x6) (+ (* (- 1) x8) (+ (* (- 2) x12) (+ (* (- 2) x13) (+ (* (- 1) x15) (+ (* (- 1) x16) (+ (* 1 x18) (+ (* (- 1) x19) (+ (* (- 2) x20) (+ (* (- 2) x23) (+ (* (- 1) x24) (+ (* (- 1) x25) (+ (* (- 1) x26) (+ (* 2 x27) (+ (* (- 1) x28) (+ (* (- 2) x33) (+ (* 1 x34) (+ (* (- 2) x35) (+ (* (- 1) x36) (+ (* (- 1) x38) (+ (* (- 1) x39) (+ (* 1 x41) (+ (* (- 1) x42) (+ (* 2 x43) (+ (* (- 1) x44) (+ (* (- 2) x45) (+ (* (- 2) x46) (+ (* (- 1) x48) (+ (* 1 x51) (+ (* (- 1) x52) (+ (* 1 x55) (+ (* (- 2) x56) (+ (* (- 2) x57) (+ (* 2 x58) (+ (* 1 x59) (+ (* 1 x61) (+ (* 2 x62) (+ (* (- 2) x63) (+ (* (- 2) x64) (+ (* (- 1) x65) (+ (* (- 2) x66) (+ (* 1 x69) (+ (* (- 1) x70) (+ (* 2 x71) (+ (* (- 1) x72) (+ (* (- 2) x74) (+ (* (- 2) x76) (+ (* 2 x78) (+ (* (- 2) x82) (+ (* 1 x84) (+ (* (- 2) x86) (+ (* 1 x87) (+ (* 1 x93) (+ (* (- 1) x94) (+ (* 2 x95) (+ (* (- 1) x97) (* (- 2) x99) ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= (- 17) (+ (* (- 1) x0) (+ (* 1 x1) (+ (* (- 1) x2) (+ (* (- 1) x3) (+ (* 2 x5) (+ (* 1 x6) (+ (* 1 x7) (+ (* 2 x9) (+ (* (- 1) x10) (+ (* (- 2) x11) (+ (* (- 1) x12) (+ (* 2 x17) (+ (* 2 x19) (+ (* 2 x20) (+ (* 1 x21) (+ (* 2 x22) (+ (* (- 2) x23) (+ (* (- 1) x24) (+ (* (- 1) x25) (+ (* 2 x27) (+ (* (- 2) x29) (+ (* (- 2) x31) (+ (* 2 x32) (+ (* (- 2) x34) (+ (* (- 2) x35) (+ (* (- 2) x36) (+ (* (- 1) x37) (+ (* 2 x38) (+ (* 2 x39) (+ (* (- 2) x44) (+ (* (- 2) x45) (+ (* (- 1) x46) (+ (* 1 x47) (+ (* 2 x48) (+ (* (- 1) x49) (+ (* 2 x51) (+ (* 1 x52) (+ (* 2 x53) (+ (* (- 2) x57) (+ (* 2 x59) (+ (* (- 2) x61) (+ (* 1 x63) (+ (* (- 1) x64) (+ (* (- 1) x65) (+ (* 1 x66) (+ (* 2 x67) (+ (* 2 x70) (+ (* 2 x71) (+ (* 1 x72) (+ (* 1 x74) (+ (* 1 x75) (+ (* (- 1) x81) (+ (* (- 1) x83) (+ (* 2 x86) (+ (* 1 x87) (+ (* 1 x89) (+ (* 2 x91) (+ (* (- 1) x92) (+ (* 2 x95) (+ (* (- 1) x96) (+ (* (- 2) x98) (* (- 1) x99) )))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= 23 (+ (* (- 2) x0) (+ (* (- 1) x4) (+ (* (- 2) x6) (+ (* (- 2) x7) (+ (* 1 x8) (+ (* 2 x10) (+ (* 1 x15) (+ (* (- 1) x16) (+ (* 1 x21) (+ (* 1 x22) (+ (* (- 2) x23) (+ (* 2 x25) (+ (* (- 2) x26) (+ (* 1 x27) (+ (* (- 1) x29) (+ (* 1 x30) (+ (* (- 2) x33) (+ (* 1 x35) (+ (* (- 2) x37) (+ (* 2 x38) (+ (* (- 2) x39) (+ (* 2 x40) (+ (* (- 1) x41) (+ (* (- 1) x44) (+ (* 1 x45) (+ (* 1 x46) (+ (* (- 1) x47) (+ (* 2 x49) (+ (* 2 x50) (+ (* 2 x53) (+ (* (- 2) x54) (+ (* (- 1) x55) (+ (* 2 x56) (+ (* (- 2) x57) (+ (* (- 2) x63) (+ (* 2 x64) (+ (* (- 2) x68) (+ (* (- 1) x69) (+ (* 2 x71) (+ (* 1 x72) (+ (* (- 1) x73) (+ (* 1 x74) (+ (* 1 x78) (+ (* 1 x79) (+ (* (- 2) x80) (+ (* 2 x82) (+ (* (- 1) x83) (+ (* (- 2) x86) (+ (* 1 x89) (+ (* (- 1) x90) (+ (* (- 2) x91) (+ (* 1 x92) (+ (* 1 x93) (+ (* (- 1) x95) (+ (* 2 x96) (+ (* 1 x98) (* (- 1) x99) ))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= (- 33) (+ (* 2 x4) (+ (* (- 1) x6) (+ (* (- 2) x9) (+ (* (- 2) x10) (+ (* 1 x11) (+ (* 1 x12) (+ (* (- 2) x13) (+ (* 2 x14) (+ (* 1 x16) (+ (* (- 2) x18) (+ (* (- 1) x20) (+ (* 2 x21) (+ (* 2 x25) (+ (* (- 1) x26) (+ (* 1 x28) (+ (* 2 x30) (+ (* 2 x31) (+ (* (- 1) x32) (+ (* 2 x34) (+ (* (- 2) x35) (+ (* 2 x36) (+ (* (- 1) x37) (+ (* 2 x39) (+ (* (- 1) x40) (+ (* 2 x41) (+ (* 2 x42) (+ (* 1 x43) (+ (* (- 1) x47) (+ (* 2 x51) (+ (* (- 2) x52) (+ (* 1 x53) (+ (* (- 1) x55) (+ (* 2 x57) (+ (* 2 x58) (+ (* (- 1) x59) (+ (* 1 x60) (+ (* 1 x63) (+ (* (- 1) x64) (+ (* 1 x65) (+ (* 2 x66) (+ (* (- 2) x68) (+ (* 1 x72) (+ (* 2 x73) (+ (* 1 x76) (+ (* (- 2) x78) (+ (* 1 x79) (+ (* 2 x80) (+ (* (- 2) x82) (+ (* (- 2) x83) (+ (* (- 1) x84) (+ (* 1 x85) (+ (* 1 x87) (+ (* 1 x88) (+ (* (- 1) x90) (+ (* 2 x91) (+ (* 2 x92) (+ (* (- 1) x93) (+ (* (- 1) x96) (* (- 2) x98) ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= 36 (+ (* 1 x0) (+ (* 1 x1) (+ (* (- 1) x2) (+ (* (- 1) x3) (+ (* (- 2) x4) (+ (* 1 x6) (+ (* 1 x8) (+ (* (- 2) x10) (+ (* 2 x16) (+ (* 2 x19) (+ (* 1 x23) (+ (* 2 x25) (+ (* 2 x27) (+ (* (- 2) x28) (+ (* (- 1) x29) (+ (* 1 x30) (+ (* 1 x32) (+ (* 1 x33) (+ (* (- 2) x35) (+ (* (- 1) x36) (+ (* 2 x37) (+ (* (- 1) x38) (+ (* 2 x39) (+ (* 2 x40) (+ (* 1 x42) (+ (* (- 1) x43) (+ (* 2 x44) (+ (* (- 2) x45) (+ (* (- 2) x46) (+ (* 1 x47) (+ (* (- 1) x48) (+ (* 1 x50) (+ (* (- 2) x53) (+ (* (- 1) x54) (+ (* 2 x55) (+ (* 1 x56) (+ (* (- 1) x58) (+ (* 1 x60) (+ (* 1 x61) (+ (* (- 1) x63) (+ (* (- 1) x64) (+ (* (- 2) x66) (+ (* (- 2) x68) (+ (* (- 1) x69) (+ (* 1 x70) (+ (* (- 2) x71) (+ (* 1 x73) (+ (* (- 1) x74) (+ (* (- 1) x75) (+ (* (- 1) x79) (+ (* (- 1) x80) (+ (* (- 2) x81) (+ (* 2 x82) (+ (* (- 1) x85) (+ (* (- 1) x86) (+ (* 1 x88) (+ (* 1 x89) (+ (* (- 2) x90) (+ (* (- 1) x92) (+ (* (- 2) x94) (+ (* 2 x97) (* (- 2) x98) )))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= (- 11) (+ (* (- 1) x0) (+ (* (- 1) x1) (+ (* (- 1) x5) (+ (* 2 x6) (+ (* 1 x8) (+ (* (- 2) x10) (+ (* 1 x11) (+ (* (- 2) x13) (+ (* (- 2) x14) (+ (* 2 x16) (+ (* 2 x17) (+ (* (- 2) x22) (+ (* (- 2) x23) (+ (* 2 x27) (+ (* 2 x28) (+ (* 2 x29) (+ (* (- 2) x31) (+ (* (- 1) x32) (+ (* (- 1) x33) (+ (* (- 2) x37) (+ (* 2 x38) (+ (* 2 x40) (+ (* (- 1) x41) (+ (* 2 x42) (+ (* 2 x45) (+ (* (- 1) x46) (+ (* (- 2) x51) (+ (* (- 2) x53) (+ (* (- 2) x55) (+ (* (- 1) x56) (+ (* 1 x57) (+ (* 1 x59) (+ (* (- 2) x61) (+ (* (- 2) x62) (+ (* 1 x64) (+ (* 2 x69) (+ (* 1 x70) (+ (* 2 x71) (+ (* (- 2) x72) (+ (* (- 1) x73) (+ (* (- 1) x77) (+ (* (- 2) x79) (+ (* 1 x81) (+ (* 2 x83) (+ (* 2 x86) (+ (* (- 2) x87) (+ (* 2 x91) (+ (* 1 x96) (+ (* 1 x98) (* (- 1) x99) )))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= 15 (+ (* 2 x0) (+ (* 1 x1) (+ (* 1 x2) (+ (* 2 x3) (+ (* (- 2) x4) (+ (* 1 x8) (+ (* 1 x11) (+ (* 1 x12) (+ (* 1 x14) (+ (* 2 x16) (+ (* 1 x17) (+ (* (- 1) x18) (+ (* 1 x24) (+ (* 2 x26) (+ (* (- 2) x29) (+ (* 2 x30) (+ (* (- 2) x36) (+ (* 2 x38) (+ (* (- 1) x40) (+ (* (- 1) x41) (+ (* (- 1) x45) (+ (* 2 x47) (+ (* (- 2) x50) (+ (* (- 2) x51) (+ (* 1 x52) (+ (* 1 x53) (+ (* 2 x54) (+ (* 2 x55) (+ (* (- 2) x57) (+ (* (- 1) x58) (+ (* (- 2) x60) (+ (* (- 2) x61) (+ (* (- 1) x63) (+ (* (- 2) x64) (+ (* 1 x66) (+ (* (- 1) x68) (+ (* (- 2) x69) (+ (* (- 1) x70) (+ (* 1 x72) (+ (* (- 2) x74) (+ (* (- 1) x75) (+ (* 1 x76) (+ (* (- 1) x77) (+ (* (- 2) x78) (+ (* (- 2) x80) (+ (* (- 2) x81) (+ (* 1 x83) (+ (* (- 1) x85) (+ (* (- 1) x87) (+ (* (- 1) x89) (+ (* 1 x90) (+ (* (- 1) x92) (+ (* (- 2) x93) (+ (* 1 x95) (+ (* 1 x96) (* 2 x99) )))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= (- 17) (+ (* 2 x2) (+ (* 2 x3) (+ (* (- 2) x4) (+ (* (- 1) x6) (+ (* (- 2) x7) (+ (* (- 1) x11) (+ (* (- 1) x12) (+ (* (- 2) x15) (+ (* (- 2) x16) (+ (* (- 1) x17) (+ (* (- 1) x18) (+ (* (- 1) x20) (+ (* 1 x24) (+ (* 2 x27) (+ (* 2 x28) (+ (* 1 x30) (+ (* (- 1) x31) (+ (* (- 2) x32) (+ (* (- 1) x34) (+ (* (- 2) x37) (+ (* (- 2) x40) (+ (* 2 x42) (+ (* 2 x43) (+ (* (- 2) x46) (+ (* 2 x49) (+ (* (- 2) x50) (+ (* 1 x56) (+ (* 1 x58) (+ (* (- 2) x59) (+ (* 1 x62) (+ (* (- 2) x63) (+ (* 2 x64) (+ (* (- 2) x65) (+ (* (- 1) x66) (+ (* 1 x67) (+ (* 1 x68) (+ (* (- 2) x69) (+ (* (- 2) x70) (+ (* 2 x71) (+ (* (- 1) x73) (+ (* 2 x74) (+ (* 2 x75) (+ (* (- 2) x76) (+ (* (- 1) x78) (+ (* 1 x79) (+ (* 1 x80) (+ (* (- 1) x82) (+ (* (- 1) x83) (+ (* 2 x84) (+ (* (- 1) x87) (+ (* 1 x88) (+ (* (- 2) x89) (+ (* 2 x90) (+ (* (- 2) x91) (+ (* (- 2) x93) (+ (* 2 x95) (+ (* 2 x98) (* (- 2) x99) )))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= (- 13) (+ (* 1 x1) (+ (* 2 x4) (+ (* (- 1) x5) (+ (* (- 1) x6) (+ (* 1 x8) (+ (* 2 x10) (+ (* (- 1) x11) (+ (* (- 2) x12) (+ (* (- 1) x13) (+ (* (- 2) x21) (+ (* (- 1) x23) (+ (* (- 1) x24) (+ (* 1 x26) (+ (* 1 x27) (+ (* 1 x30) (+ (* (- 1) x31) (+ (* (- 2) x32) (+ (* 2 x33) (+ (* (- 1) x34) (+ (* (- 2) x36) (+ (* 2 x37) (+ (* 2 x38) (+ (* (- 2) x39) (+ (* 1 x41) (+ (* 2 x42) (+ (* 2 x43) (+ (* (- 1) x44) (+ (* 1 x47) (+ (* 2 x49) (+ (* 1 x50) (+ (* 1 x53) (+ (* (- 1) x54) (+ (* (- 1) x55) (+ (* (- 2) x58) (+ (* 2 x60) (+ (* 2 x62) (+ (* (- 2) x63) (+ (* 1 x64) (+ (* 2 x65) (+ (* (- 1) x66) (+ (* (- 2) x69) (+ (* (- 2) x72) (+ (* (- 1) x73) (+ (* 2 x74) (+ (* 2 x75) (+ (* (- 1) x76) (+ (* 2 x77) (+ (* (- 1) x79) (+ (* 1 x82) (+ (* (- 1) x83) (+ (* (- 1) x86) (+ (* 1 x95) (+ (* (- 2) x96) (+ (* (- 2) x97) (* (- 2) x98) ))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= (- 9) (+ (* 2 x0) (+ (* (- 1) x2) (+ (* 1 x4) (+ (* 1 x9) (+ (* (- 2) x10) (+ (* 1 x11) (+ (* (- 2) x13) (+ (* 1 x14) (+ (* (- 2) x15) (+ (* 1 x16) (+ (* 2 x19) (+ (* 2 x20) (+ (* (- 2) x21) (+ (* 1 x24) (+ (* (- 1) x29) (+ (* (- 2) x30) (+ (* 2 x31) (+ (* 1 x32) (+ (* (- 2) x33) (+ (* (- 2) x34) (+ (* 1 x35) (+ (* (- 2) x37) (+ (* (- 2) x38) (+ (* (- 1) x39) (+ (* (- 1) x44) (+ (* (- 2) x47) (+ (* (- 1) x54) (+ (* 1 x55) (+ (* 2 x56) (+ (* 2 x58) (+ (* 1 x60) (+ (* 1 x62) (+ (* 1 x65) (+ (* 1 x66) (+ (* (- 1) x67) (+ (* (- 1) x68) (+ (* 2 x69) (+ (* 1 x70) (+ (* (- 1) x72) (+ (* (- 2) x74) (+ (* 1 x75) (+ (* (- 2) x77) (+ (* 1 x78) (+ (* 2 x81) (+ (* (- 2) x84) (+ (* (- 2) x85) (+ (* 2 x88) (+ (* 2 x91) (+ (* 2 x93) (+ (* 1 x94) (+ (* (- 2) x95) (+ (* 1 x96) (* 1 x98) ))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= (- 7) (+ (* 2 x0) (+ (* (- 2) x2) (+ (* 2 x3) (+ (* (- 1) x7) (+ (* 1 x9) (+ (* 1 x10) (+ (* 1 x14) (+ (* (- 1) x15) (+ (* 2 x16) (+ (* 1 x18) (+ (* 1 x19) (+ (* (- 1) x21) (+ (* (- 1) x28) (+ (* 1 x33) (+ (* 2 x34) (+ (* 1 x35) (+ (* (- 2) x36) (+ (* 1 x38) (+ (* 1 x39) (+ (* 2 x40) (+ (* (- 1) x41) (+ (* (- 1) x43) (+ (* 2 x44) (+ (* 2 x45) (+ (* (- 1) x47) (+ (* (- 2) x49) (+ (* (- 2) x51) (+ (* 2 x53) (+ (* (- 2) x55) (+ (* 1 x60) (+ (* 1 x64) (+ (* 1 x70) (+ (* 2 x71) (+ (* 2 x73) (+ (* (- 1) x75) (+ (* 1 x76) (+ (* (- 2) x79) (+ (* 2 x80) (+ (* (- 2) x81) (+ (* (- 2) x82) (+ (* 2 x83) (+ (* 2 x84) (+ (* 2 x85) (+ (* (- 1) x86) (+ (* 2 x87) (+ (* (- 2) x88) (+ (* 2 x90) (+ (* (- 2) x91) (+ (* (- 2) x92) (+ (* (- 2) x93) (+ (* 1 x94) (+ (* (- 1) x95) (+ (* 2 x96) (+ (* 1 x97) (+ (* 1 x98) (* 1 x99) )))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= (- 27) (+ (* 1 x2) (+ (* 1 x3) (+ (* 2 x6) (+ (* (- 2) x7) (+ (* 2 x11) (+ (* 2 x13) (+ (* 1 x15) (+ (* 2 x16) (+ (* (- 1) x18) (+ (* (- 2) x20) (+ (* 1 x21) (+ (* (- 2) x22) (+ (* (- 1) x24) (+ (* 1 x27) (+ (* 1 x31) (+ (* (- 1) x33) (+ (* (- 2) x36) (+ (* (- 1) x37) (+ (* 2 x39) (+ (* (- 1) x40) (+ (* (- 2) x41) (+ (* (- 1) x42) (+ (* 2 x44) (+ (* 2 x45) (+ (* 2 x47) (+ (* 1 x49) (+ (* 1 x50) (+ (* 1 x51) (+ (* 2 x52) (+ (* 1 x53) (+ (* 1 x55) (+ (* (- 2) x57) (+ (* (- 2) x58) (+ (* 1 x59) (+ (* (- 2) x60) (+ (* (- 1) x62) (+ (* (- 1) x64) (+ (* 1 x66) (+ (* 1 x67) (+ (* 2 x72) (+ (* (- 1) x73) (+ (* 1 x74) (+ (* (- 1) x76) (+ (* 2 x78) (+ (* 2 x79) (+ (* (- 1) x81) (+ (* (- 2) x85) (+ (* 2 x86) (+ (* (- 1) x87) (+ (* (- 1) x89) (+ (* 2 x91) (+ (* 2 x92) (+ (* (- 1) x93) (+ (* (- 2) x96) (+ (* (- 2) x98) (* 1 x99) )))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= (- 48) (+ (* 1 x0) (+ (* (- 2) x1) (+ (* 2 x3) (+ (* 1 x4) (+ (* 2 x5) (+ (* 2 x6) (+ (* (- 1) x7) (+ (* (- 2) x8) (+ (* 1 x11) (+ (* 1 x13) (+ (* 1 x14) (+ (* 1 x16) (+ (* (- 1) x19) (+ (* (- 1) x22) (+ (* 2 x23) (+ (* (- 2) x25) (+ (* (- 1) x26) (+ (* (- 2) x28) (+ (* 2 x31) (+ (* 2 x33) (+ (* (- 2) x34) (+ (* 1 x35) (+ (* 1 x36) (+ (* (- 1) x40) (+ (* (- 1) x43) (+ (* 1 x44) (+ (* (- 1) x47) (+ (* (- 1) x49) (+ (* 2 x50) (+ (* 2 x51) (+ (* 2 x52) (+ (* 2 x54) (+ (* 1 x57) (+ (* 1 x62) (+ (* (- 2) x63) (+ (* 2 x66) (+ (* (- 1) x67) (+ (* (- 1) x68) (+ (* 1 x72) (+ (* (- 2) x73) (+ (* 2 x75) (+ (* (- 2) x76) (+ (* (- 1) x77) (+ (* (- 1) x78) (+ (* (- 1) x81) (+ (* 2 x82) (+ (* 1 x83) (+ (* 2 x84) (+ (* 1 x85) (+ (* 1 x86) (+ (* 1 x88) (+ (* (- 1) x89) (+ (* 1 x90) (+ (* 1 x91) (+ (* (- 2) x93) (+ (* 2 x94) (+ (* 1 x96) (* 1 x98) )))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= (- 8) (+ (* 2 x2) (+ (* 2 x3) (+ (* (- 1) x6) (+ (* (- 1) x7) (+ (* (- 2) x8) (+ (* 2 x16) (+ (* (- 1) x18) (+ (* (- 1) x20) (+ (* 1 x22) (+ (* 2 x23) (+ (* (- 2) x24) (+ (* 2 x27) (+ (* 2 x28) (+ (* (- 2) x30) (+ (* (- 1) x32) (+ (* 1 x33) (+ (* 2 x34) (+ (* (- 2) x35) (+ (* (- 1) x36) (+ (* 2 x38) (+ (* (- 1) x40) (+ (* 2 x41) (+ (* (- 2) x42) (+ (* (- 1) x45) (+ (* 2 x49) (+ (* 2 x51) (+ (* (- 1) x53) (+ (* 2 x57) (+ (* (- 1) x59) (+ (* 2 x60) (+ (* (- 1) x61) (+ (* 2 x62) (+ (* (- 2) x64) (+ (* (- 1) x67) (+ (* (- 2) x68) (+ (* 1 x71) (+ (* (- 2) x73) (+ (* 1 x75) (+ (* (- 2) x79) (+ (* (- 1) x81) (+ (* (- 2) x82) (+ (* (- 2) x85) (+ (* 1 x86) (+ (* 2 x89) (+ (* (- 2) x92) (+ (* (- 2) x93) (+ (* (- 1) x95) (+ (* (- 1) x96) (+ (* 2 x97) (* (- 2) x98) )))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= 20 (+ (* 2 x0) (+ (* 2 x2) (+ (* (- 1) x3) (+ (* (- 1) x4) (+ (* 2 x7) (+ (* 1 x8) (+ (* 1 x9) (+ (* 2 x13) (+ (* 1 x14) (+ (* (- 2) x15) (+ (* 1 x16) (+ (* (- 1) x17) (+ (* 1 x18) (+ (* 1 x19) (+ (* 2 x20) (+ (* 1 x23) (+ (* (- 1) x24) (+ (* 2 x25) (+ (* (- 2) x26) (+ (* (- 1) x27) (+ (* (- 2) x28) (+ (* 2 x29) (+ (* 1 x30) (+ (* 1 x34) (+ (* (- 2) x36) (+ (* (- 1) x40) (+ (* (- 2) x42) (+ (* 1 x43) (+ (* 2 x50) (+ (* (- 2) x52) (+ (* 1 x55) (+ (* (- 2) x56) (+ (* (- 2) x57) (+ (* (- 2) x59) (+ (* 2 x61) (+ (* (- 1) x66) (+ (* (- 2) x70) (+ (* (- 1) x72) (+ (* (- 2) x74) (+ (* 1 x76) (+ (* 1 x77) (+ (* (- 2) x78) (+ (* 1 x79) (+ (* 2 x80) (+ (* (- 2) x83) (+ (* 1 x84) (+ (* (- 2) x85) (+ (* 1 x86) (+ (* 2 x87) (+ (* 1 x91) (+ (* 1 x94) (+ (* (- 2) x96) (* 2 x99) ))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= (- 24) (+ (* 2 x0) (+ (* (- 2) x3) (+ (* (- 1) x7) (+ (* 1 x8) (+ (* 1 x9) (+ (* (- 2) x10) (+ (* (- 1) x11) (+ (* 1 x14) (+ (* 2 x16) (+ (* 2 x17) (+ (* (- 1) x18) (+ (* 2 x19) (+ (* 2 x21) (+ (* 1 x22) (+ (* 2 x24) (+ (* (- 2) x26) (+ (* 1 x27) (+ (* (- 2) x28) (+ (* 1 x30) (+ (* (- 2) x31) (+ (* 1 x32) (+ (* (- 2) x33) (+ (* (- 2) x37) (+ (* 1 x38) (+ (* 1 x39) (+ (* (- 2) x41) (+ (* 1 x42) (+ (* 1 x43) (+ (* (- 2) x45) (+ (* 1 x46) (+ (* 2 x48) (+ (* 1 x50) (+ (* 2 x52) (+ (* 2 x53) (+ (* (- 1) x55) (+ (* (- 2) x59) (+ (* 1 x60) (+ (* (- 2) x61) (+ (* (- 2) x64) (+ (* 2 x65) (+ (* 1 x66) (+ (* (- 1) x67) (+ (* 1 x68) (+ (* (- 2) x71) (+ (* (- 1) x72) (+ (* (- 1) x74) (+ (* (- 2) x78) (+ (* 1 x80) (+ (* 2 x81) (+ (* 1 x83) (+ (* 1 x84) (+ (* (- 1) x90) (+ (* 1 x92) (+ (* (- 1) x93) (* 1 x95) ))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= 25 (+ (* (- 2) x1) (+ (* 1 x2) (+ (* 2 x4) (+ (* (- 2) x5) (+ (* 2 x6) (+ (* (- 2) x7) (+ (* (- 2) x8) (+ (* (- 2) x9) (+ (* 2 x11) (+ (* (- 2) x12) (+ (* 1 x13) (+ (* 2 x16) (+ (* (- 1) x18) (+ (* (- 1) x21) (+ (* (- 2) x23) (+ (* (- 2) x26) (+ (* (- 2) x27) (+ (* 2 x28) (+ (* 2 x29) (+ (* (- 1) x30) (+ (* (- 1) x32) (+ (* 2 x34) (+ (* (- 1) x35) (+ (* 2 x36) (+ (* 1 x40) (+ (* (- 2) x42) (+ (* 1 x44) (+ (* (- 1) x45) (+ (* 1 x46) (+ (* 1 x48) (+ (* 1 x49) (+ (* (- 1) x52) (+ (* 2 x55) (+ (* (- 1) x57) (+ (* 2 x58) (+ (* 1 x59) (+ (* (- 1) x60) (+ (* 1 x61) (+ (* (- 2) x63) (+ (* 2 x64) (+ (* (- 1) x65) (+ (* (- 1) x66) (+ (* (- 1) x67) (+ (* 1 x68) (+ (* 1 x70) (+ (* 1 x72) (+ (* (- 2) x73) (+ (* 2 x76) (+ (* 2 x78) (+ (* (- 1) x80) (+ (* 1 x81) (+ (* 1 x83) (+ (* 2 x85) (+ (* (- 1) x90) (+ (* 1 x91) (+ (* (- 2) x94) (+ (* 2 x95) (+ (* (- 2) x96) (* 2 x99) ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= (- 21) (+ (* (- 1) x0) (+ (* (- 2) x3) (+ (* 1 x4) (+ (* (- 2) x5) (+ (* (- 1) x6) (+ (* (- 1) x8) (+ (* (- 2) x10) (+ (* 1 x12) (+ (* (- 1) x13) (+ (* (- 2) x14) (+ (* 1 x15) (+ (* (- 1) x17) (+ (* 1 x19) (+ (* (- 1) x21) (+ (* 1 x24) (+ (* 2 x26) (+ (* (- 2) x27) (+ (* 2 x29) (+ (* (- 2) x30) (+ (* (- 2) x36) (+ (* (- 2) x38) (+ (* 2 x40) (+ (* 1 x43) (+ (* (- 2) x44) (+ (* (- 2) x45) (+ (* 1 x46) (+ (* 2 x47) (+ (* 1 x49) (+ (* 2 x51) (+ (* 2 x52) (+ (* 2 x53) (+ (* 1 x55) (+ (* 1 x58) (+ (* (- 2) x59) (+ (* (- 2) x60) (+ (* (- 2) x63) (+ (* (- 2) x66) (+ (* 2 x69) (+ (* (- 1) x70) (+ (* (- 1) x73) (+ (* 1 x74) (+ (* 2 x75) (+ (* (- 2) x76) (+ (* 1 x77) (+ (* (- 2) x79) (+ (* (- 1) x80) (+ (* (- 2) x82) (+ (* 2 x83) (+ (* (- 1) x84) (+ (* 2 x85) (+ (* 2 x86) (+ (* (- 1) x89) (+ (* 1 x90) (+ (* 1 x92) (+ (* 2 x93) (+ (* 1 x94) (+ (* 1 x98) (* 2 x99) )))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= 26 (+ (* (- 2) x0) (+ (* 2 x1) (+ (* (- 1) x2) (+ (* (- 2) x3) (+ (* 1 x5) (+ (* 2 x7) (+ (* (- 1) x8) (+ (* (- 2) x9) (+ (* 2 x11) (+ (* (- 2) x12) (+ (* (- 1) x14) (+ (* 2 x18) (+ (* 2 x19) (+ (* 2 x20) (+ (* 2 x21) (+ (* 2 x22) (+ (* 1 x23) (+ (* 2 x25) (+ (* (- 2) x26) (+ (* 1 x27) (+ (* (- 2) x28) (+ (* 1 x29) (+ (* (- 2) x30) (+ (* 2 x31) (+ (* 1 x32) (+ (* (- 1) x33) (+ (* 1 x34) (+ (* 1 x35) (+ (* (- 1) x41) (+ (* (- 2) x43) (+ (* (- 1) x44) (+ (* 1 x45) (+ (* (- 2) x47) (+ (* 2 x49) (+ (* 2 x50) (+ (* 1 x54) (+ (* 1 x55) (+ (* 1 x57) (+ (* (- 2) x58) (+ (* (- 1) x59) (+ (* 2 x61) (+ (* (- 2) x62) (+ (* (- 2) x63) (+ (* (- 2) x65) (+ (* (- 1) x66) (+ (* (- 2) x67) (+ (* 1 x70) (+ (* 2 x71) (+ (* (- 1) x73) (+ (* 1 x76) (+ (* (- 1) x77) (+ (* 2 x78) (+ (* (- 2) x79) (+ (* 2 x80) (+ (* (- 1) x82) (+ (* 1 x84) (+ (* 1 x85) (+ (* (- 1) x86) (+ (* 1 x88) (+ (* 1 x89) (+ (* (- 2) x90) (+ (* 2 x91) (+ (* 1 x93) (+ (* (- 1) x95) (+ (* (- 2) x96) (+ (* 2 x98) (* (- 2) x99) ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= (- 17) (+ (* (- 2) x0) (+ (* 1 x1) (+ (* (- 2) x2) (+ (* 1 x3) (+ (* 2 x4) (+ (* 2 x9) (+ (* (- 2) x10) (+ (* 2 x11) (+ (* (- 2) x12) (+ (* (- 1) x13) (+ (* 1 x15) (+ (* 1 x17) (+ (* 1 x18) (+ (* (- 1) x19) (+ (* (- 1) x20) (+ (* 2 x21) (+ (* (- 2) x22) (+ (* 1 x23) (+ (* (- 2) x26) (+ (* (- 1) x27) (+ (* 1 x28) (+ (* 1 x29) (+ (* 2 x30) (+ (* 2 x31) (+ (* (- 1) x32) (+ (* (- 1) x33) (+ (* 1 x34) (+ (* 2 x36) (+ (* 2 x38) (+ (* 2 x40) (+ (* 2 x44) (+ (* 1 x46) (+ (* (- 2) x52) (+ (* 2 x53) (+ (* (- 1) x55) (+ (* (- 2) x57) (+ (* (- 1) x58) (+ (* 2 x62) (+ (* 2 x63) (+ (* (- 2) x66) (+ (* (- 1) x68) (+ (* (- 1) x71) (+ (* (- 1) x72) (+ (* 2 x73) (+ (* 2 x76) (+ (* 1 x77) (+ (* 1 x78) (+ (* 1 x79) (+ (* (- 1) x81) (+ (* (- 1) x83) (+ (* 2 x85) (+ (* 2 x86) (+ (* (- 2) x87) (+ (* (- 1) x88) (+ (* 2 x92) (+ (* 2 x98) (* 1 x99) ))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= 11 (+ (* 2 x0) (+ (* (- 1) x1) (+ (* (- 1) x2) (+ (* (- 1) x3) (+ (* (- 1) x4) (+ (* 2 x5) (+ (* (- 1) x6) (+ (* (- 1) x7) (+ (* (- 1) x8) (+ (* 2 x9) (+ (* (- 2) x10) (+ (* (- 2) x11) (+ (* 1 x12) (+ (* 2 x14) (+ (* 1 x15) (+ (* (- 2) x16) (+ (* 2 x18) (+ (* (- 2) x19) (+ (* (- 2) x20) (+ (* 2 x21) (+ (* 2 x25) (+ (* (- 1) x27) (+ (* 2 x28) (+ (* 2 x32) (+ (* (- 1) x33) (+ (* (- 1) x34) (+ (* 2 x36) (+ (* 2 x38) (+ (* (- 1) x39) (+ (* (- 2) x40) (+ (* (- 1) x41) (+ (* (- 2) x42) (+ (* 1 x44) (+ (* (- 2) x45) (+ (* (- 1) x49) (+ (* (- 2) x50) (+ (* 1 x52) (+ (* 2 x53) (+ (* (- 1) x54) (+ (* (- 1) x56) (+ (* 2 x57) (+ (* 1 x59) (+ (* (- 2) x60) (+ (* (- 2) x61) (+ (* (- 1) x65) (+ (* (- 1) x67) (+ (* 2 x68) (+ (* (- 1) x69) (+ (* (- 2) x70) (+ (* (- 1) x71) (+ (* (- 1) x72) (+ (* (- 1) x74) (+ (* 1 x76) (+ (* 2 x77) (+ (* 1 x78) (+ (* 1 x80) (+ (* 1 x83) (+ (* (- 1) x85) (+ (* 2 x86) (+ (* (- 1) x93) (+ (* 2 x94) (+ (* (- 1) x98) (* 1 x99) ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= 7 (+ (* 2 x0) (+ (* (- 1) x4) (+ (* (- 1) x5) (+ (* 2 x6) (+ (* 2 x7) (+ (* 2 x8) (+ (* (- 1) x9) (+ (* (- 1) x10) (+ (* (- 1) x12) (+ (* (- 1) x16) (+ (* 1 x17) (+ (* 2 x21) (+ (* 2 x22) (+ (* (- 2) x24) (+ (* 2 x26) (+ (* (- 2) x28) (+ (* 2 x30) (+ (* (- 1) x32) (+ (* (- 1) x34) (+ (* 1 x37) (+ (* 2 x38) (+ (* 2 x39) (+ (* (- 2) x41) (+ (* 1 x42) (+ (* (- 2) x43) (+ (* 2 x44) (+ (* (- 1) x45) (+ (* (- 2) x48) (+ (* (- 1) x49) (+ (* 2 x50) (+ (* 1 x51) (+ (* 1 x54) (+ (* 2 x56) (+ (* (- 1) x57) (+ (* (- 2) x59) (+ (* 1 x60) (+ (* 1 x65) (+ (* (- 2) x73) (+ (* (- 1) x74) (+ (* 1 x75) (+ (* 2 x76) (+ (* 2 x77) (+ (* 2 x78) (+ (* (- 1) x81) (+ (* (- 1) x85) (+ (* (- 2) x86) (+ (* (- 2) x87) (+ (* 2 x88) (+ (* 1 x90) (+ (* (- 1) x91) (+ (* 1 x92) (+ (* (- 2) x93) (+ (* (- 1) x94) (+ (* (- 2) x95) (+ (* (- 1) x96) (+ (* (- 2) x97) (* (- 2) x99) ))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= (- 67) (+ (* (- 1) x2) (+ (* (- 1) x5) (+ (* 1 x6) (+ (* 2 x7) (+ (* 2 x8) (+ (* (- 2) x9) (+ (* 2 x10) (+ (* 1 x11) (+ (* (- 1) x14) (+ (* (- 2) x15) (+ (* 1 x18) (+ (* (- 2) x19) (+ (* (- 1) x20) (+ (* 2 x21) (+ (* 1 x24) (+ (* (- 2) x27) (+ (* 1 x30) (+ (* 2 x32) (+ (* 1 x34) (+ (* 1 x37) (+ (* 2 x42) (+ (* 2 x43) (+ (* (- 1) x45) (+ (* 1 x46) (+ (* (- 1) x47) (+ (* (- 2) x48) (+ (* 2 x49) (+ (* (- 2) x50) (+ (* 2 x53) (+ (* (- 2) x54) (+ (* 2 x55) (+ (* 1 x56) (+ (* (- 2) x58) (+ (* 1 x59) (+ (* (- 1) x60) (+ (* 1 x63) (+ (* (- 1) x64) (+ (* 2 x69) (+ (* (- 1) x70) (+ (* 2 x72) (+ (* 2 x73) (+ (* 1 x78) (+ (* 1 x79) (+ (* 2 x81) (+ (* 2 x82) (+ (* (- 1) x84) (+ (* (- 2) x86) (+ (* 2 x87) (+ (* 2 x88) (+ (* 2 x91) (+ (* (- 1) x93) (+ (* 2 x97) (* 2 x99) ))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= 50 (+ (* (- 1) x1) (+ (* 1 x3) (+ (* (- 1) x4) (+ (* (- 1) x5) (+ (* (- 2) x6) (+ (* 2 x7) (+ (* 2 x12) (+ (* (- 1) x14) (+ (* (- 2) x15) (+ (* 1 x18) (+ (* 1 x19) (+ (* (- 1) x20) (+ (* 2 x23) (+ (* (- 2) x24) (+ (* 1 x26) (+ (* (- 1) x28) (+ (* (- 1) x29) (+ (* 2 x32) (+ (* (- 1) x34) (+ (* (- 1) x35) (+ (* (- 1) x38) (+ (* 2 x39) (+ (* (- 2) x42) (+ (* (- 2) x43) (+ (* 1 x44) (+ (* 1 x45) (+ (* (- 2) x46) (+ (* (- 2) x47) (+ (* (- 2) x48) (+ (* (- 2) x50) (+ (* (- 2) x52) (+ (* (- 1) x53) (+ (* (- 2) x54) (+ (* 2 x56) (+ (* (- 1) x59) (+ (* 1 x60) (+ (* 1 x63) (+ (* (- 2) x64) (+ (* 1 x65) (+ (* (- 2) x67) (+ (* (- 2) x69) (+ (* 2 x71) (+ (* 2 x73) (+ (* (- 1) x74) (+ (* 2 x77) (+ (* (- 2) x78) (+ (* 1 x80) (+ (* (- 1) x83) (+ (* 2 x84) (+ (* 2 x85) (+ (* (- 2) x88) (+ (* (- 1) x90) (+ (* (- 1) x91) (+ (* 2 x92) (+ (* 1 x95) (+ (* (- 1) x96) (+ (* (- 2) x97) (* (- 2) x98) )))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= (- 32) (+ (* (- 1) x0) (+ (* 1 x1) (+ (* 1 x2) (+ (* 1 x5) (+ (* 1 x6) (+ (* (- 1) x10) (+ (* (- 1) x11) (+ (* 1 x12) (+ (* 1 x14) (+ (* (- 1) x17) (+ (* 1 x20) (+ (* 2 x21) (+ (* 1 x22) (+ (* (- 2) x23) (+ (* 1 x24) (+ (* (- 1) x25) (+ (* (- 2) x27) (+ (* 2 x28) (+ (* 2 x29) (+ (* (- 1) x30) (+ (* (- 2) x31) (+ (* (- 1) x32) (+ (* 2 x33) (+ (* (- 1) x35) (+ (* 2 x36) (+ (* 1 x37) (+ (* 1 x38) (+ (* (- 2) x43) (+ (* 1 x44) (+ (* (- 1) x45) (+ (* 1 x46) (+ (* 2 x47) (+ (* 2 x48) (+ (* (- 1) x49) (+ (* 2 x50) (+ (* 2 x51) (+ (* 2 x52) (+ (* (- 2) x55) (+ (* 2 x56) (+ (* 2 x58) (+ (* (- 2) x59) (+ (* (- 1) x61) (+ (* (- 1) x62) (+ (* (- 2) x65) (+ (* 1 x68) (+ (* (- 2) x70) (+ (* (- 1) x71) (+ (* 1 x72) (+ (* 1 x75) (+ (* 1 x76) (+ (* (- 1) x77) (+ (* (- 2) x78) (+ (* (- 1) x80) (+ (* 1 x81) (+ (* (- 2) x82) (+ (* (- 2) x83) (+ (* (- 2) x84) (+ (* 2 x86) (+ (* (- 2) x87) (+ (* (- 1) x88) (+ (* (- 2) x92) (+ (* (- 2) x94) (+ (* (- 2) x96) (+ (* (- 2) x97) (* (- 2) x99) ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= 2 (+ (* 2 x0) (+ (* 1 x2) (+ (* (- 2) x3) (+ (* 2 x6) (+ (* (- 1) x7) (+ (* 2 x8) (+ (* 2 x9) (+ (* 2 x12) (+ (* 2 x13) (+ (* (- 1) x15) (+ (* (- 2) x17) (+ (* 2 x18) (+ (* 2 x19) (+ (* (- 2) x22) (+ (* (- 2) x23) (+ (* (- 2) x24) (+ (* 2 x25) (+ (* (- 1) x27) (+ (* 2 x29) (+ (* (- 2) x30) (+ (* (- 2) x31) (+ (* (- 1) x32) (+ (* 2 x33) (+ (* 1 x35) (+ (* 2 x37) (+ (* (- 2) x38) (+ (* 1 x39) (+ (* (- 1) x40) (+ (* 1 x42) (+ (* 1 x46) (+ (* (- 1) x48) (+ (* (- 1) x50) (+ (* (- 1) x51) (+ (* 2 x52) (+ (* (- 2) x54) (+ (* (- 1) x57) (+ (* (- 2) x58) (+ (* (- 1) x60) (+ (* (- 1) x61) (+ (* 1 x62) (+ (* 1 x63) (+ (* 2 x66) (+ (* (- 1) x67) (+ (* (- 1) x68) (+ (* (- 2) x69) (+ (* (- 1) x70) (+ (* 1 x72) (+ (* 1 x73) (+ (* 2 x74) (+ (* (- 1) x75) (+ (* (- 1) x77) (+ (* 2 x79) (+ (* 1 x82) (+ (* 2 x83) (+ (* (- 1) x85) (+ (* 1 x86) (+ (* 1 x88) (+ (* 2 x90) (+ (* 2 x91) (+ (* 2 x92) (+ (* (- 2) x93) (+ (* (- 2) x95) (+ (* 1 x97) (+ (* (- 2) x98) (* (- 1) x99) ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= (- 1) (+ (* (- 1) x0) (+ (* (- 1) x1) (+ (* (- 2) x2) (+ (* (- 1) x3) (+ (* (- 2) x4) (+ (* 2 x5) (+ (* 2 x6) (+ (* 2 x7) (+ (* (- 1) x8) (+ (* 2 x9) (+ (* 2 x10) (+ (* 1 x12) (+ (* (- 2) x13) (+ (* 1 x14) (+ (* 2 x16) (+ (* 2 x17) (+ (* (- 2) x20) (+ (* (- 1) x21) (+ (* (- 2) x24) (+ (* (- 2) x25) (+ (* 2 x29) (+ (* (- 1) x30) (+ (* 2 x31) (+ (* 2 x32) (+ (* 2 x35) (+ (* (- 2) x37) (+ (* 2 x38) (+ (* 2 x39) (+ (* (- 2) x40) (+ (* (- 1) x45) (+ (* (- 1) x46) (+ (* 2 x47) (+ (* (- 1) x48) (+ (* 1 x51) (+ (* 2 x54) (+ (* (- 1) x56) (+ (* (- 2) x58) (+ (* 1 x59) (+ (* 1 x60) (+ (* (- 1) x62) (+ (* (- 1) x63) (+ (* (- 2) x66) (+ (* (- 2) x67) (+ (* 2 x68) (+ (* (- 1) x70) (+ (* (- 2) x72) (+ (* (- 1) x73) (+ (* (- 2) x74) (+ (* (- 1) x76) (+ (* (- 2) x77) (+ (* 2 x78) (+ (* 2 x79) (+ (* 2 x80) (+ (* 2 x82) (+ (* (- 1) x86) (+ (* (- 1) x87) (+ (* 1 x88) (+ (* (- 1) x89) (+ (* (- 1) x90) (+ (* 1 x91) (+ (* (- 1) x92) (+ (* 1 x93) (+ (* 1 x95) (+ (* 1 x97) (* 2 x99) ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= 12 (+ (* 2 x0) (+ (* 2 x2) (+ (* (- 2) x3) (+ (* (- 1) x6) (+ (* 2 x8) (+ (* (- 2) x11) (+ (* (- 2) x12) (+ (* (- 2) x14) (+ (* (- 2) x15) (+ (* (- 2) x17) (+ (* (- 2) x18) (+ (* 2 x19) (+ (* 1 x20) (+ (* (- 1) x23) (+ (* 1 x24) (+ (* (- 1) x26) (+ (* (- 1) x27) (+ (* (- 1) x28) (+ (* (- 2) x30) (+ (* (- 1) x32) (+ (* 2 x33) (+ (* 2 x35) (+ (* 1 x39) (+ (* 1 x40) (+ (* (- 2) x41) (+ (* 2 x42) (+ (* 1 x44) (+ (* 1 x45) (+ (* (- 1) x46) (+ (* 1 x47) (+ (* 1 x48) (+ (* 1 x49) (+ (* 2 x52) (+ (* 1 x54) (+ (* 2 x55) (+ (* (- 1) x57) (+ (* (- 2) x58) (+ (* 1 x60) (+ (* (- 2) x62) (+ (* (- 2) x65) (+ (* 2 x67) (+ (* 2 x68) (+ (* 2 x70) (+ (* (- 1) x71) (+ (* 2 x72) (+ (* 2 x74) (+ (* (- 2) x75) (+ (* (- 1) x77) (+ (* (- 1) x80) (+ (* 1 x83) (+ (* (- 2) x84) (+ (* 2 x85) (+ (* 2 x87) (+ (* 2 x89) (+ (* 2 x90) (+ (* 1 x92) (+ (* (- 1) x94) (+ (* 2 x96) (+ (* 1 x97) (* (- 2) x98) )))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= 7 (+ (* 2 x0) (+ (* (- 1) x1) (+ (* 1 x2) (+ (* 2 x4) (+ (* 2 x7) (+ (* 2 x8) (+ (* 1 x9) (+ (* 2 x10) (+ (* (- 1) x11) (+ (* 1 x14) (+ (* 1 x15) (+ (* (- 2) x16) (+ (* 1 x17) (+ (* (- 2) x19) (+ (* 1 x21) (+ (* 2 x23) (+ (* (- 2) x24) (+ (* 2 x26) (+ (* (- 1) x27) (+ (* 2 x28) (+ (* 1 x29) (+ (* (- 2) x30) (+ (* 2 x31) (+ (* (- 1) x33) (+ (* 1 x34) (+ (* (- 1) x37) (+ (* 2 x38) (+ (* 1 x39) (+ (* (- 1) x40) (+ (* 2 x41) (+ (* 2 x43) (+ (* (- 1) x45) (+ (* (- 1) x46) (+ (* 2 x47) (+ (* 1 x48) (+ (* 2 x49) (+ (* 1 x50) (+ (* (- 1) x52) (+ (* (- 2) x53) (+ (* (- 1) x55) (+ (* (- 2) x56) (+ (* 2 x59) (+ (* 1 x62) (+ (* 1 x63) (+ (* (- 2) x64) (+ (* 2 x65) (+ (* (- 1) x70) (+ (* (- 1) x71) (+ (* (- 2) x73) (+ (* (- 2) x75) (+ (* (- 1) x76) (+ (* (- 1) x77) (+ (* 1 x79) (+ (* 1 x80) (+ (* (- 2) x82) (+ (* 2 x83) (+ (* 2 x84) (+ (* (- 2) x85) (+ (* (- 2) x86) (+ (* 2 x87) (+ (* (- 1) x88) (+ (* 2 x89) (+ (* (- 2) x93) (+ (* 1 x95) (+ (* (- 1) x96) (+ (* (- 2) x98) (* (- 1) x99) ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= (- 52) (+ (* (- 1) x2) (+ (* 1 x3) (+ (* (- 1) x4) (+ (* 2 x5) (+ (* 2 x6) (+ (* (- 2) x7) (+ (* (- 2) x9) (+ (* (- 2) x10) (+ (* (- 1) x11) (+ (* 2 x12) (+ (* (- 1) x16) (+ (* 1 x17) (+ (* 2 x18) (+ (* 1 x19) (+ (* (- 2) x20) (+ (* (- 2) x23) (+ (* 1 x25) (+ (* 2 x26) (+ (* (- 2) x29) (+ (* (- 2) x33) (+ (* (- 1) x36) (+ (* (- 2) x37) (+ (* 1 x38) (+ (* (- 1) x40) (+ (* (- 1) x42) (+ (* 2 x44) (+ (* 1 x45) (+ (* 2 x46) (+ (* (- 1) x47) (+ (* (- 1) x52) (+ (* 2 x53) (+ (* 1 x54) (+ (* 1 x55) (+ (* (- 1) x56) (+ (* 1 x60) (+ (* 1 x61) (+ (* 2 x62) (+ (* 1 x63) (+ (* (- 2) x64) (+ (* (- 1) x65) (+ (* 1 x67) (+ (* 1 x69) (+ (* (- 1) x70) (+ (* (- 2) x71) (+ (* 1 x73) (+ (* 2 x74) (+ (* (- 2) x75) (+ (* (- 2) x77) (+ (* (- 2) x78) (+ (* (- 2) x79) (+ (* 2 x80) (+ (* (- 1) x81) (+ (* 2 x82) (+ (* (- 1) x83) (+ (* (- 1) x85) (+ (* (- 1) x86) (+ (* 2 x88) (+ (* 2 x89) (+ (* 2 x90) (+ (* (- 2) x91) (+ (* 1 x94) (+ (* 1 x96) (* 2 x98) ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= (- 39) (+ (* 2 x1) (+ (* 1 x2) (+ (* (- 2) x4) (+ (* 2 x7) (+ (* (- 1) x9) (+ (* 2 x11) (+ (* 1 x12) (+ (* 1 x13) (+ (* 2 x14) (+ (* (- 1) x16) (+ (* (- 2) x17) (+ (* (- 1) x20) (+ (* 1 x22) (+ (* 2 x23) (+ (* (- 2) x30) (+ (* 1 x31) (+ (* (- 2) x33) (+ (* 1 x35) (+ (* (- 2) x36) (+ (* (- 2) x37) (+ (* (- 2) x38) (+ (* (- 1) x39) (+ (* 2 x40) (+ (* 2 x42) (+ (* (- 2) x46) (+ (* 2 x48) (+ (* 1 x49) (+ (* (- 1) x50) (+ (* 1 x51) (+ (* (- 1) x53) (+ (* 2 x54) (+ (* (- 2) x56) (+ (* 2 x57) (+ (* (- 1) x58) (+ (* 2 x59) (+ (* 1 x60) (+ (* 2 x63) (+ (* (- 1) x65) (+ (* 2 x67) (+ (* (- 1) x69) (+ (* (- 2) x71) (+ (* 2 x72) (+ (* (- 1) x73) (+ (* 2 x74) (+ (* 1 x76) (+ (* 1 x78) (+ (* 1 x79) (+ (* (- 1) x81) (+ (* (- 2) x83) (+ (* (- 2) x86) (+ (* 1 x88) (+ (* (- 1) x89) (+ (* (- 1) x91) (+ (* 1 x96) (* (- 1) x97) ))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= (- 41) (+ (* 2 x0) (+ (* 2 x2) (+ (* 2 x3) (+ (* 2 x4) (+ (* 1 x5) (+ (* (- 2) x8) (+ (* (- 1) x9) (+ (* 1 x10) (+ (* (- 2) x11) (+ (* (- 2) x14) (+ (* 1 x15) (+ (* 2 x16) (+ (* (- 2) x20) (+ (* (- 2) x21) (+ (* (- 2) x23) (+ (* (- 1) x25) (+ (* 1 x32) (+ (* 2 x34) (+ (* (- 1) x35) (+ (* 2 x37) (+ (* (- 2) x41) (+ (* 1 x42) (+ (* 1 x43) (+ (* 2 x44) (+ (* (- 1) x46) (+ (* (- 1) x47) (+ (* 2 x48) (+ (* 2 x49) (+ (* 2 x50) (+ (* 2 x51) (+ (* 2 x53) (+ (* 1 x55) (+ (* (- 1) x56) (+ (* 2 x58) (+ (* (- 2) x59) (+ (* (- 2) x61) (+ (* 2 x63) (+ (* (- 2) x64) (+ (* 2 x65) (+ (* (- 1) x66) (+ (* 2 x70) (+ (* 2 x71) (+ (* 2 x73) (+ (* (- 2) x75) (+ (* (- 1) x76) (+ (* 2 x77) (+ (* (- 1) x79) (+ (* (- 2) x80) (+ (* 2 x81) (+ (* (- 1) x82) (+ (* (- 1) x87) (+ (* (- 1) x88) (+ (* (- 1) x91) (+ (* 2 x95) (+ (* 2 x96) (+ (* (- 2) x97) (+ (* (- 1) x98) (* (- 1) x99) )))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= (- 45) (+ (* 2 x0) (+ (* 2 x1) (+ (* (- 1) x2) (+ (* 1 x3) (+ (* 2 x4) (+ (* 2 x5) (+ (* (- 1) x9) (+ (* (- 2) x11) (+ (* (- 2) x12) (+ (* 1 x14) (+ (* (- 1) x15) (+ (* 2 x19) (+ (* (- 2) x22) (+ (* 1 x28) (+ (* 1 x30) (+ (* (- 1) x32) (+ (* (- 2) x33) (+ (* 1 x36) (+ (* (- 1) x37) (+ (* (- 1) x38) (+ (* 1 x41) (+ (* 2 x42) (+ (* (- 1) x43) (+ (* (- 1) x44) (+ (* 2 x45) (+ (* 2 x48) (+ (* 2 x50) (+ (* (- 1) x55) (+ (* (- 2) x57) (+ (* (- 1) x58) (+ (* 1 x62) (+ (* 1 x63) (+ (* 2 x64) (+ (* (- 2) x65) (+ (* 2 x67) (+ (* (- 2) x69) (+ (* 1 x70) (+ (* (- 2) x71) (+ (* 1 x72) (+ (* 2 x73) (+ (* 2 x74) (+ (* 1 x75) (+ (* 1 x78) (+ (* 1 x79) (+ (* 2 x80) (+ (* 2 x81) (+ (* (- 2) x83) (+ (* 2 x84) (+ (* 2 x85) (+ (* 1 x86) (+ (* 2 x87) (+ (* 1 x88) (+ (* 2 x91) (+ (* 1 x93) (+ (* (- 1) x97) (+ (* 1 x98) (* (- 1) x99) ))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= (- 32) (+ (* (- 1) x2) (+ (* (- 1) x3) (+ (* 1 x4) (+ (* 2 x5) (+ (* 2 x10) (+ (* 2 x11) (+ (* 2 x13) (+ (* (- 2) x15) (+ (* 2 x16) (+ (* (- 2) x17) (+ (* 2 x18) (+ (* (- 2) x20) (+ (* 1 x22) (+ (* (- 1) x23) (+ (* 2 x25) (+ (* (- 1) x27) (+ (* 2 x28) (+ (* (- 2) x29) (+ (* (- 1) x30) (+ (* (- 2) x32) (+ (* 1 x37) (+ (* (- 1) x38) (+ (* (- 2) x41) (+ (* 2 x44) (+ (* (- 2) x47) (+ (* 2 x49) (+ (* 1 x50) (+ (* 2 x51) (+ (* 1 x53) (+ (* 2 x55) (+ (* 1 x58) (+ (* (- 1) x59) (+ (* (- 2) x62) (+ (* (- 1) x64) (+ (* 2 x69) (+ (* 2 x70) (+ (* 1 x71) (+ (* (- 2) x72) (+ (* (- 2) x73) (+ (* (- 2) x76) (+ (* 2 x77) (+ (* (- 2) x79) (+ (* (- 2) x80) (+ (* (- 2) x81) (+ (* 1 x82) (+ (* 2 x83) (+ (* 1 x84) (+ (* (- 2) x85) (+ (* 2 x86) (+ (* (- 1) x88) (+ (* (- 1) x89) (+ (* 1 x91) (+ (* 2 x93) (+ (* 2 x94) (+ (* (- 2) x95) (+ (* (- 1) x97) (+ (* (- 1) x98) (* (- 2) x99) )))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= 10 (+ (* 1 x1) (+ (* 1 x2) (+ (* (- 1) x3) (+ (* 1 x4) (+ (* (- 2) x5) (+ (* 1 x7) (+ (* (- 1) x9) (+ (* 2 x10) (+ (* (- 2) x11) (+ (* 2 x13) (+ (* 1 x14) (+ (* (- 2) x16) (+ (* (- 2) x17) (+ (* (- 1) x18) (+ (* 1 x20) (+ (* 2 x21) (+ (* (- 2) x22) (+ (* (- 1) x26) (+ (* 2 x27) (+ (* 2 x32) (+ (* 2 x33) (+ (* (- 2) x34) (+ (* 1 x35) (+ (* 2 x36) (+ (* 1 x37) (+ (* (- 2) x38) (+ (* 2 x39) (+ (* (- 1) x40) (+ (* (- 2) x42) (+ (* 2 x43) (+ (* (- 1) x47) (+ (* 2 x48) (+ (* (- 2) x50) (+ (* 1 x51) (+ (* 1 x52) (+ (* (- 2) x53) (+ (* 2 x54) (+ (* 2 x59) (+ (* 1 x60) (+ (* (- 2) x61) (+ (* 2 x65) (+ (* 1 x66) (+ (* 1 x67) (+ (* 1 x68) (+ (* (- 1) x74) (+ (* (- 2) x77) (+ (* (- 2) x78) (+ (* (- 2) x79) (+ (* 2 x81) (+ (* 1 x83) (+ (* 1 x84) (+ (* (- 2) x85) (+ (* 1 x86) (+ (* 1 x89) (+ (* (- 2) x90) (+ (* 2 x91) (+ (* (- 1) x93) (+ (* (- 2) x95) (+ (* 1 x98) (* (- 1) x99) )))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= (- 1) (+ (* 2 x0) (+ (* 1 x1) (+ (* 2 x3) (+ (* (- 2) x4) (+ (* 2 x5) (+ (* 1 x7) (+ (* (- 2) x9) (+ (* 2 x11) (+ (* (- 1) x14) (+ (* 1 x15) (+ (* (- 1) x17) (+ (* 1 x18) (+ (* (- 1) x19) (+ (* (- 2) x22) (+ (* 2 x23) (+ (* (- 1) x24) (+ (* 2 x26) (+ (* (- 1) x27) (+ (* 1 x28) (+ (* 1 x29) (+ (* (- 1) x30) (+ (* 2 x32) (+ (* 2 x37) (+ (* (- 1) x38) (+ (* (- 1) x40) (+ (* 1 x42) (+ (* (- 2) x43) (+ (* 2 x44) (+ (* (- 2) x45) (+ (* 1 x46) (+ (* 2 x47) (+ (* 2 x48) (+ (* 2 x50) (+ (* (- 1) x51) (+ (* (- 1) x52) (+ (* (- 1) x53) (+ (* 2 x56) (+ (* (- 1) x57) (+ (* (- 1) x60) (+ (* 2 x62) (+ (* (- 2) x63) (+ (* 2 x64) (+ (* 2 x65) (+ (* (- 1) x66) (+ (* (- 1) x67) (+ (* 2 x68) (+ (* 2 x69) (+ (* 2 x70) (+ (* 2 x71) (+ (* 2 x72) (+ (* (- 2) x75) (+ (* 1 x76) (+ (* (- 2) x80) (+ (* 1 x81) (+ (* (- 2) x84) (+ (* 2 x85) (+ (* 2 x87) (+ (* 1 x88) (+ (* (- 2) x89) (+ (* 2 x90) (+ (* (- 1) x93) (+ (* 1 x94) (+ (* 1 x98) (* 2 x99) )))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= 20 (+ (* 2 x1) (+ (* 2 x3) (+ (* 2 x4) (+ (* 2 x7) (+ (* (- 2) x9) (+ (* 2 x10) (+ (* 1 x11) (+ (* 2 x12) (+ (* (- 1) x13) (+ (* 1 x14) (+ (* 2 x15) (+ (* (- 2) x17) (+ (* 1 x23) (+ (* (- 1) x24) (+ (* (- 2) x26) (+ (* (- 1) x27) (+ (* 2 x28) (+ (* 1 x29) (+ (* (- 1) x30) (+ (* (- 1) x31) (+ (* 1 x32) (+ (* (- 2) x33) (+ (* 2 x35) (+ (* 2 x36) (+ (* 1 x39) (+ (* (- 2) x42) (+ (* 2 x45) (+ (* 2 x46) (+ (* (- 2) x48) (+ (* (- 1) x50) (+ (* (- 1) x52) (+ (* (- 1) x54) (+ (* (- 2) x56) (+ (* (- 1) x57) (+ (* 2 x58) (+ (* (- 2) x60) (+ (* 1 x61) (+ (* (- 1) x63) (+ (* (- 1) x65) (+ (* (- 2) x66) (+ (* 2 x67) (+ (* 2 x68) (+ (* (- 2) x69) (+ (* (- 2) x70) (+ (* 1 x71) (+ (* (- 2) x72) (+ (* (- 2) x74) (+ (* 1 x78) (+ (* 2 x80) (+ (* 2 x85) (+ (* 2 x86) (+ (* (- 1) x87) (+ (* (- 2) x88) (+ (* 2 x89) (+ (* (- 1) x91) (+ (* (- 2) x92) (+ (* (- 2) x93) (+ (* 1 x94) (+ (* (- 2) x95) (+ (* (- 2) x96) (+ (* (- 2) x97) (* 1 x99) )))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= 94 (+ (* (- 1) x0) (+ (* 2 x1) (+ (* (- 1) x3) (+ (* (- 1) x4) (+ (* (- 1) x5) (+ (* 2 x6) (+ (* (- 1) x7) (+ (* (- 2) x8) (+ (* 2 x10) (+ (* 2 x11) (+ (* (- 2) x12) (+ (* (- 1) x16) (+ (* 2 x17) (+ (* 1 x18) (+ (* (- 1) x20) (+ (* (- 1) x21) (+ (* (- 1) x24) (+ (* (- 2) x25) (+ (* 2 x26) (+ (* 1 x27) (+ (* (- 1) x28) (+ (* 1 x29) (+ (* (- 1) x31) (+ (* 1 x32) (+ (* (- 2) x33) (+ (* 1 x34) (+ (* 1 x35) (+ (* (- 2) x36) (+ (* 2 x37) (+ (* 2 x38) (+ (* 1 x39) (+ (* 2 x41) (+ (* (- 2) x42) (+ (* 1 x43) (+ (* 2 x44) (+ (* 1 x45) (+ (* (- 2) x47) (+ (* (- 2) x48) (+ (* (- 1) x52) (+ (* (- 2) x53) (+ (* (- 1) x54) (+ (* 2 x56) (+ (* 1 x59) (+ (* 2 x60) (+ (* 2 x61) (+ (* (- 1) x62) (+ (* 1 x63) (+ (* 2 x64) (+ (* (- 1) x65) (+ (* 1 x66) (+ (* (- 2) x67) (+ (* (- 1) x68) (+ (* (- 1) x71) (+ (* (- 1) x74) (+ (* 2 x75) (+ (* (- 2) x76) (+ (* 2 x77) (+ (* (- 2) x78) (+ (* (- 2) x79) (+ (* (- 2) x80) (+ (* (- 1) x81) (+ (* 2 x82) (+ (* (- 1) x83) (+ (* (- 2) x84) (+ (* (- 1) x86) (+ (* 1 x87) (+ (* (- 2) x89) (+ (* (- 2) x90) (+ (* (- 2) x91) (+ (* 2 x92) (+ (* (- 2) x96) (+ (* 1 x97) (* 1 x98) ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= 14 (+ (* 2 x0) (+ (* 1 x1) (+ (* (- 1) x6) (+ (* (- 2) x12) (+ (* 2 x13) (+ (* 2 x14) (+ (* 2 x17) (+ (* (- 1) x19) (+ (* 2 x21) (+ (* 2 x22) (+ (* 1 x24) (+ (* (- 1) x25) (+ (* (- 1) x26) (+ (* (- 2) x29) (+ (* 2 x31) (+ (* (- 1) x33) (+ (* 1 x36) (+ (* 2 x37) (+ (* 1 x38) (+ (* (- 2) x40) (+ (* 2 x42) (+ (* 2 x43) (+ (* 2 x45) (+ (* (- 1) x48) (+ (* 2 x49) (+ (* 1 x50) (+ (* 2 x52) (+ (* (- 2) x53) (+ (* (- 2) x54) (+ (* 1 x55) (+ (* (- 2) x56) (+ (* 2 x57) (+ (* 2 x60) (+ (* (- 1) x62) (+ (* 1 x65) (+ (* 2 x67) (+ (* (- 2) x69) (+ (* (- 2) x70) (+ (* (- 1) x73) (+ (* 2 x77) (+ (* (- 1) x78) (+ (* 2 x79) (+ (* 2 x80) (+ (* 2 x82) (+ (* 2 x88) (+ (* (- 1) x89) (+ (* (- 2) x90) (+ (* 2 x91) (+ (* (- 2) x92) (+ (* (- 1) x93) (+ (* 2 x94) (+ (* (- 2) x95) (+ (* (- 2) x96) (+ (* 1 x97) (+ (* (- 2) x98) (* (- 1) x99) )))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= 42 (+ (* 1 x0) (+ (* 2 x2) (+ (* 1 x5) (+ (* 2 x6) (+ (* 2 x7) (+ (* 1 x8) (+ (* 1 x9) (+ (* 2 x11) (+ (* (- 2) x14) (+ (* 2 x15) (+ (* (- 1) x16) (+ (* 2 x17) (+ (* (- 1) x18) (+ (* 2 x21) (+ (* (- 2) x22) (+ (* (- 2) x23) (+ (* (- 1) x24) (+ (* (- 2) x25) (+ (* 1 x26) (+ (* 2 x29) (+ (* 1 x30) (+ (* (- 2) x31) (+ (* 1 x34) (+ (* (- 1) x37) (+ (* (- 2) x40) (+ (* 1 x45) (+ (* (- 2) x46) (+ (* 2 x47) (+ (* (- 1) x50) (+ (* (- 1) x53) (+ (* 2 x54) (+ (* (- 1) x55) (+ (* (- 2) x57) (+ (* (- 2) x58) (+ (* 2 x59) (+ (* 1 x61) (+ (* (- 2) x62) (+ (* 2 x63) (+ (* 2 x64) (+ (* (- 2) x65) (+ (* 1 x66) (+ (* (- 1) x68) (+ (* 1 x69) (+ (* 2 x71) (+ (* 1 x73) (+ (* (- 2) x79) (+ (* (- 1) x80) (+ (* 2 x83) (+ (* (- 1) x86) (+ (* 2 x87) (+ (* (- 2) x88) (+ (* (- 1) x89) (+ (* 2 x90) (+ (* 1 x91) (+ (* 1 x92) (+ (* 2 x93) (+ (* (- 2) x94) (+ (* (- 1) x96) (+ (* 2 x97) (* (- 1) x99) )))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= (- 6) (+ (* (- 2) x0) (+ (* 1 x1) (+ (* 1 x2) (+ (* (- 2) x3) (+ (* 1 x4) (+ (* 2 x5) (+ (* (- 1) x7) (+ (* (- 1) x9) (+ (* (- 1) x11) (+ (* 1 x13) (+ (* 2 x14) (+ (* 1 x17) (+ (* 1 x20) (+ (* 2 x22) (+ (* 1 x24) (+ (* 1 x25) (+ (* 1 x27) (+ (* (- 1) x31) (+ (* 1 x33) (+ (* (- 2) x34) (+ (* (- 2) x35) (+ (* (- 2) x37) (+ (* 1 x39) (+ (* 1 x40) (+ (* (- 2) x41) (+ (* (- 1) x42) (+ (* (- 1) x43) (+ (* (- 1) x44) (+ (* 1 x45) (+ (* 1 x47) (+ (* 2 x48) (+ (* 2 x52) (+ (* 2 x53) (+ (* (- 2) x56) (+ (* (- 1) x57) (+ (* (- 1) x58) (+ (* (- 2) x61) (+ (* 2 x63) (+ (* (- 2) x66) (+ (* (- 2) x67) (+ (* 2 x69) (+ (* 2 x71) (+ (* 1 x72) (+ (* (- 2) x75) (+ (* (- 1) x76) (+ (* 1 x78) (+ (* (- 2) x79) (+ (* 1 x80) (+ (* 1 x82) (+ (* (- 2) x84) (+ (* 1 x85) (+ (* 2 x87) (+ (* 2 x88) (+ (* (- 1) x89) (+ (* (- 2) x91) (+ (* 2 x94) (+ (* 1 x95) (+ (* (- 2) x96) (+ (* 1 x97) (* (- 2) x98) )))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= 31 (+ (* (- 2) x0) (+ (* 1 x1) (+ (* (- 2) x3) (+ (* (- 2) x4) (+ (* 2 x5) (+ (* 1 x6) (+ (* (- 1) x7) (+ (* (- 2) x8) (+ (* 2 x9) (+ (* 1 x10) (+ (* 1 x11) (+ (* 1 x12) (+ (* (- 2) x14) (+ (* (- 2) x15) (+ (* (- 1) x16) (+ (* 2 x18) (+ (* 2 x19) (+ (* 1 x20) (+ (* 1 x21) (+ (* (- 2) x23) (+ (* 1 x24) (+ (* (- 1) x26) (+ (* (- 1) x27) (+ (* 2 x28) (+ (* 1 x29) (+ (* (- 2) x31) (+ (* 1 x32) (+ (* (- 1) x33) (+ (* 1 x34) (+ (* (- 1) x36) (+ (* 2 x40) (+ (* (- 1) x42) (+ (* (- 1) x47) (+ (* (- 1) x48) (+ (* (- 1) x49) (+ (* (- 2) x50) (+ (* (- 1) x51) (+ (* (- 2) x54) (+ (* (- 1) x56) (+ (* 2 x57) (+ (* (- 1) x58) (+ (* 2 x60) (+ (* (- 1) x64) (+ (* 1 x65) (+ (* (- 2) x68) (+ (* 1 x72) (+ (* 2 x73) (+ (* (- 2) x74) (+ (* 1 x75) (+ (* (- 2) x76) (+ (* 1 x79) (+ (* 2 x80) (+ (* (- 1) x81) (+ (* (- 2) x82) (+ (* 2 x83) (+ (* (- 2) x84) (+ (* (- 2) x86) (+ (* (- 1) x88) (+ (* (- 1) x89) (+ (* (- 2) x91) (+ (* (- 1) x92) (* 1 x98) )))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= (- 5) (+ (* (- 1) x0) (+ (* 1 x1) (+ (* 2 x2) (+ (* 1 x4) (+ (* 1 x5) (+ (* (- 2) x6) (+ (* (- 1) x8) (+ (* (- 1) x10) (+ (* (- 1) x12) (+ (* (- 2) x13) (+ (* 1 x16) (+ (* 2 x20) (+ (* (- 2) x21) (+ (* (- 2) x22) (+ (* 1 x24) (+ (* 1 x25) (+ (* (- 1) x26) (+ (* (- 2) x27) (+ (* (- 1) x29) (+ (* (- 1) x30) (+ (* (- 1) x31) (+ (* (- 1) x32) (+ (* 1 x33) (+ (* (- 1) x34) (+ (* 1 x37) (+ (* 2 x38) (+ (* (- 2) x39) (+ (* 1 x40) (+ (* (- 1) x41) (+ (* 1 x42) (+ (* 2 x48) (+ (* (- 2) x49) (+ (* (- 1) x51) (+ (* (- 2) x52) (+ (* (- 1) x53) (+ (* 2 x57) (+ (* (- 2) x58) (+ (* (- 2) x60) (+ (* 2 x62) (+ (* (- 2) x63) (+ (* 2 x65) (+ (* 2 x66) (+ (* 1 x68) (+ (* (- 1) x69) (+ (* 1 x70) (+ (* (- 1) x71) (+ (* 2 x72) (+ (* (- 1) x74) (+ (* (- 2) x75) (+ (* 1 x76) (+ (* (- 2) x77) (+ (* (- 2) x79) (+ (* 1 x80) (+ (* 2 x82) (+ (* 1 x83) (+ (* 2 x84) (+ (* (- 1) x85) (+ (* (- 2) x86) (+ (* 1 x89) (+ (* (- 1) x90) (+ (* 2 x91) (+ (* (- 2) x92) (+ (* (- 2) x93) (+ (* (- 2) x94) (+ (* (- 1) x97) (+ (* 1 x98) (* 2 x99) ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= (- 24) (+ (* (- 1) x0) (+ (* (- 2) x1) (+ (* (- 1) x3) (+ (* (- 2) x4) (+ (* 1 x8) (+ (* (- 2) x9) (+ (* (- 1) x10) (+ (* 2 x11) (+ (* (- 1) x13) (+ (* (- 1) x15) (+ (* 2 x16) (+ (* (- 1) x18) (+ (* (- 2) x20) (+ (* 1 x23) (+ (* 2 x24) (+ (* 1 x26) (+ (* (- 1) x27) (+ (* 2 x29) (+ (* 2 x30) (+ (* (- 1) x32) (+ (* (- 1) x33) (+ (* (- 2) x38) (+ (* (- 1) x39) (+ (* (- 1) x40) (+ (* (- 1) x44) (+ (* (- 1) x45) (+ (* 2 x48) (+ (* 1 x49) (+ (* 1 x50) (+ (* 1 x51) (+ (* (- 2) x54) (+ (* 2 x56) (+ (* (- 2) x57) (+ (* 1 x58) (+ (* (- 1) x59) (+ (* 2 x60) (+ (* 2 x61) (+ (* 1 x64) (+ (* (- 2) x67) (+ (* (- 1) x68) (+ (* 1 x71) (+ (* 1 x72) (+ (* (- 1) x75) (+ (* 2 x76) (+ (* 2 x79) (+ (* 1 x80) (+ (* 2 x81) (+ (* (- 2) x82) (+ (* (- 2) x87) (+ (* 2 x88) (+ (* (- 1) x89) (+ (* 1 x90) (+ (* 2 x94) (+ (* (- 2) x95) (+ (* 1 x96) (+ (* 2 x97) (+ (* (- 2) x98) (* 1 x99) )))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= (- 38) (+ (* (- 1) x0) (+ (* (- 1) x3) (+ (* 1 x4) (+ (* (- 1) x5) (+ (* 2 x6) (+ (* (- 2) x7) (+ (* 2 x10) (+ (* (- 1) x11) (+ (* (- 2) x12) (+ (* (- 2) x13) (+ (* 1 x15) (+ (* (- 1) x17) (+ (* 1 x18) (+ (* 2 x19) (+ (* (- 1) x21) (+ (* (- 2) x22) (+ (* 1 x23) (+ (* 1 x24) (+ (* (- 1) x25) (+ (* 2 x26) (+ (* 2 x27) (+ (* 1 x28) (+ (* (- 2) x29) (+ (* (- 1) x30) (+ (* 1 x32) (+ (* (- 1) x33) (+ (* 1 x34) (+ (* (- 2) x36) (+ (* (- 2) x37) (+ (* (- 2) x38) (+ (* (- 2) x39) (+ (* 2 x44) (+ (* (- 2) x45) (+ (* 1 x46) (+ (* (- 2) x49) (+ (* 2 x50) (+ (* 1 x51) (+ (* 1 x52) (+ (* (- 1) x54) (+ (* 1 x55) (+ (* 1 x56) (+ (* (- 1) x59) (+ (* 2 x64) (+ (* (- 1) x65) (+ (* (- 1) x67) (+ (* 1 x69) (+ (* 1 x70) (+ (* (- 2) x71) (+ (* (- 2) x72) (+ (* 2 x76) (+ (* (- 1) x81) (+ (* (- 1) x89) (+ (* 1 x90) (+ (* 2 x94) (+ (* (- 2) x95) (+ (* (- 2) x96) (* 2 x97) ))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= (- 8) (+ (* (- 1) x0) (+ (* 2 x1) (+ (* (- 1) x2) (+ (* (- 1) x3) (+ (* 2 x5) (+ (* 2 x9) (+ (* 2 x11) (+ (* 2 x12) (+ (* (- 1) x16) (+ (* (- 1) x17) (+ (* 1 x19) (+ (* (- 1) x21) (+ (* 1 x22) (+ (* 2 x23) (+ (* 2 x24) (+ (* (- 1) x26) (+ (* (- 1) x27) (+ (* 2 x28) (+ (* 2 x31) (+ (* 1 x35) (+ (* (- 2) x38) (+ (* (- 1) x39) (+ (* (- 1) x40) (+ (* 1 x42) (+ (* (- 2) x43) (+ (* 1 x44) (+ (* (- 1) x46) (+ (* 1 x47) (+ (* (- 1) x51) (+ (* 1 x54) (+ (* 2 x57) (+ (* (- 1) x60) (+ (* 1 x61) (+ (* (- 1) x63) (+ (* (- 2) x64) (+ (* (- 2) x65) (+ (* 1 x66) (+ (* (- 1) x67) (+ (* (- 1) x68) (+ (* (- 2) x71) (+ (* 1 x74) (+ (* 1 x75) (+ (* (- 1) x76) (+ (* 2 x77) (+ (* (- 1) x78) (+ (* 1 x82) (+ (* 2 x83) (+ (* 2 x84) (+ (* (- 2) x85) (+ (* (- 2) x86) (+ (* 2 x87) (+ (* 1 x89) (+ (* (- 2) x90) (+ (* (- 2) x92) (+ (* 2 x93) (+ (* (- 2) x94) (+ (* (- 1) x95) (+ (* 2 x96) (+ (* 1 x97) (+ (* (- 2) x98) (* 1 x99) ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= (- 6) (+ (* 2 x0) (+ (* (- 1) x2) (+ (* 1 x3) (+ (* (- 1) x6) (+ (* (- 1) x7) (+ (* 1 x10) (+ (* 2 x11) (+ (* 1 x12) (+ (* 2 x13) (+ (* 2 x14) (+ (* (- 2) x15) (+ (* 1 x18) (+ (* 1 x21) (+ (* 1 x25) (+ (* (- 1) x27) (+ (* (- 1) x29) (+ (* 2 x30) (+ (* (- 1) x31) (+ (* 1 x33) (+ (* 2 x34) (+ (* (- 2) x36) (+ (* 1 x38) (+ (* 1 x41) (+ (* 1 x44) (+ (* (- 1) x47) (+ (* (- 2) x48) (+ (* 1 x49) (+ (* (- 2) x50) (+ (* 1 x52) (+ (* (- 2) x53) (+ (* 2 x57) (+ (* 2 x58) (+ (* 2 x59) (+ (* (- 2) x60) (+ (* (- 2) x61) (+ (* 1 x62) (+ (* (- 1) x64) (+ (* (- 2) x65) (+ (* 2 x66) (+ (* (- 1) x67) (+ (* (- 2) x68) (+ (* 1 x69) (+ (* (- 2) x72) (+ (* 2 x73) (+ (* (- 1) x74) (+ (* 1 x75) (+ (* 1 x76) (+ (* (- 1) x77) (+ (* 1 x79) (+ (* (- 2) x81) (+ (* (- 1) x83) (+ (* 2 x85) (+ (* 2 x87) (+ (* (- 1) x88) (+ (* (- 1) x89) (+ (* 2 x90) (+ (* 2 x94) (+ (* (- 1) x95) (+ (* (- 2) x97) (* 1 x98) )))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= (- 35) (+ (* 2 x2) (+ (* 1 x3) (+ (* (- 2) x4) (+ (* 2 x6) (+ (* (- 1) x9) (+ (* 2 x12) (+ (* 2 x13) (+ (* 2 x14) (+ (* 2 x15) (+ (* (- 1) x17) (+ (* 1 x18) (+ (* 2 x19) (+ (* (- 2) x20) (+ (* (- 2) x21) (+ (* (- 2) x23) (+ (* 2 x24) (+ (* (- 2) x26) (+ (* 2 x28) (+ (* 2 x30) (+ (* (- 2) x31) (+ (* (- 1) x32) (+ (* (- 1) x33) (+ (* (- 2) x36) (+ (* 1 x37) (+ (* (- 1) x38) (+ (* (- 1) x39) (+ (* 2 x44) (+ (* (- 1) x46) (+ (* (- 2) x48) (+ (* 1 x49) (+ (* 2 x50) (+ (* 1 x51) (+ (* (- 1) x52) (+ (* 1 x53) (+ (* 2 x55) (+ (* 2 x57) (+ (* (- 1) x58) (+ (* (- 1) x61) (+ (* 1 x62) (+ (* 1 x65) (+ (* 1 x67) (+ (* (- 1) x68) (+ (* (- 1) x70) (+ (* (- 2) x72) (+ (* (- 2) x73) (+ (* 1 x74) (+ (* 1 x76) (+ (* (- 1) x77) (+ (* (- 1) x78) (+ (* (- 2) x80) (+ (* (- 2) x81) (+ (* (- 1) x82) (+ (* (- 2) x84) (+ (* (- 2) x88) (+ (* 2 x89) (+ (* 1 x90) (+ (* 1 x91) (+ (* 2 x92) (+ (* 2 x93) (+ (* (- 1) x95) (* (- 1) x99) ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= (- 10) (+ (* (- 2) x2) (+ (* 2 x4) (+ (* (- 2) x5) (+ (* (- 2) x6) (+ (* (- 2) x8) (+ (* 2 x9) (+ (* 2 x10) (+ (* 2 x13) (+ (* (- 2) x17) (+ (* (- 2) x18) (+ (* (- 2) x20) (+ (* 1 x21) (+ (* (- 1) x22) (+ (* 2 x24) (+ (* (- 2) x25) (+ (* 1 x26) (+ (* 1 x27) (+ (* (- 1) x28) (+ (* (- 1) x29) (+ (* (- 2) x31) (+ (* (- 1) x32) (+ (* 1 x33) (+ (* 2 x34) (+ (* (- 2) x35) (+ (* 2 x36) (+ (* (- 2) x37) (+ (* 1 x38) (+ (* 1 x39) (+ (* 2 x41) (+ (* 1 x42) (+ (* (- 1) x43) (+ (* 2 x44) (+ (* (- 1) x45) (+ (* (- 2) x47) (+ (* (- 2) x48) (+ (* 2 x49) (+ (* (- 2) x50) (+ (* (- 2) x51) (+ (* (- 2) x53) (+ (* 1 x54) (+ (* (- 1) x55) (+ (* (- 2) x56) (+ (* (- 2) x57) (+ (* (- 1) x58) (+ (* (- 1) x59) (+ (* (- 1) x61) (+ (* (- 1) x62) (+ (* (- 1) x63) (+ (* 2 x64) (+ (* (- 1) x69) (+ (* (- 2) x70) (+ (* 1 x72) (+ (* 1 x74) (+ (* (- 2) x75) (+ (* (- 2) x78) (+ (* 1 x79) (+ (* (- 1) x82) (+ (* 2 x84) (+ (* (- 2) x85) (+ (* (- 1) x87) (+ (* (- 2) x88) (+ (* 2 x90) (+ (* 2 x91) (+ (* (- 2) x92) (+ (* (- 2) x93) (+ (* (- 1) x94) (+ (* (- 2) x96) (* 2 x99) )))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= (- 60) (+ (* (- 2) x1) (+ (* (- 2) x6) (+ (* (- 2) x8) (+ (* 2 x11) (+ (* (- 1) x12) (+ (* (- 2) x13) (+ (* 1 x14) (+ (* (- 2) x15) (+ (* (- 1) x16) (+ (* 2 x17) (+ (* (- 1) x21) (+ (* (- 2) x22) (+ (* (- 2) x23) (+ (* (- 2) x24) (+ (* 1 x25) (+ (* (- 2) x26) (+ (* 2 x28) (+ (* 2 x29) (+ (* 2 x30) (+ (* 2 x32) (+ (* (- 1) x35) (+ (* 1 x36) (+ (* 2 x37) (+ (* (- 2) x38) (+ (* (- 1) x39) (+ (* 1 x41) (+ (* 2 x43) (+ (* (- 2) x47) (+ (* 2 x52) (+ (* 2 x53) (+ (* 2 x54) (+ (* 1 x55) (+ (* (- 2) x58) (+ (* (- 2) x59) (+ (* 1 x60) (+ (* (- 1) x63) (+ (* 1 x65) (+ (* (- 1) x66) (+ (* 2 x68) (+ (* (- 1) x71) (+ (* (- 2) x72) (+ (* (- 1) x73) (+ (* 2 x75) (+ (* 2 x77) (+ (* 2 x78) (+ (* (- 2) x80) (+ (* 2 x81) (+ (* (- 1) x82) (+ (* (- 2) x83) (+ (* 2 x84) (+ (* 2 x86) (+ (* 1 x87) (+ (* (- 2) x93) (+ (* 1 x96) (+ (* (- 2) x98) (* (- 2) x99) )))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= 43 (+ (* (- 2) x2) (+ (* 2 x4) (+ (* (- 1) x6) (+ (* 2 x8) (+ (* 1 x9) (+ (* (- 2) x10) (+ (* (- 1) x12) (+ (* (- 2) x13) (+ (* 2 x17) (+ (* (- 1) x20) (+ (* (- 1) x21) (+ (* 2 x22) (+ (* 1 x23) (+ (* (- 2) x24) (+ (* 1 x25) (+ (* 1 x26) (+ (* (- 1) x27) (+ (* 1 x30) (+ (* (- 1) x32) (+ (* 2 x34) (+ (* (- 1) x35) (+ (* 2 x36) (+ (* 2 x38) (+ (* 2 x40) (+ (* 1 x41) (+ (* (- 2) x42) (+ (* 1 x43) (+ (* 1 x47) (+ (* 1 x48) (+ (* 2 x51) (+ (* 2 x52) (+ (* (- 1) x53) (+ (* 2 x55) (+ (* 1 x56) (+ (* 1 x59) (+ (* (- 1) x60) (+ (* 2 x61) (+ (* (- 2) x63) (+ (* (- 2) x64) (+ (* (- 1) x66) (+ (* (- 1) x68) (+ (* (- 2) x69) (+ (* 2 x71) (+ (* (- 1) x73) (+ (* 1 x74) (+ (* 1 x78) (+ (* (- 1) x79) (+ (* 1 x80) (+ (* 2 x82) (+ (* (- 2) x84) (+ (* (- 1) x85) (+ (* 1 x86) (+ (* 2 x87) (+ (* 2 x88) (+ (* (- 1) x90) (+ (* (- 1) x91) (+ (* (- 1) x92) (+ (* 1 x93) (+ (* (- 2) x95) (+ (* 1 x96) (+ (* 1 x97) (* 1 x99) )))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= 11 (+ (* 2 x1) (+ (* 2 x3) (+ (* (- 1) x5) (+ (* (- 1) x6) (+ (* (- 2) x7) (+ (* (- 1) x9) (+ (* 2 x11) (+ (* 2 x15) (+ (* 2 x16) (+ (* (- 2) x17) (+ (* 2 x19) (+ (* (- 1) x20) (+ (* (- 1) x21) (+ (* 2 x22) (+ (* (- 2) x28) (+ (* (- 1) x33) (+ (* 1 x34) (+ (* (- 2) x35) (+ (* (- 2) x38) (+ (* (- 1) x39) (+ (* 1 x40) (+ (* 1 x43) (+ (* (- 2) x46) (+ (* 1 x48) (+ (* (- 2) x49) (+ (* (- 1) x51) (+ (* (- 1) x58) (+ (* 2 x59) (+ (* 1 x61) (+ (* 1 x62) (+ (* (- 2) x67) (+ (* 1 x72) (+ (* 1 x73) (+ (* (- 1) x74) (+ (* (- 2) x75) (+ (* 2 x76) (+ (* (- 1) x77) (+ (* 2 x78) (+ (* (- 1) x79) (+ (* (- 2) x80) (+ (* 1 x84) (+ (* (- 2) x85) (+ (* (- 1) x87) (+ (* (- 2) x89) (+ (* (- 2) x91) (+ (* 1 x92) (+ (* 1 x93) (+ (* (- 1) x97) (+ (* (- 2) x98) (* 1 x99) )))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= (- 5) (+ (* (- 2) x1) (+ (* 1 x2) (+ (* (- 2) x3) (+ (* (- 2) x4) (+ (* 1 x6) (+ (* 1 x7) (+ (* 2 x9) (+ (* 2 x10) (+ (* (- 1) x12) (+ (* 1 x13) (+ (* 2 x14) (+ (* 1 x15) (+ (* 1 x17) (+ (* 2 x18) (+ (* 2 x19) (+ (* 1 x21) (+ (* (- 2) x22) (+ (* (- 2) x25) (+ (* 2 x26) (+ (* (- 2) x29) (+ (* (- 1) x32) (+ (* (- 1) x35) (+ (* (- 1) x36) (+ (* 1 x38) (+ (* 1 x40) (+ (* 1 x41) (+ (* 2 x42) (+ (* 1 x44) (+ (* (- 1) x46) (+ (* 2 x48) (+ (* 2 x51) (+ (* (- 1) x52) (+ (* (- 1) x53) (+ (* 2 x54) (+ (* 2 x55) (+ (* (- 1) x57) (+ (* (- 2) x58) (+ (* (- 2) x61) (+ (* (- 1) x62) (+ (* 1 x64) (+ (* (- 1) x65) (+ (* 1 x66) (+ (* (- 2) x68) (+ (* 1 x75) (+ (* (- 1) x76) (+ (* (- 2) x77) (+ (* 1 x81) (+ (* (- 2) x83) (+ (* (- 1) x85) (+ (* (- 2) x88) (+ (* (- 2) x90) (+ (* 2 x91) (+ (* (- 1) x93) (+ (* (- 2) x94) (+ (* (- 2) x95) (+ (* (- 2) x97) (+ (* 1 x98) (* 2 x99) )))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= (- 21) (+ (* (- 1) x4) (+ (* 2 x5) (+ (* 2 x6) (+ (* (- 2) x8) (+ (* (- 1) x9) (+ (* 2 x10) (+ (* 2 x13) (+ (* (- 2) x15) (+ (* (- 1) x16) (+ (* (- 2) x17) (+ (* (- 2) x19) (+ (* (- 1) x20) (+ (* (- 2) x21) (+ (* (- 1) x24) (+ (* 1 x25) (+ (* 1 x27) (+ (* 2 x28) (+ (* (- 2) x29) (+ (* 2 x31) (+ (* 2 x33) (+ (* 1 x34) (+ (* (- 1) x35) (+ (* 2 x36) (+ (* (- 2) x37) (+ (* 1 x41) (+ (* 2 x44) (+ (* 2 x45) (+ (* 1 x47) (+ (* (- 2) x48) (+ (* (- 1) x49) (+ (* 2 x50) (+ (* 2 x51) (+ (* 1 x53) (+ (* 1 x55) (+ (* (- 1) x56) (+ (* (- 1) x58) (+ (* 2 x59) (+ (* (- 1) x60) (+ (* 2 x61) (+ (* 1 x62) (+ (* 2 x63) (+ (* (- 1) x65) (+ (* 2 x68) (+ (* (- 2) x70) (+ (* 2 x71) (+ (* 1 x72) (+ (* (- 2) x73) (+ (* (- 1) x74) (+ (* 2 x75) (+ (* 1 x79) (+ (* (- 2) x80) (+ (* (- 2) x81) (+ (* 2 x83) (+ (* (- 2) x84) (+ (* (- 2) x85) (+ (* 1 x90) (+ (* (- 2) x92) (+ (* (- 1) x93) (+ (* (- 2) x94) (+ (* 1 x95) (+ (* (- 2) x96) (* 2 x97) )))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= (- 29) (+ (* 1 x0) (+ (* 2 x1) (+ (* (- 2) x2) (+ (* 2 x3) (+ (* 2 x5) (+ (* 1 x6) (+ (* (- 2) x7) (+ (* 1 x8) (+ (* (- 2) x10) (+ (* 2 x11) (+ (* (- 1) x16) (+ (* (- 2) x18) (+ (* 2 x19) (+ (* 1 x20) (+ (* (- 2) x21) (+ (* (- 2) x22) (+ (* 2 x24) (+ (* 1 x25) (+ (* (- 2) x26) (+ (* (- 1) x28) (+ (* 2 x29) (+ (* 1 x32) (+ (* 2 x33) (+ (* (- 2) x34) (+ (* 2 x35) (+ (* 1 x36) (+ (* (- 2) x37) (+ (* (- 2) x38) (+ (* (- 2) x41) (+ (* 2 x42) (+ (* (- 1) x43) (+ (* (- 1) x46) (+ (* (- 2) x47) (+ (* (- 2) x48) (+ (* 1 x49) (+ (* (- 1) x51) (+ (* (- 2) x53) (+ (* 2 x54) (+ (* (- 2) x55) (+ (* (- 2) x56) (+ (* 1 x57) (+ (* (- 1) x58) (+ (* (- 2) x61) (+ (* (- 2) x62) (+ (* (- 1) x64) (+ (* (- 2) x65) (+ (* 2 x66) (+ (* 2 x67) (+ (* 2 x69) (+ (* 2 x70) (+ (* (- 2) x71) (+ (* 1 x72) (+ (* 2 x73) (+ (* (- 1) x74) (+ (* 2 x76) (+ (* (- 2) x79) (+ (* 1 x80) (+ (* (- 2) x81) (+ (* (- 2) x83) (+ (* (- 2) x86) (+ (* (- 1) x88) (+ (* (- 2) x90) (+ (* 2 x91) (+ (* (- 2) x92) (+ (* 2 x94) (+ (* (- 1) x95) (+ (* (- 1) x97) (* 2 x98) )))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= 26 (+ (* 1 x3) (+ (* 1 x5) (+ (* 2 x6) (+ (* (- 1) x8) (+ (* 2 x10) (+ (* (- 2) x14) (+ (* (- 1) x16) (+ (* 1 x17) (+ (* 1 x19) (+ (* 2 x20) (+ (* (- 2) x21) (+ (* 1 x22) (+ (* 1 x24) (+ (* (- 1) x25) (+ (* 2 x26) (+ (* (- 2) x27) (+ (* (- 2) x30) (+ (* (- 2) x32) (+ (* (- 1) x34) (+ (* 2 x36) (+ (* 1 x37) (+ (* (- 2) x39) (+ (* (- 2) x40) (+ (* (- 2) x42) (+ (* (- 2) x45) (+ (* 1 x48) (+ (* (- 1) x49) (+ (* 2 x53) (+ (* 1 x54) (+ (* (- 2) x56) (+ (* 2 x57) (+ (* (- 2) x62) (+ (* (- 1) x64) (+ (* (- 2) x65) (+ (* 2 x66) (+ (* 2 x67) (+ (* 1 x68) (+ (* (- 2) x69) (+ (* (- 1) x74) (+ (* 1 x77) (+ (* 1 x79) (+ (* (- 1) x80) (+ (* (- 1) x81) (+ (* 1 x82) (+ (* (- 1) x85) (+ (* (- 1) x87) (+ (* (- 2) x88) (+ (* (- 1) x89) (+ (* (- 2) x90) (+ (* (- 2) x96) (+ (* 1 x98) (* 1 x99) )))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= 57 (+ (* 1 x0) (+ (* (- 1) x1) (+ (* (- 1) x2) (+ (* (- 2) x3) (+ (* 1 x5) (+ (* 2 x6) (+ (* 1 x7) (+ (* (- 2) x8) (+ (* (- 2) x10) (+ (* (- 1) x13) (+ (* (- 1) x14) (+ (* (- 1) x15) (+ (* 2 x17) (+ (* (- 2) x19) (+ (* (- 2) x21) (+ (* (- 2) x22) (+ (* (- 2) x24) (+ (* 1 x26) (+ (* 1 x27) (+ (* (- 2) x28) (+ (* (- 1) x29) (+ (* (- 2) x30) (+ (* (- 2) x32) (+ (* 1 x35) (+ (* (- 2) x36) (+ (* (- 2) x38) (+ (* (- 2) x40) (+ (* (- 1) x42) (+ (* 2 x44) (+ (* 2 x45) (+ (* (- 1) x46) (+ (* 1 x47) (+ (* (- 1) x48) (+ (* 1 x49) (+ (* 2 x50) (+ (* (- 1) x51) (+ (* 1 x52) (+ (* 1 x54) (+ (* (- 1) x56) (+ (* (- 2) x57) (+ (* 2 x59) (+ (* 2 x60) (+ (* 2 x61) (+ (* 1 x65) (+ (* (- 2) x66) (+ (* (- 1) x67) (+ (* (- 1) x69) (+ (* 1 x71) (+ (* 1 x72) (+ (* (- 2) x73) (+ (* (- 2) x74) (+ (* (- 1) x75) (+ (* 2 x77) (+ (* (- 1) x81) (+ (* (- 2) x82) (+ (* 1 x83) (+ (* (- 2) x85) (+ (* 2 x88) (+ (* 1 x89) (+ (* 2 x91) (+ (* (- 2) x92) (+ (* (- 1) x94) (+ (* 1 x97) (* 1 x99) )))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= 1 (+ (* (- 2) x0) (+ (* (- 1) x3) (+ (* 1 x5) (+ (* (- 2) x7) (+ (* (- 1) x8) (+ (* 2 x10) (+ (* 1 x12) (+ (* (- 2) x14) (+ (* (- 2) x15) (+ (* 1 x17) (+ (* (- 1) x19) (+ (* (- 1) x21) (+ (* (- 2) x22) (+ (* 1 x23) (+ (* (- 1) x24) (+ (* (- 1) x25) (+ (* 2 x27) (+ (* 2 x28) (+ (* (- 2) x29) (+ (* 1 x30) (+ (* (- 2) x31) (+ (* (- 1) x35) (+ (* 2 x37) (+ (* 2 x38) (+ (* (- 1) x39) (+ (* 1 x40) (+ (* 2 x41) (+ (* 1 x42) (+ (* (- 1) x44) (+ (* 1 x49) (+ (* 1 x50) (+ (* 2 x51) (+ (* (- 1) x52) (+ (* (- 2) x53) (+ (* (- 2) x54) (+ (* 1 x55) (+ (* 1 x56) (+ (* (- 1) x57) (+ (* (- 1) x59) (+ (* 1 x60) (+ (* 1 x63) (+ (* (- 2) x64) (+ (* (- 2) x65) (+ (* (- 2) x66) (+ (* (- 2) x67) (+ (* (- 2) x68) (+ (* 1 x69) (+ (* 2 x71) (+ (* (- 1) x72) (+ (* 2 x73) (+ (* (- 1) x74) (+ (* (- 2) x78) (+ (* (- 2) x79) (+ (* 1 x80) (+ (* (- 2) x81) (+ (* 2 x82) (+ (* 2 x84) (+ (* (- 2) x87) (+ (* (- 1) x88) (+ (* (- 1) x89) (+ (* 2 x90) (+ (* 2 x92) (+ (* 2 x93) (+ (* (- 2) x94) (* (- 1) x99) ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= 4 (+ (* (- 2) x1) (+ (* (- 2) x3) (+ (* (- 1) x4) (+ (* 1 x5) (+ (* (- 2) x6) (+ (* (- 1) x7) (+ (* 1 x8) (+ (* (- 2) x9) (+ (* 1 x10) (+ (* 2 x12) (+ (* 2 x13) (+ (* (- 2) x14) (+ (* 1 x15) (+ (* 2 x16) (+ (* (- 1) x17) (+ (* (- 2) x19) (+ (* (- 2) x20) (+ (* (- 2) x22) (+ (* 1 x26) (+ (* (- 1) x28) (+ (* (- 1) x29) (+ (* 1 x30) (+ (* (- 1) x32) (+ (* (- 1) x34) (+ (* 2 x35) (+ (* (- 1) x37) (+ (* (- 2) x39) (+ (* (- 2) x41) (+ (* (- 2) x42) (+ (* 1 x44) (+ (* (- 1) x46) (+ (* 1 x47) (+ (* 2 x48) (+ (* (- 1) x49) (+ (* (- 2) x50) (+ (* 1 x51) (+ (* (- 1) x53) (+ (* (- 1) x54) (+ (* 2 x57) (+ (* 2 x59) (+ (* 2 x60) (+ (* 2 x61) (+ (* 1 x62) (+ (* (- 1) x64) (+ (* 1 x65) (+ (* (- 2) x67) (+ (* 1 x68) (+ (* (- 1) x70) (+ (* (- 2) x73) (+ (* 2 x74) (+ (* 2 x75) (+ (* (- 1) x77) (+ (* (- 1) x78) (+ (* (- 2) x80) (+ (* 1 x81) (+ (* 2 x83) (+ (* 1 x84) (+ (* 2 x85) (+ (* 1 x86) (+ (* (- 1) x87) (+ (* 1 x90) (+ (* (- 2) x93) (+ (* 1 x94) (+ (* 2 x95) (+ (* (- 2) x97) (* (- 2) x99) )))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= (- 18) (+ (* (- 1) x0) (+ (* 2 x1) (+ (* (- 1) x5) (+ (* 2 x7) (+ (* (- 2) x9) (+ (* (- 1) x10) (+ (* 2 x11) (+ (* (- 1) x13) (+ (* (- 1) x15) (+ (* 2 x16) (+ (* (- 1) x17) (+ (* (- 2) x19) (+ (* (- 1) x20) (+ (* 2 x21) (+ (* (- 1) x24) (+ (* (- 1) x25) (+ (* (- 1) x27) (+ (* (- 1) x28) (+ (* 1 x29) (+ (* 1 x31) (+ (* (- 1) x32) (+ (* 2 x33) (+ (* 1 x34) (+ (* (- 2) x35) (+ (* (- 2) x36) (+ (* 1 x40) (+ (* 1 x41) (+ (* (- 1) x42) (+ (* (- 1) x43) (+ (* (- 2) x47) (+ (* (- 2) x49) (+ (* 1 x51) (+ (* (- 2) x52) (+ (* 2 x53) (+ (* 1 x54) (+ (* 2 x55) (+ (* (- 1) x57) (+ (* (- 2) x59) (+ (* 2 x61) (+ (* 1 x62) (+ (* 1 x66) (+ (* 1 x67) (+ (* 1 x68) (+ (* 2 x69) (+ (* 2 x70) (+ (* 1 x71) (+ (* (- 2) x73) (+ (* 1 x74) (+ (* 1 x75) (+ (* (- 2) x78) (+ (* (- 2) x80) (+ (* (- 2) x82) (+ (* (- 2) x84) (+ (* 2 x88) (+ (* 1 x89) (+ (* 1 x90) (+ (* (- 1) x91) (+ (* 1 x92) (+ (* (- 2) x95) (+ (* (- 1) x97) (* 1 x99) ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= 16 (+ (* 2 x0) (+ (* 1 x1) (+ (* 1 x4) (+ (* 1 x6) (+ (* 1 x7) (+ (* (- 2) x8) (+ (* (- 1) x12) (+ (* 1 x17) (+ (* 2 x20) (+ (* 2 x21) (+ (* 1 x22) (+ (* (- 2) x23) (+ (* 2 x25) (+ (* (- 2) x26) (+ (* (- 1) x27) (+ (* (- 1) x30) (+ (* (- 1) x32) (+ (* (- 1) x33) (+ (* 1 x34) (+ (* (- 1) x35) (+ (* 1 x36) (+ (* 1 x38) (+ (* (- 1) x39) (+ (* (- 2) x43) (+ (* (- 2) x44) (+ (* 1 x46) (+ (* 2 x51) (+ (* 1 x52) (+ (* 2 x56) (+ (* 1 x57) (+ (* (- 2) x58) (+ (* 2 x59) (+ (* (- 1) x60) (+ (* 2 x61) (+ (* (- 1) x63) (+ (* 1 x64) (+ (* (- 2) x65) (+ (* 1 x66) (+ (* (- 1) x68) (+ (* (- 2) x72) (+ (* (- 1) x73) (+ (* 2 x74) (+ (* (- 2) x75) (+ (* (- 1) x80) (+ (* 2 x81) (+ (* 1 x82) (+ (* 2 x83) (+ (* 1 x84) (+ (* (- 1) x85) (+ (* 1 x88) (+ (* 1 x89) (+ (* 1 x90) (+ (* 1 x91) (+ (* (- 1) x92) (+ (* (- 2) x93) (+ (* 1 x94) (+ (* (- 1) x96) (* (- 2) x97) )))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= (- 48) (+ (* (- 2) x0) (+ (* 1 x2) (+ (* (- 2) x3) (+ (* 1 x4) (+ (* 2 x5) (+ (* 1 x6) (+ (* 1 x7) (+ (* 2 x10) (+ (* 2 x11) (+ (* (- 2) x13) (+ (* 1 x15) (+ (* (- 2) x16) (+ (* 1 x19) (+ (* (- 1) x20) (+ (* 1 x21) (+ (* 2 x22) (+ (* 2 x23) (+ (* (- 1) x26) (+ (* 1 x27) (+ (* 2 x28) (+ (* (- 2) x30) (+ (* 2 x31) (+ (* 2 x36) (+ (* 1 x39) (+ (* 1 x41) (+ (* (- 1) x43) (+ (* 2 x45) (+ (* 1 x48) (+ (* (- 1) x49) (+ (* (- 1) x50) (+ (* 2 x51) (+ (* (- 1) x56) (+ (* 1 x57) (+ (* (- 2) x58) (+ (* (- 1) x59) (+ (* (- 2) x61) (+ (* 2 x62) (+ (* 1 x63) (+ (* (- 2) x65) (+ (* 2 x68) (+ (* (- 2) x69) (+ (* (- 2) x70) (+ (* (- 1) x72) (+ (* (- 1) x73) (+ (* 2 x74) (+ (* (- 2) x75) (+ (* 2 x76) (+ (* (- 1) x77) (+ (* (- 1) x78) (+ (* (- 2) x83) (+ (* (- 2) x86) (+ (* 1 x88) (+ (* (- 1) x89) (+ (* 2 x90) (+ (* (- 1) x92) (+ (* 2 x93) (+ (* 2 x94) (+ (* 2 x95) (+ (* 1 x96) (+ (* 1 x97) (+ (* (- 2) x98) (* (- 2) x99) )))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= 3 (+ (* (- 1) x1) (+ (* (- 2) x2) (+ (* (- 1) x3) (+ (* (- 2) x4) (+ (* 1 x5) (+ (* (- 1) x7) (+ (* 1 x8) (+ (* 1 x10) (+ (* (- 2) x14) (+ (* 2 x15) (+ (* (- 1) x19) (+ (* (- 1) x21) (+ (* (- 1) x22) (+ (* (- 2) x23) (+ (* 1 x25) (+ (* (- 1) x26) (+ (* 2 x28) (+ (* 1 x32) (+ (* (- 1) x36) (+ (* (- 2) x37) (+ (* 1 x38) (+ (* (- 2) x40) (+ (* 1 x41) (+ (* 2 x42) (+ (* 1 x44) (+ (* 2 x46) (+ (* 1 x47) (+ (* (- 2) x49) (+ (* (- 2) x50) (+ (* (- 2) x51) (+ (* 2 x52) (+ (* (- 1) x58) (+ (* (- 1) x59) (+ (* 2 x60) (+ (* (- 2) x61) (+ (* 2 x62) (+ (* (- 1) x64) (+ (* (- 1) x65) (+ (* (- 1) x68) (+ (* (- 1) x70) (+ (* 1 x71) (+ (* 1 x74) (+ (* 1 x77) (+ (* 1 x78) (+ (* (- 2) x81) (+ (* (- 1) x83) (+ (* (- 1) x87) (+ (* (- 2) x91) (+ (* (- 2) x92) (+ (* 2 x94) (+ (* 1 x95) (+ (* (- 1) x96) (+ (* 2 x97) (* 2 x98) )))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= 28 (+ (* (- 2) x0) (+ (* (- 1) x1) (+ (* (- 2) x3) (+ (* 1 x6) (+ (* (- 1) x7) (+ (* 1 x9) (+ (* 2 x10) (+ (* (- 1) x11) (+ (* (- 1) x13) (+ (* 1 x14) (+ (* 1 x15) (+ (* 1 x19) (+ (* (- 2) x23) (+ (* (- 2) x24) (+ (* 2 x25) (+ (* (- 1) x26) (+ (* 1 x27) (+ (* (- 1) x28) (+ (* 1 x29) (+ (* 1 x30) (+ (* (- 1) x31) (+ (* (- 1) x35) (+ (* (- 2) x36) (+ (* (- 2) x37) (+ (* (- 2) x39) (+ (* (- 1) x41) (+ (* 1 x43) (+ (* 2 x44) (+ (* (- 2) x45) (+ (* 2 x46) (+ (* (- 2) x48) (+ (* (- 1) x49) (+ (* 1 x50) (+ (* 1 x51) (+ (* 1 x52) (+ (* (- 2) x54) (+ (* (- 1) x56) (+ (* (- 2) x57) (+ (* (- 1) x58) (+ (* (- 1) x61) (+ (* (- 1) x63) (+ (* (- 2) x67) (+ (* (- 2) x69) (+ (* 2 x70) (+ (* 2 x71) (+ (* 2 x73) (+ (* (- 2) x74) (+ (* 1 x77) (+ (* (- 2) x78) (+ (* (- 2) x80) (+ (* 2 x81) (+ (* 2 x83) (+ (* (- 1) x84) (+ (* (- 2) x85) (+ (* (- 1) x87) (+ (* (- 1) x88) (+ (* (- 1) x89) (+ (* (- 2) x95) (+ (* 1 x96) (* (- 1) x97) )))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= (- 30) (+ (* 1 x1) (+ (* 2 x4) (+ (* 2 x5) (+ (* (- 2) x6) (+ (* 1 x7) (+ (* (- 1) x8) (+ (* 1 x9) (+ (* (- 1) x13) (+ (* (- 2) x16) (+ (* 1 x18) (+ (* 2 x20) (+ (* (- 2) x23) (+ (* 1 x27) (+ (* 1 x28) (+ (* 2 x31) (+ (* (- 1) x32) (+ (* (- 1) x36) (+ (* 2 x37) (+ (* 1 x39) (+ (* 2 x40) (+ (* 2 x41) (+ (* 1 x42) (+ (* 1 x43) (+ (* 2 x44) (+ (* 1 x46) (+ (* 1 x47) (+ (* 2 x50) (+ (* 2 x51) (+ (* 1 x52) (+ (* 2 x56) (+ (* 1 x59) (+ (* (- 2) x60) (+ (* (- 1) x61) (+ (* (- 2) x64) (+ (* 2 x66) (+ (* (- 2) x67) (+ (* (- 1) x68) (+ (* 2 x69) (+ (* 2 x70) (+ (* (- 1) x71) (+ (* 1 x73) (+ (* 2 x74) (+ (* 2 x76) (+ (* (- 2) x77) (+ (* 2 x79) (+ (* 2 x80) (+ (* 1 x83) (+ (* (- 1) x84) (+ (* 2 x85) (+ (* 1 x86) (+ (* (- 1) x87) (+ (* 1 x89) (+ (* 1 x90) (+ (* 1 x91) (+ (* (- 1) x92) (+ (* (- 2) x93) (+ (* (- 1) x94) (+ (* (- 1) x95) (+ (* (- 2) x97) (* (- 2) x98) )))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= (- 5) (+ (* (- 2) x0) (+ (* (- 2) x1) (+ (* (- 2) x4) (+ (* (- 1) x5) (+ (* 2 x7) (+ (* 2 x8) (+ (* (- 1) x9) (+ (* 1 x12) (+ (* 2 x17) (+ (* (- 2) x18) (+ (* 1 x19) (+ (* 1 x20) (+ (* (- 2) x21) (+ (* 2 x22) (+ (* (- 1) x23) (+ (* (- 2) x24) (+ (* (- 1) x25) (+ (* 2 x26) (+ (* 1 x27) (+ (* (- 1) x28) (+ (* (- 1) x31) (+ (* 2 x33) (+ (* (- 1) x34) (+ (* (- 2) x35) (+ (* (- 1) x36) (+ (* 2 x37) (+ (* (- 2) x39) (+ (* 1 x40) (+ (* 2 x41) (+ (* (- 2) x44) (+ (* (- 2) x45) (+ (* 1 x46) (+ (* 2 x47) (+ (* 1 x48) (+ (* (- 2) x50) (+ (* (- 2) x51) (+ (* (- 2) x54) (+ (* 1 x55) (+ (* 2 x56) (+ (* 2 x57) (+ (* (- 1) x58) (+ (* 2 x60) (+ (* (- 2) x62) (+ (* 1 x63) (+ (* 1 x65) (+ (* (- 1) x66) (+ (* (- 1) x67) (+ (* (- 1) x68) (+ (* 1 x69) (+ (* (- 2) x70) (+ (* (- 1) x71) (+ (* (- 1) x75) (+ (* (- 1) x76) (+ (* 2 x78) (+ (* 1 x79) (+ (* (- 1) x80) (+ (* (- 1) x81) (+ (* 1 x85) (+ (* (- 1) x86) (+ (* (- 2) x87) (+ (* (- 2) x90) (+ (* (- 2) x91) (+ (* (- 2) x92) (+ (* 2 x93) (+ (* 2 x94) (+ (* (- 2) x95) (+ (* (- 2) x96) (+ (* 2 x97) (* (- 2) x98) ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= (- 17) (+ (* 2 x3) (+ (* (- 1) x8) (+ (* (- 2) x9) (+ (* (- 2) x11) (+ (* 2 x14) (+ (* (- 1) x15) (+ (* 2 x16) (+ (* (- 2) x17) (+ (* 1 x20) (+ (* 1 x21) (+ (* (- 2) x23) (+ (* 1 x24) (+ (* (- 2) x26) (+ (* 1 x28) (+ (* (- 2) x29) (+ (* (- 1) x31) (+ (* 1 x37) (+ (* (- 1) x38) (+ (* (- 2) x39) (+ (* (- 2) x40) (+ (* (- 1) x41) (+ (* 2 x43) (+ (* (- 2) x45) (+ (* (- 2) x46) (+ (* 1 x48) (+ (* (- 1) x50) (+ (* 2 x51) (+ (* 1 x52) (+ (* 1 x58) (+ (* 1 x60) (+ (* 2 x61) (+ (* 1 x64) (+ (* 1 x66) (+ (* 2 x71) (+ (* (- 2) x73) (+ (* 2 x77) (+ (* 2 x78) (+ (* (- 2) x80) (+ (* (- 1) x82) (+ (* 2 x85) (+ (* 1 x86) (+ (* (- 2) x88) (+ (* 2 x91) (+ (* 1 x94) (+ (* 1 x95) (+ (* (- 2) x96) (+ (* (- 1) x97) (* 1 x98) )))))))))))))))))))))))))))))))))))))))))))))))) 
(<= (- 16) (+ (* 1 x0) (+ (* (- 2) x1) (+ (* (- 1) x2) (+ (* 1 x7) (+ (* 1 x10) (+ (* (- 2) x11) (+ (* 1 x13) (+ (* (- 1) x20) (+ (* (- 1) x21) (+ (* (- 1) x22) (+ (* 1 x23) (+ (* 2 x24) (+ (* (- 2) x25) (+ (* 1 x28) (+ (* (- 1) x30) (+ (* 2 x31) (+ (* (- 2) x34) (+ (* (- 1) x35) (+ (* (- 2) x36) (+ (* 1 x37) (+ (* 1 x38) (+ (* 1 x39) (+ (* 2 x40) (+ (* (- 2) x42) (+ (* (- 2) x43) (+ (* (- 2) x44) (+ (* 2 x46) (+ (* 2 x52) (+ (* (- 1) x54) (+ (* (- 2) x57) (+ (* (- 1) x58) (+ (* (- 2) x60) (+ (* (- 1) x65) (+ (* (- 1) x68) (+ (* (- 1) x69) (+ (* (- 2) x72) (+ (* (- 1) x73) (+ (* 1 x78) (+ (* 1 x79) (+ (* 2 x80) (+ (* 1 x81) (+ (* 1 x82) (+ (* (- 1) x85) (+ (* 2 x86) (+ (* (- 1) x87) (+ (* 1 x88) (+ (* 1 x89) (+ (* 2 x90) (+ (* 1 x91) (+ (* 2 x96) (+ (* 2 x98) (* 2 x99) )))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= (- 6) (+ (* 1 x0) (+ (* (- 2) x3) (+ (* 1 x4) (+ (* (- 2) x5) (+ (* (- 1) x6) (+ (* 2 x9) (+ (* 1 x10) (+ (* (- 2) x11) (+ (* 2 x13) (+ (* (- 2) x15) (+ (* (- 1) x16) (+ (* (- 1) x17) (+ (* 1 x18) (+ (* (- 2) x23) (+ (* (- 1) x24) (+ (* 2 x27) (+ (* (- 1) x28) (+ (* 1 x31) (+ (* (- 2) x32) (+ (* 2 x33) (+ (* (- 2) x36) (+ (* (- 2) x37) (+ (* 1 x39) (+ (* (- 1) x40) (+ (* (- 2) x41) (+ (* (- 2) x44) (+ (* 2 x46) (+ (* (- 1) x47) (+ (* (- 2) x48) (+ (* (- 1) x52) (+ (* (- 2) x53) (+ (* 2 x54) (+ (* (- 1) x55) (+ (* 2 x56) (+ (* (- 1) x58) (+ (* (- 2) x60) (+ (* 2 x62) (+ (* 2 x63) (+ (* 2 x64) (+ (* (- 2) x65) (+ (* (- 1) x66) (+ (* 1 x67) (+ (* (- 2) x68) (+ (* (- 1) x70) (+ (* 1 x71) (+ (* 2 x72) (+ (* 2 x74) (+ (* 1 x76) (+ (* (- 1) x77) (+ (* 1 x78) (+ (* (- 2) x79) (+ (* (- 1) x81) (+ (* (- 2) x82) (+ (* (- 1) x84) (+ (* (- 1) x85) (+ (* (- 1) x86) (+ (* 2 x90) (+ (* (- 2) x92) (+ (* 1 x94) (+ (* (- 2) x96) (+ (* (- 1) x97) (* 1 x99) )))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= 28 (+ (* (- 1) x2) (+ (* 1 x3) (+ (* 1 x5) (+ (* 2 x7) (+ (* 1 x9) (+ (* 2 x10) (+ (* 2 x11) (+ (* (- 1) x12) (+ (* (- 1) x16) (+ (* 2 x17) (+ (* 2 x18) (+ (* 2 x20) (+ (* 2 x21) (+ (* (- 1) x23) (+ (* (- 1) x24) (+ (* (- 2) x27) (+ (* (- 2) x28) (+ (* (- 2) x30) (+ (* (- 1) x31) (+ (* (- 1) x32) (+ (* (- 2) x33) (+ (* (- 2) x34) (+ (* 1 x35) (+ (* (- 1) x36) (+ (* (- 2) x37) (+ (* (- 1) x38) (+ (* (- 2) x40) (+ (* (- 1) x46) (+ (* (- 1) x48) (+ (* 2 x50) (+ (* 2 x51) (+ (* (- 2) x52) (+ (* 2 x53) (+ (* (- 1) x54) (+ (* (- 1) x55) (+ (* 2 x56) (+ (* 1 x57) (+ (* 2 x58) (+ (* 1 x60) (+ (* 2 x62) (+ (* (- 1) x63) (+ (* (- 1) x68) (+ (* 1 x69) (+ (* (- 1) x70) (+ (* 2 x71) (+ (* (- 2) x72) (+ (* 2 x73) (+ (* (- 2) x74) (+ (* 2 x75) (+ (* 1 x77) (+ (* (- 2) x81) (+ (* 1 x82) (+ (* (- 2) x84) (+ (* 2 x85) (+ (* 2 x87) (+ (* (- 2) x89) (+ (* 1 x91) (+ (* (- 2) x92) (+ (* 2 x93) (* 2 x99) )))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= 10 (+ (* (- 1) x0) (+ (* (- 2) x2) (+ (* (- 2) x4) (+ (* (- 2) x6) (+ (* (- 1) x8) (+ (* (- 1) x10) (+ (* 2 x11) (+ (* 1 x14) (+ (* (- 2) x15) (+ (* (- 2) x19) (+ (* 1 x20) (+ (* (- 1) x26) (+ (* (- 2) x27) (+ (* (- 2) x29) (+ (* 1 x30) (+ (* 1 x34) (+ (* (- 1) x35) (+ (* 1 x37) (+ (* 2 x38) (+ (* 1 x43) (+ (* 2 x45) (+ (* 1 x47) (+ (* 1 x50) (+ (* 2 x52) (+ (* 1 x54) (+ (* 1 x55) (+ (* 1 x57) (+ (* 1 x58) (+ (* 1 x59) (+ (* 1 x60) (+ (* (- 1) x62) (+ (* (- 1) x64) (+ (* 1 x65) (+ (* 1 x66) (+ (* (- 2) x67) (+ (* (- 2) x69) (+ (* (- 2) x72) (+ (* 2 x76) (+ (* (- 2) x79) (+ (* 2 x81) (+ (* 2 x82) (+ (* 2 x84) (+ (* 2 x86) (+ (* 1 x88) (+ (* (- 2) x89) (+ (* (- 1) x90) (+ (* 1 x94) (+ (* (- 2) x95) (+ (* 2 x96) (+ (* 1 x97) (* (- 1) x98) ))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= (- 19) (+ (* 1 x0) (+ (* 1 x7) (+ (* 2 x9) (+ (* 2 x10) (+ (* (- 1) x12) (+ (* 1 x16) (+ (* 1 x18) (+ (* 2 x19) (+ (* (- 2) x21) (+ (* 2 x23) (+ (* 1 x26) (+ (* (- 1) x27) (+ (* (- 1) x28) (+ (* 1 x30) (+ (* 2 x31) (+ (* 1 x32) (+ (* 1 x33) (+ (* (- 2) x35) (+ (* (- 1) x36) (+ (* (- 1) x38) (+ (* (- 2) x39) (+ (* 2 x40) (+ (* (- 1) x41) (+ (* 1 x42) (+ (* 2 x43) (+ (* 2 x44) (+ (* 2 x47) (+ (* 1 x49) (+ (* (- 2) x50) (+ (* 2 x51) (+ (* (- 2) x52) (+ (* 2 x53) (+ (* (- 2) x54) (+ (* (- 1) x55) (+ (* (- 2) x56) (+ (* 1 x59) (+ (* (- 1) x60) (+ (* 2 x61) (+ (* 2 x62) (+ (* (- 2) x63) (+ (* 1 x64) (+ (* 1 x65) (+ (* (- 2) x66) (+ (* (- 2) x67) (+ (* (- 2) x69) (+ (* 1 x70) (+ (* (- 1) x72) (+ (* 2 x73) (+ (* (- 1) x74) (+ (* (- 1) x76) (+ (* 2 x79) (+ (* (- 1) x80) (+ (* (- 1) x81) (+ (* 2 x82) (+ (* (- 1) x84) (+ (* 1 x85) (+ (* 2 x86) (+ (* 1 x87) (+ (* 1 x88) (+ (* (- 1) x90) (+ (* (- 2) x92) (+ (* 1 x94) (+ (* 2 x95) (+ (* 2 x96) (* (- 1) x98) ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= (- 2) (+ (* 2 x0) (+ (* 2 x2) (+ (* (- 1) x4) (+ (* (- 2) x5) (+ (* 2 x6) (+ (* (- 1) x8) (+ (* (- 1) x9) (+ (* 2 x10) (+ (* 1 x12) (+ (* 2 x14) (+ (* 2 x15) (+ (* 2 x16) (+ (* 2 x17) (+ (* (- 2) x18) (+ (* (- 1) x19) (+ (* (- 1) x20) (+ (* 2 x22) (+ (* (- 2) x23) (+ (* (- 1) x24) (+ (* 2 x25) (+ (* 2 x26) (+ (* 2 x29) (+ (* (- 2) x32) (+ (* 2 x35) (+ (* 1 x40) (+ (* 1 x41) (+ (* 1 x43) (+ (* 2 x44) (+ (* 1 x45) (+ (* 2 x46) (+ (* (- 1) x47) (+ (* (- 2) x48) (+ (* (- 2) x49) (+ (* 2 x51) (+ (* 2 x52) (+ (* (- 2) x54) (+ (* 1 x55) (+ (* (- 1) x57) (+ (* (- 1) x58) (+ (* 2 x62) (+ (* 1 x63) (+ (* (- 1) x65) (+ (* (- 2) x66) (+ (* (- 2) x67) (+ (* (- 1) x68) (+ (* (- 1) x75) (+ (* (- 1) x76) (+ (* 2 x77) (+ (* (- 2) x78) (+ (* (- 1) x80) (+ (* 1 x81) (+ (* 1 x82) (+ (* (- 1) x83) (+ (* (- 1) x84) (+ (* (- 2) x85) (+ (* 1 x87) (+ (* 1 x89) (+ (* 2 x90) (+ (* 2 x92) (+ (* 1 x93) (+ (* (- 1) x94) (+ (* (- 2) x95) (+ (* 2 x96) (+ (* (- 1) x97) (* 2 x98) ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= 2 (+ (* 1 x1) (+ (* (- 1) x2) (+ (* 2 x4) (+ (* (- 1) x5) (+ (* (- 2) x6) (+ (* 2 x7) (+ (* (- 1) x8) (+ (* 1 x9) (+ (* (- 1) x11) (+ (* (- 1) x13) (+ (* 1 x16) (+ (* (- 1) x17) (+ (* (- 1) x18) (+ (* (- 2) x19) (+ (* 1 x20) (+ (* 1 x23) (+ (* (- 2) x25) (+ (* (- 2) x26) (+ (* 2 x27) (+ (* 2 x28) (+ (* 2 x31) (+ (* 1 x34) (+ (* (- 2) x35) (+ (* (- 2) x36) (+ (* (- 2) x37) (+ (* 2 x38) (+ (* 1 x42) (+ (* 1 x43) (+ (* 2 x45) (+ (* (- 2) x46) (+ (* 1 x48) (+ (* (- 1) x49) (+ (* (- 1) x50) (+ (* (- 1) x51) (+ (* (- 1) x52) (+ (* (- 1) x54) (+ (* 1 x56) (+ (* 1 x57) (+ (* 2 x59) (+ (* 1 x60) (+ (* 1 x61) (+ (* 1 x62) (+ (* 1 x63) (+ (* (- 1) x64) (+ (* (- 2) x65) (+ (* (- 2) x66) (+ (* 1 x68) (+ (* (- 2) x71) (+ (* (- 2) x72) (+ (* (- 1) x74) (+ (* 2 x77) (+ (* 1 x78) (+ (* (- 1) x79) (+ (* (- 2) x80) (+ (* 2 x81) (+ (* (- 1) x82) (+ (* 2 x83) (+ (* (- 2) x85) (+ (* 1 x86) (+ (* (- 2) x87) (+ (* (- 2) x92) (+ (* 1 x94) (+ (* 2 x95) (+ (* 2 x97) (+ (* 1 x98) (* 2 x99) )))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= (- 22) (+ (* (- 1) x0) (+ (* (- 1) x2) (+ (* (- 1) x3) (+ (* 1 x4) (+ (* (- 2) x5) (+ (* (- 2) x7) (+ (* (- 2) x8) (+ (* (- 2) x9) (+ (* 2 x10) (+ (* (- 2) x13) (+ (* (- 1) x18) (+ (* (- 1) x20) (+ (* (- 1) x21) (+ (* 1 x22) (+ (* (- 2) x23) (+ (* (- 1) x24) (+ (* (- 2) x26) (+ (* 2 x27) (+ (* (- 1) x28) (+ (* (- 2) x30) (+ (* (- 2) x35) (+ (* (- 1) x36) (+ (* (- 1) x37) (+ (* (- 2) x38) (+ (* 1 x40) (+ (* 1 x44) (+ (* (- 1) x45) (+ (* 2 x46) (+ (* 2 x49) (+ (* 1 x50) (+ (* 2 x52) (+ (* (- 1) x57) (+ (* (- 2) x58) (+ (* 1 x60) (+ (* (- 1) x61) (+ (* (- 1) x63) (+ (* (- 1) x65) (+ (* 1 x66) (+ (* (- 1) x67) (+ (* 2 x68) (+ (* (- 1) x71) (+ (* (- 2) x72) (+ (* (- 2) x76) (+ (* (- 1) x77) (+ (* 1 x79) (+ (* 2 x81) (+ (* 1 x82) (+ (* 1 x83) (+ (* (- 2) x85) (+ (* 1 x86) (+ (* (- 1) x87) (+ (* 2 x90) (+ (* (- 1) x92) (+ (* 2 x93) (+ (* 2 x94) (+ (* 1 x95) (+ (* (- 2) x96) (* 2 x99) )))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= (- 22) (+ (* (- 2) x1) (+ (* 1 x2) (+ (* 2 x5) (+ (* (- 1) x9) (+ (* (- 1) x10) (+ (* (- 1) x11) (+ (* 2 x12) (+ (* 1 x13) (+ (* (- 1) x16) (+ (* (- 2) x17) (+ (* 2 x20) (+ (* (- 1) x23) (+ (* (- 1) x24) (+ (* 1 x25) (+ (* 1 x26) (+ (* (- 1) x28) (+ (* 1 x30) (+ (* 1 x32) (+ (* 2 x33) (+ (* (- 1) x34) (+ (* 1 x35) (+ (* (- 2) x36) (+ (* 1 x37) (+ (* (- 1) x38) (+ (* 1 x40) (+ (* (- 1) x41) (+ (* 1 x42) (+ (* 1 x43) (+ (* (- 1) x45) (+ (* 1 x46) (+ (* 1 x48) (+ (* (- 1) x49) (+ (* (- 2) x51) (+ (* 1 x52) (+ (* 2 x54) (+ (* 2 x55) (+ (* (- 2) x56) (+ (* 2 x58) (+ (* 2 x64) (+ (* 1 x66) (+ (* (- 1) x68) (+ (* 1 x69) (+ (* 2 x70) (+ (* (- 1) x71) (+ (* 2 x73) (+ (* (- 2) x76) (+ (* 1 x78) (+ (* 2 x79) (+ (* 1 x81) (+ (* 2 x82) (+ (* 1 x83) (+ (* (- 1) x84) (+ (* 1 x86) (+ (* (- 2) x87) (+ (* (- 1) x88) (+ (* 2 x89) (+ (* (- 2) x90) (+ (* (- 1) x91) (+ (* 1 x94) (+ (* 2 x95) (+ (* 1 x96) (* (- 1) x97) )))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= 771 (+ (* (- 5) x0) (+ (* (- 2) x1) (+ (* (- 3) x2) (+ (* 45 x3) (+ (* 10 x4) (+ (* (- 27) x5) (+ (* (- 39) x6) (+ (* 1 x7) (+ (* 42 x8) (+ (* 17 x9) (+ (* (- 46) x10) (+ (* (- 71) x11) (+ (* 4 x12) (+ (* 17 x13) (+ (* 1 x14) (+ (* 42 x15) (+ (* (- 37) x16) (+ (* (- 27) x17) (+ (* 2 x18) (+ (* (- 43) x19) (+ (* 28 x20) (+ (* 28 x21) (+ (* (- 20) x22) (+ (* 55 x23) (+ (* 8 x24) (+ (* (- 17) x25) (+ (* 8 x26) (+ (* (- 33) x27) (+ (* (- 8) x28) (+ (* (- 14) x29) (+ (* (- 15) x30) (+ (* 29 x31) (+ (* 55 x32) (+ (* 15 x33) (+ (* (- 62) x34) (+ (* 25 x35) (+ (* 49 x36) (+ (* 46 x37) (+ (* (- 21) x38) (+ (* 10 x39) (+ (* (- 34) x40) (+ (* 19 x41) (+ (* (- 11) x42) (+ (* (- 17) x43) (+ (* (- 92) x44) (+ (* (- 4) x45) (+ (* (- 5) x46) (+ (* (- 18) x47) (+ (* (- 34) x48) (+ (* (- 10) x49) (+ (* (- 41) x50) (+ (* (- 107) x51) (+ (* (- 69) x52) (+ (* (- 25) x53) (+ (* 15 x54) (+ (* (- 39) x55) (+ (* (- 10) x56) (+ (* 38 x57) (+ (* 67 x58) (+ (* (- 35) x59) (+ (* 2 x60) (+ (* (- 15) x61) (+ (* 12 x63) (+ (* 52 x64) (+ (* 40 x65) (+ (* 5 x66) (+ (* 63 x67) (+ (* 33 x68) (+ (* (- 1) x69) (+ (* 16 x70) (+ (* (- 37) x71) (+ (* 11 x72) (+ (* 20 x73) (+ (* 8 x74) (+ (* 4 x75) (+ (* (- 37) x76) (+ (* (- 29) x77) (+ (* (- 1) x78) (+ (* 35 x79) (+ (* 21 x80) (+ (* 4 x81) (+ (* (- 13) x82) (+ (* (- 43) x83) (+ (* 9 x84) (+ (* 26 x85) (+ (* (- 44) x86) (+ (* (- 1) x87) (+ (* (- 16) x88) (+ (* 17 x89) (+ (* (- 36) x90) (+ (* (- 48) x91) (+ (* 30 x92) (+ (* 21 x93) (+ (* (- 27) x94) (+ (* 31 x95) (+ (* 21 x96) (+ (* (- 11) x97) (+ (* 35 x98) (* (- 7) x99) ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= (- 1221) (+ (* (- 47) x0) (+ (* 3 x1) (+ (* 22 x2) (+ (* (- 84) x3) (+ (* 4 x4) (+ (* 59 x5) (+ (* 60 x6) (+ (* (- 40) x7) (+ (* (- 52) x8) (+ (* (- 46) x9) (+ (* 61 x10) (+ (* 109 x11) (+ (* 9 x12) (+ (* (- 40) x13) (+ (* (- 25) x14) (+ (* 3 x15) (+ (* 57 x16) (+ (* 23 x17) (+ (* 1 x18) (+ (* 57 x19) (+ (* (- 69) x20) (+ (* (- 55) x21) (+ (* 46 x22) (+ (* (- 102) x23) (+ (* 34 x24) (+ (* 23 x25) (+ (* (- 10) x26) (+ (* 28 x27) (+ (* 43 x28) (+ (* 17 x29) (+ (* 29 x30) (+ (* (- 40) x31) (+ (* (- 88) x32) (+ (* (- 28) x33) (+ (* 78 x34) (+ (* (- 60) x35) (+ (* (- 55) x36) (+ (* (- 81) x37) (+ (* 24 x38) (+ (* (- 32) x39) (+ (* 83 x40) (+ (* (- 7) x41) (+ (* (- 14) x42) (+ (* 10 x43) (+ (* 109 x44) (+ (* 28 x45) (+ (* 47 x46) (+ (* 30 x47) (+ (* 73 x48) (+ (* (- 9) x49) (+ (* 64 x50) (+ (* 161 x51) (+ (* 80 x52) (+ (* 57 x53) (+ (* (- 56) x54) (+ (* 60 x55) (+ (* 16 x56) (+ (* (- 70) x57) (+ (* (- 93) x58) (+ (* 53 x59) (+ (* (- 30) x60) (+ (* 4 x61) (+ (* 13 x62) (+ (* 7 x63) (+ (* (- 89) x64) (+ (* (- 83) x65) (+ (* (- 2) x66) (+ (* (- 91) x67) (+ (* (- 64) x68) (+ (* 12 x69) (+ (* (- 24) x70) (+ (* 44 x71) (+ (* (- 33) x72) (+ (* (- 13) x73) (+ (* 21 x74) (+ (* (- 19) x75) (+ (* 74 x76) (+ (* (- 10) x77) (+ (* 2 x78) (+ (* (- 49) x79) (+ (* (- 60) x80) (+ (* 31 x81) (+ (* 13 x82) (+ (* 69 x83) (+ (* (- 86) x84) (+ (* (- 37) x85) (+ (* 62 x86) (+ (* (- 20) x87) (+ (* 24 x88) (+ (* (- 20) x89) (+ (* 77 x90) (+ (* 53 x91) (+ (* 12 x92) (+ (* 13 x93) (+ (* 23 x94) (+ (* (- 61) x95) (+ (* (- 7) x96) (+ (* 14 x97) (+ (* (- 25) x98) (* 42 x99) )))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= 1844 (+ (* 76 x0) (+ (* (- 14) x1) (+ (* (- 6) x2) (+ (* 144 x3) (+ (* (- 10) x4) (+ (* (- 80) x5) (+ (* (- 120) x6) (+ (* 35 x7) (+ (* 105 x8) (+ (* 84 x9) (+ (* (- 128) x10) (+ (* (- 205) x11) (+ (* (- 8) x12) (+ (* 72 x13) (+ (* 27 x14) (+ (* (- 24) x15) (+ (* (- 114) x16) (+ (* (- 60) x17) (+ (* (- 20) x18) (+ (* (- 81) x19) (+ (* 132 x20) (+ (* 83 x21) (+ (* (- 92) x22) (+ (* 179 x23) (+ (* (- 30) x24) (+ (* (- 49) x25) (+ (* 4 x26) (+ (* (- 46) x27) (+ (* (- 82) x28) (+ (* (- 7) x29) (+ (* (- 40) x30) (+ (* 57 x31) (+ (* 146 x32) (+ (* 65 x33) (+ (* (- 146) x34) (+ (* 130 x35) (+ (* 116 x36) (+ (* 156 x37) (+ (* (- 57) x38) (+ (* 35 x39) (+ (* (- 177) x40) (+ (* (- 19) x41) (+ (* 41 x42) (+ (* (- 10) x43) (+ (* (- 222) x44) (+ (* (- 50) x45) (+ (* (- 106) x46) (+ (* (- 47) x47) (+ (* (- 74) x48) (+ (* 40 x49) (+ (* (- 117) x50) (+ (* (- 298) x51) (+ (* (- 133) x52) (+ (* (- 117) x53) (+ (* 98 x54) (+ (* (- 148) x55) (+ (* (- 44) x56) (+ (* 122 x57) (+ (* 171 x58) (+ (* (- 113) x59) (+ (* 30 x60) (+ (* (- 27) x61) (+ (* (- 44) x62) (+ (* (- 24) x63) (+ (* 147 x64) (+ (* 134 x65) (+ (* 34 x66) (+ (* 177 x67) (+ (* 145 x68) (+ (* (- 23) x69) (+ (* 40 x70) (+ (* (- 94) x71) (+ (* 77 x72) (+ (* 31 x73) (+ (* (- 48) x74) (+ (* 20 x75) (+ (* (- 128) x76) (+ (* 7 x77) (+ (* (- 12) x78) (+ (* 68 x79) (+ (* 122 x80) (+ (* (- 23) x81) (+ (* (- 41) x82) (+ (* (- 126) x83) (+ (* 170 x84) (+ (* 58 x85) (+ (* (- 109) x86) (+ (* 25 x87) (+ (* (- 46) x88) (+ (* 17 x89) (+ (* (- 122) x90) (+ (* (- 78) x91) (+ (* (- 42) x92) (+ (* (- 20) x93) (+ (* (- 39) x94) (+ (* 115 x95) (+ (* 31 x96) (+ (* (- 39) x97) (+ (* 41 x98) (* (- 103) x99) )))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= (- 786) (+ (* 16 x0) (+ (* (- 30) x1) (+ (* (- 14) x2) (+ (* (- 41) x3) (+ (* (- 43) x4) (+ (* (- 1) x5) (+ (* 39 x6) (+ (* (- 1) x7) (+ (* (- 45) x8) (+ (* (- 10) x9) (+ (* 52 x10) (+ (* 50 x11) (+ (* 8 x12) (+ (* 28 x13) (+ (* 19 x14) (+ (* (- 85) x15) (+ (* 9 x16) (+ (* 56 x17) (+ (* (- 24) x18) (+ (* 2 x19) (+ (* (- 12) x20) (+ (* (- 13) x21) (+ (* 33 x22) (+ (* (- 74) x23) (+ (* (- 66) x24) (+ (* 24 x25) (+ (* (- 9) x26) (+ (* 56 x27) (+ (* (- 22) x28) (+ (* 15 x29) (+ (* 49 x30) (+ (* (- 40) x31) (+ (* (- 67) x32) (+ (* 10 x33) (+ (* 45 x34) (+ (* (- 13) x35) (+ (* (- 53) x36) (+ (* (- 21) x37) (+ (* 32 x38) (+ (* (- 16) x39) (+ (* 23 x40) (+ (* (- 33) x41) (+ (* 32 x42) (+ (* 26 x43) (+ (* 104 x44) (+ (* (- 1) x45) (+ (* 8 x47) (+ (* 8 x48) (+ (* 17 x49) (+ (* 40 x50) (+ (* 97 x51) (+ (* 106 x52) (+ (* 18 x53) (+ (* 9 x54) (+ (* 20 x55) (+ (* 45 x56) (+ (* (- 46) x57) (+ (* (- 64) x58) (+ (* 26 x59) (+ (* 21 x60) (+ (* 20 x61) (+ (* (- 55) x62) (+ (* 4 x63) (+ (* (- 65) x64) (+ (* (- 29) x65) (+ (* (- 12) x66) (+ (* (- 67) x67) (+ (* (- 36) x68) (+ (* 34 x69) (+ (* (- 30) x70) (+ (* 9 x72) (+ (* (- 36) x73) (+ (* (- 8) x74) (+ (* 20 x75) (+ (* 18 x76) (+ (* 79 x77) (+ (* 5 x78) (+ (* (- 42) x79) (+ (* (- 24) x80) (+ (* (- 29) x81) (+ (* 6 x82) (+ (* 30 x83) (+ (* 46 x84) (+ (* (- 47) x85) (+ (* 31 x86) (+ (* (- 27) x87) (+ (* (- 5) x88) (+ (* (- 1) x89) (+ (* 12 x90) (+ (* 28 x91) (+ (* (- 45) x92) (+ (* (- 53) x93) (+ (* 4 x94) (+ (* (- 20) x95) (+ (* (- 55) x96) (+ (* (- 5) x97) (+ (* (- 49) x98) (* (- 46) x99) )))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= (- 692) (+ (* (- 59) x0) (+ (* 14 x1) (+ (* (- 34) x2) (+ (* (- 39) x3) (+ (* 22 x4) (+ (* 21 x5) (+ (* 99 x6) (+ (* 33 x7) (+ (* (- 57) x8) (+ (* (- 23) x9) (+ (* 51 x10) (+ (* 157 x11) (+ (* (- 23) x12) (+ (* (- 69) x13) (+ (* (- 18) x14) (+ (* 57 x15) (+ (* 81 x16) (+ (* 81 x17) (+ (* 32 x18) (+ (* 11 x19) (+ (* (- 36) x20) (+ (* (- 44) x21) (+ (* 68 x22) (+ (* (- 82) x23) (+ (* (- 35) x24) (+ (* 27 x25) (+ (* 10 x26) (+ (* (- 11) x27) (+ (* 43 x28) (+ (* (- 8) x29) (+ (* 1 x30) (+ (* 26 x31) (+ (* (- 52) x32) (+ (* (- 10) x33) (+ (* 84 x34) (+ (* (- 79) x35) (+ (* (- 91) x36) (+ (* (- 96) x37) (+ (* 42 x38) (+ (* 133 x40) (+ (* 36 x41) (+ (* (- 48) x42) (+ (* 11 x43) (+ (* 139 x44) (+ (* 50 x45) (+ (* 67 x46) (+ (* 26 x47) (+ (* (- 16) x48) (+ (* (- 63) x49) (+ (* 106 x50) (+ (* 159 x51) (+ (* 16 x52) (+ (* 109 x53) (+ (* (- 2) x54) (+ (* 129 x55) (+ (* 7 x56) (+ (* (- 72) x57) (+ (* (- 92) x58) (+ (* 82 x59) (+ (* (- 6) x60) (+ (* 50 x61) (+ (* 20 x62) (+ (* 2 x63) (+ (* (- 80) x64) (+ (* (- 15) x65) (+ (* (- 46) x66) (+ (* (- 95) x67) (+ (* (- 82) x68) (+ (* 43 x69) (+ (* 9 x70) (+ (* 85 x71) (+ (* (- 61) x72) (+ (* (- 60) x73) (+ (* 36 x74) (+ (* 23 x75) (+ (* 65 x76) (+ (* (- 25) x77) (+ (* 57 x78) (+ (* 8 x79) (+ (* (- 108) x80) (+ (* (- 41) x81) (+ (* 45 x82) (+ (* 55 x83) (+ (* (- 122) x84) (+ (* (- 52) x85) (+ (* 50 x86) (+ (* 11 x87) (+ (* 7 x88) (+ (* 37 x89) (+ (* (- 9) x90) (+ (* 38 x91) (+ (* 59 x92) (+ (* 58 x93) (+ (* (- 28) x94) (+ (* (- 72) x95) (+ (* (- 17) x96) (+ (* 49 x97) (+ (* (- 3) x98) (* 93 x99) ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= 599 (+ (* 53 x0) (+ (* 87 x1) (+ (* 174 x2) (+ (* (- 69) x3) (+ (* 44 x4) (+ (* 115 x5) (+ (* (- 167) x6) (+ (* (- 144) x7) (+ (* 87 x8) (+ (* (- 16) x9) (+ (* (- 27) x10) (+ (* (- 195) x11) (+ (* 56 x12) (+ (* 32 x13) (+ (* (- 64) x14) (+ (* 19 x15) (+ (* (- 48) x16) (+ (* (- 230) x17) (+ (* (- 19) x18) (+ (* 182 x19) (+ (* (- 63) x20) (+ (* 17 x21) (+ (* (- 89) x22) (+ (* 72 x23) (+ (* 305 x24) (+ (* (- 39) x25) (+ (* (- 50) x26) (+ (* 15 x27) (+ (* 31 x28) (+ (* 47 x29) (+ (* (- 52) x30) (+ (* (- 134) x31) (+ (* 11 x32) (+ (* (- 104) x33) (+ (* (- 45) x34) (+ (* 65 x35) (+ (* 162 x36) (+ (* 33 x37) (+ (* (- 52) x38) (+ (* (- 60) x39) (+ (* (- 178) x40) (+ (* (- 65) x41) (+ (* 28 x42) (+ (* (- 37) x43) (+ (* (- 244) x44) (+ (* (- 43) x45) (+ (* (- 44) x46) (+ (* (- 3) x47) (+ (* 249 x48) (+ (* 123 x49) (+ (* (- 171) x50) (+ (* (- 108) x51) (+ (* (- 19) x52) (+ (* (- 131) x53) (+ (* (- 160) x54) (+ (* (- 188) x55) (+ (* (- 80) x56) (+ (* 85 x57) (+ (* 59 x58) (+ (* (- 95) x59) (+ (* (- 108) x60) (+ (* (- 154) x61) (+ (* 110 x62) (+ (* 15 x63) (+ (* 79 x64) (+ (* (- 154) x65) (+ (* 139 x66) (+ (* 99 x67) (+ (* 81 x68) (+ (* (- 201) x69) (+ (* (- 37) x70) (+ (* (- 45) x71) (+ (* 50 x72) (+ (* 218 x73) (+ (* (- 29) x74) (+ (* (- 223) x75) (+ (* 48 x76) (+ (* (- 104) x77) (+ (* (- 190) x78) (+ (* (- 111) x79) (+ (* 162 x80) (+ (* 228 x81) (+ (* (- 73) x82) (+ (* 31 x83) (+ (* 143 x85) (+ (* (- 17) x86) (+ (* 22 x87) (+ (* 75 x88) (+ (* (- 164) x89) (+ (* 250 x90) (+ (* 39 x91) (+ (* (- 67) x92) (+ (* (- 39) x93) (+ (* 168 x94) (+ (* 43 x95) (+ (* 117 x96) (+ (* (- 35) x97) (+ (* 20 x98) (* (- 23) x99) ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= (- 2338) (+ (* (- 208) x0) (+ (* 71 x1) (+ (* 128 x2) (+ (* (- 247) x3) (+ (* 65 x4) (+ (* 217 x5) (+ (* 82 x6) (+ (* (- 207) x7) (+ (* (- 64) x8) (+ (* (- 192) x9) (+ (* 138 x10) (+ (* 172 x11) (+ (* 54 x12) (+ (* (- 121) x13) (+ (* (- 104) x14) (+ (* 164 x15) (+ (* 123 x16) (+ (* (- 91) x17) (+ (* 47 x18) (+ (* 191 x19) (+ (* (- 276) x20) (+ (* (- 124) x21) (+ (* 69 x22) (+ (* (- 224) x23) (+ (* 315 x24) (+ (* 30 x25) (+ (* (- 28) x26) (+ (* 67 x27) (+ (* 231 x28) (+ (* (- 30) x29) (+ (* 30 x30) (+ (* (- 156) x31) (+ (* (- 176) x32) (+ (* (- 189) x33) (+ (* 119 x34) (+ (* (- 179) x35) (+ (* (- 30) x36) (+ (* (- 181) x37) (+ (* 2 x38) (+ (* (- 93) x39) (+ (* 235 x40) (+ (* 37 x41) (+ (* (- 79) x42) (+ (* (- 41) x43) (+ (* 111 x44) (+ (* 89 x45) (+ (* 162 x46) (+ (* 59 x47) (+ (* 211 x48) (+ (* (- 27) x49) (+ (* 66 x50) (+ (* 306 x51) (+ (* 86 x52) (+ (* 97 x53) (+ (* (- 350) x54) (+ (* 122 x55) (+ (* 12 x56) (+ (* (- 142) x57) (+ (* (- 166) x58) (+ (* 95 x59) (+ (* (- 111) x60) (+ (* (- 115) x61) (+ (* 153 x62) (+ (* 89 x63) (+ (* (- 110) x64) (+ (* (- 289) x65) (+ (* 20 x66) (+ (* (- 147) x67) (+ (* (- 166) x68) (+ (* (- 42) x69) (+ (* (- 70) x70) (+ (* 110 x71) (+ (* (- 133) x72) (+ (* 124 x73) (+ (* 95 x74) (+ (* (- 152) x75) (+ (* 195 x76) (+ (* (- 155) x77) (+ (* (- 71) x78) (+ (* (- 110) x79) (+ (* (- 97) x80) (+ (* 197 x81) (+ (* 35 x82) (+ (* 161 x83) (+ (* (- 392) x84) (+ (* 37 x85) (+ (* 113 x86) (+ (* (- 48) x87) (+ (* 109 x88) (+ (* (- 124) x89) (+ (* 342 x90) (+ (* 68 x91) (+ (* 128 x92) (+ (* 122 x93) (+ (* 132 x94) (+ (* (- 150) x95) (+ (* 70 x96) (+ (* 43 x97) (+ (* 9 x98) (* 194 x99) )))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= (- 942) (+ (* (- 36) x0) (+ (* 75 x1) (+ (* (- 81) x2) (+ (* (- 27) x3) (+ (* 114 x4) (+ (* 21 x5) (+ (* 185 x6) (+ (* 134 x7) (+ (* (- 95) x8) (+ (* (- 24) x9) (+ (* 37 x10) (+ (* 280 x11) (+ (* (- 42) x12) (+ (* (- 163) x13) (+ (* (- 37) x14) (+ (* 133 x15) (+ (* 189 x16) (+ (* 85 x17) (+ (* 69 x18) (+ (* 36 x19) (+ (* (- 30) x20) (+ (* (- 99) x21) (+ (* 112 x22) (+ (* (- 75) x23) (+ (* (- 50) x24) (+ (* 67 x25) (+ (* 11 x26) (+ (* (- 104) x27) (+ (* 48 x28) (+ (* 17 x29) (+ (* (- 45) x30) (+ (* 113 x31) (+ (* (- 58) x32) (+ (* 11 x33) (+ (* 202 x34) (+ (* (- 136) x35) (+ (* (- 121) x36) (+ (* (- 177) x37) (+ (* 57 x38) (+ (* 43 x39) (+ (* 204 x40) (+ (* 68 x41) (+ (* (- 116) x42) (+ (* (- 4) x43) (+ (* 256 x44) (+ (* 58 x45) (+ (* 127 x46) (+ (* 52 x47) (+ (* (- 14) x48) (+ (* (- 127) x49) (+ (* 190 x50) (+ (* 292 x51) (+ (* 28 x52) (+ (* 224 x53) (+ (* 61 x54) (+ (* 239 x55) (+ (* (- 9) x56) (+ (* (- 60) x57) (+ (* (- 141) x58) (+ (* 151 x59) (+ (* (- 48) x60) (+ (* 160 x61) (+ (* 102 x62) (+ (* (- 22) x63) (+ (* (- 145) x64) (+ (* 18 x65) (+ (* (- 74) x66) (+ (* (- 163) x67) (+ (* (- 141) x68) (+ (* 13 x69) (+ (* 55 x70) (+ (* 172 x71) (+ (* (- 112) x72) (+ (* (- 135) x73) (+ (* 64 x74) (+ (* 36 x75) (+ (* 147 x76) (+ (* (- 38) x77) (+ (* 92 x78) (+ (* (- 7) x79) (+ (* (- 190) x80) (+ (* (- 78) x81) (+ (* 96 x82) (+ (* 141 x83) (+ (* (- 221) x84) (+ (* (- 66) x85) (+ (* 123 x86) (+ (* 73 x87) (+ (* 41 x88) (+ (* 75 x89) (+ (* (- 44) x90) (+ (* 88 x91) (+ (* 116 x92) (+ (* 101 x93) (+ (* (- 49) x94) (+ (* (- 138) x95) (+ (* (- 1) x96) (+ (* 96 x97) (+ (* (- 14) x98) (* 192 x99) )))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= 1526 (+ (* (- 152) x0) (+ (* (- 45) x1) (+ (* (- 47) x2) (+ (* 82 x3) (+ (* (- 23) x4) (+ (* (- 95) x5) (+ (* (- 55) x6) (+ (* (- 77) x7) (+ (* 88 x8) (+ (* (- 42) x9) (+ (* (- 92) x10) (+ (* (- 69) x11) (+ (* (- 3) x12) (+ (* 29 x13) (+ (* 10 x14) (+ (* 102 x15) (+ (* (- 101) x16) (+ (* (- 24) x17) (+ (* (- 6) x18) (+ (* (- 154) x19) (+ (* (- 25) x20) (+ (* 56 x21) (+ (* (- 50) x22) (+ (* 87 x23) (+ (* 30 x24) (+ (* (- 65) x25) (+ (* 53 x26) (+ (* (- 16) x27) (+ (* 47 x28) (+ (* (- 98) x29) (+ (* 10 x30) (+ (* 64 x31) (+ (* 112 x32) (+ (* (- 6) x33) (+ (* (- 187) x34) (+ (* 19 x35) (+ (* 63 x36) (+ (* 113 x37) (+ (* (- 103) x38) (+ (* 33 x39) (+ (* 65 x40) (+ (* 103 x41) (+ (* (- 26) x42) (+ (* (- 43) x43) (+ (* (- 194) x44) (+ (* 34 x45) (+ (* (- 3) x46) (+ (* (- 67) x47) (+ (* (- 176) x48) (+ (* (- 44) x49) (+ (* (- 114) x50) (+ (* (- 288) x51) (+ (* (- 174) x52) (+ (* (- 76) x53) (+ (* (- 64) x54) (+ (* (- 28) x55) (+ (* 6 x56) (+ (* 16 x57) (+ (* 150 x58) (+ (* (- 54) x59) (+ (* 76 x60) (+ (* (- 78) x61) (+ (* (- 30) x62) (+ (* 58 x63) (+ (* 162 x64) (+ (* 82 x65) (+ (* (- 14) x66) (+ (* 142 x67) (+ (* 30 x68) (+ (* 93 x69) (+ (* 24 x70) (+ (* (- 110) x71) (+ (* 5 x72) (+ (* 34 x73) (+ (* 26 x74) (+ (* 85 x75) (+ (* (- 154) x76) (+ (* (- 71) x77) (+ (* 68 x78) (+ (* 172 x79) (+ (* (- 11) x80) (+ (* (- 18) x81) (+ (* (- 15) x82) (+ (* (- 150) x83) (+ (* (- 93) x84) (+ (* 37 x85) (+ (* (- 109) x86) (+ (* (- 67) x87) (+ (* (- 33) x88) (+ (* 34 x89) (+ (* (- 106) x90) (+ (* (- 166) x91) (+ (* 151 x92) (+ (* 129 x93) (+ (* (- 66) x94) (+ (* 51 x95) (+ (* 51 x96) (+ (* 3 x97) (+ (* 127 x98) (* 25 x99) )))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= (- 2242) (+ (* (- 87) x0) (+ (* (- 232) x1) (+ (* (- 40) x2) (+ (* (- 142) x3) (+ (* (- 236) x4) (+ (* (- 80) x5) (+ (* 41 x6) (+ (* (- 146) x7) (+ (* (- 120) x8) (+ (* (- 126) x9) (+ (* 189 x10) (+ (* 53 x11) (+ (* 35 x12) (+ (* 133 x13) (+ (* 117 x14) (+ (* (- 270) x15) (+ (* (- 62) x16) (+ (* 171 x17) (+ (* (- 86) x18) (+ (* (- 122) x19) (+ (* (- 167) x20) (+ (* 23 x21) (+ (* 1 x22) (+ (* (- 221) x23) (+ (* (- 173) x24) (+ (* (- 20) x25) (+ (* 39 x26) (+ (* 279 x27) (+ (* 51 x28) (+ (* (- 126) x29) (+ (* 212 x30) (+ (* (- 169) x31) (+ (* (- 138) x32) (+ (* (- 63) x33) (+ (* (- 61) x34) (+ (* (- 58) x35) (+ (* (- 137) x36) (+ (* 42 x37) (+ (* 34 x38) (+ (* (- 39) x39) (+ (* 167 x40) (+ (* (- 17) x41) (+ (* 121 x42) (+ (* 65 x43) (+ (* 202 x44) (+ (* 13 x45) (+ (* (- 32) x46) (+ (* (- 13) x47) (+ (* (- 171) x48) (+ (* 67 x49) (+ (* 9 x50) (+ (* 113 x51) (+ (* 212 x52) (+ (* (- 153) x53) (+ (* (- 135) x54) (+ (* 52 x55) (+ (* 215 x56) (+ (* (- 182) x57) (+ (* (- 94) x58) (+ (* 46 x59) (+ (* 184 x60) (+ (* (- 79) x61) (+ (* (- 204) x62) (+ (* 36 x63) (+ (* (- 7) x64) (+ (* (- 54) x65) (+ (* (- 87) x66) (+ (* (- 91) x67) (+ (* (- 71) x68) (+ (* 211 x69) (+ (* (- 138) x70) (+ (* (- 85) x71) (+ (* 9 x72) (+ (* (- 80) x73) (+ (* (- 21) x74) (+ (* 185 x75) (+ (* (- 119) x76) (+ (* 186 x77) (+ (* 68 x78) (+ (* 15 x79) (+ (* (- 37) x80) (+ (* (- 39) x81) (+ (* (- 6) x82) (+ (* (- 73) x83) (+ (* 120 x84) (+ (* (- 127) x85) (+ (* (- 23) x86) (+ (* (- 183) x87) (+ (* (- 34) x88) (+ (* (- 11) x89) (+ (* 30 x90) (+ (* (- 71) x91) (+ (* (- 94) x92) (+ (* (- 143) x93) (+ (* (- 1) x94) (+ (* 18 x95) (+ (* (- 185) x96) (+ (* (- 77) x97) (+ (* (- 96) x98) (* (- 118) x99) )))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 
(<= 643 (+ (* (- 20) x0) (+ (* 110 x1) (+ (* (- 41) x2) (+ (* 108 x3) (+ (* 164 x4) (+ (* 21 x5) (+ (* 103 x6) (+ (* 193 x7) (+ (* (- 2) x8) (+ (* 82 x9) (+ (* (- 82) x10) (+ (* 138 x11) (+ (* (- 36) x12) (+ (* (- 158) x13) (+ (* (- 63) x14) (+ (* 313 x15) (+ (* 126 x16) (+ (* 45 x17) (+ (* 95 x18) (+ (* (- 15) x19) (+ (* 117 x20) (+ (* (- 59) x21) (+ (* 119 x22) (+ (* 67 x23) (+ (* (- 17) x24) (+ (* 33 x25) (+ (* 48 x26) (+ (* (- 237) x27) (+ (* 4 x28) (+ (* 53 x29) (+ (* (- 127) x30) (+ (* 232 x31) (+ (* 78 x32) (+ (* 91 x33) (+ (* 94 x34) (+ (* (- 70) x35) (+ (* (- 67) x36) (+ (* (- 127) x37) (+ (* 44 x38) (+ (* 53 x39) (+ (* 73 x40) (+ (* 119 x41) (+ (* (- 164) x42) (+ (* (- 25) x43) (+ (* 28 x44) (+ (* 29 x45) (+ (* 138 x46) (+ (* 58 x47) (+ (* 22 x48) (+ (* (- 203) x49) (+ (* 152 x50) (+ (* 95 x51) (+ (* (- 160) x52) (+ (* 250 x53) (+ (* 185 x54) (+ (* 158 x55) (+ (* (- 138) x56) (+ (* 25 x57) (+ (* 12 x58) (+ (* 77 x59) (+ (* (- 131) x60) (+ (* 130 x61) (+ (* 149 x62) (+ (* (- 4) x63) (+ (* (- 131) x64) (+ (* 96 x65) (+ (* (- 39) x66) (+ (* (- 56) x67) (+ (* (- 69) x68) (+ (* (- 18) x69) (+ (* 120 x70) (+ (* 137 x71) (+ (* (- 94) x72) (+ (* (- 89) x73) (+ (* 79 x74) (+ (* (- 23) x75) (+ (* 128 x76) (+ (* (- 184) x77) (+ (* 84 x78) (+ (* 101 x79) (+ (* (- 175) x80) (+ (* (- 89) x81) (+ (* 30 x82) (+ (* 83 x83) (+ (* (- 229) x84) (+ (* (- 14) x85) (+ (* 87 x86) (+ (* 83 x87) (+ (* (- 19) x88) (+ (* 150 x89) (+ (* (- 117) x90) (+ (* 25 x91) (+ (* 218 x92) (+ (* 169 x93) (+ (* (- 118) x94) (+ (* (- 66) x95) (+ (* 113 x96) (+ (* 69 x97) (+ (* 89 x98) (* 222 x99) ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
(check-sat)
(exit)