mirror of
https://github.com/KevinMidboe/linguist.git
synced 2025-10-29 17:50:22 +00:00
124 lines
4.8 KiB
Plaintext
124 lines
4.8 KiB
Plaintext
(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)
|