(benchmark toroidal_queen_2_1.smt
:status unsat
:logic QF_IDL
:extrafuns ((x0 Int))
:extrafuns ((x1 Int))
:extrafuns ((x2 Int))
:formula
( and
( <= (- x0 x2 ) 1 )
( >= (- x0 x2 ) 0 )
( <= (- x1 x2 ) 1 )
( >= (- x1 x2 ) 0 )
(not ( = x0 x1 ))
(not ( = (- x0 x1 ) 1 ))
(not ( = (- x0 x1 ) (~ 1) ))
))
