-
Notifications
You must be signed in to change notification settings - Fork 3
/
Copy pathsage-CNF-convert.txt
17 lines (15 loc) · 24.8 KB
/
sage-CNF-convert.txt
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
B.<K0,K1,K2,K3,K4,K5,K6,K7,K8,K9,K10,K11,K12,K13,K14,K15,K16,K17,K18,K19,K20,K21,K22,K23,K24,K25,K26,K27,K28,K29,K30,K31,K32,K33,K34,K35,K36,K37,K38,K39,K40,K41,K42,K43,K44,K45,K46,K47,K48,K49,K50,K51,K52,K53,K54,K55,K56,K57,K58,K59,K60,K61,K62,K63,A0,A1,A2,A3,A4,A5,A6,A7,A8,A9,A10,A11,A12,A13,A14,A15,A16,A17,A18,A19,A20,A21,A22,A23,A24,A25,A26,A27,A28,A29,A30,A31,A32,A33,A34,A35,A36,A37,A38,A39,A40,A41,A42,A43,A44,A45,A46,A47,A48,A49,A50,A51,A52,A53,A54,A55,A56,A57,A58,A59,A60,A61,A62,A63,A64,A65,A66,A67,A68,A69,A70,A71,A72,A73,A74,A75,A76,A77,A78,A79,A80,A81,A82,A83,A84,A85,A86,A87,A88,A89,A90,A91,A92,A93,A94,A95,A96,A97,A98,A99,A100,A101,A102,A103,A104,A105,A106,A107,A108,A109,A110,A111,A112,A113,A114,A115,A116,A117,A118,A119,A120,A121,A122,A123,A124,A125,A126,A127,A128,A129,A130,A131,A132,A133,A134,A135,A136,A137,A138,A139,A140,A141,A142,A143,A144,A145,A146,A147,A148,A149,A150,A151,A152,A153,A154,A155,A156,A157,A158,A159,B0,B1,B2,B3,B4,B5,B6,B7,B8,B9,B10,B11,B12,B13,B14,B15,B16,B17,B18,B19,B20,B21,B22,B23,B24,B25,B26,B27,B28,B29,B30,B31,B32,B33,B34,B35,B36,B37,B38,B39,B40,B41,B42,B43,B44,B45,B46,B47,B48,B49,B50,B51,B52,B53,B54,B55,B56,B57,B58,B59,B60,B61,B62,B63,B64,B65,B66,B67,B68,B69,B70,B71,B72,B73,B74,B75,B76,B77,B78,B79,B80,B81,B82,B83,B84,B85,B86,B87,B88,B89,B90,B91,B92,B93,B94,B95,B96,B97,B98,B99,B100,B101,B102,B103,B104,B105,B106,B107,B108,B109,B110,B111,B112,B113,B114,B115,B116,B117,B118,B119,B120,B121,B122,B123,B124,B125,B126,B127,B128,B129,B130,B131,B132,B133,B134,B135,B136,B137,B138,B139,B140,B141,B142,B143,B144,B145,B146,B147,B148,B149,B150,B151,B152,B153,B154,B155,B156,B157,B158,B159,L0,L1,L2,L3,L4,L5,L6,L7,L8,L9,L10,L11,L12,L13,L14,L15,L16,L17,L18,L19,L20,L21,L22,L23,L24,L25,L26,L27,L28,L29,L30,L31,L32,L33,L34,L35,L36,L37,L38,L39,L40,L41,L42,L43,L44,L45,L46,L47,L48,L49,L50,L51,L52,L53,L54,L55,L56,L57,L58,L59,L60,L61,L62,L63,L64,L65,L66,L67,L68,L69,L70,L71,L72,L73,L74,L75,L76,L77,L78,L79,L80,L81,L82,L83,L84,L85,L86,L87,L88,L89,L90,L91,L92,L93,L94,L95,L96,L97,L98,L99,L100,L101,L102,L103,L104,L105,L106,L107,L108,L109,L110,L111,L112,L113,L114,L115,L116,L117,L118,L119,L120,L121,L122,L123,L124,L125,L126,L127,L128,L129,L130,L131,L132,L133,L134,L135,L136,L137,L138,L139,L140,L141,L142,L143,L144,L145,L146,L147,L148,L149,L150,L151,L152,L153,L154,L155,L156,L157,L158,L159,L160,L161,L162,L163,L164,L165,L166,L167,L168,L169,L170,L171,L172,L173,L174,L175,L176,L177,L178,L179,L180,L181,L182,L183,L184,L185,L186,L187,L188,L189,L190,L191>=BooleanPolynomialRing()
from sage.sat.converters.polybori import CNFEncoder
from sage.sat.solvers.dimacs import DIMACS
fn = tmp_filename()
solver = DIMACS(filename=fn)
e = CNFEncoder(solver, B)
e([L0+0,L1+1,L2+1,L3+0,L4+0,L5+0,L6+1,L7+0,L8+1,L9+0,L10+0,L11+1,L12+0,L13+1,L14+1,L15+1,L16+0,L17+0,L18+0,L19+0,L20+1,L21+0,L22+1,L23+0,L24+1,L25+1,L26+1,L27+0,L28+0,L29+0,L30+1,L31+1,L160+0,L161+1,L162+1,L163+0,L164+1,L165+0,L166+0,L167+0,L168+1,L169+1,L170+0,L171+0,L172+1,L173+0,L174+0,L175+1,L176+0,L177+1,L178+0,L179+0,L180+1,L181+0,L182+1,L183+0,L184+0,L185+1,L186+1,L187+1,L188+1,L189+0,L190+0,L191+1,K0+0,K1+0,K2+1,K3+1,K4+0,K5+1,K6+0,K7+0,K8+1,K9+1,K10+0,K11+1,K12+1,K13+1,K14+1,K15+1,K16+1,K17+0,K18+0,K19+1,K20+0,K21+1,K22+1,K23+0,K24+0,K25+0,K26+0,K27+1,K28+1,K29+1,K30+0,K31+0,L32+K0+L0+L16+L9+L1+L31*L20+B0+L26*L20+L26*L1+L20*L9+L9*L1+B0*L9+B0*L20+A0*L9+A0*L20,A0+L31*L26,B0+L31*L1,L33+K1+L1+L17+L10+L2+L32*L21+B1+L27*L21+L27*L2+L21*L10+L10*L2+B1*L10+B1*L21+A1*L10+A1*L21,A1+L32*L27,B1+L32*L2,L34+K2+L2+L18+L11+L3+L33*L22+B2+L28*L22+L28*L3+L22*L11+L11*L3+B2*L11+B2*L22+A2*L11+A2*L22,A2+L33*L28,B2+L33*L3,L35+K3+L3+L19+L12+L4+L34*L23+B3+L29*L23+L29*L4+L23*L12+L12*L4+B3*L12+B3*L23+A3*L12+A3*L23,A3+L34*L29,B3+L34*L4,L36+K4+L4+L20+L13+L5+L35*L24+B4+L30*L24+L30*L5+L24*L13+L13*L5+B4*L13+B4*L24+A4*L13+A4*L24,A4+L35*L30,B4+L35*L5,L37+K5+L5+L21+L14+L6+L36*L25+B5+L31*L25+L31*L6+L25*L14+L14*L6+B5*L14+B5*L25+A5*L14+A5*L25,A5+L36*L31,B5+L36*L6,L38+K6+L6+L22+L15+L7+L37*L26+B6+L32*L26+L32*L7+L26*L15+L15*L7+B6*L15+B6*L26+A6*L15+A6*L26,A6+L37*L32,B6+L37*L7,L39+K7+L7+L23+L16+L8+L38*L27+B7+L33*L27+L33*L8+L27*L16+L16*L8+B7*L16+B7*L27+A7*L16+A7*L27,A7+L38*L33,B7+L38*L8,L40+K8+L8+L24+L17+L9+L39*L28+B8+L34*L28+L34*L9+L28*L17+L17*L9+B8*L17+B8*L28+A8*L17+A8*L28,A8+L39*L34,B8+L39*L9,L41+K9+L9+L25+L18+L10+L40*L29+B9+L35*L29+L35*L10+L29*L18+L18*L10+B9*L18+B9*L29+A9*L18+A9*L29,A9+L40*L35,B9+L40*L10,L42+K10+L10+L26+L19+L11+L41*L30+B10+L36*L30+L36*L11+L30*L19+L19*L11+B10*L19+B10*L30+A10*L19+A10*L30,A10+L41*L36,B10+L41*L11,L43+K11+L11+L27+L20+L12+L42*L31+B11+L37*L31+L37*L12+L31*L20+L20*L12+B11*L20+B11*L31+A11*L20+A11*L31,A11+L42*L37,B11+L42*L12,L44+K12+L12+L28+L21+L13+L43*L32+B12+L38*L32+L38*L13+L32*L21+L21*L13+B12*L21+B12*L32+A12*L21+A12*L32,A12+L43*L38,B12+L43*L13,L45+K13+L13+L29+L22+L14+L44*L33+B13+L39*L33+L39*L14+L33*L22+L22*L14+B13*L22+B13*L33+A13*L22+A13*L33,A13+L44*L39,B13+L44*L14,L46+K14+L14+L30+L23+L15+L45*L34+B14+L40*L34+L40*L15+L34*L23+L23*L15+B14*L23+B14*L34+A14*L23+A14*L34,A14+L45*L40,B14+L45*L15,L47+K15+L15+L31+L24+L16+L46*L35+B15+L41*L35+L41*L16+L35*L24+L24*L16+B15*L24+B15*L35+A15*L24+A15*L35,A15+L46*L41,B15+L46*L16,L48+K16+L16+L32+L25+L17+L47*L36+B16+L42*L36+L42*L17+L36*L25+L25*L17+B16*L25+B16*L36+A16*L25+A16*L36,A16+L47*L42,B16+L47*L17,L49+K17+L17+L33+L26+L18+L48*L37+B17+L43*L37+L43*L18+L37*L26+L26*L18+B17*L26+B17*L37+A17*L26+A17*L37,A17+L48*L43,B17+L48*L18,L50+K18+L18+L34+L27+L19+L49*L38+B18+L44*L38+L44*L19+L38*L27+L27*L19+B18*L27+B18*L38+A18*L27+A18*L38,A18+L49*L44,B18+L49*L19,L51+K19+L19+L35+L28+L20+L50*L39+B19+L45*L39+L45*L20+L39*L28+L28*L20+B19*L28+B19*L39+A19*L28+A19*L39,A19+L50*L45,B19+L50*L20,L52+K20+L20+L36+L29+L21+L51*L40+B20+L46*L40+L46*L21+L40*L29+L29*L21+B20*L29+B20*L40+A20*L29+A20*L40,A20+L51*L46,B20+L51*L21,L53+K21+L21+L37+L30+L22+L52*L41+B21+L47*L41+L47*L22+L41*L30+L30*L22+B21*L30+B21*L41+A21*L30+A21*L41,A21+L52*L47,B21+L52*L22,L54+K22+L22+L38+L31+L23+L53*L42+B22+L48*L42+L48*L23+L42*L31+L31*L23+B22*L31+B22*L42+A22*L31+A22*L42,A22+L53*L48,B22+L53*L23,L55+K23+L23+L39+L32+L24+L54*L43+B23+L49*L43+L49*L24+L43*L32+L32*L24+B23*L32+B23*L43+A23*L32+A23*L43,A23+L54*L49,B23+L54*L24,L56+K24+L24+L40+L33+L25+L55*L44+B24+L50*L44+L50*L25+L44*L33+L33*L25+B24*L33+B24*L44+A24*L33+A24*L44,A24+L55*L50,B24+L55*L25,L57+K25+L25+L41+L34+L26+L56*L45+B25+L51*L45+L51*L26+L45*L34+L34*L26+B25*L34+B25*L45+A25*L34+A25*L45,A25+L56*L51,B25+L56*L26,L58+K26+L26+L42+L35+L27+L57*L46+B26+L52*L46+L52*L27+L46*L35+L35*L27+B26*L35+B26*L46+A26*L35+A26*L46,A26+L57*L52,B26+L57*L27,L59+K27+L27+L43+L36+L28+L58*L47+B27+L53*L47+L53*L28+L47*L36+L36*L28+B27*L36+B27*L47+A27*L36+A27*L47,A27+L58*L53,B27+L58*L28,L60+K28+L28+L44+L37+L29+L59*L48+B28+L54*L48+L54*L29+L48*L37+L37*L29+B28*L37+B28*L48+A28*L37+A28*L48,A28+L59*L54,B28+L59*L29,L61+K29+L29+L45+L38+L30+L60*L49+B29+L55*L49+L55*L30+L49*L38+L38*L30+B29*L38+B29*L49+A29*L38+A29*L49,A29+L60*L55,B29+L60*L30,L62+K30+L30+L46+L39+L31+L61*L50+B30+L56*L50+L56*L31+L50*L39+L39*L31+B30*L39+B30*L50+A30*L39+A30*L50,A30+L61*L56,B30+L61*L31,L63+K31+L31+L47+L40+L32+L62*L51+B31+L57*L51+L57*L32+L51*L40+L40*L32+B31*L40+B31*L51+A31*L40+A31*L51,A31+L62*L57,B31+L62*L32,L64+K32+L32+L48+L41+L33+L63*L52+B32+L58*L52+L58*L33+L52*L41+L41*L33+B32*L41+B32*L52+A32*L41+A32*L52,A32+L63*L58,B32+L63*L33,L65+K33+L33+L49+L42+L34+L64*L53+B33+L59*L53+L59*L34+L53*L42+L42*L34+B33*L42+B33*L53+A33*L42+A33*L53,A33+L64*L59,B33+L64*L34,L66+K34+L34+L50+L43+L35+L65*L54+B34+L60*L54+L60*L35+L54*L43+L43*L35+B34*L43+B34*L54+A34*L43+A34*L54,A34+L65*L60,B34+L65*L35,L67+K35+L35+L51+L44+L36+L66*L55+B35+L61*L55+L61*L36+L55*L44+L44*L36+B35*L44+B35*L55+A35*L44+A35*L55,A35+L66*L61,B35+L66*L36,L68+K36+L36+L52+L45+L37+L67*L56+B36+L62*L56+L62*L37+L56*L45+L45*L37+B36*L45+B36*L56+A36*L45+A36*L56,A36+L67*L62,B36+L67*L37,L69+K37+L37+L53+L46+L38+L68*L57+B37+L63*L57+L63*L38+L57*L46+L46*L38+B37*L46+B37*L57+A37*L46+A37*L57,A37+L68*L63,B37+L68*L38,L70+K38+L38+L54+L47+L39+L69*L58+B38+L64*L58+L64*L39+L58*L47+L47*L39+B38*L47+B38*L58+A38*L47+A38*L58,A38+L69*L64,B38+L69*L39,L71+K39+L39+L55+L48+L40+L70*L59+B39+L65*L59+L65*L40+L59*L48+L48*L40+B39*L48+B39*L59+A39*L48+A39*L59,A39+L70*L65,B39+L70*L40,L72+K40+L40+L56+L49+L41+L71*L60+B40+L66*L60+L66*L41+L60*L49+L49*L41+B40*L49+B40*L60+A40*L49+A40*L60,A40+L71*L66,B40+L71*L41,L73+K41+L41+L57+L50+L42+L72*L61+B41+L67*L61+L67*L42+L61*L50+L50*L42+B41*L50+B41*L61+A41*L50+A41*L61,A41+L72*L67,B41+L72*L42,L74+K42+L42+L58+L51+L43+L73*L62+B42+L68*L62+L68*L43+L62*L51+L51*L43+B42*L51+B42*L62+A42*L51+A42*L62,A42+L73*L68,B42+L73*L43,L75+K43+L43+L59+L52+L44+L74*L63+B43+L69*L63+L69*L44+L63*L52+L52*L44+B43*L52+B43*L63+A43*L52+A43*L63,A43+L74*L69,B43+L74*L44,L76+K44+L44+L60+L53+L45+L75*L64+B44+L70*L64+L70*L45+L64*L53+L53*L45+B44*L53+B44*L64+A44*L53+A44*L64,A44+L75*L70,B44+L75*L45,L77+K45+L45+L61+L54+L46+L76*L65+B45+L71*L65+L71*L46+L65*L54+L54*L46+B45*L54+B45*L65+A45*L54+A45*L65,A45+L76*L71,B45+L76*L46,L78+K46+L46+L62+L55+L47+L77*L66+B46+L72*L66+L72*L47+L66*L55+L55*L47+B46*L55+B46*L66+A46*L55+A46*L66,A46+L77*L72,B46+L77*L47,L79+K47+L47+L63+L56+L48+L78*L67+B47+L73*L67+L73*L48+L67*L56+L56*L48+B47*L56+B47*L67+A47*L56+A47*L67,A47+L78*L73,B47+L78*L48,L80+K48+L48+L64+L57+L49+L79*L68+B48+L74*L68+L74*L49+L68*L57+L57*L49+B48*L57+B48*L68+A48*L57+A48*L68,A48+L79*L74,B48+L79*L49,L81+K49+L49+L65+L58+L50+L80*L69+B49+L75*L69+L75*L50+L69*L58+L58*L50+B49*L58+B49*L69+A49*L58+A49*L69,A49+L80*L75,B49+L80*L50,L82+K50+L50+L66+L59+L51+L81*L70+B50+L76*L70+L76*L51+L70*L59+L59*L51+B50*L59+B50*L70+A50*L59+A50*L70,A50+L81*L76,B50+L81*L51,L83+K51+L51+L67+L60+L52+L82*L71+B51+L77*L71+L77*L52+L71*L60+L60*L52+B51*L60+B51*L71+A51*L60+A51*L71,A51+L82*L77,B51+L82*L52,L84+K52+L52+L68+L61+L53+L83*L72+B52+L78*L72+L78*L53+L72*L61+L61*L53+B52*L61+B52*L72+A52*L61+A52*L72,A52+L83*L78,B52+L83*L53,L85+K53+L53+L69+L62+L54+L84*L73+B53+L79*L73+L79*L54+L73*L62+L62*L54+B53*L62+B53*L73+A53*L62+A53*L73,A53+L84*L79,B53+L84*L54,L86+K54+L54+L70+L63+L55+L85*L74+B54+L80*L74+L80*L55+L74*L63+L63*L55+B54*L63+B54*L74+A54*L63+A54*L74,A54+L85*L80,B54+L85*L55,L87+K55+L55+L71+L64+L56+L86*L75+B55+L81*L75+L81*L56+L75*L64+L64*L56+B55*L64+B55*L75+A55*L64+A55*L75,A55+L86*L81,B55+L86*L56,L88+K56+L56+L72+L65+L57+L87*L76+B56+L82*L76+L82*L57+L76*L65+L65*L57+B56*L65+B56*L76+A56*L65+A56*L76,A56+L87*L82,B56+L87*L57,L89+K57+L57+L73+L66+L58+L88*L77+B57+L83*L77+L83*L58+L77*L66+L66*L58+B57*L66+B57*L77+A57*L66+A57*L77,A57+L88*L83,B57+L88*L58,L90+K58+L58+L74+L67+L59+L89*L78+B58+L84*L78+L84*L59+L78*L67+L67*L59+B58*L67+B58*L78+A58*L67+A58*L78,A58+L89*L84,B58+L89*L59,L91+K59+L59+L75+L68+L60+L90*L79+B59+L85*L79+L85*L60+L79*L68+L68*L60+B59*L68+B59*L79+A59*L68+A59*L79,A59+L90*L85,B59+L90*L60,L92+K60+L60+L76+L69+L61+L91*L80+B60+L86*L80+L86*L61+L80*L69+L69*L61+B60*L69+B60*L80+A60*L69+A60*L80,A60+L91*L86,B60+L91*L61,L93+K61+L61+L77+L70+L62+L92*L81+B61+L87*L81+L87*L62+L81*L70+L70*L62+B61*L70+B61*L81+A61*L70+A61*L81,A61+L92*L87,B61+L92*L62,L94+K62+L62+L78+L71+L63+L93*L82+B62+L88*L82+L88*L63+L82*L71+L71*L63+B62*L71+B62*L82+A62*L71+A62*L82,A62+L93*L88,B62+L93*L63,L95+K63+L63+L79+L72+L64+L94*L83+B63+L89*L83+L89*L64+L83*L72+L72*L64+B63*L72+B63*L83+A63*L72+A63*L83,A63+L94*L89,B63+L94*L64,L96+K0+L64+L80+L73+L65+L95*L84+B64+L90*L84+L90*L65+L84*L73+L73*L65+B64*L73+B64*L84+A64*L73+A64*L84,A64+L95*L90,B64+L95*L65,L97+K1+L65+L81+L74+L66+L96*L85+B65+L91*L85+L91*L66+L85*L74+L74*L66+B65*L74+B65*L85+A65*L74+A65*L85,A65+L96*L91,B65+L96*L66,L98+K2+L66+L82+L75+L67+L97*L86+B66+L92*L86+L92*L67+L86*L75+L75*L67+B66*L75+B66*L86+A66*L75+A66*L86,A66+L97*L92,B66+L97*L67,L99+K3+L67+L83+L76+L68+L98*L87+B67+L93*L87+L93*L68+L87*L76+L76*L68+B67*L76+B67*L87+A67*L76+A67*L87,A67+L98*L93,B67+L98*L68,L100+K4+L68+L84+L77+L69+L99*L88+B68+L94*L88+L94*L69+L88*L77+L77*L69+B68*L77+B68*L88+A68*L77+A68*L88,A68+L99*L94,B68+L99*L69,L101+K5+L69+L85+L78+L70+L100*L89+B69+L95*L89+L95*L70+L89*L78+L78*L70+B69*L78+B69*L89+A69*L78+A69*L89,A69+L100*L95,B69+L100*L70,L102+K6+L70+L86+L79+L71+L101*L90+B70+L96*L90+L96*L71+L90*L79+L79*L71+B70*L79+B70*L90+A70*L79+A70*L90,A70+L101*L96,B70+L101*L71,L103+K7+L71+L87+L80+L72+L102*L91+B71+L97*L91+L97*L72+L91*L80+L80*L72+B71*L80+B71*L91+A71*L80+A71*L91,A71+L102*L97,B71+L102*L72,L104+K8+L72+L88+L81+L73+L103*L92+B72+L98*L92+L98*L73+L92*L81+L81*L73+B72*L81+B72*L92+A72*L81+A72*L92,A72+L103*L98,B72+L103*L73,L105+K9+L73+L89+L82+L74+L104*L93+B73+L99*L93+L99*L74+L93*L82+L82*L74+B73*L82+B73*L93+A73*L82+A73*L93,A73+L104*L99,B73+L104*L74,L106+K10+L74+L90+L83+L75+L105*L94+B74+L100*L94+L100*L75+L94*L83+L83*L75+B74*L83+B74*L94+A74*L83+A74*L94,A74+L105*L100,B74+L105*L75,L107+K11+L75+L91+L84+L76+L106*L95+B75+L101*L95+L101*L76+L95*L84+L84*L76+B75*L84+B75*L95+A75*L84+A75*L95,A75+L106*L101,B75+L106*L76,L108+K12+L76+L92+L85+L77+L107*L96+B76+L102*L96+L102*L77+L96*L85+L85*L77+B76*L85+B76*L96+A76*L85+A76*L96,A76+L107*L102,B76+L107*L77,L109+K13+L77+L93+L86+L78+L108*L97+B77+L103*L97+L103*L78+L97*L86+L86*L78+B77*L86+B77*L97+A77*L86+A77*L97,A77+L108*L103,B77+L108*L78,L110+K14+L78+L94+L87+L79+L109*L98+B78+L104*L98+L104*L79+L98*L87+L87*L79+B78*L87+B78*L98+A78*L87+A78*L98,A78+L109*L104,B78+L109*L79,L111+K15+L79+L95+L88+L80+L110*L99+B79+L105*L99+L105*L80+L99*L88+L88*L80+B79*L88+B79*L99+A79*L88+A79*L99,A79+L110*L105,B79+L110*L80,L112+K16+L80+L96+L89+L81+L111*L100+B80+L106*L100+L106*L81+L100*L89+L89*L81+B80*L89+B80*L100+A80*L89+A80*L100,A80+L111*L106,B80+L111*L81,L113+K17+L81+L97+L90+L82+L112*L101+B81+L107*L101+L107*L82+L101*L90+L90*L82+B81*L90+B81*L101+A81*L90+A81*L101,A81+L112*L107,B81+L112*L82,L114+K18+L82+L98+L91+L83+L113*L102+B82+L108*L102+L108*L83+L102*L91+L91*L83+B82*L91+B82*L102+A82*L91+A82*L102,A82+L113*L108,B82+L113*L83,L115+K19+L83+L99+L92+L84+L114*L103+B83+L109*L103+L109*L84+L103*L92+L92*L84+B83*L92+B83*L103+A83*L92+A83*L103,A83+L114*L109,B83+L114*L84,L116+K20+L84+L100+L93+L85+L115*L104+B84+L110*L104+L110*L85+L104*L93+L93*L85+B84*L93+B84*L104+A84*L93+A84*L104,A84+L115*L110,B84+L115*L85,L117+K21+L85+L101+L94+L86+L116*L105+B85+L111*L105+L111*L86+L105*L94+L94*L86+B85*L94+B85*L105+A85*L94+A85*L105,A85+L116*L111,B85+L116*L86,L118+K22+L86+L102+L95+L87+L117*L106+B86+L112*L106+L112*L87+L106*L95+L95*L87+B86*L95+B86*L106+A86*L95+A86*L106,A86+L117*L112,B86+L117*L87,L119+K23+L87+L103+L96+L88+L118*L107+B87+L113*L107+L113*L88+L107*L96+L96*L88+B87*L96+B87*L107+A87*L96+A87*L107,A87+L118*L113,B87+L118*L88,L120+K24+L88+L104+L97+L89+L119*L108+B88+L114*L108+L114*L89+L108*L97+L97*L89+B88*L97+B88*L108+A88*L97+A88*L108,A88+L119*L114,B88+L119*L89,L121+K25+L89+L105+L98+L90+L120*L109+B89+L115*L109+L115*L90+L109*L98+L98*L90+B89*L98+B89*L109+A89*L98+A89*L109,A89+L120*L115,B89+L120*L90,L122+K26+L90+L106+L99+L91+L121*L110+B90+L116*L110+L116*L91+L110*L99+L99*L91+B90*L99+B90*L110+A90*L99+A90*L110,A90+L121*L116,B90+L121*L91,L123+K27+L91+L107+L100+L92+L122*L111+B91+L117*L111+L117*L92+L111*L100+L100*L92+B91*L100+B91*L111+A91*L100+A91*L111,A91+L122*L117,B91+L122*L92,L124+K28+L92+L108+L101+L93+L123*L112+B92+L118*L112+L118*L93+L112*L101+L101*L93+B92*L101+B92*L112+A92*L101+A92*L112,A92+L123*L118,B92+L123*L93,L125+K29+L93+L109+L102+L94+L124*L113+B93+L119*L113+L119*L94+L113*L102+L102*L94+B93*L102+B93*L113+A93*L102+A93*L113,A93+L124*L119,B93+L124*L94,L126+K30+L94+L110+L103+L95+L125*L114+B94+L120*L114+L120*L95+L114*L103+L103*L95+B94*L103+B94*L114+A94*L103+A94*L114,A94+L125*L120,B94+L125*L95,L127+K31+L95+L111+L104+L96+L126*L115+B95+L121*L115+L121*L96+L115*L104+L104*L96+B95*L104+B95*L115+A95*L104+A95*L115,A95+L126*L121,B95+L126*L96,L128+K32+L96+L112+L105+L97+L127*L116+B96+L122*L116+L122*L97+L116*L105+L105*L97+B96*L105+B96*L116+A96*L105+A96*L116,A96+L127*L122,B96+L127*L97,L129+K33+L97+L113+L106+L98+L128*L117+B97+L123*L117+L123*L98+L117*L106+L106*L98+B97*L106+B97*L117+A97*L106+A97*L117,A97+L128*L123,B97+L128*L98,L130+K34+L98+L114+L107+L99+L129*L118+B98+L124*L118+L124*L99+L118*L107+L107*L99+B98*L107+B98*L118+A98*L107+A98*L118,A98+L129*L124,B98+L129*L99,L131+K35+L99+L115+L108+L100+L130*L119+B99+L125*L119+L125*L100+L119*L108+L108*L100+B99*L108+B99*L119+A99*L108+A99*L119,A99+L130*L125,B99+L130*L100,L132+K36+L100+L116+L109+L101+L131*L120+B100+L126*L120+L126*L101+L120*L109+L109*L101+B100*L109+B100*L120+A100*L109+A100*L120,A100+L131*L126,B100+L131*L101,L133+K37+L101+L117+L110+L102+L132*L121+B101+L127*L121+L127*L102+L121*L110+L110*L102+B101*L110+B101*L121+A101*L110+A101*L121,A101+L132*L127,B101+L132*L102,L134+K38+L102+L118+L111+L103+L133*L122+B102+L128*L122+L128*L103+L122*L111+L111*L103+B102*L111+B102*L122+A102*L111+A102*L122,A102+L133*L128,B102+L133*L103,L135+K39+L103+L119+L112+L104+L134*L123+B103+L129*L123+L129*L104+L123*L112+L112*L104+B103*L112+B103*L123+A103*L112+A103*L123,A103+L134*L129,B103+L134*L104,L136+K40+L104+L120+L113+L105+L135*L124+B104+L130*L124+L130*L105+L124*L113+L113*L105+B104*L113+B104*L124+A104*L113+A104*L124,A104+L135*L130,B104+L135*L105,L137+K41+L105+L121+L114+L106+L136*L125+B105+L131*L125+L131*L106+L125*L114+L114*L106+B105*L114+B105*L125+A105*L114+A105*L125,A105+L136*L131,B105+L136*L106,L138+K42+L106+L122+L115+L107+L137*L126+B106+L132*L126+L132*L107+L126*L115+L115*L107+B106*L115+B106*L126+A106*L115+A106*L126,A106+L137*L132,B106+L137*L107,L139+K43+L107+L123+L116+L108+L138*L127+B107+L133*L127+L133*L108+L127*L116+L116*L108+B107*L116+B107*L127+A107*L116+A107*L127,A107+L138*L133,B107+L138*L108,L140+K44+L108+L124+L117+L109+L139*L128+B108+L134*L128+L134*L109+L128*L117+L117*L109+B108*L117+B108*L128+A108*L117+A108*L128,A108+L139*L134,B108+L139*L109,L141+K45+L109+L125+L118+L110+L140*L129+B109+L135*L129+L135*L110+L129*L118+L118*L110+B109*L118+B109*L129+A109*L118+A109*L129,A109+L140*L135,B109+L140*L110,L142+K46+L110+L126+L119+L111+L141*L130+B110+L136*L130+L136*L111+L130*L119+L119*L111+B110*L119+B110*L130+A110*L119+A110*L130,A110+L141*L136,B110+L141*L111,L143+K47+L111+L127+L120+L112+L142*L131+B111+L137*L131+L137*L112+L131*L120+L120*L112+B111*L120+B111*L131+A111*L120+A111*L131,A111+L142*L137,B111+L142*L112,L144+K48+L112+L128+L121+L113+L143*L132+B112+L138*L132+L138*L113+L132*L121+L121*L113+B112*L121+B112*L132+A112*L121+A112*L132,A112+L143*L138,B112+L143*L113,L145+K49+L113+L129+L122+L114+L144*L133+B113+L139*L133+L139*L114+L133*L122+L122*L114+B113*L122+B113*L133+A113*L122+A113*L133,A113+L144*L139,B113+L144*L114,L146+K50+L114+L130+L123+L115+L145*L134+B114+L140*L134+L140*L115+L134*L123+L123*L115+B114*L123+B114*L134+A114*L123+A114*L134,A114+L145*L140,B114+L145*L115,L147+K51+L115+L131+L124+L116+L146*L135+B115+L141*L135+L141*L116+L135*L124+L124*L116+B115*L124+B115*L135+A115*L124+A115*L135,A115+L146*L141,B115+L146*L116,L148+K52+L116+L132+L125+L117+L147*L136+B116+L142*L136+L142*L117+L136*L125+L125*L117+B116*L125+B116*L136+A116*L125+A116*L136,A116+L147*L142,B116+L147*L117,L149+K53+L117+L133+L126+L118+L148*L137+B117+L143*L137+L143*L118+L137*L126+L126*L118+B117*L126+B117*L137+A117*L126+A117*L137,A117+L148*L143,B117+L148*L118,L150+K54+L118+L134+L127+L119+L149*L138+B118+L144*L138+L144*L119+L138*L127+L127*L119+B118*L127+B118*L138+A118*L127+A118*L138,A118+L149*L144,B118+L149*L119,L151+K55+L119+L135+L128+L120+L150*L139+B119+L145*L139+L145*L120+L139*L128+L128*L120+B119*L128+B119*L139+A119*L128+A119*L139,A119+L150*L145,B119+L150*L120,L152+K56+L120+L136+L129+L121+L151*L140+B120+L146*L140+L146*L121+L140*L129+L129*L121+B120*L129+B120*L140+A120*L129+A120*L140,A120+L151*L146,B120+L151*L121,L153+K57+L121+L137+L130+L122+L152*L141+B121+L147*L141+L147*L122+L141*L130+L130*L122+B121*L130+B121*L141+A121*L130+A121*L141,A121+L152*L147,B121+L152*L122,L154+K58+L122+L138+L131+L123+L153*L142+B122+L148*L142+L148*L123+L142*L131+L131*L123+B122*L131+B122*L142+A122*L131+A122*L142,A122+L153*L148,B122+L153*L123,L155+K59+L123+L139+L132+L124+L154*L143+B123+L149*L143+L149*L124+L143*L132+L132*L124+B123*L132+B123*L143+A123*L132+A123*L143,A123+L154*L149,B123+L154*L124,L156+K60+L124+L140+L133+L125+L155*L144+B124+L150*L144+L150*L125+L144*L133+L133*L125+B124*L133+B124*L144+A124*L133+A124*L144,A124+L155*L150,B124+L155*L125,L157+K61+L125+L141+L134+L126+L156*L145+B125+L151*L145+L151*L126+L145*L134+L134*L126+B125*L134+B125*L145+A125*L134+A125*L145,A125+L156*L151,B125+L156*L126,L158+K62+L126+L142+L135+L127+L157*L146+B126+L152*L146+L152*L127+L146*L135+L135*L127+B126*L135+B126*L146+A126*L135+A126*L146,A126+L157*L152,B126+L157*L127,L159+K63+L127+L143+L136+L128+L158*L147+B127+L153*L147+L153*L128+L147*L136+L136*L128+B127*L136+B127*L147+A127*L136+A127*L147,A127+L158*L153,B127+L158*L128,L160+K0+L128+L144+L137+L129+L159*L148+B128+L154*L148+L154*L129+L148*L137+L137*L129+B128*L137+B128*L148+A128*L137+A128*L148,A128+L159*L154,B128+L159*L129,L161+K1+L129+L145+L138+L130+L160*L149+B129+L155*L149+L155*L130+L149*L138+L138*L130+B129*L138+B129*L149+A129*L138+A129*L149,A129+L160*L155,B129+L160*L130,L162+K2+L130+L146+L139+L131+L161*L150+B130+L156*L150+L156*L131+L150*L139+L139*L131+B130*L139+B130*L150+A130*L139+A130*L150,A130+L161*L156,B130+L161*L131,L163+K3+L131+L147+L140+L132+L162*L151+B131+L157*L151+L157*L132+L151*L140+L140*L132+B131*L140+B131*L151+A131*L140+A131*L151,A131+L162*L157,B131+L162*L132,L164+K4+L132+L148+L141+L133+L163*L152+B132+L158*L152+L158*L133+L152*L141+L141*L133+B132*L141+B132*L152+A132*L141+A132*L152,A132+L163*L158,B132+L163*L133,L165+K5+L133+L149+L142+L134+L164*L153+B133+L159*L153+L159*L134+L153*L142+L142*L134+B133*L142+B133*L153+A133*L142+A133*L153,A133+L164*L159,B133+L164*L134,L166+K6+L134+L150+L143+L135+L165*L154+B134+L160*L154+L160*L135+L154*L143+L143*L135+B134*L143+B134*L154+A134*L143+A134*L154,A134+L165*L160,B134+L165*L135,L167+K7+L135+L151+L144+L136+L166*L155+B135+L161*L155+L161*L136+L155*L144+L144*L136+B135*L144+B135*L155+A135*L144+A135*L155,A135+L166*L161,B135+L166*L136,L168+K8+L136+L152+L145+L137+L167*L156+B136+L162*L156+L162*L137+L156*L145+L145*L137+B136*L145+B136*L156+A136*L145+A136*L156,A136+L167*L162,B136+L167*L137,L169+K9+L137+L153+L146+L138+L168*L157+B137+L163*L157+L163*L138+L157*L146+L146*L138+B137*L146+B137*L157+A137*L146+A137*L157,A137+L168*L163,B137+L168*L138,L170+K10+L138+L154+L147+L139+L169*L158+B138+L164*L158+L164*L139+L158*L147+L147*L139+B138*L147+B138*L158+A138*L147+A138*L158,A138+L169*L164,B138+L169*L139,L171+K11+L139+L155+L148+L140+L170*L159+B139+L165*L159+L165*L140+L159*L148+L148*L140+B139*L148+B139*L159+A139*L148+A139*L159,A139+L170*L165,B139+L170*L140,L172+K12+L140+L156+L149+L141+L171*L160+B140+L166*L160+L166*L141+L160*L149+L149*L141+B140*L149+B140*L160+A140*L149+A140*L160,A140+L171*L166,B140+L171*L141,L173+K13+L141+L157+L150+L142+L172*L161+B141+L167*L161+L167*L142+L161*L150+L150*L142+B141*L150+B141*L161+A141*L150+A141*L161,A141+L172*L167,B141+L172*L142,L174+K14+L142+L158+L151+L143+L173*L162+B142+L168*L162+L168*L143+L162*L151+L151*L143+B142*L151+B142*L162+A142*L151+A142*L162,A142+L173*L168,B142+L173*L143,L175+K15+L143+L159+L152+L144+L174*L163+B143+L169*L163+L169*L144+L163*L152+L152*L144+B143*L152+B143*L163+A143*L152+A143*L163,A143+L174*L169,B143+L174*L144,L176+K16+L144+L160+L153+L145+L175*L164+B144+L170*L164+L170*L145+L164*L153+L153*L145+B144*L153+B144*L164+A144*L153+A144*L164,A144+L175*L170,B144+L175*L145,L177+K17+L145+L161+L154+L146+L176*L165+B145+L171*L165+L171*L146+L165*L154+L154*L146+B145*L154+B145*L165+A145*L154+A145*L165,A145+L176*L171,B145+L176*L146,L178+K18+L146+L162+L155+L147+L177*L166+B146+L172*L166+L172*L147+L166*L155+L155*L147+B146*L155+B146*L166+A146*L155+A146*L166,A146+L177*L172,B146+L177*L147,L179+K19+L147+L163+L156+L148+L178*L167+B147+L173*L167+L173*L148+L167*L156+L156*L148+B147*L156+B147*L167+A147*L156+A147*L167,A147+L178*L173,B147+L178*L148,L180+K20+L148+L164+L157+L149+L179*L168+B148+L174*L168+L174*L149+L168*L157+L157*L149+B148*L157+B148*L168+A148*L157+A148*L168,A148+L179*L174,B148+L179*L149,L181+K21+L149+L165+L158+L150+L180*L169+B149+L175*L169+L175*L150+L169*L158+L158*L150+B149*L158+B149*L169+A149*L158+A149*L169,A149+L180*L175,B149+L180*L150,L182+K22+L150+L166+L159+L151+L181*L170+B150+L176*L170+L176*L151+L170*L159+L159*L151+B150*L159+B150*L170+A150*L159+A150*L170,A150+L181*L176,B150+L181*L151,L183+K23+L151+L167+L160+L152+L182*L171+B151+L177*L171+L177*L152+L171*L160+L160*L152+B151*L160+B151*L171+A151*L160+A151*L171,A151+L182*L177,B151+L182*L152,L184+K24+L152+L168+L161+L153+L183*L172+B152+L178*L172+L178*L153+L172*L161+L161*L153+B152*L161+B152*L172+A152*L161+A152*L172,A152+L183*L178,B152+L183*L153,L185+K25+L153+L169+L162+L154+L184*L173+B153+L179*L173+L179*L154+L173*L162+L162*L154+B153*L162+B153*L173+A153*L162+A153*L173,A153+L184*L179,B153+L184*L154,L186+K26+L154+L170+L163+L155+L185*L174+B154+L180*L174+L180*L155+L174*L163+L163*L155+B154*L163+B154*L174+A154*L163+A154*L174,A154+L185*L180,B154+L185*L155,L187+K27+L155+L171+L164+L156+L186*L175+B155+L181*L175+L181*L156+L175*L164+L164*L156+B155*L164+B155*L175+A155*L164+A155*L175,A155+L186*L181,B155+L186*L156,L188+K28+L156+L172+L165+L157+L187*L176+B156+L182*L176+L182*L157+L176*L165+L165*L157+B156*L165+B156*L176+A156*L165+A156*L176,A156+L187*L182,B156+L187*L157,L189+K29+L157+L173+L166+L158+L188*L177+B157+L183*L177+L183*L158+L177*L166+L166*L158+B157*L166+B157*L177+A157*L166+A157*L177,A157+L188*L183,B157+L188*L158,L190+K30+L158+L174+L167+L159+L189*L178+B158+L184*L178+L184*L159+L178*L167+L167*L159+B158*L167+B158*L178+A158*L167+A158*L178,A158+L189*L184,B158+L189*L159,L191+K31+L159+L175+L168+L160+L190*L179+B159+L185*L179+L185*L160+L179*L168+L168*L160+B159*L168+B159*L179+A159*L168+A159*L179,A159+L190*L185,B159+L190*L160])
_ = solver.write()
print open(fn).read()
# write output of cnf to file (need to copy extra, doesn't output it all)
#
# f = file('/home/cahlen/Dropbox/keeloq/main160.cnf','w')
# f.write(open(fn).read())
# import sys
# sys.stdout = open('file', 'w')