source: vis_dev/cusp-1.1/examples/diamonds.10.2.i.a.u/diamonds.10.2.i.a.u.smt @ 23

(benchmark diamonds.10.2.i.a.u.smt
:source {
Diamond benchmarks generated by Ofer Strichman
(see http://iew3.technion.ac.il/Home/Users/ofers.phtml).

Translated into SMT-LIB format by Albert Oliveras.
}
:status unsat
:category { crafted }
:difficulty { 0 }
:logic QF_IDL
:extrafuns ((x0_0 Int))
:extrafuns ((x0 Int))
:extrafuns ((x0__0 Int))
:extrafuns ((x0_1 Int))
:extrafuns ((x0__1 Int))
:extrafuns ((x1 Int))
:extrafuns ((x1_0 Int))
:extrafuns ((x10 Int))
:extrafuns ((x1__0 Int))
:extrafuns ((x1_1 Int))
:extrafuns ((x1__1 Int))
:extrafuns ((x2 Int))
:extrafuns ((x2_0 Int))
:extrafuns ((x2__0 Int))
:extrafuns ((x2_1 Int))
:extrafuns ((x2__1 Int))
:extrafuns ((x3 Int))
:extrafuns ((x3_0 Int))
:extrafuns ((x3__0 Int))
:extrafuns ((x3_1 Int))
:extrafuns ((x3__1 Int))
:extrafuns ((x4 Int))
:extrafuns ((x4_0 Int))
:extrafuns ((x4__0 Int))
:extrafuns ((x4_1 Int))
:extrafuns ((x4__1 Int))
:extrafuns ((x5 Int))
:extrafuns ((x5_0 Int))
:extrafuns ((x5__0 Int))
:extrafuns ((x5_1 Int))
:extrafuns ((x5__1 Int))
:extrafuns ((x6 Int))
:extrafuns ((x6_0 Int))
:extrafuns ((x6__0 Int))
:extrafuns ((x6_1 Int))
:extrafuns ((x6__1 Int))
:extrafuns ((x7 Int))
:extrafuns ((x7_0 Int))
:extrafuns ((x7__0 Int))
:extrafuns ((x7_1 Int))
:extrafuns ((x7__1 Int))
:extrafuns ((x8 Int))
:extrafuns ((x8_0 Int))
:extrafuns ((x8__0 Int))
:extrafuns ((x8_1 Int))
:extrafuns ((x8__1 Int))
:extrafuns ((x9 Int))
:extrafuns ((x9_0 Int))
:extrafuns ((x9__0 Int))
:extrafuns ((x9_1 Int))
:extrafuns ((x9__1 Int))
:formula
( and
(or  (not ( >= ( - x0_0 x0 ) 1 ))  (not ( >= ( - x0__0 x0 ) 1 ))  )
(or  (not ( >= ( - x0_0 x0 ) 1 ))  (not ( >= ( - x0__1 x0__0 ) 1 ))  )
(or  (not ( >= ( - x0_0 x0 ) 1 ))  (not ( >= ( - x1 x0__1 ) 1 ))  )
(or  (not ( >= ( - x0_1 x0_0 ) 1 ))  (not ( >= ( - x0__0 x0 ) 1 ))  )
(or  (not ( >= ( - x0_1 x0_0 ) 1 ))  (not ( >= ( - x0__1 x0__0 ) 1 ))  )
(or  (not ( >= ( - x0_1 x0_0 ) 1 ))  (not ( >= ( - x1 x0__1 ) 1 ))  )
(or  (not ( >= ( - x1 x0_1 ) 1 ))  (not ( >= ( - x0__0 x0 ) 1 ))  )
(or  (not ( >= ( - x1 x0_1 ) 1 ))  (not ( >= ( - x0__1 x0__0 ) 1 ))  )
(or  (not ( >= ( - x1 x0_1 ) 1 ))  (not ( >= ( - x1 x0__1 ) 1 ))  )
(or  (not ( >= ( - x1_0 x1 ) 1 ))  (not ( >= ( - x1__0 x1 ) 1 ))  )
(or  (not ( >= ( - x1_0 x1 ) 1 ))  (not ( >= ( - x1__1 x1__0 ) 1 ))  )
(or  (not ( >= ( - x1_0 x1 ) 1 ))  (not ( >= ( - x2 x1__1 ) 1 ))  )
(or  (not ( >= ( - x1_1 x1_0 ) 1 ))  (not ( >= ( - x1__0 x1 ) 1 ))  )
(or  (not ( >= ( - x1_1 x1_0 ) 1 ))  (not ( >= ( - x1__1 x1__0 ) 1 ))  )
(or  (not ( >= ( - x1_1 x1_0 ) 1 ))  (not ( >= ( - x2 x1__1 ) 1 ))  )
(or  (not ( >= ( - x2 x1_1 ) 1 ))  (not ( >= ( - x1__0 x1 ) 1 ))  )
(or  (not ( >= ( - x2 x1_1 ) 1 ))  (not ( >= ( - x1__1 x1__0 ) 1 ))  )
(or  (not ( >= ( - x2 x1_1 ) 1 ))  (not ( >= ( - x2 x1__1 ) 1 ))  )
(or  (not ( >= ( - x2_0 x2 ) 1 ))  (not ( >= ( - x2__0 x2 ) 1 ))  )
(or  (not ( >= ( - x2_0 x2 ) 1 ))  (not ( >= ( - x2__1 x2__0 ) 1 ))  )
(or  (not ( >= ( - x2_0 x2 ) 1 ))  (not ( >= ( - x3 x2__1 ) 1 ))  )
(or  (not ( >= ( - x2_1 x2_0 ) 1 ))  (not ( >= ( - x2__0 x2 ) 1 ))  )
(or  (not ( >= ( - x2_1 x2_0 ) 1 ))  (not ( >= ( - x2__1 x2__0 ) 1 ))  )
(or  (not ( >= ( - x2_1 x2_0 ) 1 ))  (not ( >= ( - x3 x2__1 ) 1 ))  )
(or  (not ( >= ( - x3 x2_1 ) 1 ))  (not ( >= ( - x2__0 x2 ) 1 ))  )
(or  (not ( >= ( - x3 x2_1 ) 1 ))  (not ( >= ( - x2__1 x2__0 ) 1 ))  )
(or  (not ( >= ( - x3 x2_1 ) 1 ))  (not ( >= ( - x3 x2__1 ) 1 ))  )
(or  (not ( >= ( - x3_0 x3 ) 1 ))  (not ( >= ( - x3__0 x3 ) 1 ))  )
(or  (not ( >= ( - x3_0 x3 ) 1 ))  (not ( >= ( - x3__1 x3__0 ) 1 ))  )
(or  (not ( >= ( - x3_0 x3 ) 1 ))  (not ( >= ( - x4 x3__1 ) 1 ))  )
(or  (not ( >= ( - x3_1 x3_0 ) 1 ))  (not ( >= ( - x3__0 x3 ) 1 ))  )
(or  (not ( >= ( - x3_1 x3_0 ) 1 ))  (not ( >= ( - x3__1 x3__0 ) 1 ))  )
(or  (not ( >= ( - x3_1 x3_0 ) 1 ))  (not ( >= ( - x4 x3__1 ) 1 ))  )
(or  (not ( >= ( - x4 x3_1 ) 1 ))  (not ( >= ( - x3__0 x3 ) 1 ))  )
(or  (not ( >= ( - x4 x3_1 ) 1 ))  (not ( >= ( - x3__1 x3__0 ) 1 ))  )
(or  (not ( >= ( - x4 x3_1 ) 1 ))  (not ( >= ( - x4 x3__1 ) 1 ))  )
(or  (not ( >= ( - x4_0 x4 ) 1 ))  (not ( >= ( - x4__0 x4 ) 1 ))  )
(or  (not ( >= ( - x4_0 x4 ) 1 ))  (not ( >= ( - x4__1 x4__0 ) 1 ))  )
(or  (not ( >= ( - x4_0 x4 ) 1 ))  (not ( >= ( - x5 x4__1 ) 1 ))  )
(or  (not ( >= ( - x4_1 x4_0 ) 1 ))  (not ( >= ( - x4__0 x4 ) 1 ))  )
(or  (not ( >= ( - x4_1 x4_0 ) 1 ))  (not ( >= ( - x4__1 x4__0 ) 1 ))  )
(or  (not ( >= ( - x4_1 x4_0 ) 1 ))  (not ( >= ( - x5 x4__1 ) 1 ))  )
(or  (not ( >= ( - x5 x4_1 ) 1 ))  (not ( >= ( - x4__0 x4 ) 1 ))  )
(or  (not ( >= ( - x5 x4_1 ) 1 ))  (not ( >= ( - x4__1 x4__0 ) 1 ))  )
(or  (not ( >= ( - x5 x4_1 ) 1 ))  (not ( >= ( - x5 x4__1 ) 1 ))  )
(or  (not ( >= ( - x5_0 x5 ) 1 ))  (not ( >= ( - x5__0 x5 ) 1 ))  )
(or  (not ( >= ( - x5_0 x5 ) 1 ))  (not ( >= ( - x5__1 x5__0 ) 1 ))  )
(or  (not ( >= ( - x5_0 x5 ) 1 ))  (not ( >= ( - x6 x5__1 ) 1 ))  )
(or  (not ( >= ( - x5_1 x5_0 ) 1 ))  (not ( >= ( - x5__0 x5 ) 1 ))  )
(or  (not ( >= ( - x5_1 x5_0 ) 1 ))  (not ( >= ( - x5__1 x5__0 ) 1 ))  )
(or  (not ( >= ( - x5_1 x5_0 ) 1 ))  (not ( >= ( - x6 x5__1 ) 1 ))  )
(or  (not ( >= ( - x6 x5_1 ) 1 ))  (not ( >= ( - x5__0 x5 ) 1 ))  )
(or  (not ( >= ( - x6 x5_1 ) 1 ))  (not ( >= ( - x5__1 x5__0 ) 1 ))  )
(or  (not ( >= ( - x6 x5_1 ) 1 ))  (not ( >= ( - x6 x5__1 ) 1 ))  )
(or  (not ( >= ( - x6_0 x6 ) 1 ))  (not ( >= ( - x6__0 x6 ) 1 ))  )
(or  (not ( >= ( - x6_0 x6 ) 1 ))  (not ( >= ( - x6__1 x6__0 ) 1 ))  )
(or  (not ( >= ( - x6_0 x6 ) 1 ))  (not ( >= ( - x7 x6__1 ) 1 ))  )
(or  (not ( >= ( - x6_1 x6_0 ) 1 ))  (not ( >= ( - x6__0 x6 ) 1 ))  )
(or  (not ( >= ( - x6_1 x6_0 ) 1 ))  (not ( >= ( - x6__1 x6__0 ) 1 ))  )
(or  (not ( >= ( - x6_1 x6_0 ) 1 ))  (not ( >= ( - x7 x6__1 ) 1 ))  )
(or  (not ( >= ( - x7 x6_1 ) 1 ))  (not ( >= ( - x6__0 x6 ) 1 ))  )
(or  (not ( >= ( - x7 x6_1 ) 1 ))  (not ( >= ( - x6__1 x6__0 ) 1 ))  )
(or  (not ( >= ( - x7 x6_1 ) 1 ))  (not ( >= ( - x7 x6__1 ) 1 ))  )
(or  (not ( >= ( - x7_0 x7 ) 1 ))  (not ( >= ( - x7__0 x7 ) 1 ))  )
(or  (not ( >= ( - x7_0 x7 ) 1 ))  (not ( >= ( - x7__1 x7__0 ) 1 ))  )
(or  (not ( >= ( - x7_0 x7 ) 1 ))  (not ( >= ( - x8 x7__1 ) 1 ))  )
(or  (not ( >= ( - x7_1 x7_0 ) 1 ))  (not ( >= ( - x7__0 x7 ) 1 ))  )
(or  (not ( >= ( - x7_1 x7_0 ) 1 ))  (not ( >= ( - x7__1 x7__0 ) 1 ))  )
(or  (not ( >= ( - x7_1 x7_0 ) 1 ))  (not ( >= ( - x8 x7__1 ) 1 ))  )
(or  (not ( >= ( - x8 x7_1 ) 1 ))  (not ( >= ( - x7__0 x7 ) 1 ))  )
(or  (not ( >= ( - x8 x7_1 ) 1 ))  (not ( >= ( - x7__1 x7__0 ) 1 ))  )
(or  (not ( >= ( - x8 x7_1 ) 1 ))  (not ( >= ( - x8 x7__1 ) 1 ))  )
(or  (not ( >= ( - x8_0 x8 ) 1 ))  (not ( >= ( - x8__0 x8 ) 1 ))  )
(or  (not ( >= ( - x8_0 x8 ) 1 ))  (not ( >= ( - x8__1 x8__0 ) 1 ))  )
(or  (not ( >= ( - x8_0 x8 ) 1 ))  (not ( >= ( - x9 x8__1 ) 1 ))  )
(or  (not ( >= ( - x8_1 x8_0 ) 1 ))  (not ( >= ( - x8__0 x8 ) 1 ))  )
(or  (not ( >= ( - x8_1 x8_0 ) 1 ))  (not ( >= ( - x8__1 x8__0 ) 1 ))  )
(or  (not ( >= ( - x8_1 x8_0 ) 1 ))  (not ( >= ( - x9 x8__1 ) 1 ))  )
(or  (not ( >= ( - x9 x8_1 ) 1 ))  (not ( >= ( - x8__0 x8 ) 1 ))  )
(or  (not ( >= ( - x9 x8_1 ) 1 ))  (not ( >= ( - x8__1 x8__0 ) 1 ))  )
(or  (not ( >= ( - x9 x8_1 ) 1 ))  (not ( >= ( - x9 x8__1 ) 1 ))  )
(or  (not ( >= ( - x9_0 x9 ) 1 ))  (not ( >= ( - x9__0 x9 ) 1 ))  )
(or  (not ( >= ( - x9_0 x9 ) 1 ))  (not ( >= ( - x9__1 x9__0 ) 1 ))  )
(or  (not ( >= ( - x9_0 x9 ) 1 ))  (not ( >= ( - x10 x9__1 ) 1 ))  )
(or  (not ( >= ( - x9_1 x9_0 ) 1 ))  (not ( >= ( - x9__0 x9 ) 1 ))  )
(or  (not ( >= ( - x9_1 x9_0 ) 1 ))  (not ( >= ( - x9__1 x9__0 ) 1 ))  )
(or  (not ( >= ( - x9_1 x9_0 ) 1 ))  (not ( >= ( - x10 x9__1 ) 1 ))  )
(or  (not ( >= ( - x10 x9_1 ) 1 ))  (not ( >= ( - x9__0 x9 ) 1 ))  )
(or  (not ( >= ( - x10 x9_1 ) 1 ))  (not ( >= ( - x9__1 x9__0 ) 1 ))  )
(or  (not ( >= ( - x10 x9_1 ) 1 ))  (not ( >= ( - x10 x9__1 ) 1 ))  )
( >= ( - x10 x0 ) 1 ) 
))