9r_149_solution.txt

[yunwen@paljas gift128]$ g++ gift128_rk_exact.cpp -o testas5.out
[yunwen@paljas gift128]$ ./testas5.out 9 149 > testas5.smt2
[yunwen@paljas gift128]$ export PATH=$PATH:/volume1/scratch/yunwen/aca/boolector-2.4.1-with-lingeling-bbc/boolector/bin/
[yunwen@paljas gift128]$ time boolector --hex testas5.smt2
sat
((a0_0 #x0))
((a1_0 #x6))
((a2_0 #x0))
((a3_0 #x0))
((a4_0 #x0))
((a5_0 #x0))
((a6_0 #x0))
((a7_0 #x0))
((a8_0 #x0))
((a9_0 #x0))
((a10_0 #x0))
((a11_0 #x0))
((a12_0 #x0))
((a13_0 #x0))
((a14_0 #x0))
((a15_0 #x0))
((a16_0 #x0))
((a17_0 #x0))
((a18_0 #x0))
((a19_0 #xe))
((a20_0 #x0))
((a21_0 #x0))
((a22_0 #x0))
((a23_0 #x0))
((a24_0 #x0))
((a25_0 #x0))
((a26_0 #x6))
((a27_0 #x0))
((a28_0 #x0))
((a29_0 #x0))
((a30_0 #x0))
((a31_0 #x0))
((b0_0 #x0))
((b1_0 #x2))
((b2_0 #x0))
((b3_0 #x0))
((b4_0 #x0))
((b5_0 #x0))
((b6_0 #x0))
((b7_0 #x0))
((b8_0 #x0))
((b9_0 #x0))
((b10_0 #x0))
((b11_0 #x0))
((b12_0 #x0))
((b13_0 #x0))
((b14_0 #x0))
((b15_0 #x0))
((b16_0 #x0))
((b17_0 #x0))
((b18_0 #x0))
((b19_0 #x4))
((b20_0 #x0))
((b21_0 #x0))
((b22_0 #x0))
((b23_0 #x0))
((b24_0 #x0))
((b25_0 #x0))
((b26_0 #x2))
((b27_0 #x0))
((b28_0 #x0))
((b29_0 #x0))
((b30_0 #x0))
((b31_0 #x0))
((k0_0 #x0001))
((k0_2 #x4000))
((k1_0 #x0000))
((k1_2 #x1000))
((a0_1 #x0))
((a1_1 #x0))
((a2_1 #x0))
((a3_1 #x0))
((a4_1 #x0))
((a5_1 #x0))
((a6_1 #x0))
((a7_1 #x0))
((a8_1 #x0))
((a9_1 #x0))
((a10_1 #x0))
((a11_1 #x0))
((a12_1 #x0))
((a13_1 #x0))
((a14_1 #x0))
((a15_1 #x0))
((a16_1 #x0))
((a17_1 #x0))
((a18_1 #x0))
((a19_1 #x0))
((a20_1 #x0))
((a21_1 #x0))
((a22_1 #x0))
((a23_1 #x0))
((a24_1 #x0))
((a25_1 #x0))
((a26_1 #x0))
((a27_1 #x0))
((a28_1 #x0))
((a29_1 #x0))
((a30_1 #x0))
((a31_1 #x0))
((b0_1 #x0))
((b1_1 #x0))
((b2_1 #x0))
((b3_1 #x0))
((b4_1 #x0))
((b5_1 #x0))
((b6_1 #x0))
((b7_1 #x0))
((b8_1 #x0))
((b9_1 #x0))
((b10_1 #x0))
((b11_1 #x0))
((b12_1 #x0))
((b13_1 #x0))
((b14_1 #x0))
((b15_1 #x0))
((b16_1 #x0))
((b17_1 #x0))
((b18_1 #x0))
((b19_1 #x0))
((b20_1 #x0))
((b21_1 #x0))
((b22_1 #x0))
((b23_1 #x0))
((b24_1 #x0))
((b25_1 #x0))
((b26_1 #x0))
((b27_1 #x0))
((b28_1 #x0))
((b29_1 #x0))
((b30_1 #x0))
((b31_1 #x0))
((k0_1 #x0000))
((k0_3 #x0000))
((k1_1 #x0000))
((k1_3 #x0008))
((a0_2 #x0))
((a1_2 #x0))
((a2_2 #x0))
((a3_2 #x0))
((a4_2 #x0))
((a5_2 #x0))
((a6_2 #x0))
((a7_2 #x0))
((a8_2 #x0))
((a9_2 #x0))
((a10_2 #x0))
((a11_2 #x0))
((a12_2 #x0))
((a13_2 #x0))
((a14_2 #x0))
((a15_2 #x0))
((a16_2 #x0))
((a17_2 #x0))
((a18_2 #x0))
((a19_2 #x4))
((a20_2 #x0))
((a21_2 #x0))
((a22_2 #x0))
((a23_2 #x0))
((a24_2 #x0))
((a25_2 #x0))
((a26_2 #x0))
((a27_2 #x0))
((a28_2 #x0))
((a29_2 #x0))
((a30_2 #x0))
((a31_2 #x0))
((b0_2 #x0))
((b1_2 #x0))
((b2_2 #x0))
((b3_2 #x0))
((b4_2 #x0))
((b5_2 #x0))
((b6_2 #x0))
((b7_2 #x0))
((b8_2 #x0))
((b9_2 #x0))
((b10_2 #x0))
((b11_2 #x0))
((b12_2 #x0))
((b13_2 #x0))
((b14_2 #x0))
((b15_2 #x0))
((b16_2 #x0))
((b17_2 #x0))
((b18_2 #x0))
((b19_2 #x3))
((b20_2 #x0))
((b21_2 #x0))
((b22_2 #x0))
((b23_2 #x0))
((b24_2 #x0))
((b25_2 #x0))
((b26_2 #x0))
((b27_2 #x0))
((b28_2 #x0))
((b29_2 #x0))
((b30_2 #x0))
((b31_2 #x0))
((k0_2 #x4000))
((k0_4 #x0010))
((k1_2 #x1000))
((k1_4 #x0000))
((a0_3 #x0))
((a1_3 #x0))
((a2_3 #x0))
((a3_3 #x0))
((a4_3 #x0))
((a5_3 #x0))
((a6_3 #x0))
((a7_3 #x0))
((a8_3 #x0))
((a9_3 #x0))
((a10_3 #x0))
((a11_3 #x0))
((a12_3 #x5))
((a13_3 #x0))
((a14_3 #x2))
((a15_3 #x0))
((a16_3 #x0))
((a17_3 #x0))
((a18_3 #x0))
((a19_3 #x0))
((a20_3 #x0))
((a21_3 #x0))
((a22_3 #x0))
((a23_3 #x0))
((a24_3 #x0))
((a25_3 #x0))
((a26_3 #x0))
((a27_3 #x0))
((a28_3 #x0))
((a29_3 #x0))
((a30_3 #x0))
((a31_3 #x0))
((b0_3 #x0))
((b1_3 #x0))
((b2_3 #x0))
((b3_3 #x0))
((b4_3 #x0))
((b5_3 #x0))
((b6_3 #x0))
((b7_3 #x0))
((b8_3 #x0))
((b9_3 #x0))
((b10_3 #x0))
((b11_3 #x0))
((b12_3 #x2))
((b13_3 #x0))
((b14_3 #x5))
((b15_3 #x0))
((b16_3 #x0))
((b17_3 #x0))
((b18_3 #x0))
((b19_3 #x0))
((b20_3 #x0))
((b21_3 #x0))
((b22_3 #x0))
((b23_3 #x0))
((b24_3 #x0))
((b25_3 #x0))
((b26_3 #x0))
((b27_3 #x0))
((b28_3 #x0))
((b29_3 #x0))
((b30_3 #x0))
((b31_3 #x0))
((k0_3 #x0000))
((k0_5 #x0000))
((k1_3 #x0008))
((k1_5 #x0000))
((a0_4 #x0))
((a1_4 #x0))
((a2_4 #x0))
((a3_4 #x0))
((a4_4 #x0))
((a5_4 #x0))
((a6_4 #x0))
((a7_4 #x0))
((a8_4 #x0))
((a9_4 #x0))
((a10_4 #x0))
((a11_4 #x2))
((a12_4 #x0))
((a13_4 #x0))
((a14_4 #x0))
((a15_4 #x0))
((a16_4 #x0))
((a17_4 #x0))
((a18_4 #x0))
((a19_4 #x1))
((a20_4 #x0))
((a21_4 #x0))
((a22_4 #x0))
((a23_4 #x0))
((a24_4 #x0))
((a25_4 #x0))
((a26_4 #x0))
((a27_4 #x0))
((a28_4 #x0))
((a29_4 #x0))
((a30_4 #x0))
((a31_4 #x0))
((b0_4 #x0))
((b1_4 #x0))
((b2_4 #x0))
((b3_4 #x0))
((b4_4 #x0))
((b5_4 #x0))
((b6_4 #x0))
((b7_4 #x0))
((b8_4 #x0))
((b9_4 #x0))
((b10_4 #x0))
((b11_4 #x6))
((b12_4 #x0))
((b13_4 #x0))
((b14_4 #x0))
((b15_4 #x0))
((b16_4 #x0))
((b17_4 #x0))
((b18_4 #x0))
((b19_4 #x8))
((b20_4 #x0))
((b21_4 #x0))
((b22_4 #x0))
((b23_4 #x0))
((b24_4 #x0))
((b25_4 #x0))
((b26_4 #x0))
((b27_4 #x0))
((b28_4 #x0))
((b29_4 #x0))
((b30_4 #x0))
((b31_4 #x0))
((k0_4 #x0010))
((k0_6 #x0004))
((k1_4 #x0000))
((k1_6 #x0400))
((a0_5 #x0))
((a1_5 #x0))
((a2_5 #x0))
((a3_5 #x0))
((a4_5 #xa))
((a5_5 #x0))
((a6_5 #x0))
((a7_5 #x0))
((a8_5 #x0))
((a9_5 #x0))
((a10_5 #x0))
((a11_5 #x0))
((a12_5 #x0))
((a13_5 #x0))
((a14_5 #x0))
((a15_5 #x0))
((a16_5 #x0))
((a17_5 #x0))
((a18_5 #x0))
((a19_5 #x0))
((a20_5 #x0))
((a21_5 #x0))
((a22_5 #x0))
((a23_5 #x0))
((a24_5 #x0))
((a25_5 #x0))
((a26_5 #x0))
((a27_5 #x0))
((a28_5 #x0))
((a29_5 #x0))
((a30_5 #x0))
((a31_5 #x0))
((b0_5 #x0))
((b1_5 #x0))
((b2_5 #x0))
((b3_5 #x0))
((b4_5 #x6))
((b5_5 #x0))
((b6_5 #x0))
((b7_5 #x0))
((b8_5 #x0))
((b9_5 #x0))
((b10_5 #x0))
((b11_5 #x0))
((b12_5 #x0))
((b13_5 #x0))
((b14_5 #x0))
((b15_5 #x0))
((b16_5 #x0))
((b17_5 #x0))
((b18_5 #x0))
((b19_5 #x0))
((b20_5 #x0))
((b21_5 #x0))
((b22_5 #x0))
((b23_5 #x0))
((b24_5 #x0))
((b25_5 #x0))
((b26_5 #x0))
((b27_5 #x0))
((b28_5 #x0))
((b29_5 #x0))
((b30_5 #x0))
((b31_5 #x0))
((k0_5 #x0000))
((k0_7 #x0000))
((k1_5 #x0000))
((k1_7 #x0002))
((a0_6 #x0))
((a1_6 #x0))
((a2_6 #x0))
((a3_6 #x0))
((a4_6 #x0))
((a5_6 #x0))
((a6_6 #x0))
((a7_6 #x0))
((a8_6 #x0))
((a9_6 #x2))
((a10_6 #x0))
((a11_6 #x0))
((a12_6 #x0))
((a13_6 #x0))
((a14_6 #x0))
((a15_6 #x0))
((a16_6 #x0))
((a17_6 #x0))
((a18_6 #x0))
((a19_6 #x0))
((a20_6 #x0))
((a21_6 #x0))
((a22_6 #x0))
((a23_6 #x0))
((a24_6 #x0))
((a25_6 #x0))
((a26_6 #x0))
((a27_6 #x0))
((a28_6 #x0))
((a29_6 #x0))
((a30_6 #x0))
((a31_6 #x0))
((b0_6 #x0))
((b1_6 #x0))
((b2_6 #x0))
((b3_6 #x0))
((b4_6 #x0))
((b5_6 #x0))
((b6_6 #x0))
((b7_6 #x0))
((b8_6 #x0))
((b9_6 #x6))
((b10_6 #x0))
((b11_6 #x0))
((b12_6 #x0))
((b13_6 #x0))
((b14_6 #x0))
((b15_6 #x0))
((b16_6 #x0))
((b17_6 #x0))
((b18_6 #x0))
((b19_6 #x0))
((b20_6 #x0))
((b21_6 #x0))
((b22_6 #x0))
((b23_6 #x0))
((b24_6 #x0))
((b25_6 #x0))
((b26_6 #x0))
((b27_6 #x0))
((b28_6 #x0))
((b29_6 #x0))
((b30_6 #x0))
((b31_6 #x0))
((k0_6 #x0004))
((k0_8 #x0100))
((k1_6 #x0400))
((k1_8 #x0000))
((a0_7 #x0))
((a1_7 #x0))
((a2_7 #x0))
((a3_7 #x0))
((a4_7 #x0))
((a5_7 #x0))
((a6_7 #x0))
((a7_7 #x0))
((a8_7 #x0))
((a9_7 #x0))
((a10_7 #x0))
((a11_7 #x0))
((a12_7 #x0))
((a13_7 #x0))
((a14_7 #x0))
((a15_7 #x0))
((a16_7 #x0))
((a17_7 #x0))
((a18_7 #x0))
((a19_7 #x0))
((a20_7 #x0))
((a21_7 #x0))
((a22_7 #x0))
((a23_7 #x0))
((a24_7 #x2))
((a25_7 #x0))
((a26_7 #x0))
((a27_7 #x0))
((a28_7 #x0))
((a29_7 #x0))
((a30_7 #x0))
((a31_7 #x0))
((b0_7 #x0))
((b1_7 #x0))
((b2_7 #x0))
((b3_7 #x0))
((b4_7 #x0))
((b5_7 #x0))
((b6_7 #x0))
((b7_7 #x0))
((b8_7 #x0))
((b9_7 #x0))
((b10_7 #x0))
((b11_7 #x0))
((b12_7 #x0))
((b13_7 #x0))
((b14_7 #x0))
((b15_7 #x0))
((b16_7 #x0))
((b17_7 #x0))
((b18_7 #x0))
((b19_7 #x0))
((b20_7 #x0))
((b21_7 #x0))
((b22_7 #x0))
((b23_7 #x0))
((b24_7 #x6))
((b25_7 #x0))
((b26_7 #x0))
((b27_7 #x0))
((b28_7 #x0))
((b29_7 #x0))
((b30_7 #x0))
((b31_7 #x0))
((k0_7 #x0000))
((k0_9 #x0000))
((k1_7 #x0002))
((k1_9 #x0000))
((a0_8 #x0))
((a1_8 #x4))
((a2_8 #x0))
((a3_8 #x0))
((a4_8 #x0))
((a5_8 #x0))
((a6_8 #x0))
((a7_8 #x0))
((a8_8 #x0))
((a9_8 #x0))
((a10_8 #x0))
((a11_8 #x0))
((a12_8 #x0))
((a13_8 #x0))
((a14_8 #x2))
((a15_8 #x0))
((a16_8 #x0))
((a17_8 #x0))
((a18_8 #x0))
((a19_8 #x0))
((a20_8 #x0))
((a21_8 #x0))
((a22_8 #x4))
((a23_8 #x0))
((a24_8 #x0))
((a25_8 #x0))
((a26_8 #x0))
((a27_8 #x0))
((a28_8 #x0))
((a29_8 #x0))
((a30_8 #x0))
((a31_8 #x0))
((b0_8 #x0))
((b1_8 #x7))
((b2_8 #x0))
((b3_8 #x0))
((b4_8 #x0))
((b5_8 #x0))
((b6_8 #x0))
((b7_8 #x0))
((b8_8 #x0))
((b9_8 #x0))
((b10_8 #x0))
((b11_8 #x0))
((b12_8 #x0))
((b13_8 #x0))
((b14_8 #x5))
((b15_8 #x0))
((b16_8 #x0))
((b17_8 #x0))
((b18_8 #x0))
((b19_8 #x0))
((b20_8 #x0))
((b21_8 #x0))
((b22_8 #x7))
((b23_8 #x0))
((b24_8 #x0))
((b25_8 #x0))
((b26_8 #x0))
((b27_8 #x0))
((b28_8 #x0))
((b29_8 #x0))
((b30_8 #x0))
((b31_8 #x0))
((k0_8 #x0100))
((k0_10 #x0040))
((k1_8 #x0000))
((k1_10 #x0100))
((a0_9 #x2))
((a1_9 #x0))
((a2_9 #x0))
((a3_9 #x4))
((a4_9 #x0))
((a5_9 #x4))
((a6_9 #x0))
((a7_9 #x0))
((a8_9 #x6))
((a9_9 #x0))
((a10_9 #x0))
((a11_9 #x0))
((a12_9 #x0))
((a13_9 #x0))
((a14_9 #x0))
((a15_9 #x0))
((a16_9 #x0))
((a17_9 #x0))
((a18_9 #x0))
((a19_9 #x1))
((a20_9 #x0))
((a21_9 #x1))
((a22_9 #x2))
((a23_9 #x0))
((a24_9 #x5))
((a25_9 #x0))
((a26_9 #x0))
((a27_9 #x0))
((a28_9 #x0))
((a29_9 #x2))
((a30_9 #x0))
((a31_9 #x0))
((weight1 #x0009))
((weight2 #x0003))
((weight3 #x0002))

real	4128m14.858s
user	4124m39.333s
sys	0m50.328s
[yunwen@paljas gift128]$