% b_3_7_343

:- declare(3, 7).

false :- a_1_6, a_2_7, a_3_7.
false :- a_1_5, a_2_7, a_3_7.
false :- a_1_4, a_2_7, a_3_7.
false :- a_1_3, a_2_7, a_3_7.
false :- a_1_2, a_2_7, a_3_7.
false :- a_1_1, a_2_7, a_3_7.
false :- a_1_7, a_2_6, a_3_7.
false :- a_1_6, a_2_6, a_3_7.
false :- a_1_5, a_2_6, a_3_7.
false :- a_1_4, a_2_6, a_3_7.
false :- a_1_3, a_2_6, a_3_7.
false :- a_1_2, a_2_6, a_3_7.
false :- a_1_1, a_2_6, a_3_7.
false :- a_1_7, a_2_5, a_3_7.
false :- a_1_6, a_2_5, a_3_7.
false :- a_1_5, a_2_5, a_3_7.
false :- a_1_4, a_2_5, a_3_7.
false :- a_1_3, a_2_5, a_3_7.
false :- a_1_2, a_2_5, a_3_7.
false :- a_1_1, a_2_5, a_3_7.
false :- a_1_7, a_2_4, a_3_7.
false :- a_1_6, a_2_4, a_3_7.
false :- a_1_5, a_2_4, a_3_7.
false :- a_1_4, a_2_4, a_3_7.
false :- a_1_3, a_2_4, a_3_7.
false :- a_1_2, a_2_4, a_3_7.
false :- a_1_1, a_2_4, a_3_7.
false :- a_1_7, a_2_3, a_3_7.
false :- a_1_6, a_2_3, a_3_7.
false :- a_1_5, a_2_3, a_3_7.
false :- a_1_4, a_2_3, a_3_7.
false :- a_1_3, a_2_3, a_3_7.
false :- a_1_2, a_2_3, a_3_7.
false :- a_1_1, a_2_3, a_3_7.
false :- a_1_7, a_2_2, a_3_7.
false :- a_1_6, a_2_2, a_3_7.
false :- a_1_5, a_2_2, a_3_7.
false :- a_1_4, a_2_2, a_3_7.
false :- a_1_3, a_2_2, a_3_7.
false :- a_1_2, a_2_2, a_3_7.
false :- a_1_1, a_2_2, a_3_7.
false :- a_1_7, a_2_1, a_3_7.
false :- a_1_6, a_2_1, a_3_7.
false :- a_1_5, a_2_1, a_3_7.
false :- a_1_4, a_2_1, a_3_7.
false :- a_1_3, a_2_1, a_3_7.
false :- a_1_2, a_2_1, a_3_7.
false :- a_1_1, a_2_1, a_3_7.
false :- a_1_7, a_2_7, a_3_6.
false :- a_1_6, a_2_7, a_3_6.
false :- a_1_5, a_2_7, a_3_6.
false :- a_1_4, a_2_7, a_3_6.
false :- a_1_3, a_2_7, a_3_6.
false :- a_1_2, a_2_7, a_3_6.
false :- a_1_1, a_2_7, a_3_6.
false :- a_1_7, a_2_6, a_3_6.
false :- a_1_6, a_2_6, a_3_6.
false :- a_1_5, a_2_6, a_3_6.
false :- a_1_4, a_2_6, a_3_6.
false :- a_1_3, a_2_6, a_3_6.
false :- a_1_2, a_2_6, a_3_6.
false :- a_1_1, a_2_6, a_3_6.
false :- a_1_7, a_2_5, a_3_6.
false :- a_1_6, a_2_5, a_3_6.
false :- a_1_5, a_2_5, a_3_6.
false :- a_1_4, a_2_5, a_3_6.
false :- a_1_3, a_2_5, a_3_6.
false :- a_1_2, a_2_5, a_3_6.
false :- a_1_1, a_2_5, a_3_6.
false :- a_1_7, a_2_4, a_3_6.
false :- a_1_6, a_2_4, a_3_6.
false :- a_1_5, a_2_4, a_3_6.
false :- a_1_4, a_2_4, a_3_6.
false :- a_1_3, a_2_4, a_3_6.
false :- a_1_2, a_2_4, a_3_6.
false :- a_1_1, a_2_4, a_3_6.
false :- a_1_7, a_2_3, a_3_6.
false :- a_1_6, a_2_3, a_3_6.
false :- a_1_5, a_2_3, a_3_6.
false :- a_1_4, a_2_3, a_3_6.
false :- a_1_3, a_2_3, a_3_6.
false :- a_1_2, a_2_3, a_3_6.
false :- a_1_1, a_2_3, a_3_6.
false :- a_1_7, a_2_2, a_3_6.
false :- a_1_6, a_2_2, a_3_6.
false :- a_1_5, a_2_2, a_3_6.
false :- a_1_4, a_2_2, a_3_6.
false :- a_1_3, a_2_2, a_3_6.
false :- a_1_2, a_2_2, a_3_6.
false :- a_1_1, a_2_2, a_3_6.
false :- a_1_7, a_2_1, a_3_6.
false :- a_1_6, a_2_1, a_3_6.
false :- a_1_5, a_2_1, a_3_6.
false :- a_1_4, a_2_1, a_3_6.
false :- a_1_3, a_2_1, a_3_6.
false :- a_1_2, a_2_1, a_3_6.
false :- a_1_1, a_2_1, a_3_6.
false :- a_1_7, a_2_7, a_3_5.
false :- a_1_6, a_2_7, a_3_5.
false :- a_1_5, a_2_7, a_3_5.
false :- a_1_4, a_2_7, a_3_5.
false :- a_1_3, a_2_7, a_3_5.
false :- a_1_2, a_2_7, a_3_5.
false :- a_1_1, a_2_7, a_3_5.
false :- a_1_7, a_2_6, a_3_5.
false :- a_1_6, a_2_6, a_3_5.
false :- a_1_5, a_2_6, a_3_5.
false :- a_1_4, a_2_6, a_3_5.
false :- a_1_3, a_2_6, a_3_5.
false :- a_1_2, a_2_6, a_3_5.
false :- a_1_1, a_2_6, a_3_5.
false :- a_1_7, a_2_5, a_3_5.
false :- a_1_6, a_2_5, a_3_5.
false :- a_1_5, a_2_5, a_3_5.
false :- a_1_4, a_2_5, a_3_5.
false :- a_1_3, a_2_5, a_3_5.
false :- a_1_2, a_2_5, a_3_5.
false :- a_1_1, a_2_5, a_3_5.
false :- a_1_7, a_2_4, a_3_5.
false :- a_1_6, a_2_4, a_3_5.
false :- a_1_5, a_2_4, a_3_5.
false :- a_1_4, a_2_4, a_3_5.
false :- a_1_3, a_2_4, a_3_5.
false :- a_1_2, a_2_4, a_3_5.
false :- a_1_1, a_2_4, a_3_5.
false :- a_1_7, a_2_3, a_3_5.
false :- a_1_6, a_2_3, a_3_5.
false :- a_1_5, a_2_3, a_3_5.
false :- a_1_4, a_2_3, a_3_5.
false :- a_1_3, a_2_3, a_3_5.
false :- a_1_2, a_2_3, a_3_5.
false :- a_1_1, a_2_3, a_3_5.
false :- a_1_7, a_2_2, a_3_5.
false :- a_1_6, a_2_2, a_3_5.
false :- a_1_5, a_2_2, a_3_5.
false :- a_1_4, a_2_2, a_3_5.
false :- a_1_3, a_2_2, a_3_5.
false :- a_1_2, a_2_2, a_3_5.
false :- a_1_1, a_2_2, a_3_5.
false :- a_1_7, a_2_1, a_3_5.
false :- a_1_6, a_2_1, a_3_5.
false :- a_1_5, a_2_1, a_3_5.
false :- a_1_4, a_2_1, a_3_5.
false :- a_1_3, a_2_1, a_3_5.
false :- a_1_2, a_2_1, a_3_5.
false :- a_1_1, a_2_1, a_3_5.
false :- a_1_7, a_2_7, a_3_4.
false :- a_1_6, a_2_7, a_3_4.
false :- a_1_5, a_2_7, a_3_4.
false :- a_1_4, a_2_7, a_3_4.
false :- a_1_3, a_2_7, a_3_4.
false :- a_1_2, a_2_7, a_3_4.
false :- a_1_1, a_2_7, a_3_4.
false :- a_1_7, a_2_6, a_3_4.
false :- a_1_6, a_2_6, a_3_4.
false :- a_1_5, a_2_6, a_3_4.
false :- a_1_4, a_2_6, a_3_4.
false :- a_1_3, a_2_6, a_3_4.
false :- a_1_2, a_2_6, a_3_4.
false :- a_1_1, a_2_6, a_3_4.
false :- a_1_7, a_2_5, a_3_4.
false :- a_1_6, a_2_5, a_3_4.
false :- a_1_5, a_2_5, a_3_4.
false :- a_1_4, a_2_5, a_3_4.
false :- a_1_3, a_2_5, a_3_4.
false :- a_1_2, a_2_5, a_3_4.
false :- a_1_1, a_2_5, a_3_4.
false :- a_1_7, a_2_4, a_3_4.
false :- a_1_6, a_2_4, a_3_4.
false :- a_1_5, a_2_4, a_3_4.
false :- a_1_4, a_2_4, a_3_4.
false :- a_1_3, a_2_4, a_3_4.
false :- a_1_2, a_2_4, a_3_4.
false :- a_1_1, a_2_4, a_3_4.
false :- a_1_7, a_2_3, a_3_4.
false :- a_1_6, a_2_3, a_3_4.
false :- a_1_5, a_2_3, a_3_4.
false :- a_1_4, a_2_3, a_3_4.
false :- a_1_3, a_2_3, a_3_4.
false :- a_1_2, a_2_3, a_3_4.
false :- a_1_1, a_2_3, a_3_4.
false :- a_1_7, a_2_2, a_3_4.
false :- a_1_6, a_2_2, a_3_4.
false :- a_1_5, a_2_2, a_3_4.
false :- a_1_4, a_2_2, a_3_4.
false :- a_1_3, a_2_2, a_3_4.
false :- a_1_2, a_2_2, a_3_4.
false :- a_1_1, a_2_2, a_3_4.
false :- a_1_7, a_2_1, a_3_4.
false :- a_1_6, a_2_1, a_3_4.
false :- a_1_5, a_2_1, a_3_4.
false :- a_1_4, a_2_1, a_3_4.
false :- a_1_3, a_2_1, a_3_4.
false :- a_1_2, a_2_1, a_3_4.
false :- a_1_1, a_2_1, a_3_4.
false :- a_1_7, a_2_7, a_3_3.
false :- a_1_6, a_2_7, a_3_3.
false :- a_1_5, a_2_7, a_3_3.
false :- a_1_4, a_2_7, a_3_3.
false :- a_1_3, a_2_7, a_3_3.
false :- a_1_2, a_2_7, a_3_3.
false :- a_1_1, a_2_7, a_3_3.
false :- a_1_7, a_2_6, a_3_3.
false :- a_1_6, a_2_6, a_3_3.
false :- a_1_5, a_2_6, a_3_3.
false :- a_1_4, a_2_6, a_3_3.
false :- a_1_3, a_2_6, a_3_3.
false :- a_1_2, a_2_6, a_3_3.
false :- a_1_1, a_2_6, a_3_3.
false :- a_1_7, a_2_5, a_3_3.
false :- a_1_6, a_2_5, a_3_3.
false :- a_1_5, a_2_5, a_3_3.
false :- a_1_4, a_2_5, a_3_3.
false :- a_1_3, a_2_5, a_3_3.
false :- a_1_2, a_2_5, a_3_3.
false :- a_1_1, a_2_5, a_3_3.
false :- a_1_7, a_2_4, a_3_3.
false :- a_1_6, a_2_4, a_3_3.
false :- a_1_5, a_2_4, a_3_3.
false :- a_1_4, a_2_4, a_3_3.
false :- a_1_3, a_2_4, a_3_3.
false :- a_1_2, a_2_4, a_3_3.
false :- a_1_1, a_2_4, a_3_3.
false :- a_1_7, a_2_3, a_3_3.
false :- a_1_6, a_2_3, a_3_3.
false :- a_1_5, a_2_3, a_3_3.
false :- a_1_4, a_2_3, a_3_3.
false :- a_1_3, a_2_3, a_3_3.
false :- a_1_2, a_2_3, a_3_3.
false :- a_1_1, a_2_3, a_3_3.
false :- a_1_7, a_2_2, a_3_3.
false :- a_1_6, a_2_2, a_3_3.
false :- a_1_5, a_2_2, a_3_3.
false :- a_1_4, a_2_2, a_3_3.
false :- a_1_3, a_2_2, a_3_3.
false :- a_1_2, a_2_2, a_3_3.
false :- a_1_1, a_2_2, a_3_3.
false :- a_1_7, a_2_1, a_3_3.
false :- a_1_6, a_2_1, a_3_3.
false :- a_1_5, a_2_1, a_3_3.
false :- a_1_4, a_2_1, a_3_3.
false :- a_1_3, a_2_1, a_3_3.
false :- a_1_2, a_2_1, a_3_3.
false :- a_1_1, a_2_1, a_3_3.
false :- a_1_7, a_2_7, a_3_2.
false :- a_1_6, a_2_7, a_3_2.
false :- a_1_5, a_2_7, a_3_2.
false :- a_1_4, a_2_7, a_3_2.
false :- a_1_3, a_2_7, a_3_2.
false :- a_1_2, a_2_7, a_3_2.
false :- a_1_1, a_2_7, a_3_2.
false :- a_1_7, a_2_6, a_3_2.
false :- a_1_6, a_2_6, a_3_2.
false :- a_1_5, a_2_6, a_3_2.
false :- a_1_4, a_2_6, a_3_2.
false :- a_1_3, a_2_6, a_3_2.
false :- a_1_2, a_2_6, a_3_2.
false :- a_1_1, a_2_6, a_3_2.
false :- a_1_7, a_2_5, a_3_2.
false :- a_1_6, a_2_5, a_3_2.
false :- a_1_5, a_2_5, a_3_2.
false :- a_1_4, a_2_5, a_3_2.
false :- a_1_3, a_2_5, a_3_2.
false :- a_1_2, a_2_5, a_3_2.
false :- a_1_1, a_2_5, a_3_2.
false :- a_1_7, a_2_4, a_3_2.
false :- a_1_6, a_2_4, a_3_2.
false :- a_1_5, a_2_4, a_3_2.
false :- a_1_4, a_2_4, a_3_2.
false :- a_1_3, a_2_4, a_3_2.
false :- a_1_2, a_2_4, a_3_2.
false :- a_1_1, a_2_4, a_3_2.
false :- a_1_7, a_2_3, a_3_2.
false :- a_1_6, a_2_3, a_3_2.
false :- a_1_5, a_2_3, a_3_2.
false :- a_1_4, a_2_3, a_3_2.
false :- a_1_3, a_2_3, a_3_2.
false :- a_1_2, a_2_3, a_3_2.
false :- a_1_1, a_2_3, a_3_2.
false :- a_1_7, a_2_2, a_3_2.
false :- a_1_6, a_2_2, a_3_2.
false :- a_1_5, a_2_2, a_3_2.
false :- a_1_4, a_2_2, a_3_2.
false :- a_1_3, a_2_2, a_3_2.
false :- a_1_2, a_2_2, a_3_2.
false :- a_1_1, a_2_2, a_3_2.
false :- a_1_7, a_2_1, a_3_2.
false :- a_1_6, a_2_1, a_3_2.
false :- a_1_5, a_2_1, a_3_2.
false :- a_1_4, a_2_1, a_3_2.
false :- a_1_3, a_2_1, a_3_2.
false :- a_1_2, a_2_1, a_3_2.
false :- a_1_1, a_2_1, a_3_2.
false :- a_1_7, a_2_7, a_3_1.
false :- a_1_6, a_2_7, a_3_1.
false :- a_1_5, a_2_7, a_3_1.
false :- a_1_4, a_2_7, a_3_1.
false :- a_1_3, a_2_7, a_3_1.
false :- a_1_2, a_2_7, a_3_1.
false :- a_1_1, a_2_7, a_3_1.
false :- a_1_7, a_2_6, a_3_1.
false :- a_1_6, a_2_6, a_3_1.
false :- a_1_5, a_2_6, a_3_1.
false :- a_1_4, a_2_6, a_3_1.
false :- a_1_3, a_2_6, a_3_1.
false :- a_1_2, a_2_6, a_3_1.
false :- a_1_1, a_2_6, a_3_1.
false :- a_1_7, a_2_5, a_3_1.
false :- a_1_6, a_2_5, a_3_1.
false :- a_1_5, a_2_5, a_3_1.
false :- a_1_4, a_2_5, a_3_1.
false :- a_1_3, a_2_5, a_3_1.
false :- a_1_2, a_2_5, a_3_1.
false :- a_1_1, a_2_5, a_3_1.
false :- a_1_7, a_2_4, a_3_1.
false :- a_1_6, a_2_4, a_3_1.
false :- a_1_5, a_2_4, a_3_1.
false :- a_1_4, a_2_4, a_3_1.
false :- a_1_3, a_2_4, a_3_1.
false :- a_1_2, a_2_4, a_3_1.
false :- a_1_1, a_2_4, a_3_1.
false :- a_1_7, a_2_3, a_3_1.
false :- a_1_6, a_2_3, a_3_1.
false :- a_1_5, a_2_3, a_3_1.
false :- a_1_4, a_2_3, a_3_1.
false :- a_1_3, a_2_3, a_3_1.
false :- a_1_2, a_2_3, a_3_1.
false :- a_1_1, a_2_3, a_3_1.
false :- a_1_7, a_2_2, a_3_1.
false :- a_1_6, a_2_2, a_3_1.
false :- a_1_5, a_2_2, a_3_1.
false :- a_1_4, a_2_2, a_3_1.
false :- a_1_3, a_2_2, a_3_1.
false :- a_1_2, a_2_2, a_3_1.
false :- a_1_1, a_2_2, a_3_1.
false :- a_1_7, a_2_1, a_3_1.
false :- a_1_6, a_2_1, a_3_1.
false :- a_1_5, a_2_1, a_3_1.
false :- a_1_4, a_2_1, a_3_1.
false :- a_1_3, a_2_1, a_3_1.
false :- a_1_2, a_2_1, a_3_1.
false :- a_1_1, a_2_1, a_3_1.
true ---> a_3_1 ; a_3_2 ; a_3_3 ; a_3_4 ; a_3_5 ; a_3_6 ; a_3_7.
true ---> a_2_1 ; a_2_2 ; a_2_3 ; a_2_4 ; a_2_5 ; a_2_6 ; a_2_7.
true ---> a_1_1 ; a_1_2 ; a_1_3 ; a_1_4 ; a_1_5 ; a_1_6 ; a_1_7.