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