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