/* 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],

    lp_integers(Vars),

    lp_domain(Vars,0,1),

    1-X1+1-X7 $>= 1,
    1-X1 + 1-X13 $>= 1,
    1-X1 + 1-X19$>=1,
    1-X1 + 1-X25$>=1,
    1-X1 + 1-X31$>=1,
    1-X1 + 1-X37$>=1,
    1-X7 + 1-X13$>=1,
    1-X7 + 1-X19$>=1,
    1-X7 + 1-X25$>=1,
    1-X7 + 1-X31$>=1,
    1-X7 + 1-X37$>=1,
    1-X13 + 1-X19$>=1,
    1-X13 + 1-X25$>=1,
    1-X13 + 1-X31$>=1,
    1-X13 + 1-X37$>=1,
    1-X19 + 1-X25$>=1,
    1-X19 + 1-X31$>=1,
    1-X19 + 1-X37$>=1,
    1-X25 + 1-X31$>=1,
    1-X25 + 1-X37$>=1,
    1-X31 + 1-X37$>=1,
    1-X2 + 1-X8$>=1,
    1-X2 + 1-X14$>=1,
    1-X2 + 1-X20$>=1,
    1-X2 + 1-X26$>=1,
    1-X2 + 1-X32$>=1,
    1-X2 + 1-X38$>=1,
    1-X8 + 1-X14$>=1,
    1-X8 + 1-X20$>=1,
    1-X8 + 1-X26$>=1,
    1-X8 + 1-X32$>=1,
    1-X8 + 1-X38$>=1,
    1-X14 + 1-X20$>=1,
    1-X14 + 1-X26$>=1,
    1-X14 + 1-X32$>=1,
    1-X14 + 1-X38$>=1,
    1-X20 + 1-X26$>=1,
    1-X20 + 1-X32$>=1,
    1-X20 + 1-X38$>=1,
    1-X26 + 1-X32$>=1,
    1-X26 + 1-X38$>=1,
    1-X32 + 1-X38$>=1,
    1-X3 + 1-X9$>=1,
    1-X3 + 1-X15$>=1,
    1-X3 + 1-X21$>=1,
    1-X3 + 1-X27$>=1,
    1-X3 + 1-X33$>=1,
    1-X3 + 1-X39$>=1,
    1-X9 + 1-X15$>=1,
    1-X9 + 1-X21$>=1,
    1-X9 + 1-X27$>=1,
    1-X9 + 1-X33$>=1,
    1-X9 + 1-X39$>=1,
    1-X15 + 1-X21$>=1,
    1-X15 + 1-X27$>=1,
    1-X15 + 1-X33$>=1,
    1-X15 + 1-X39$>=1,
    1-X21 + 1-X27$>=1,
    1-X21 + 1-X33$>=1,
    1-X21 + 1-X39$>=1,
    1-X27 + 1-X33$>=1,
    1-X27 + 1-X39$>=1,
    1-X33 + 1-X39$>=1, 
    1-X4 + 1-X10$>=1,
    1-X4 + 1-X16$>=1,
    1-X4 + 1-X22$>=1, 
    1-X4 + 1-X28$>=1,
    1-X4 + 1-X34$>=1,
    1-X4 + 1-X40$>=1,
    1-X10 + 1-X16$>=1,
    1-X10 + 1-X22$>=1,
    1-X10 + 1-X28$>=1,
    1-X10 + 1-X34$>=1,
    1-X10 + 1-X40$>=1,
    1-X16 + 1-X22$>=1,
    1-X16 + 1-X28$>=1,
    1-X16 + 1-X34$>=1,
    1-X16 + 1-X40$>=1,
    1-X22 + 1-X28$>=1,
    1-X22 + 1-X34$>=1,
    1-X22 + 1-X40$>=1,
    1-X28 + 1-X34$>=1,
    1-X28 + 1-X40$>=1,
    1-X34 + 1-X40$>=1,
    1-X5 + 1-X11$>=1,
    1-X5 + 1-X17$>=1,
    1-X5 + 1-X23$>=1,
    1-X5 + 1-X29$>=1,
    1-X5 + 1-X35$>=1,
    1-X5 + 1-X41$>=1,
    1-X11 + 1-X17$>=1,
    1-X11 + 1-X23$>=1,
    1-X11 + 1-X29$>=1,
    1-X11 + 1-X35$>=1,
    1-X11 + 1-X41$>=1,
    1-X17 + 1-X23$>=1,
    1-X17 + 1-X29$>=1,
    1-X17 + 1-X35$>=1,
    1-X17 + 1-X41$>=1,
    1-X23 + 1-X29$>=1,
    1-X23 + 1-X35$>=1,
    1-X23 + 1-X41$>=1,
    1-X29 + 1-X35$>=1,
    1-X29 + 1-X41$>=1,
    1-X35 + 1-X41$>=1,
    1-X6 + 1-X12$>=1,
    1-X6 + 1-X18$>=1,
    1-X6 + 1-X24$>=1,
    1-X6 + 1-X30$>=1,
    1-X6 + 1-X36$>=1,
    1-X6 + 1-X42$>=1,
    1-X12 + 1-X18$>=1,
    1-X12 + 1-X24$>=1,
    1-X12 + 1-X30$>=1,
    1-X12 + 1-X36$>=1,
    1-X12 + 1-X42$>=1,
    1-X18 + 1-X24$>=1,
    1-X18 + 1-X30$>=1,
    1-X18 + 1-X36$>=1,
    1-X18 + 1-X42$>=1,
    1-X24 + 1-X30$>=1,
    1-X24 + 1-X36$>=1,
    1-X24 + 1-X42$>=1,
    1-X30 + 1-X36$>=1,
    1-X30 + 1-X42$>=1,
    1-X36 + 1-X42$>=1,
    X6+X5+X4+X3+X2+X1$>=1,
    X12 + X11 + X10 + X9 + X8 + X7$>=1,
    X18 + X17 + X16 + X15 + X14 + X13$>=1,
    X13 + X24 + X23 + X22 + X21 + X20 + X19$>=1,
    X30 + X29 + X28 + X27 + X26 + X25$>=1,
    X36 + X35 + X34 + X33 + X32 + X31$>=1,
    X42 + X41 + X40 + X39 + X38 + X37$>=1,
    lp_solve(Vars),
    format("sol(~w)~n",[Vars]).