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