(set-logic QF_IDL)
(set-info :source |
Queens benchmarks generated by Hyondeuk Kim in SMT-LIB format.
|)
(set-info :smt-lib-version 2.0)
(set-info :category "crafted")
(set-info :status sat)
(declare-fun x0 () Int)
(declare-fun x1 () Int)
(declare-fun x2 () Int)
(declare-fun x3 () Int)
(declare-fun x4 () Int)
(declare-fun x5 () Int)
(declare-fun x6 () Int)
(declare-fun x7 () Int)
(declare-fun x8 () Int)
(declare-fun x9 () Int)
(declare-fun x10 () Int)
(assert 
  (let 
    ((?v_0 (- x0 x10)) 
     (?v_1 (- x1 x10)) 
     (?v_2 (- x2 x10))
     (?v_3 (- x3 x10))
     (?v_4 (- x4 x10))
     (?v_5 (- x5 x10))
     (?v_6 (- x6 x10))
     (?v_7 (- x7 x10))
     (?v_8 (- x8 x10)) 
     (?v_9 (- x9 x10)) 
     (?v_10 (- x0 x1))
     (?v_11 (- x0 x2))
     (?v_12 (- x0 x3)) 
     (?v_13 (- x0 x4))
     (?v_14 (- x0 x5))
     (?v_15 (- x0 x6))
     (?v_16 (- x0 x7))
     (?v_17 (- x0 x8))
     (?v_18 (- x0 x9))
     (?v_19 (- x1 x2))
     (?v_20 (- x1 x3))
     (?v_21 (- x1 x4))
     (?v_22 (- x1 x5))
     (?v_23 (- x1 x6))
     (?v_24 (- x1 x7)) 
     (?v_25 (- x1 x8)) 
     (?v_26 (- x1 x9))
     (?v_27 (- x2 x3)) 
     (?v_28 (- x2 x4))
     (?v_29 (- x2 x5))
     (?v_30 (- x2 x6))
     (?v_31 (- x2 x7))
     (?v_32 (- x2 x8))
     (?v_33 (- x2 x9))
     (?v_34 (- x3 x4))
     (?v_35 (- x3 x5))
     (?v_36 (- x3 x6))
     (?v_37 (- x3 x7))
     (?v_38 (- x3 x8))
     (?v_39 (- x3 x9))
     (?v_40 (- x4 x5))
     (?v_41 (- x4 x6))
     (?v_42 (- x4 x7))
     (?v_43 (- x4 x8))
     (?v_44 (- x4 x9))
     (?v_45 (- x5 x6))
     (?v_46 (- x5 x7))
     (?v_47 (- x5 x8)) 
     (?v_48 (- x5 x9))
     (?v_49 (- x6 x7))
     (?v_50 (- x6 x8))
     (?v_51 (- x6 x9))
     (?v_52 (- x7 x8))
     (?v_53 (- x7 x9)) 
     (?v_54 (- x8 x9))) 
  (and (<= ?v_0 9) (>= ?v_0 0) (<= ?v_1 9) (>= ?v_1 0) (<= ?v_2 9) (>= ?v_2 0) 
       (<= ?v_3 9) (>= ?v_3 0) (<= ?v_4 9) (>= ?v_4 0) (<= ?v_5 9) (>= ?v_5 0) 
       (<= ?v_6 9) (>= ?v_6 0) (<= ?v_7 9) (>= ?v_7 0) (<= ?v_8 9) (>= ?v_8 0) 
       (<= ?v_9 9) (>= ?v_9 0)
       (not (= x0 x1)) (not (= x0 x2)) (not (= x0 x3)) (not (= x0 x4))
       (not (= x0 x5)) (not (= x0 x6)) (not (= x0 x7)) (not (= x0 x8)) 
       (not (= x0 x9)) (not (= x1 x2)) (not (= x1 x3)) (not (= x1 x4)) 
       (not (= x1 x5)) (not (= x1 x6)) (not (= x1 x7)) (not (= x1 x8)) 
       (not (= x1 x9)) (not (= x2 x3)) (not (= x2 x4)) (not (= x2 x5)) 
       (not (= x2 x6)) (not (= x2 x7)) (not (= x2 x8)) (not (= x2 x9))
       (not (= x3 x4)) (not (= x3 x5)) (not (= x3 x6)) (not (= x3 x7)) 
       (not (= x3 x8)) (not (= x3 x9)) (not (= x4 x5)) (not (= x4 x6)) 
       (not (= x4 x7)) (not (= x4 x8)) (not (= x4 x9)) (not (= x5 x6)) 
       (not (= x5 x7)) (not (= x5 x8)) (not (= x5 x9)) (not (= x6 x7)) 
       (not (= x6 x8)) (not (= x6 x9)) (not (= x7 x8)) (not (= x7 x9)) 
       (not (= x8 x9)) 
       (not (= ?v_10 1)) (not (= ?v_10 (- 1))) (not (= ?v_11 2)) 
       (not (= ?v_11 (- 2))) (not (= ?v_12 3)) (not (= ?v_12 (- 3))) 
       (not (= ?v_13 4)) (not (= ?v_13 (- 4))) (not (= ?v_14 5)) 
       (not (= ?v_14 (- 5))) (not (= ?v_15 6)) (not (= ?v_15 (- 6)))
       (not (= ?v_16 7)) (not (= ?v_16 (- 7))) (not (= ?v_17 8)) 
       (not (= ?v_17 (- 8))) (not (= ?v_18 9)) (not (= ?v_18 (- 9))) 
       (not (= ?v_19 1)) (not (= ?v_19 (- 1))) (not (= ?v_20 2)) 
       (not (= ?v_20 (- 2))) (not (= ?v_21 3)) (not (= ?v_21 (- 3))) 
       (not (= ?v_22 4)) (not (= ?v_22 (- 4))) (not (= ?v_23 5)) 
       (not (= ?v_23 (- 5))) (not (= ?v_24 6)) (not (= ?v_24 (- 6))) 
       (not (= ?v_25 7)) (not (= ?v_25 (- 7))) (not (= ?v_26 8)) 
       (not (= ?v_26 (- 8))) (not (= ?v_27 1)) (not (= ?v_27 (- 1))) 
       (not (= ?v_28 2)) (not (= ?v_28 (- 2))) (not (= ?v_29 3)) 
       (not (= ?v_29 (- 3))) (not (= ?v_30 4)) (not (= ?v_30 (- 4))) 
       (not (= ?v_31 5)) (not (= ?v_31 (- 5))) (not (= ?v_32 6))
       (not (= ?v_32 (- 6))) (not (= ?v_33 7)) (not (= ?v_33 (- 7))) 
       (not (= ?v_34 1)) (not (= ?v_34 (- 1))) (not (= ?v_35 2)) 
       (not (= ?v_35 (- 2))) (not (= ?v_36 3)) (not (= ?v_36 (- 3)))
       (not (= ?v_37 4)) (not (= ?v_37 (- 4))) (not (= ?v_38 5)) 
       (not (= ?v_38 (- 5))) (not (= ?v_39 6)) (not (= ?v_39 (- 6))) 
       (not (= ?v_40 1)) (not (= ?v_40 (- 1))) (not (= ?v_41 2)) 
       (not (= ?v_41 (- 2))) (not (= ?v_42 3)) (not (= ?v_42 (- 3)))
       (not (= ?v_43 4)) (not (= ?v_43 (- 4))) (not (= ?v_44 5))
       (not (= ?v_44 (- 5))) (not (= ?v_45 1)) (not (= ?v_45 (- 1))) 
       (not (= ?v_46 2)) (not (= ?v_46 (- 2))) (not (= ?v_47 3)) 
       (not (= ?v_47 (- 3))) (not (= ?v_48 4)) (not (= ?v_48 (- 4))) 
       (not (= ?v_49 1)) (not (= ?v_49 (- 1))) (not (= ?v_50 2)) 
       (not (= ?v_50 (- 2))) (not (= ?v_51 3)) (not (= ?v_51 (- 3))) 
       (not (= ?v_52 1)) (not (= ?v_52 (- 1))) (not (= ?v_53 2)) 
       (not (= ?v_53 (- 2))) (not (= ?v_54 1)) (not (= ?v_54 (- 1))))))
(check-sat)
(exit)