(benchmark DTP_k2_n35_c210_s20.smt :source { Randomly generated benchmarks. Contact TSAT++ group at http://www.ai.dist.unige.it/Tsat for more information. Translated into SMT-LIB format by Albert Oliveras. } :status unknown :logic QF_IDL :extrafuns ((x2 Int)) :extrafuns ((x13 Int)) :extrafuns ((x0 Int)) :extrafuns ((x10 Int)) :extrafuns ((x1 Int)) :extrafuns ((x11 Int)) :extrafuns ((x12 Int)) :extrafuns ((x18 Int)) :extrafuns ((x15 Int)) :extrafuns ((x14 Int)) :extrafuns ((x16 Int)) :extrafuns ((x17 Int)) :extrafuns ((x19 Int)) :extrafuns ((x32 Int)) :extrafuns ((x20 Int)) :extrafuns ((x24 Int)) :extrafuns ((x21 Int)) :extrafuns ((x23 Int)) :extrafuns ((x22 Int)) :extrafuns ((x28 Int)) :extrafuns ((x25 Int)) :extrafuns ((x27 Int)) :extrafuns ((x26 Int)) :extrafuns ((x30 Int)) :extrafuns ((x29 Int)) :extrafuns ((x3 Int)) :extrafuns ((x31 Int)) :extrafuns ((x8 Int)) :extrafuns ((x33 Int)) :extrafuns ((x5 Int)) :extrafuns ((x4 Int)) :extrafuns ((x34 Int)) :extrafuns ((x7 Int)) :extrafuns ((x6 Int)) :extrafuns ((x9 Int)) :formula ( and (or (not ( >= ( - x2 x13 ) 48 )) (not ( >= ( - x32 x0 ) 5 )) ) (or (not ( >= ( - x20 x24 ) 17 )) ( >= ( - x28 x25 ) 31 ) ) (or (not ( >= ( - x13 x10 ) 46 )) ( >= ( - x8 x25 ) 13 ) ) (or (not ( >= ( - x18 x11 ) 14 )) (not ( >= ( - x24 x25 ) 86 )) ) (or (not ( >= ( - x0 x33 ) 11 )) (not ( >= ( - x27 x24 ) 45 )) ) (or (not ( >= ( - x5 x8 ) 19 )) ( >= ( - x10 x28 ) 54 ) ) (or ( >= ( - x4 x26 ) 25 ) ( >= ( - x9 x15 ) 99 ) ) (or (not ( >= ( - x30 x20 ) 37 )) ( >= ( - x28 x7 ) 54 ) ) (or (not ( >= ( - x13 x10 ) 21 )) ( >= ( - x18 x21 ) 91 ) ) (or (not ( >= ( - x29 x8 ) 83 )) (not ( >= ( - x34 x18 ) 59 )) ) (or ( >= ( - x8 x4 ) 18 ) (not ( >= ( - x2 x3 ) 79 )) ) (or ( >= ( - x7 x9 ) 89 ) ( >= ( - x32 x15 ) 61 ) ) (or ( >= ( - x16 x33 ) 76 ) ( >= ( - x13 x23 ) 38 ) ) (or ( >= ( - x19 x28 ) 77 ) ( >= ( - x21 x16 ) 40 ) ) (or (not ( >= ( - x10 x30 ) 47 )) (not ( >= ( - x33 x2 ) 68 )) ) (or (not ( >= ( - x6 x23 ) 35 )) ( >= ( - x21 x14 ) 94 ) ) (or ( >= ( - x14 x21 ) 70 ) ( >= ( - x33 x0 ) 71 ) ) (or ( >= ( - x16 x1 ) 5 ) (not ( >= ( - x23 x26 ) 56 )) ) (or ( >= ( - x24 x34 ) 70 ) (not ( >= ( - x31 x1 ) 41 )) ) (or (not ( >= ( - x24 x31 ) 19 )) (not ( >= ( - x15 x0 ) 1 )) ) (or ( >= ( - x10 x33 ) 89 ) (not ( >= ( - x25 x5 ) 23 )) ) (or (not ( >= ( - x6 x5 ) 71 )) (not ( >= ( - x3 x8 ) 27 )) ) (or ( >= ( - x3 x0 ) 22 ) (not ( >= ( - x10 x28 ) 96 )) ) (or ( >= ( - x10 x17 ) 32 ) (not ( >= ( - x2 x9 ) 94 )) ) (or ( >= ( - x24 x30 ) 13 ) ( >= ( - x25 x10 ) 4 ) ) (or ( >= ( - x13 x7 ) 16 ) ( >= ( - x32 x8 ) 28 ) ) (or (not ( >= ( - x29 x13 ) 58 )) (not ( >= ( - x24 x8 ) 60 )) ) (or (not ( >= ( - x20 x4 ) 4 )) (not ( >= ( - x30 x10 ) 62 )) ) (or (not ( >= ( - x27 x24 ) 78 )) (not ( >= ( - x27 x29 ) 64 )) ) (or (not ( >= ( - x34 x23 ) 56 )) ( >= ( - x2 x33 ) 12 ) ) (or ( >= ( - x30 x2 ) 39 ) (not ( >= ( - x24 x32 ) 53 )) ) (or ( >= ( - x34 x22 ) 71 ) ( >= ( - x4 x27 ) 80 ) ) (or ( >= ( - x29 x6 ) 49 ) (not ( >= ( - x7 x11 ) 43 )) ) (or ( >= ( - x30 x17 ) 83 ) (not ( >= ( - x31 x2 ) 92 )) ) (or (not ( >= ( - x0 x30 ) 78 )) ( >= ( - x8 x10 ) 31 ) ) (or ( >= ( - x11 x2 ) 3 ) (not ( >= ( - x29 x3 ) 8 )) ) (or ( >= ( - x4 x6 ) 72 ) ( >= ( - x29 x25 ) 90 ) ) (or ( >= ( - x9 x26 ) 36 ) ( >= ( - x28 x5 ) 3 ) ) (or ( >= ( - x19 x15 ) 88 ) (not ( >= ( - x29 x1 ) 41 )) ) (or (not ( >= ( - x13 x18 ) 62 )) ( >= ( - x14 x34 ) 66 ) ) (or ( >= ( - x18 x10 ) 17 ) (not ( >= ( - x3 x28 ) 12 )) ) (or ( >= ( - x7 x8 ) 21 ) ( >= ( - x32 x27 ) 72 ) ) (or ( >= ( - x5 x20 ) 2 ) ( >= ( - x7 x33 ) 19 ) ) (or (not ( >= ( - x15 x4 ) 65 )) (not ( >= ( - x7 x13 ) 48 )) ) (or ( >= ( - x15 x32 ) 50 ) ( >= ( - x0 x2 ) 26 ) ) (or ( >= ( - x33 x23 ) 18 ) (not ( >= ( - x5 x1 ) 58 )) ) (or ( >= ( - x30 x13 ) 66 ) ( >= ( - x27 x12 ) 56 ) ) (or ( >= ( - x20 x29 ) 71 ) ( >= ( - x17 x31 ) 42 ) ) (or ( >= ( - x22 x21 ) 85 ) ( >= ( - x13 x14 ) 71 ) ) (or ( >= ( - x2 x16 ) 80 ) ( >= ( - x16 x22 ) 94 ) ) (or ( >= ( - x4 x10 ) 54 ) ( >= ( - x22 x23 ) 46 ) ) (or (not ( >= ( - x21 x23 ) 71 )) ( >= ( - x30 x33 ) 38 ) ) (or (not ( >= ( - x9 x23 ) 19 )) (not ( >= ( - x9 x3 ) 76 )) ) (or ( >= ( - x14 x8 ) 43 ) (not ( >= ( - x6 x4 ) 76 )) ) (or (not ( >= ( - x4 x12 ) 13 )) (not ( >= ( - x5 x27 ) 40 )) ) (or (not ( >= ( - x12 x25 ) 97 )) ( >= ( - x22 x1 ) 14 ) ) (or (not ( >= ( - x34 x30 ) 81 )) ( >= ( - x29 x4 ) 1 ) ) (or ( >= ( - x8 x21 ) 85 ) (not ( >= ( - x12 x33 ) 70 )) ) (or ( >= ( - x6 x24 ) 21 ) ( >= ( - x3 x25 ) 91 ) ) (or ( >= ( - x20 x0 ) 4 ) (not ( >= ( - x6 x23 ) 51 )) ) (or (not ( >= ( - x20 x30 ) 41 )) (not ( >= ( - x33 x4 ) 56 )) ) (or ( >= ( - x16 x18 ) 15 ) ( >= ( - x12 x8 ) 73 ) ) (or (not ( >= ( - x13 x23 ) 56 )) ( >= ( - x27 x2 ) 82 ) ) (or (not ( >= ( - x29 x25 ) 46 )) ( >= ( - x25 x30 ) 87 ) ) (or ( >= ( - x0 x31 ) 87 ) (not ( >= ( - x13 x33 ) 41 )) ) (or (not ( >= ( - x13 x34 ) 36 )) (not ( >= ( - x29 x23 ) 87 )) ) (or (not ( >= ( - x21 x10 ) 38 )) ( >= ( - x33 x3 ) 80 ) ) (or ( >= ( - x21 x15 ) 23 ) ( >= ( - x10 x6 ) 48 ) ) (or ( >= ( - x28 x2 ) 19 ) (not ( >= ( - x5 x7 ) 94 )) ) (or ( >= ( - x7 x6 ) 67 ) (not ( >= ( - x27 x1 ) 37 )) ) (or (not ( >= ( - x7 x12 ) 25 )) ( >= ( - x25 x21 ) 22 ) ) (or ( >= ( - x29 x26 ) 64 ) (not ( >= ( - x28 x2 ) 36 )) ) (or (not ( >= ( - x19 x18 ) 97 )) ( >= ( - x26 x22 ) 70 ) ) (or (not ( >= ( - x20 x29 ) 13 )) (not ( >= ( - x34 x30 ) 17 )) ) (or (not ( >= ( - x1 x23 ) 89 )) (not ( >= ( - x19 x21 ) 61 )) ) (or ( >= ( - x27 x7 ) 19 ) (not ( >= ( - x21 x28 ) 2 )) ) (or (not ( >= ( - x0 x21 ) 33 )) (not ( >= ( - x7 x12 ) 98 )) ) (or (not ( >= ( - x27 x5 ) 7 )) (not ( >= ( - x23 x19 ) 52 )) ) (or ( >= ( - x27 x8 ) 42 ) (not ( >= ( - x9 x23 ) 44 )) ) (or ( >= ( - x12 x32 ) 55 ) ( >= ( - x31 x17 ) 6 ) ) (or (not ( >= ( - x21 x13 ) 93 )) ( >= ( - x22 x2 ) 46 ) ) (or ( >= ( - x20 x11 ) 52 ) (not ( >= ( - x25 x3 ) 36 )) ) (or ( >= ( - x2 x18 ) 42 ) (not ( >= ( - x26 x6 ) 46 )) ) (or ( >= ( - x23 x26 ) 5 ) (not ( >= ( - x32 x3 ) 74 )) ) (or (not ( >= ( - x32 x22 ) 5 )) ( >= ( - x4 x3 ) 86 ) ) (or (not ( >= ( - x13 x9 ) 65 )) ( >= ( - x2 x3 ) 28 ) ) (or ( >= ( - x29 x18 ) 55 ) (not ( >= ( - x5 x14 ) 46 )) ) (or (not ( >= ( - x7 x3 ) 92 )) ( >= ( - x21 x16 ) 97 ) ) (or ( >= ( - x21 x29 ) 47 ) ( >= ( - x21 x30 ) 54 ) ) (or (not ( >= ( - x32 x18 ) 27 )) (not ( >= ( - x33 x34 ) 4 )) ) (or (not ( >= ( - x26 x8 ) 58 )) (not ( >= ( - x17 x27 ) 46 )) ) (or ( >= ( - x6 x17 ) 60 ) ( >= ( - x27 x0 ) 73 ) ) (or (not ( >= ( - x8 x4 ) 31 )) ( >= ( - x15 x8 ) 38 ) ) (or (not ( >= ( - x19 x12 ) 18 )) ( >= ( - x5 x34 ) 10 ) ) (or (not ( >= ( - x6 x31 ) 93 )) (not ( >= ( - x32 x30 ) 41 )) ) (or (not ( >= ( - x18 x28 ) 97 )) (not ( >= ( - x32 x3 ) 15 )) ) (or (not ( >= ( - x14 x2 ) 42 )) (not ( >= ( - x2 x13 ) 51 )) ) (or (not ( >= ( - x0 x31 ) 47 )) ( >= ( - x33 x19 ) 92 ) ) (or ( >= ( - x23 x14 ) 89 ) ( >= ( - x8 x21 ) 42 ) ) (or ( >= ( - x14 x16 ) 81 ) ( >= ( - x13 x8 ) 18 ) ) (or (not ( >= ( - x31 x5 ) 21 )) (not ( >= ( - x7 x5 ) 50 )) ) (or (not ( >= ( - x15 x5 ) 35 )) ( >= ( - x28 x31 ) 21 ) ) (or ( >= ( - x28 x0 ) 22 ) ( >= ( - x6 x27 ) 12 ) ) (or ( >= ( - x27 x14 ) 71 ) ( >= ( - x8 x28 ) 8 ) ) (or (not ( >= ( - x28 x9 ) 57 )) (not ( >= ( - x17 x27 ) 89 )) ) (or ( >= ( - x20 x19 ) 9 ) (not ( >= ( - x20 x13 ) 76 )) ) (or ( >= ( - x31 x9 ) 9 ) (not ( >= ( - x26 x34 ) 35 )) ) (or (not ( >= ( - x3 x20 ) 95 )) (not ( >= ( - x29 x7 ) 3 )) ) (or ( >= ( - x33 x34 ) 42 ) (not ( >= ( - x1 x32 ) 19 )) ) (or ( >= ( - x4 x26 ) 87 ) ( >= ( - x31 x33 ) 10 ) ) (or (not ( >= ( - x30 x20 ) 10 )) ( >= ( - x16 x2 ) 64 ) ) (or ( >= ( - x11 x6 ) 54 ) (not ( >= ( - x12 x32 ) 97 )) ) (or ( >= ( - x23 x32 ) 56 ) (not ( >= ( - x29 x25 ) 8 )) ) (or (not ( >= ( - x16 x12 ) 88 )) (not ( >= ( - x13 x25 ) 90 )) ) (or (not ( >= ( - x31 x23 ) 19 )) (not ( >= ( - x30 x8 ) 92 )) ) (or (not ( >= ( - x1 x33 ) 44 )) (not ( >= ( - x7 x28 ) 13 )) ) (or ( >= ( - x33 x22 ) 71 ) ( >= ( - x2 x32 ) 45 ) ) (or (not ( >= ( - x6 x14 ) 28 )) ( >= ( - x24 x4 ) 21 ) ) (or (not ( >= ( - x9 x3 ) 29 )) ( >= ( - x12 x23 ) 37 ) ) (or ( >= ( - x33 x5 ) 64 ) ( >= ( - x5 x11 ) 93 ) ) (or ( >= ( - x14 x15 ) 41 ) ( >= ( - x22 x21 ) 84 ) ) (or (not ( >= ( - x30 x3 ) 95 )) (not ( >= ( - x16 x14 ) 45 )) ) (or ( >= ( - x20 x18 ) 98 ) ( >= ( - x1 x16 ) 88 ) ) (or ( >= ( - x1 x19 ) 46 ) ( >= ( - x24 x0 ) 32 ) ) (or ( >= ( - x12 x15 ) 56 ) ( >= ( - x5 x10 ) 67 ) ) (or (not ( >= ( - x11 x20 ) 92 )) ( >= ( - x28 x19 ) 10 ) ) (or (not ( >= ( - x17 x15 ) 58 )) ( >= ( - x22 x14 ) 26 ) ) (or (not ( >= ( - x22 x9 ) 29 )) ( >= ( - x23 x28 ) 30 ) ) (or ( >= ( - x30 x9 ) 37 ) ( >= ( - x32 x33 ) 39 ) ) (or ( >= ( - x20 x32 ) 29 ) ( >= ( - x11 x33 ) 46 ) ) (or (not ( >= ( - x24 x33 ) 13 )) (not ( >= ( - x29 x11 ) 26 )) ) (or (not ( >= ( - x18 x15 ) 36 )) ( >= ( - x12 x7 ) 51 ) ) (or (not ( >= ( - x7 x34 ) 99 )) ( >= ( - x16 x12 ) 50 ) ) (or ( >= ( - x28 x19 ) 88 ) ( >= ( - x25 x10 ) 45 ) ) (or ( >= ( - x2 x7 ) 13 ) (not ( >= ( - x24 x3 ) 80 )) ) (or (not ( >= ( - x31 x19 ) 31 )) (not ( >= ( - x29 x16 ) 23 )) ) (or (not ( >= ( - x22 x26 ) 35 )) (not ( >= ( - x22 x3 ) 99 )) ) (or (not ( >= ( - x6 x33 ) 91 )) ( >= ( - x6 x9 ) 79 ) ) (or (not ( >= ( - x2 x29 ) 54 )) ( >= ( - x12 x18 ) 98 ) ) (or ( >= ( - x31 x6 ) 15 ) ( >= ( - x3 x4 ) 10 ) ) (or (not ( >= ( - x11 x8 ) 3 )) ( >= ( - x3 x7 ) 31 ) ) (or (not ( >= ( - x3 x1 ) 69 )) ( >= ( - x33 x3 ) 47 ) ) (or (not ( >= ( - x14 x16 ) 31 )) ( >= ( - x24 x3 ) 59 ) ) (or (not ( >= ( - x23 x4 ) 21 )) ( >= ( - x28 x23 ) 16 ) ) (or (not ( >= ( - x27 x2 ) 8 )) (not ( >= ( - x31 x21 ) 88 )) ) (or (not ( >= ( - x8 x4 ) 97 )) ( >= ( - x3 x18 ) 57 ) ) (or ( >= ( - x31 x20 ) 85 ) ( >= ( - x27 x25 ) 24 ) ) (or ( >= ( - x11 x1 ) 9 ) (not ( >= ( - x16 x32 ) 1 )) ) (or ( >= ( - x16 x28 ) 88 ) ( >= ( - x20 x16 ) 69 ) ) (or (not ( >= ( - x21 x1 ) 1 )) (not ( >= ( - x4 x33 ) 47 )) ) (or ( >= ( - x30 x10 ) 49 ) ( >= ( - x25 x5 ) 40 ) ) (or ( >= ( - x31 x12 ) 2 ) (not ( >= ( - x20 x8 ) 37 )) ) (or (not ( >= ( - x20 x25 ) 95 )) ( >= ( - x24 x23 ) 44 ) ) (or (not ( >= ( - x3 x5 ) 10 )) ( >= ( - x4 x28 ) 72 ) ) (or (not ( >= ( - x30 x14 ) 93 )) ( >= ( - x1 x22 ) 43 ) ) (or ( >= ( - x24 x14 ) 89 ) (not ( >= ( - x15 x5 ) 85 )) ) (or (not ( >= ( - x24 x19 ) 15 )) (not ( >= ( - x29 x33 ) 46 )) ) (or (not ( >= ( - x29 x12 ) 72 )) ( >= ( - x30 x5 ) 71 ) ) (or (not ( >= ( - x30 x10 ) 43 )) ( >= ( - x17 x2 ) 45 ) ) (or (not ( >= ( - x21 x34 ) 77 )) (not ( >= ( - x6 x28 ) 10 )) ) (or ( >= ( - x21 x33 ) 52 ) (not ( >= ( - x31 x16 ) 15 )) ) (or ( >= ( - x16 x17 ) 13 ) (not ( >= ( - x13 x20 ) 23 )) ) (or ( >= ( - x8 x32 ) 87 ) (not ( >= ( - x16 x30 ) 22 )) ) (or ( >= ( - x21 x33 ) 3 ) (not ( >= ( - x26 x7 ) 67 )) ) (or (not ( >= ( - x12 x1 ) 29 )) (not ( >= ( - x34 x13 ) 67 )) ) (or ( >= ( - x7 x18 ) 6 ) (not ( >= ( - x15 x12 ) 80 )) ) (or (not ( >= ( - x12 x18 ) 3 )) (not ( >= ( - x24 x4 ) 48 )) ) (or ( >= ( - x31 x20 ) 80 ) (not ( >= ( - x32 x33 ) 76 )) ) (or (not ( >= ( - x1 x4 ) 91 )) ( >= ( - x7 x18 ) 78 ) ) (or ( >= ( - x3 x14 ) 64 ) (not ( >= ( - x32 x6 ) 7 )) ) (or ( >= ( - x8 x5 ) 22 ) ( >= ( - x2 x29 ) 44 ) ) (or (not ( >= ( - x24 x10 ) 88 )) (not ( >= ( - x6 x20 ) 54 )) ) (or ( >= ( - x34 x18 ) 20 ) ( >= ( - x5 x2 ) 20 ) ) (or (not ( >= ( - x6 x26 ) 60 )) (not ( >= ( - x26 x28 ) 33 )) ) (or ( >= ( - x10 x4 ) 35 ) ( >= ( - x4 x13 ) 58 ) ) (or ( >= ( - x29 x23 ) 56 ) ( >= ( - x31 x3 ) 44 ) ) (or (not ( >= ( - x14 x24 ) 22 )) (not ( >= ( - x20 x1 ) 95 )) ) (or (not ( >= ( - x26 x19 ) 70 )) (not ( >= ( - x3 x5 ) 34 )) ) (or ( >= ( - x24 x33 ) 7 ) ( >= ( - x27 x3 ) 58 ) ) (or (not ( >= ( - x12 x3 ) 7 )) (not ( >= ( - x25 x29 ) 64 )) ) (or ( >= ( - x8 x23 ) 13 ) (not ( >= ( - x23 x6 ) 63 )) ) (or (not ( >= ( - x4 x15 ) 49 )) (not ( >= ( - x9 x12 ) 58 )) ) (or (not ( >= ( - x1 x6 ) 49 )) ( >= ( - x18 x17 ) 89 ) ) (or (not ( >= ( - x16 x28 ) 27 )) (not ( >= ( - x31 x20 ) 48 )) ) (or (not ( >= ( - x17 x19 ) 17 )) ( >= ( - x22 x2 ) 75 ) ) (or (not ( >= ( - x23 x11 ) 34 )) ( >= ( - x10 x19 ) 45 ) ) (or (not ( >= ( - x0 x1 ) 75 )) (not ( >= ( - x4 x27 ) 16 )) ) (or ( >= ( - x9 x14 ) 34 ) (not ( >= ( - x6 x2 ) 67 )) ) (or ( >= ( - x16 x3 ) 59 ) ( >= ( - x8 x17 ) 95 ) ) (or ( >= ( - x18 x30 ) 33 ) (not ( >= ( - x6 x12 ) 60 )) ) (or (not ( >= ( - x10 x20 ) 86 )) (not ( >= ( - x31 x12 ) 40 )) ) (or (not ( >= ( - x23 x11 ) 74 )) (not ( >= ( - x17 x13 ) 7 )) ) (or (not ( >= ( - x24 x29 ) 82 )) ( >= ( - x1 x0 ) 6 ) ) (or (not ( >= ( - x1 x9 ) 99 )) ( >= ( - x34 x7 ) 84 ) ) (or (not ( >= ( - x34 x27 ) 32 )) (not ( >= ( - x12 x20 ) 96 )) ) (or ( >= ( - x6 x34 ) 99 ) ( >= ( - x30 x2 ) 42 ) ) (or ( >= ( - x32 x7 ) 49 ) ( >= ( - x1 x12 ) 70 ) ) (or (not ( >= ( - x3 x17 ) 67 )) (not ( >= ( - x31 x8 ) 37 )) ) (or (not ( >= ( - x0 x32 ) 100 )) (not ( >= ( - x25 x32 ) 81 )) ) (or (not ( >= ( - x14 x19 ) 35 )) (not ( >= ( - x0 x34 ) 33 )) ) (or ( >= ( - x18 x16 ) 1 ) ( >= ( - x7 x19 ) 66 ) ) (or (not ( >= ( - x22 x13 ) 48 )) (not ( >= ( - x2 x19 ) 90 )) ) (or (not ( >= ( - x17 x28 ) 39 )) (not ( >= ( - x10 x21 ) 77 )) ) (or (not ( >= ( - x26 x10 ) 55 )) ( >= ( - x6 x34 ) 80 ) ) (or ( >= ( - x22 x25 ) 61 ) (not ( >= ( - x24 x32 ) 36 )) ) (or (not ( >= ( - x4 x26 ) 3 )) (not ( >= ( - x31 x0 ) 92 )) ) (or ( >= ( - x29 x20 ) 13 ) (not ( >= ( - x21 x31 ) 35 )) ) (or (not ( >= ( - x30 x18 ) 17 )) (not ( >= ( - x32 x29 ) 20 )) ) (or ( >= ( - x23 x32 ) 88 ) ( >= ( - x3 x0 ) 77 ) ) (or ( >= ( - x16 x30 ) 48 ) (not ( >= ( - x4 x32 ) 64 )) ) ))