50
(x36 v x50 v x45) ^ (x48 v -x5 v x47) ^ (-x42 v x39 v -x36) ^ (x25 v -x17 v x20) ^ (-x38 v x28 v x1) ^ (-x43 v x27 v x13) ^ (x41 v -x7 v -x50) ^ (x18 v -x25 v -x8) ^ (-x5 v x38 v -x46) ^ (-x45 v x9 v -x33) ^ (x26 v x27 v x7) ^ (x13 v -x37 v -x10) ^ (-x11 v x44 v -x30) ^ (-x13 v x38 v x33) ^ (x44 v x50 v -x49) ^ (x17 v -x25 v -x29) ^ (x43 v -x10 v x6) ^ (-x39 v x49 v x7) ^ (x4 v x39 v x31) ^ (x18 v -x12 v -x24) ^ (-x50 v -x40 v x44) ^ (-x27 v -x20 v x48) ^ (x21 v x44 v -x47) ^ (x46 v x5 v -x3) ^ (-x34 v x18 v -x2) ^ (x24 v x43 v -x29) ^ (-x48 v -x28 v x17) ^ (x13 v -x22 v x36) ^ (-x2 v -x9 v -x24) ^ (-x12 v x4 v x29) ^ (x43 v -x35 v -x25) ^ (x49 v -x31 v x15) ^ (-x24 v -x23 v x36) ^ (-x5 v -x41 v -x27) ^ (-x39 v -x48 v -x5) ^ (x22 v -x33 v -x2) ^ (-x34 v x30 v -x42) ^ (-x6 v -x39 v x30) ^ (x29 v -x34 v -x45) ^ (x27 v -x23 v -x13) ^ (-x21 v -x41 v x20) ^ (x16 v x25 v x20) ^ (x2 v -x9 v x42) ^ (-x24 v x18 v x44) ^ (x37 v -x42 v x40) ^ (-x7 v -x6 v -x27) ^ (-x36 v -x46 v x32) ^ (-x31 v x29 v x47) ^ (-x30 v -x33 v x2) ^ (x23 v x11 v x13) ^ (-x49 v -x35 v x7) ^ (x1 v x46 v -x39) ^ (-x22 v -x26 v -x21) ^ (-x15 v x30 v x27) ^ (x1 v -x45 v x39) ^ (-x15 v -x24 v x25) ^ (x11 v -x36 v -x43) ^ (-x14 v x46 v -x35) ^ (-x11 v -x13 v -x21) ^ (-x5 v -x48 v -x38) ^ (x44 v x35 v -x48) ^ (x11 v x21 v -x48) ^ (x27 v x34 v -x4) ^ (-x29 v x50 v -x38) ^ (x12 v x42 v -x33) ^ (-x11 v -x38 v -x34) ^ (-x13 v -x47 v -x33) ^ (x34 v -x18 v x14) ^ (-x30 v x38 v x17) ^ (-x9 v -x18 v x35)