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