(benchmark DTP_k2_n35_c210_s1.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 ((x18 Int)) :extrafuns ((x0 Int)) :extrafuns ((x11 Int)) :extrafuns ((x10 Int)) :extrafuns ((x1 Int)) :extrafuns ((x16 Int)) :extrafuns ((x12 Int)) :extrafuns ((x13 Int)) :extrafuns ((x14 Int)) :extrafuns ((x15 Int)) :extrafuns ((x17 Int)) :extrafuns ((x32 Int)) :extrafuns ((x31 Int)) :extrafuns ((x3 Int)) :extrafuns ((x19 Int)) :extrafuns ((x21 Int)) :extrafuns ((x20 Int)) :extrafuns ((x2 Int)) :extrafuns ((x25 Int)) :extrafuns ((x24 Int)) :extrafuns ((x22 Int)) :extrafuns ((x23 Int)) :extrafuns ((x26 Int)) :extrafuns ((x28 Int)) :extrafuns ((x27 Int)) :extrafuns ((x29 Int)) :extrafuns ((x30 Int)) :extrafuns ((x5 Int)) :extrafuns ((x4 Int)) :extrafuns ((x34 Int)) :extrafuns ((x33 Int)) :extrafuns ((x8 Int)) :extrafuns ((x7 Int)) :extrafuns ((x6 Int)) :extrafuns ((x9 Int)) :formula ( and (or (not ( >= ( - x18 x0 ) 45 )) ( >= ( - x32 x5 ) 63 ) ) (or ( >= ( - x31 x32 ) 97 ) (not ( >= ( - x4 x18 ) 74 )) ) (or (not ( >= ( - x11 x3 ) 73 )) (not ( >= ( - x19 x11 ) 37 )) ) (or (not ( >= ( - x21 x3 ) 70 )) (not ( >= ( - x16 x20 ) 21 )) ) (or (not ( >= ( - x25 x5 ) 57 )) ( >= ( - x12 x2 ) 6 ) ) (or (not ( >= ( - x3 x13 ) 40 )) ( >= ( - x20 x8 ) 86 ) ) (or ( >= ( - x21 x2 ) 82 ) ( >= ( - x24 x4 ) 37 ) ) (or (not ( >= ( - x5 x34 ) 48 )) (not ( >= ( - x26 x17 ) 35 )) ) (or ( >= ( - x4 x9 ) 3 ) ( >= ( - x12 x33 ) 30 ) ) (or (not ( >= ( - x28 x24 ) 78 )) (not ( >= ( - x18 x22 ) 24 )) ) (or (not ( >= ( - x14 x2 ) 14 )) (not ( >= ( - x0 x9 ) 84 )) ) (or ( >= ( - x26 x8 ) 83 ) ( >= ( - x32 x28 ) 98 ) ) (or (not ( >= ( - x14 x17 ) 3 )) ( >= ( - x11 x10 ) 89 ) ) (or (not ( >= ( - x4 x29 ) 97 )) (not ( >= ( - x2 x7 ) 73 )) ) (or (not ( >= ( - x30 x32 ) 58 )) (not ( >= ( - x17 x4 ) 58 )) ) (or ( >= ( - x30 x5 ) 98 ) ( >= ( - x11 x5 ) 38 ) ) (or (not ( >= ( - x13 x14 ) 58 )) (not ( >= ( - x16 x19 ) 65 )) ) (or (not ( >= ( - x1 x4 ) 21 )) (not ( >= ( - x30 x2 ) 89 )) ) (or ( >= ( - x34 x27 ) 59 ) (not ( >= ( - x17 x1 ) 59 )) ) (or (not ( >= ( - x3 x24 ) 13 )) ( >= ( - x6 x0 ) 50 ) ) (or ( >= ( - x31 x7 ) 88 ) (not ( >= ( - x7 x23 ) 33 )) ) (or ( >= ( - x13 x14 ) 86 ) (not ( >= ( - x16 x3 ) 37 )) ) (or ( >= ( - x6 x30 ) 27 ) (not ( >= ( - x8 x29 ) 64 )) ) (or (not ( >= ( - x2 x20 ) 77 )) (not ( >= ( - x9 x15 ) 71 )) ) (or (not ( >= ( - x9 x17 ) 25 )) ( >= ( - x9 x7 ) 21 ) ) (or ( >= ( - x12 x30 ) 17 ) (not ( >= ( - x3 x22 ) 97 )) ) (or (not ( >= ( - x34 x14 ) 18 )) (not ( >= ( - x15 x34 ) 32 )) ) (or ( >= ( - x5 x30 ) 57 ) (not ( >= ( - x27 x0 ) 63 )) ) (or ( >= ( - x31 x24 ) 28 ) ( >= ( - x15 x16 ) 28 ) ) (or ( >= ( - x27 x33 ) 97 ) (not ( >= ( - x23 x9 ) 41 )) ) (or (not ( >= ( - x23 x13 ) 10 )) ( >= ( - x15 x20 ) 20 ) ) (or ( >= ( - x5 x2 ) 72 ) (not ( >= ( - x22 x12 ) 31 )) ) (or (not ( >= ( - x13 x30 ) 61 )) (not ( >= ( - x0 x30 ) 66 )) ) (or ( >= ( - x17 x3 ) 77 ) (not ( >= ( - x4 x8 ) 42 )) ) (or (not ( >= ( - x9 x25 ) 82 )) (not ( >= ( - x21 x31 ) 89 )) ) (or ( >= ( - x34 x3 ) 25 ) ( >= ( - x34 x6 ) 18 ) ) (or (not ( >= ( - x1 x21 ) 13 )) (not ( >= ( - x32 x30 ) 8 )) ) (or (not ( >= ( - x30 x23 ) 7 )) (not ( >= ( - x26 x0 ) 52 )) ) (or (not ( >= ( - x27 x8 ) 93 )) ( >= ( - x23 x10 ) 60 ) ) (or (not ( >= ( - x24 x13 ) 55 )) (not ( >= ( - x32 x29 ) 70 )) ) (or (not ( >= ( - x21 x6 ) 4 )) (not ( >= ( - x14 x17 ) 36 )) ) (or ( >= ( - x28 x21 ) 91 ) (not ( >= ( - x22 x17 ) 98 )) ) (or (not ( >= ( - x5 x23 ) 17 )) ( >= ( - x24 x33 ) 53 ) ) (or (not ( >= ( - x25 x23 ) 8 )) ( >= ( - x34 x14 ) 73 ) ) (or (not ( >= ( - x26 x27 ) 63 )) ( >= ( - x7 x0 ) 54 ) ) (or ( >= ( - x2 x34 ) 39 ) (not ( >= ( - x8 x33 ) 78 )) ) (or ( >= ( - x19 x18 ) 51 ) (not ( >= ( - x6 x32 ) 43 )) ) (or (not ( >= ( - x3 x26 ) 40 )) ( >= ( - x17 x19 ) 40 ) ) (or ( >= ( - x13 x14 ) 74 ) (not ( >= ( - x17 x31 ) 6 )) ) (or ( >= ( - x15 x24 ) 5 ) ( >= ( - x0 x14 ) 79 ) ) (or (not ( >= ( - x5 x14 ) 76 )) ( >= ( - x28 x33 ) 27 ) ) (or ( >= ( - x26 x27 ) 16 ) (not ( >= ( - x18 x3 ) 92 )) ) (or (not ( >= ( - x9 x26 ) 71 )) (not ( >= ( - x16 x15 ) 89 )) ) (or ( >= ( - x32 x28 ) 19 ) (not ( >= ( - x22 x32 ) 40 )) ) (or (not ( >= ( - x32 x29 ) 68 )) ( >= ( - x30 x3 ) 66 ) ) (or (not ( >= ( - x13 x18 ) 70 )) (not ( >= ( - x13 x34 ) 17 )) ) (or ( >= ( - x7 x29 ) 8 ) ( >= ( - x5 x17 ) 50 ) ) (or (not ( >= ( - x30 x22 ) 16 )) ( >= ( - x13 x12 ) 64 ) ) (or (not ( >= ( - x27 x23 ) 42 )) ( >= ( - x10 x31 ) 54 ) ) (or ( >= ( - x31 x18 ) 12 ) (not ( >= ( - x14 x10 ) 88 )) ) (or ( >= ( - x26 x24 ) 93 ) (not ( >= ( - x5 x15 ) 91 )) ) (or ( >= ( - x23 x11 ) 66 ) ( >= ( - x28 x8 ) 94 ) ) (or ( >= ( - x17 x25 ) 8 ) (not ( >= ( - x30 x29 ) 19 )) ) (or (not ( >= ( - x30 x22 ) 63 )) (not ( >= ( - x28 x18 ) 43 )) ) (or (not ( >= ( - x7 x12 ) 57 )) ( >= ( - x21 x10 ) 10 ) ) (or ( >= ( - x12 x23 ) 39 ) (not ( >= ( - x10 x28 ) 80 )) ) (or (not ( >= ( - x15 x19 ) 38 )) ( >= ( - x19 x16 ) 77 ) ) (or (not ( >= ( - x24 x28 ) 94 )) ( >= ( - x3 x4 ) 7 ) ) (or (not ( >= ( - x15 x20 ) 39 )) ( >= ( - x34 x18 ) 50 ) ) (or (not ( >= ( - x11 x0 ) 86 )) (not ( >= ( - x2 x18 ) 47 )) ) (or ( >= ( - x26 x13 ) 49 ) (not ( >= ( - x9 x22 ) 54 )) ) (or ( >= ( - x29 x3 ) 91 ) ( >= ( - x5 x33 ) 43 ) ) (or (not ( >= ( - x23 x26 ) 8 )) (not ( >= ( - x29 x27 ) 70 )) ) (or (not ( >= ( - x9 x25 ) 2 )) ( >= ( - x28 x10 ) 3 ) ) (or (not ( >= ( - x13 x29 ) 47 )) ( >= ( - x34 x28 ) 11 ) ) (or ( >= ( - x4 x18 ) 10 ) (not ( >= ( - x11 x15 ) 95 )) ) (or ( >= ( - x0 x25 ) 80 ) ( >= ( - x14 x24 ) 41 ) ) (or ( >= ( - x4 x6 ) 14 ) ( >= ( - x1 x19 ) 43 ) ) (or ( >= ( - x26 x33 ) 9 ) ( >= ( - x25 x17 ) 28 ) ) (or ( >= ( - x11 x1 ) 96 ) ( >= ( - x31 x25 ) 28 ) ) (or ( >= ( - x7 x19 ) 66 ) ( >= ( - x24 x34 ) 6 ) ) (or (not ( >= ( - x25 x15 ) 10 )) ( >= ( - x6 x17 ) 86 ) ) (or ( >= ( - x6 x1 ) 25 ) (not ( >= ( - x19 x6 ) 56 )) ) (or (not ( >= ( - x21 x17 ) 29 )) ( >= ( - x1 x8 ) 73 ) ) (or (not ( >= ( - x1 x31 ) 29 )) (not ( >= ( - x12 x29 ) 44 )) ) (or (not ( >= ( - x0 x4 ) 68 )) ( >= ( - x14 x2 ) 13 ) ) (or ( >= ( - x0 x8 ) 96 ) ( >= ( - x5 x10 ) 78 ) ) (or ( >= ( - x21 x15 ) 88 ) ( >= ( - x26 x1 ) 87 ) ) (or (not ( >= ( - x0 x6 ) 17 )) (not ( >= ( - x2 x16 ) 38 )) ) (or (not ( >= ( - x8 x4 ) 14 )) ( >= ( - x34 x13 ) 64 ) ) (or (not ( >= ( - x23 x9 ) 62 )) (not ( >= ( - x26 x17 ) 85 )) ) (or (not ( >= ( - x22 x1 ) 91 )) (not ( >= ( - x17 x29 ) 74 )) ) (or ( >= ( - x13 x2 ) 23 ) (not ( >= ( - x4 x7 ) 28 )) ) (or ( >= ( - x0 x18 ) 52 ) ( >= ( - x27 x14 ) 38 ) ) (or (not ( >= ( - x13 x32 ) 65 )) (not ( >= ( - x24 x13 ) 84 )) ) (or ( >= ( - x3 x1 ) 18 ) (not ( >= ( - x7 x16 ) 92 )) ) (or (not ( >= ( - x1 x34 ) 43 )) (not ( >= ( - x7 x5 ) 11 )) ) (or ( >= ( - x9 x20 ) 19 ) ( >= ( - x6 x12 ) 4 ) ) (or ( >= ( - x1 x4 ) 47 ) (not ( >= ( - x27 x20 ) 13 )) ) (or ( >= ( - x19 x33 ) 80 ) (not ( >= ( - x23 x22 ) 16 )) ) (or ( >= ( - x16 x7 ) 9 ) ( >= ( - x5 x26 ) 21 ) ) (or (not ( >= ( - x29 x26 ) 91 )) ( >= ( - x33 x29 ) 98 ) ) (or ( >= ( - x19 x15 ) 5 ) ( >= ( - x31 x19 ) 91 ) ) (or (not ( >= ( - x2 x33 ) 46 )) (not ( >= ( - x26 x31 ) 7 )) ) (or ( >= ( - x30 x18 ) 82 ) (not ( >= ( - x16 x2 ) 87 )) ) (or (not ( >= ( - x15 x1 ) 51 )) ( >= ( - x13 x10 ) 89 ) ) (or (not ( >= ( - x33 x30 ) 71 )) (not ( >= ( - x15 x7 ) 28 )) ) (or (not ( >= ( - x26 x18 ) 9 )) ( >= ( - x29 x0 ) 63 ) ) (or (not ( >= ( - x4 x14 ) 54 )) ( >= ( - x20 x9 ) 40 ) ) (or ( >= ( - x9 x21 ) 29 ) ( >= ( - x7 x2 ) 83 ) ) (or (not ( >= ( - x0 x32 ) 20 )) ( >= ( - x13 x33 ) 15 ) ) (or (not ( >= ( - x4 x7 ) 47 )) ( >= ( - x16 x9 ) 41 ) ) (or ( >= ( - x12 x18 ) 12 ) (not ( >= ( - x25 x10 ) 72 )) ) (or (not ( >= ( - x7 x4 ) 28 )) ( >= ( - x29 x0 ) 10 ) ) (or ( >= ( - x29 x33 ) 50 ) (not ( >= ( - x6 x10 ) 88 )) ) (or (not ( >= ( - x21 x28 ) 94 )) (not ( >= ( - x22 x11 ) 76 )) ) (or ( >= ( - x10 x21 ) 94 ) (not ( >= ( - x28 x32 ) 39 )) ) (or ( >= ( - x16 x20 ) 9 ) (not ( >= ( - x19 x3 ) 53 )) ) (or ( >= ( - x34 x12 ) 68 ) ( >= ( - x30 x15 ) 60 ) ) (or ( >= ( - x4 x32 ) 1 ) (not ( >= ( - x23 x3 ) 68 )) ) (or (not ( >= ( - x31 x18 ) 76 )) ( >= ( - x6 x15 ) 13 ) ) (or ( >= ( - x2 x21 ) 97 ) (not ( >= ( - x19 x10 ) 54 )) ) (or (not ( >= ( - x7 x20 ) 51 )) ( >= ( - x9 x3 ) 35 ) ) (or (not ( >= ( - x21 x13 ) 30 )) ( >= ( - x18 x30 ) 92 ) ) (or ( >= ( - x27 x20 ) 3 ) ( >= ( - x28 x33 ) 27 ) ) (or ( >= ( - x32 x26 ) 67 ) ( >= ( - x29 x33 ) 18 ) ) (or ( >= ( - x1 x25 ) 93 ) ( >= ( - x26 x12 ) 17 ) ) (or (not ( >= ( - x32 x22 ) 28 )) ( >= ( - x21 x32 ) 4 ) ) (or ( >= ( - x25 x29 ) 56 ) (not ( >= ( - x17 x1 ) 42 )) ) (or ( >= ( - x1 x33 ) 32 ) (not ( >= ( - x28 x25 ) 27 )) ) (or (not ( >= ( - x14 x12 ) 18 )) (not ( >= ( - x28 x30 ) 21 )) ) (or ( >= ( - x22 x29 ) 26 ) (not ( >= ( - x17 x33 ) 63 )) ) (or ( >= ( - x3 x5 ) 49 ) (not ( >= ( - x5 x7 ) 55 )) ) (or (not ( >= ( - x9 x14 ) 5 )) ( >= ( - x31 x20 ) 48 ) ) (or ( >= ( - x6 x34 ) 92 ) ( >= ( - x20 x6 ) 81 ) ) (or (not ( >= ( - x18 x14 ) 72 )) (not ( >= ( - x30 x15 ) 20 )) ) (or (not ( >= ( - x12 x2 ) 51 )) (not ( >= ( - x26 x27 ) 33 )) ) (or ( >= ( - x1 x21 ) 28 ) ( >= ( - x2 x6 ) 54 ) ) (or (not ( >= ( - x31 x21 ) 99 )) (not ( >= ( - x1 x29 ) 17 )) ) (or (not ( >= ( - x11 x15 ) 48 )) ( >= ( - x15 x9 ) 88 ) ) (or ( >= ( - x1 x29 ) 34 ) ( >= ( - x28 x3 ) 83 ) ) (or ( >= ( - x32 x22 ) 24 ) ( >= ( - x23 x0 ) 45 ) ) (or (not ( >= ( - x21 x28 ) 97 )) ( >= ( - x4 x3 ) 67 ) ) (or ( >= ( - x7 x16 ) 53 ) (not ( >= ( - x32 x3 ) 8 )) ) (or (not ( >= ( - x23 x6 ) 9 )) (not ( >= ( - x6 x15 ) 10 )) ) (or ( >= ( - x15 x25 ) 2 ) ( >= ( - x32 x23 ) 2 ) ) (or (not ( >= ( - x33 x24 ) 69 )) (not ( >= ( - x20 x9 ) 10 )) ) (or (not ( >= ( - x9 x32 ) 56 )) (not ( >= ( - x3 x26 ) 85 )) ) (or ( >= ( - x23 x12 ) 16 ) (not ( >= ( - x26 x11 ) 55 )) ) (or (not ( >= ( - x17 x29 ) 69 )) ( >= ( - x0 x13 ) 13 ) ) (or (not ( >= ( - x25 x33 ) 42 )) ( >= ( - x29 x32 ) 85 ) ) (or (not ( >= ( - x14 x34 ) 44 )) (not ( >= ( - x11 x33 ) 65 )) ) (or ( >= ( - x29 x21 ) 60 ) ( >= ( - x34 x18 ) 25 ) ) (or (not ( >= ( - x32 x3 ) 92 )) ( >= ( - x32 x16 ) 79 ) ) (or (not ( >= ( - x20 x17 ) 28 )) (not ( >= ( - x28 x8 ) 51 )) ) (or (not ( >= ( - x2 x23 ) 28 )) (not ( >= ( - x4 x5 ) 16 )) ) (or ( >= ( - x10 x20 ) 41 ) ( >= ( - x3 x0 ) 76 ) ) (or (not ( >= ( - x18 x19 ) 100 )) (not ( >= ( - x23 x5 ) 78 )) ) (or (not ( >= ( - x25 x27 ) 46 )) ( >= ( - x3 x32 ) 46 ) ) (or ( >= ( - x8 x30 ) 80 ) (not ( >= ( - x32 x20 ) 30 )) ) (or ( >= ( - x33 x11 ) 20 ) (not ( >= ( - x9 x0 ) 67 )) ) (or (not ( >= ( - x17 x19 ) 45 )) (not ( >= ( - x5 x24 ) 8 )) ) (or ( >= ( - x8 x16 ) 78 ) (not ( >= ( - x26 x0 ) 51 )) ) (or (not ( >= ( - x10 x20 ) 39 )) (not ( >= ( - x2 x25 ) 11 )) ) (or (not ( >= ( - x12 x34 ) 38 )) (not ( >= ( - x27 x2 ) 79 )) ) (or (not ( >= ( - x0 x14 ) 96 )) (not ( >= ( - x9 x11 ) 66 )) ) (or (not ( >= ( - x14 x22 ) 10 )) ( >= ( - x6 x23 ) 2 ) ) (or (not ( >= ( - x27 x24 ) 81 )) (not ( >= ( - x20 x24 ) 39 )) ) (or ( >= ( - x27 x12 ) 51 ) (not ( >= ( - x26 x4 ) 85 )) ) (or (not ( >= ( - x28 x31 ) 51 )) ( >= ( - x13 x26 ) 2 ) ) (or ( >= ( - x33 x21 ) 55 ) ( >= ( - x15 x13 ) 1 ) ) (or ( >= ( - x18 x3 ) 21 ) (not ( >= ( - x6 x15 ) 87 )) ) (or ( >= ( - x11 x14 ) 26 ) (not ( >= ( - x1 x9 ) 58 )) ) (or ( >= ( - x26 x32 ) 90 ) ( >= ( - x11 x2 ) 78 ) ) (or ( >= ( - x11 x9 ) 39 ) (not ( >= ( - x14 x21 ) 8 )) ) (or (not ( >= ( - x3 x33 ) 65 )) ( >= ( - x16 x15 ) 55 ) ) (or (not ( >= ( - x16 x15 ) 39 )) ( >= ( - x6 x13 ) 66 ) ) (or (not ( >= ( - x12 x17 ) 22 )) (not ( >= ( - x12 x29 ) 99 )) ) (or ( >= ( - x20 x4 ) 66 ) ( >= ( - x32 x21 ) 48 ) ) (or ( >= ( - x18 x26 ) 44 ) (not ( >= ( - x28 x22 ) 77 )) ) (or ( >= ( - x26 x27 ) 6 ) (not ( >= ( - x26 x31 ) 57 )) ) (or (not ( >= ( - x23 x27 ) 88 )) (not ( >= ( - x25 x10 ) 36 )) ) (or ( >= ( - x28 x11 ) 55 ) ( >= ( - x10 x4 ) 34 ) ) (or (not ( >= ( - x15 x31 ) 48 )) ( >= ( - x12 x13 ) 98 ) ) (or ( >= ( - x24 x3 ) 45 ) (not ( >= ( - x4 x27 ) 56 )) ) (or ( >= ( - x33 x7 ) 40 ) (not ( >= ( - x5 x15 ) 87 )) ) (or (not ( >= ( - x5 x3 ) 43 )) (not ( >= ( - x22 x1 ) 86 )) ) (or ( >= ( - x5 x15 ) 37 ) ( >= ( - x18 x3 ) 31 ) ) (or (not ( >= ( - x33 x23 ) 54 )) ( >= ( - x34 x30 ) 49 ) ) (or (not ( >= ( - x14 x28 ) 24 )) ( >= ( - x23 x3 ) 80 ) ) (or (not ( >= ( - x30 x4 ) 73 )) ( >= ( - x16 x23 ) 61 ) ) (or ( >= ( - x31 x22 ) 87 ) ( >= ( - x20 x19 ) 27 ) ) (or ( >= ( - x31 x22 ) 9 ) (not ( >= ( - x11 x29 ) 16 )) ) (or (not ( >= ( - x17 x14 ) 47 )) ( >= ( - x33 x1 ) 21 ) ) (or ( >= ( - x18 x17 ) 5 ) (not ( >= ( - x13 x29 ) 55 )) ) (or (not ( >= ( - x3 x10 ) 69 )) ( >= ( - x4 x32 ) 23 ) ) (or ( >= ( - x32 x17 ) 23 ) (not ( >= ( - x25 x6 ) 40 )) ) (or (not ( >= ( - x1 x27 ) 49 )) (not ( >= ( - x14 x10 ) 13 )) ) (or ( >= ( - x8 x10 ) 61 ) ( >= ( - x3 x9 ) 9 ) ) (or ( >= ( - x15 x11 ) 46 ) (not ( >= ( - x8 x29 ) 85 )) ) (or ( >= ( - x0 x26 ) 42 ) (not ( >= ( - x0 x34 ) 94 )) ) (or ( >= ( - x2 x30 ) 93 ) ( >= ( - x4 x32 ) 72 ) ) (or ( >= ( - x15 x25 ) 56 ) (not ( >= ( - x31 x10 ) 16 )) ) (or (not ( >= ( - x8 x13 ) 31 )) (not ( >= ( - x17 x30 ) 80 )) ) (or (not ( >= ( - x25 x20 ) 81 )) ( >= ( - x23 x8 ) 9 ) ) (or ( >= ( - x12 x21 ) 34 ) (not ( >= ( - x0 x6 ) 28 )) ) (or ( >= ( - x11 x4 ) 85 ) (not ( >= ( - x13 x10 ) 24 )) ) (or (not ( >= ( - x1 x3 ) 32 )) (not ( >= ( - x4 x23 ) 38 )) ) (or ( >= ( - x24 x9 ) 14 ) ( >= ( - x34 x29 ) 97 ) ) (or (not ( >= ( - x19 x5 ) 24 )) (not ( >= ( - x32 x1 ) 8 )) ) ))