/* SAT, the Satisfiability Problem                           */
/* Translated from the GLPK example sat.mod, by Neng-Fa Zhou */

go:-
    Vars=[X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12,X13,X14,X15,X16,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28,X29,X30,X31,X32,X33,X34,X35,X36,X37,X38,X39,X40,X41,X42],

    Slats=[Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9,Y10,Y11,Y12,Y13,Y14,Y15,Y16,Y17,Y18,Y19,Y20,Y21,Y22,Y23,Y24,Y25,Y26,Y27,Y28,Y29,Y30,Y31,Y32,Y33,Y34,Y35,Y36,Y37,Y38,Y39,Y40,Y41,Y42,Y43,Y44,Y45,Y46,Y47,Y48,Y49,Y50,Y51,Y52,Y53,Y54,Y55,Y56,Y57,Y58,Y59,Y60,Y61,Y62,Y63,Y64,Y65,Y66,Y67,Y68,Y69,Y70,Y71,Y72,Y73,Y74,Y75,Y76,Y77,Y78,Y79,Y80,Y81,Y82,Y83,Y84,Y85,Y86,Y87,Y88,Y89,Y90,Y91,Y92,Y93,Y94,Y95,Y96,Y97,Y98,Y99,Y100,Y101,Y102,Y103,Y104,Y105,Y106,Y107,Y108,Y109,Y110,Y111,Y112,Y113,Y114,Y115,Y116,Y117,Y118,Y119,Y120,Y121,Y122,Y123,Y124,Y125,Y126,Y127,Y128,Y129,Y130,Y131,Y132,Y133],
    lp_integers(Vars),
    lp_integers(Slats),

    lp_domain(Vars,0,1),
    lp_domain(Slats,0,1),

    1-X1+1-X7  + Y1 $>= 1,
    1-X1 + 1-X13  + Y2 $>= 1,
    1-X1 + 1-X19 + Y3 $>=1,
    1-X1 + 1-X25 + Y4 $>=1,
    1-X1 + 1-X31 + Y5 $>=1,
    1-X1 + 1-X37 + Y6 $>=1,
    1-X7 + 1-X13 + Y7 $>=1,
    1-X7 + 1-X19 + Y8 $>=1,
    1-X7 + 1-X25 + Y9 $>=1,
    1-X7 + 1-X31 + Y10 $>=1,
    1-X7 + 1-X37 + Y11 $>=1,
    1-X13 + 1-X19 + Y12 $>=1,
    1-X13 + 1-X25 + Y13 $>=1,
    1-X13 + 1-X31 + Y14 $>=1,
    1-X13 + 1-X37 + Y15 $>=1,
    1-X19 + 1-X25 + Y16 $>=1,
    1-X19 + 1-X31 + Y17 $>=1,
    1-X19 + 1-X37 + Y18 $>=1,
    1-X25 + 1-X31 + Y19 $>=1,
    1-X25 + 1-X37 + Y20 $>=1,
    1-X31 + 1-X37 + Y21 $>=1,
    1-X2 + 1-X8 + Y22 $>=1,
    1-X2 + 1-X14 + Y23 $>=1,
    1-X2 + 1-X20 + Y24 $>=1,
    1-X2 + 1-X26 + Y25 $>=1,
    1-X2 + 1-X32 + Y26 $>=1,
    1-X2 + 1-X38 + Y27 $>=1,
    1-X8 + 1-X14 + Y28 $>=1,
    1-X8 + 1-X20 + Y29 $>=1,
    1-X8 + 1-X26 + Y30 $>=1,
    1-X8 + 1-X32 + Y31 $>=1,
    1-X8 + 1-X38 + Y32 $>=1,
    1-X14 + 1-X20 + Y33 $>=1,
    1-X14 + 1-X26 + Y34 $>=1,
    1-X14 + 1-X32 + Y35 $>=1,
    1-X14 + 1-X38 + Y36 $>=1,
    1-X20 + 1-X26 + Y37 $>=1,
    1-X20 + 1-X32 + Y38 $>=1,
    1-X20 + 1-X38 + Y39 $>=1,
    1-X26 + 1-X32 + Y40 $>=1,
    1-X26 + 1-X38 + Y41 $>=1,
    1-X32 + 1-X38 + Y42 $>=1,
    1-X3 + 1-X9 + Y43 $>=1,
    1-X3 + 1-X15 + Y44 $>=1,
    1-X3 + 1-X21 + Y45 $>=1,
    1-X3 + 1-X27 + Y46 $>=1,
    1-X3 + 1-X33 + Y47 $>=1,
    1-X3 + 1-X39 + Y48 $>=1,
    1-X9 + 1-X15 + Y49 $>=1,
    1-X9 + 1-X21 + Y50 $>=1,
    1-X9 + 1-X27 + Y51 $>=1,
    1-X9 + 1-X33 + Y52 $>=1,
    1-X9 + 1-X39 + Y53 $>=1,
    1-X15 + 1-X21 + Y54 $>=1,
    1-X15 + 1-X27 + Y55 $>=1,
    1-X15 + 1-X33 + Y56 $>=1,
    1-X15 + 1-X39 + Y57 $>=1,
    1-X21 + 1-X27 + Y58 $>=1,
    1-X21 + 1-X33 + Y59 $>=1,
    1-X21 + 1-X39 + Y60 $>=1,
    1-X27 + 1-X33 + Y61 $>=1,
    1-X27 + 1-X39 + Y62 $>=1,
    1-X33 + 1-X39 + Y63 $>=1, 
    1-X4 + 1-X10 + Y64 $>=1,
    1-X4 + 1-X16 + Y65 $>=1,
    1-X4 + 1-X22 + Y66 $>=1, 
    1-X4 + 1-X28 + Y67 $>=1,
    1-X4 + 1-X34 + Y68 $>=1,
    1-X4 + 1-X40 + Y69 $>=1,
    1-X10 + 1-X16 + Y70 $>=1,
    1-X10 + 1-X22 + Y71 $>=1,
    1-X10 + 1-X28 + Y72 $>=1,
    1-X10 + 1-X34 + Y73 $>=1,
    1-X10 + 1-X40 + Y74 $>=1,
    1-X16 + 1-X22 + Y75 $>=1,
    1-X16 + 1-X28 + Y76 $>=1,
    1-X16 + 1-X34 + Y77 $>=1,
    1-X16 + 1-X40 + Y78 $>=1,
    1-X22 + 1-X28 + Y79 $>=1,
    1-X22 + 1-X34 + Y80 $>=1,
    1-X22 + 1-X40 + Y81 $>=1,
    1-X28 + 1-X34 + Y82 $>=1,
    1-X28 + 1-X40 + Y83 $>=1,
    1-X34 + 1-X40 + Y84 $>=1,
    1-X5 + 1-X11 + Y85 $>=1,
    1-X5 + 1-X17 + Y86 $>=1,
    1-X5 + 1-X23 + Y87 $>=1,
    1-X5 + 1-X29 + Y88 $>=1,
    1-X5 + 1-X35 + Y89 $>=1,
    1-X5 + 1-X41 + Y90 $>=1,
    1-X11 + 1-X17 + Y91 $>=1,
    1-X11 + 1-X23 + Y92 $>=1,
    1-X11 + 1-X29 + Y93 $>=1,
    1-X11 + 1-X35 + Y94 $>=1,
    1-X11 + 1-X41 + Y95 $>=1,
    1-X17 + 1-X23 + Y96 $>=1,
    1-X17 + 1-X29 + Y97 $>=1,
    1-X17 + 1-X35 + Y98 $>=1,
    1-X17 + 1-X41 + Y99 $>=1,
    1-X23 + 1-X29 + Y100 $>=1,
    1-X23 + 1-X35 + Y101 $>=1,
    1-X23 + 1-X41 + Y102 $>=1,
    1-X29 + 1-X35 + Y103 $>=1,
    1-X29 + 1-X41 + Y104 $>=1,
    1-X35 + 1-X41 + Y105 $>=1,
    1-X6 + 1-X12 + Y106 $>=1,
    1-X6 + 1-X18 +  Y107 $>=1,
    1-X6 + 1-X24 + Y108 $>=1,
    1-X6 + 1-X30 + Y109 $>=1,
    1-X6 + 1-X36 + Y110 $>=1,
    1-X6 + 1-X42 + Y111 $>=1,
    1-X12 + 1-X18 + Y112 $>=1,
    1-X12 + 1-X24 + Y113 $>=1,
    1-X12 + 1-X30 + Y114 $>=1,
    1-X12 + 1-X36 + Y115 $>=1,
    1-X12 + 1-X42 + Y116 $>=1,
    1-X18 + 1-X24 + Y117 $>=1,
    1-X18 + 1-X30 + Y118 $>=1,
    1-X18 + 1-X36 + Y119 $>=1,
    1-X18 + 1-X42 + Y120 $>=1,
    1-X24 + 1-X30 + Y121 $>=1,
    1-X24 + 1-X36 + Y122 $>=1,
    1-X24 + 1-X42 + Y123 $>=1,
    1-X30 + 1-X36 + Y124 $>=1,
    1-X30 + 1-X42 + Y125 $>=1,
    1-X36 + 1-X42 + Y126 $>=1,
    X6+X5+X4+X3+X2+X1 + Y127 $>=1,
    X12 + X11 + X10 + X9 + X8 + X7 + Y128 $>=1,
    X18 + X17 + X16 + X15 + X14 + X13 + Y129 $>=1,
    X13 + X24 + X23 + X22 + X21 + X20 + X19 + Y130 $>=1,
    X30 + X29 + X28 + X27 + X26 + X25 + Y131 $>=1,
    X36 + X35 + X34 + X33 + X32 + X31 + Y132 $>=1,
    X42 + X41 + X40 + X39 + X38 + X37 + Y133 $>=1,

    append(Vars,Slats,AllVars),
    lp_solve(AllVars,min(sum(Slats))),
    format("sol(~w)~n",[AllVars]).