source: vis_dev/cusp-1.1/examples/DTP_k2_n35_c175_s1/DTP_k2_n35_c175_s1.smt @ 106

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