OKlibrary  0.2.1.6
SchurProblems.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 17.4.2009 (Swansea) */
00002 /* Copyright 2009, 2012 Oliver Kullmann
00003 This file is part of the OKlibrary. OKlibrary is free software; you can redistribute
00004 it and/or modify it under the terms of the GNU General Public License as published by
00005 the Free Software Foundation and included in this library; either version 3 of the
00006 License, or any later version. */
00007 
00022 oklib_include("OKlib/ComputerAlgebra/Hypergraphs/Lisp/Generators/Schur.mac")$
00023 oklib_include("OKlib/ComputerAlgebra/Hypergraphs/Lisp/Colouring.mac")$
00024 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Generators/NonBooleanTranslations.mac")$
00025 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/NonBoolean.mac")$
00026 oklib_include("OKlib/ComputerAlgebra/NumberTheory/Lisp/Auxiliary.mac")$
00027 oklib_include("OKlib/ComputerAlgebra/RamseyTheory/Lisp/Schur/Numbers.mac")$
00028 oklib_include("OKlib/ComputerAlgebra/Hypergraphs/Lisp/SetSystems.mac")$
00029 oklib_include("OKlib/ComputerAlgebra/DataStructures/Lisp/Lists.mac")$
00030 oklib_include("OKlib/ComputerAlgebra/Combinatorics/Lisp/Enumeration/Permutations.mac")$
00031 
00032 
00033 /* *****************
00034    * Schur triples *
00035    *****************
00036 */
00037 
00038 /* The non-boolean formal clause-set expressing the Schur problem with
00039    r parts and n vertices (note that the subsumption-free hypergraph is used).
00040    Prerequisites: r, n natural numbers, n, r >= 0.
00041 */
00042 schur_nbfclud(r,n) := col2sat_stdohg2stdnbfclud(schurtriples_me_ohg(n), create_list(i,i,1,r))$
00043 schur_nbfcsud(r,n) :=
00044  nbfclud2nbfcsud(schur_nbfclud(r,n))$
00045 
00046 /* Statistics: */
00047 nvar_schur_nbfcsud(r,n) := nver_schurtriples_hg(n)$
00048 nval_schur_nbfcsud(r,n) := r$
00049 ncl_list_schur_nbfcsud(r,n) := if r=0 then [] else
00050  map(lambda([p],[p[1],r*p[2]]), nhyp_list_schurtriples_me_hg(n))$
00051 ncl_schur_nbfcsud(r,n) := r * nhyp_schurtriples_me_hg(n)$
00052 
00053 
00054 /* The palindromic forms: */
00055 pd_schur_nbfclud(r,n) := col2sat_stdohg2stdnbfclud(schurtriples_pd_ohg(n), create_list(i,i,1,r))$
00056 pd_schur_nbfcsud(r,n) :=
00057  nbfclud2nbfcsud(pd_schur_nbfclud(r,n))$
00058 
00059 /* Statistics: */
00060 nvar_pd_schur_nbfcsud(r,n) := nver_schurtriples_pd_hg(n)$
00061 
00062 
00063 /* The weak forms: */
00064 wschur_nbfclud(r,n) := col2sat_stdohg2stdnbfclud(wschurtriples_ohg(n), create_list(i,i,1,r))$
00065 wschur_nbfcsud(r,n) :=
00066  nbfclud2nbfcsud(wschur_nbfclud(r,n))$
00067 
00068 /* The palindromic weak forms: */
00069 pd_wschur_nbfclud(r,n) := col2sat_stdohg2stdnbfclud(wschurtriples_pd_ohg(n), create_list(i,i,1,r))$
00070 pd_wschur_nbfcsud(r,n) :=
00071  nbfclud2nbfcsud(pd_wschur_nbfclud(r,n))$
00072 
00073 /* Statistics: */
00074 nvar_pd_wschur_nbfcsud(r,n) := nver_wschurtriples_pd_hg(n)$
00075 
00076 
00077 /* *****************
00078    * Group triples *
00079    *****************
00080 */
00081 
00082 /* The modular form (in ZZ_{n+1}): */
00083 mschur_nbfclud(r,n) := col2sat_stdohg2stdnbfclud(mschurtriples_me_ohg(n), create_list(i,i,1,r))$
00084 mschur_nbfcsud(r,n) := col2sat_stdhg2stdnbfcsud(mschurtriples_me_hg(n), setn(r))$
00085 
00086 wmschur_nbfclud(r,n) := col2sat_stdohg2stdnbfclud(wmschurtriples_ohg(n), create_list(i,i,1,r))$
00087 wmschur_nbfcsud(r,n) := col2sat_stdhg2stdnbfcsud(wmschurtriples_hg(n), setn(r))$
00088 
00089 
00090 /* Using the symmetric groups instead of the cyclic groups: */
00091 symmetrictriples_nbfclud(r,n) := col2sat_stdohg2stdnbfclud(symmetrictriples_me_ohg(n), create_list(i,i,1,r))$
00092 symmetrictriples_nbfcsud(r,n) := col2sat_stdhg2stdnbfcsud(symmetrictriples_me_hg(n), setn(r))$
00093 
00094 wsymmetrictriples_nbfclud(r,n) := col2sat_stdohg2stdnbfclud(wsymmetrictriples_ohg(n), create_list(i,i,1,r))$
00095 wsymmetrictriples_nbfcsud(r,n) := col2sat_stdhg2stdnbfcsud(wsymmetrictriples_hg(n), create_list(i,i,1,r))$
00096 
00097 
00098 /* *********************
00099    * Symmetry breaking *
00100    *********************
00101 */
00102 
00103 /* Note:
00104     - These clause-sets contain unit-clauses (and are thus not
00105       subsumption-free).
00106 */
00107 
00108 /* Adding symmetry-breaking clauses (regarding the parts (colours)), forcing
00109    vertex 1 to be in part 1; now we must have n >= 1:
00110 */
00111 schur_set_first_vertex_nbcl(r) := create_list({[1,i]},i,2,r)$
00112 
00113 schur_sb_nbfclud(r,n) := block([S : schur_nbfclud(r,n)],
00114  [S[1], append(schur_set_first_vertex_nbcl(r), S[2]), S[3]])$
00115 schur_sb_nbfcsud(r,n) := nbfclud2nbfcsud(schur_sb_nbfclud(r,n))$
00116 
00117 wschur_sb_nbfclud(r,n) := block([S : wschur_nbfclud(r,n)],
00118  [S[1], append(schur_set_first_vertex_nbcl(r), S[2]), S[3]])$
00119 wschur_sb_nbfcsud(r,n) := nbfclud2nbfcsud(wschur_sb_nbfclud(r,n))$
00120 
00121 
00122 /* ****************************
00123    * Heuristical restrictions *
00124    ****************************
00125 */
00126 
00127 /* "Full symmetry-breaking"
00128 
00129    The idea is as follows: Consider r parts (colours), we know that
00130    a valid partition of the first schur(r-1) vertices must use all r
00131    parts --- the (heuristical) principle is now to place vertex schur(r-1)
00132    in part r, and to do that for all 1 <= r' <= r.
00133 */
00134 
00135 /* Strengthening schur_set_first_vertex_nbcl(r): */
00136 schur_fullsb_nbcl(r,n) := block(
00137  [L : sublist(create_list(seconde(schur(i)),i,0,r-1),
00138               lambda([x], is(x <= n)))],
00139   listify(singletons(lunion(
00140     map(cartesian_product,
00141         map(set, L),
00142         create_list(disjoin(i,setn(r)),i,1,length(L)))))))$
00143 
00144 schur_fullsb_nbfclud(r,n) := block([S : schur_nbfclud(r,n)],
00145  [S[1], append(schur_fullsb_nbcl(r,n), S[2]), S[3]])$
00146 schur_fullsb_nbfcsud(r,n) := nbfclud2nbfcsud(schur_fullsb_nbfclud(r,n))$
00147 
00148 wschur_fullsb_nbcl(r,n) := block(
00149  [L : sublist(create_list(seconde(wschur(i)),i,0,r-1),
00150               lambda([x], is(x <= n)))],
00151   listify(singletons(lunion(
00152     map(cartesian_product,
00153         map(set, L),
00154         create_list(disjoin(i,setn(r)),i,1,length(L)))))))$
00155 
00156 wschur_fullsb_nbfclud(r,n) := block([S : wschur_nbfclud(r,n)],
00157  [S[1], append(wschur_fullsb_nbcl(r,n), S[2]), S[3]])$
00158 wschur_fullsb_nbfcsud(r,n) := nbfclud2nbfcsud(wschur_fullsb_nbfclud(r,n))$
00159 
00160 /* Palindromic forms: */
00161 pd_schur_fullsb_nbfclud(r,n) := block([S : pd_schur_nbfclud(r,n)],
00162  [S[1], append(schur_fullsb_nbcl(r,ceiling(n/2)), S[2]), S[3]])$
00163 pd_schur_fullsb_nbfcsud(r,n) := nbfclud2nbfcsud(pd_schur_fullsb_nbfclud(r,n))$
00164 
00165 pd_wschur_fullsb_nbfclud(r,n) := block([S : pd_wschur_nbfclud(r,n)],
00166  [S[1], append(wschur_fullsb_nbcl(r,ceiling(n/2)), S[2]), S[3]])$
00167 pd_wschur_fullsb_nbfcsud(r,n) := nbfclud2nbfcsud(pd_wschur_fullsb_nbfclud(r,n))$
00168 
00169 
00170 /* Removing the first k vertices from the last part (colour; we must
00171    have r >= 1, n >= k): The observation here is that apparently this
00172    "often" can be done "w.l.o.g.", or at least it yields good restrictions
00173    worth to study.
00174 
00175 */
00176 schur_remove_first_vertices_nbcl(k,r) := create_list({[i,r]},i,1,k)$
00177 
00178 schur_rm_nbfclud(r,n,k) := block([S : schur_nbfclud(r,n)],
00179  [S[1], append(schur_remove_first_vertices_nbcl(k,r), S[2]), S[3]])$
00180 schur_rm_nbfcsud(r,n,k) := nbfclud2nbfcsud(schur_rm_nbfclud(r,n,k))$
00181 
00182 /* Remarks:
00183     - These clause-sets contain unit-clauses (and are thus not
00184       subsumption-free).
00185     - Removing from the last part is compatible with full symmetry-breaking
00186       (according to schur_fullsb_nbfclud).
00187 */
00188 
00189 /* Palindromic forms (here k <= ceiling(n/2) must hold): */
00190 
00191 pd_schur_rm_nbfclud(r,n,k) := block([S : pd_schur_nbfclud(r,n)],
00192  [S[1], append(schur_remove_first_vertices_nbcl(k,r), S[2]), S[3]])$
00193 pd_schur_rm_nbfcsud(r,n,k) := nbfclud2nbfcsud(pd_schur_rm_nbfclud(r,n,k))$
00194 
00195 pd_schur_fullsb_rm_nbfclud(r,n,k) := block([S : pd_schur_rm_nbfclud(r,n,k)],
00196  [S[1], append(schur_fullsb_nbcl(r,ceiling(n/2)), S[2]), S[3]])$
00197 pd_schur_fullsb_rm_nbfcsud(r,n,k) := nbfclud2nbfcsud(pd_schur_fullsb_rm_nbfclud(r,n,k))$
00198 
00199 
00200 /* ****************************************
00201    * Translation into boolean clause-sets *
00202    ****************************************
00203 */
00204 
00205 /* Strong direct translation: */
00206 
00207 schur_aloamo_fcl(r,n) := nbfclud2fcl_aloamo(schur_nbfclud(r,n))$
00208 schur_aloamo_fcs(r,n) := fcl2fcs(schur_aloamo_fcl(r,n))$
00209 
00210 pd_schur_aloamo_fcl(r,n) := nbfclud2fcl_aloamo(pd_schur_nbfclud(r,n))$
00211 pd_schur_aloamo_fcs(r,n) := fcl2fcs(pd_schur_aloamo_fcl(r,n))$
00212 
00213 wschur_aloamo_fcl(r,n) := nbfclud2fcl_aloamo(wschur_nbfclud(r,n))$
00214 wschur_aloamo_fcs(r,n) := fcl2fcs(wschur_aloamo_fcl(r,n))$
00215 
00216 pd_wschur_aloamo_fcl(r,n) := nbfclud2fcl_aloamo(pd_wschur_nbfclud(r,n))$
00217 pd_wschur_aloamo_fcs(r,n) := fcl2fcs(pd_wschur_aloamo_fcl(r,n))$
00218 
00219 
00220 mschur_aloamo_fcl(r,n) := nbfclud2fcl_aloamo(mschur_nbfclud(r,n))$
00221 mschur_aloamo_fcs(r,n) := nbfcsud2fcs_aloamo(mschur_nbfcsud(r,n))$
00222 
00223 wmschur_aloamo_fcl(r,n) := nbfclud2fcl_aloamo(wmschur_nbfclud(r,n))$
00224 wmschur_aloamo_fcs(r,n) := nbfcsud2fcs_aloamo(wmschur_nbfcsud(r,n))$
00225 
00226 symmetrictriples_aloamo_fcl(r,n) := nbfclud2fcl_aloamo(symmetrictriples_nbfclud(r,n))$
00227 symmetrictriples_aloamo_fcs(r,n) := nbfcsud2fcs_aloamo(symmetrictriples_nbfcsud(r,n))$
00228 
00229 wsymmetrictriples_aloamo_fcl(r,n) := nbfclud2fcl_aloamo(wsymmetrictriples_nbfclud(r,n))$
00230 wsymmetrictriples_aloamo_fcs(r,n) := nbfcsud2fcs_aloamo(wsymmetrictriples_nbfcsud(r,n))$
00231 
00232 
00233 schur_sb_aloamo_fcl(r,n) := nbfclud2fcl_aloamo(schur_sb_nbfclud(r,n))$
00234 schur_sb_aloamo_fcs(r,n) := fcl2fcs(schur_sb_aloamo_fcl(r,n))$
00235 
00236 wschur_sb_aloamo_fcl(r,n) := nbfclud2fcl_aloamo(wschur_sb_nbfclud(r,n))$
00237 wschur_sb_aloamo_fcs(r,n) := fcl2fcs(wschur_sb_aloamo_fcl(r,n))$
00238 
00239 schur_fullsb_aloamo_fcl(r,n) := nbfclud2fcl_aloamo(schur_fullsb_nbfclud(r,n))$
00240 schur_fullsb_aloamo_fcs(r,n) := fcl2fcs(schur_fullsb_aloamo_fcl(r,n))$
00241 
00242 wschur_fullsb_aloamo_fcl(r,n) := nbfclud2fcl_aloamo(wschur_fullsb_nbfclud(r,n))$
00243 wschur_fullsb_aloamo_fcs(r,n) := fcl2fcs(wschur_fullsb_aloamo_fcl(r,n))$
00244 
00245 pd_schur_fullsb_aloamo_fcl(r,n) := nbfclud2fcl_aloamo(pd_schur_fullsb_nbfclud(r,n))$
00246 pd_schur_fullsb_aloamo_fcs(r,n) := fcl2fcs(pd_schur_fullsb_aloamo_fcl(r,n))$
00247 
00248 pd_wschur_fullsb_aloamo_fcl(r,n) := nbfclud2fcl_aloamo(pd_wschur_fullsb_nbfclud(r,n))$
00249 pd_wschur_fullsb_aloamo_fcs(r,n) := fcl2fcs(pd_wschur_fullsb_aloamo_fcl(r,n))$
00250 
00251 
00252 schur_rm_aloamo_fcl(r,n,k) := nbfclud2fcl_aloamo(schur_rm_nbfclud(r,n,k))$
00253 schur_rm_aloamo_fcs(r,n,k) := fcl2fcs(schur_rm_aloamo_fcl(r,n,k))$
00254 
00255 pd_schur_rm_aloamo_fcl(r,n,k) := nbfclud2fcl_aloamo(pd_schur_rm_nbfclud(r,n,k))$
00256 pd_schur_rm_aloamo_fcs(r,n,k) := fcl2fcs(pd_schur_rm_aloamo_fcl(r,n,k))$
00257 
00258 pd_schur_fullsb_rm_aloamo_fcl(r,n,k) := nbfclud2fcl_aloamo(pd_schur_fullsb_rm_nbfclud(r,n,k))$
00259 pd_schur_fullsb_rm_aloamo_fcs(r,n,k) := fcl2fcs(pd_schur_fullsb_rm_aloamo_fcl(r,n,k))$
00260 
00261 
00262 
00263 /* Statistics: */
00264 nvar_schur_aloamo_fcl(r,n) :=
00265  nvar_schur_nbfcsud(r,n) * nval_schur_nbfcsud(r,n)$
00266 nvar_schur_aloamo_fcs(r,n) := nvar_schur_aloamo_fcl(r,n)$
00267 ncl_list_schur_aloamo_fcl(r,n) := if n=0 then []
00268  elseif r=0 then [[0,n]]
00269  elseif r=1 then cons([1,n], ncl_list_schur_nbfcsud(r,n))
00270  elseif n=1 then if r=2 then [[2,2]] else [[2,binomial(r,2)],[r,1]]
00271  elseif n<=3 then if r=2 then [[2,2+2*n]] else [[2,r+n*binomial(r,2)],[r,n]]
00272  else block([C2,C3],  /* now n >= 4, r >= 2 */
00273   [C2,C3] : map(second,ncl_list_schur_nbfcsud(r,n)),
00274   if r=2 then [[2,C2+n+n], [3,C3]]
00275   elseif r=3 then [[2,C2+3*n],[3,C3+n]]
00276   else [[2,C2+n*binomial(r,2)],[3,C3],[r,n]])$
00277 ncl_list_schur_aloamo_fcs(r,n) := if n=0 then []
00278  elseif r=0 then [[0,1]] else ncl_list_schur_aloamo_fcl(r,n)$
00279 
00280 
00281 /* Weak and strong standard nested translation
00282    (now r >= 1 must hold):
00283 */
00284 
00285 schur_standnest_fcl(r,n) := nbfclud2fcl_standnest(schur_nbfclud(r,n))$
00286 schur_standnest_fcs(r,n) := fcl2fcs(schur_standnest_fcl(r,n))$
00287 
00288 schur_standnest_strong_fcl(r,n) := nbfclud2fcl_standnest_strong(schur_nbfclud(r,n))$
00289 schur_standnest_strong_fcs(r,n) := fcl2fcs(schur_standnest_strong_fcl(r,n))$
00290 
00291 
00292 /* Logarithmic translation
00293    (now r >= 1 must hold):
00294 */
00295 
00296 schur_logarithmic_fcl(r,n) := nbfclud2fcl_logarithmic(schur_nbfclud(r,n))$
00297 schur_logarithmic_fcs(r,n) := fcl2fcs(schur_logarithmic_fcl(r,n))$
00298 
00299 
00300 
00301 /* *******************
00302    * Standardisation *
00303    *******************
00304 */
00305 
00306 /* Direct translation: */
00307 
00308 schur_aloamo_stdfcl(r,n) := (
00309   [block([s : standardise_schur_aloamo(r,n)],
00310      s(schur_aloamo_fcl(r,n))),
00311    block([invs : invstandardise_schur_aloamo(r,n)],
00312      create_list(invs(i), i,1,n*r))])$
00313 /* We have schur_aloamo_stdfcl(r,n) =
00314    standardise_fcl(schur_aloamo_fcl(r,n)).
00315 */
00316 
00317 pd_schur_aloamo_stdfcl(r,n) := (
00318   [block([s : standardise_pd_schur_aloamo(r,n)],
00319      s(pd_schur_aloamo_fcl(r,n))),
00320    block([invs : invstandardise_pd_schur_aloamo(r,n)],
00321      create_list(invs(i), i,1,nvar_pd_schur_nbfcsud(r,n)*r))])$
00322 /* We have pd_schur_aloamo_stdfcl(r,n) =
00323    standardise_fcl(pd_schur_aloamo_fcl(r,n)).
00324 */
00325 
00326 wschur_aloamo_stdfcl(r,n) := (
00327   [block([s : standardise_schur_aloamo(r,n)],
00328      s(wschur_aloamo_fcl(r,n))),
00329    block([invs : invstandardise_schur_aloamo(r,n)],
00330      create_list(invs(i), i,1,n*r))])$
00331 /* We have wschur_aloamo_stdfcl(r,n) =
00332    standardise_fcl(wschur_aloamo_fcl(r,n)).
00333 */
00334 
00335 pd_wschur_aloamo_stdfcl(r,n) := (
00336   [block([s : standardise_pd_wschur_aloamo(r,n)],
00337      s(pd_wschur_aloamo_fcl(r,n))),
00338    block([invs : invstandardise_pd_wschur_aloamo(r,n)],
00339      create_list(invs(i), i,1,nvar_pd_wschur_nbfcsud(r,n)*r))])$
00340 /* We have pd_wschur_aloamo_stdfcl(r,n) =
00341    standardise_fcl(pd_wschur_aloamo_fcl(r,n)).
00342 */
00343 
00344 
00345 mschur_aloamo_stdfcl(r,n) := (
00346   [block([s : standardise_schur_aloamo(r,n)],
00347      s(mschur_aloamo_fcl(r,n))),
00348    block([invs : invstandardise_schur_aloamo(r,n)],
00349      create_list(invs(i), i,1,n*r))])$
00350 /* We have mschur_aloamo_stdfcl(r,n) =
00351    standardise_fcl(mschur_aloamo_fcl(r,n)).
00352 */
00353 
00354 wmschur_aloamo_stdfcl(r,n) := (
00355   [block([s : standardise_schur_aloamo(r,n)],
00356      s(wmschur_aloamo_fcl(r,n))),
00357    block([invs : invstandardise_schur_aloamo(r,n)],
00358      create_list(invs(i), i,1,n*r))])$
00359 /* We have wmschur_aloamo_stdfcl(r,n) =
00360    standardise_fcl(wmschur_aloamo_fcl(r,n)).
00361 */
00362 
00363 symmetrictriples_aloamo_stdfcl(r,n) := (
00364   [block([s : standardise_symmetrictriples_aloamo(r,n)],
00365      s(symmetrictriples_aloamo_fcl(r,n))),
00366    block([invs : invstandardise_symmetrictriples_aloamo(r,n)],
00367      create_list(invs(i), i,1,(n!-1)*r))])$
00368 /* We have symmetrictriples_aloamo_stdfcl(r,n) =
00369    standardise_fcl(symmetrictriples_aloamo_fcl(r,n)).
00370 */
00371 
00372 wsymmetrictriples_aloamo_stdfcl(r,n) := (
00373   [block([s : standardise_symmetrictriples_aloamo(r,n)],
00374      s(wsymmetrictriples_aloamo_fcl(r,n))),
00375    block([invs : invstandardise_symmetrictriples_aloamo(r,n)],
00376      create_list(invs(i), i,1,(n!-1)*r))])$
00377 /* We have wsymmetrictriples_aloamo_stdfcl(r,n) =
00378    standardise_fcl(wsymmetrictriples_aloamo_fcl(r,n)).
00379 */
00380 
00381 
00382 schur_sb_aloamo_stdfcl(r,n) := (
00383   [block([s : standardise_schur_aloamo(r,n)],
00384      s(schur_sb_aloamo_fcl(r,n))),
00385    block([invs : invstandardise_schur_aloamo(r,n)],
00386      create_list(invs(i), i,1,n*r))])$
00387 /* We have schur_sb_aloamo_stdfcl(r,n) =
00388    standardise_fcl(schur_sb_aloamo_fcl(r,n)).
00389 */
00390 
00391 wschur_sb_aloamo_stdfcl(r,n) := (
00392   [block([s : standardise_schur_aloamo(r,n)],
00393      s(wschur_sb_aloamo_fcl(r,n))),
00394    block([invs : invstandardise_schur_aloamo(r,n)],
00395      create_list(invs(i), i,1,n*r))])$
00396 /* We have wschur_sb_aloamo_stdfcl(r,n) =
00397    standardise_fcl(wschur_sb_aloamo_fcl(r,n)).
00398 */
00399 
00400 schur_fullsb_aloamo_stdfcl(r,n) := (
00401   [block([s : standardise_schur_aloamo(r,n)],
00402      s(schur_fullsb_aloamo_fcl(r,n))),
00403    block([invs : invstandardise_schur_aloamo(r,n)],
00404      create_list(invs(i), i,1,n*r))])$
00405 /* We have schur_fullsb_aloamo_stdfcl(r,n) =
00406    standardise_fcl(schur_fullsb_aloamo_fcl(r,n)).
00407 */
00408 
00409 wschur_fullsb_aloamo_stdfcl(r,n) := (
00410   [block([s : standardise_schur_aloamo(r,n)],
00411      s(wschur_fullsb_aloamo_fcl(r,n))),
00412    block([invs : invstandardise_schur_aloamo(r,n)],
00413      create_list(invs(i), i,1,n*r))])$
00414 /* We have wschur_fullsb_aloamo_stdfcl(r,n) =
00415    standardise_fcl(wschur_fullsb_aloamo_fcl(r,n)).
00416 */
00417 
00418 pd_schur_fullsb_aloamo_stdfcl(r,n) := (
00419   [block([s : standardise_pd_schur_aloamo(r,n)],
00420      s(pd_schur_fullsb_aloamo_fcl(r,n))),
00421    block([invs : invstandardise_pd_schur_aloamo(r,n)],
00422      create_list(invs(i), i,1,nvar_pd_schur_nbfcsud(r,n)*r))])$
00423 /* We have pd_schur_fullsb_aloamo_stdfcl(r,n) =
00424    standardise_fcl(pd_schur_fullsb_aloamo_fcl(r,n)).
00425 */
00426 
00427 pd_wschur_fullsb_aloamo_stdfcl(r,n) := (
00428   [block([s : standardise_pd_wschur_aloamo(r,n)],
00429      s(pd_wschur_fullsb_aloamo_fcl(r,n))),
00430    block([invs : invstandardise_pd_wschur_aloamo(r,n)],
00431      create_list(invs(i), i,1,nvar_pd_wschur_nbfcsud(r,n)*r))])$
00432 /* We have pd_wschur_fullsb_aloamo_stdfcl(r,n) =
00433    standardise_fcl(pd_wschur_fullsb_aloamo_fcl(r,n)).
00434 */
00435 
00436 
00437 schur_rm_aloamo_stdfcl(r,n,k) := (
00438   [block([s : standardise_schur_aloamo(r,n)],
00439      s(schur_rm_aloamo_fcl(r,n,k))),
00440    block([invs : invstandardise_schur_aloamo(r,n)],
00441      create_list(invs(i), i,1,n*r))])$
00442 /* We have schur_rm_aloamo_stdfcl(r,n,k) =
00443    standardise_fcl(schur_rm_aloamo_fcl(r,n,k)).
00444 */
00445 
00446 pd_schur_rm_aloamo_stdfcl(r,n,k) := (
00447   [block([s : standardise_pd_schur_aloamo(r,n)],
00448      s(pd_schur_rm_aloamo_fcl(r,n,k))),
00449    block([invs : invstandardise_pd_schur_aloamo(r,n)],
00450      create_list(invs(i), i,1,nvar_pd_schur_nbfcsud(r,n)*r))])$
00451 /* We have pd_schur_rm_aloamo_stdfcl(r,n,k) =
00452    standardise_fcl(pd_schur_rm_aloamo_fcl(r,n,k)).
00453 */
00454 
00455 pd_schur_fullsb_rm_aloamo_stdfcl(r,n,k) := (
00456   [block([s : standardise_pd_schur_aloamo(r,n)],
00457      s(pd_schur_fullsb_rm_aloamo_fcl(r,n,k))),
00458    block([invs : invstandardise_pd_schur_aloamo(r,n)],
00459      create_list(invs(i), i,1,nvar_pd_schur_nbfcsud(r,n)*r))])$
00460 /* We have pd_schur_fullsb_rm_aloamo_stdfcl(r,n,k) =
00461    standardise_fcl(pd_schur_fullsb_rm_aloamo_fcl(r,n,k)).
00462 */
00463 
00464 
00465 /* Translation functions for standardising resp. de-standardising
00466    terms resp. individual variables:
00467 */
00468 standardise_schur_aloamo(r,n) :=
00469   buildq([r], lambda([t], ev(t, nbv(v,i):=(v-1)*r+i, nbv)))$
00470 invstandardise_schur_aloamo(r,n) :=
00471   buildq([r], lambda([i], block([d : divide(i-1,r)+1],
00472     nbv_var(d[1], d[2]))))$
00473 
00474 standardise_pd_schur_aloamo(r,n) := if mod(n+1,3)#0 then
00475   buildq([r], lambda([t], ev(t, nbv(v,i):=(v-1)*r+i, nbv)))
00476  else
00477   buildq([r,excl:2*(n+1)/3,repl:ceiling(n/2)],
00478    lambda([t], ev(t, nbv(v,i):= if v=excl then repl*r+i else (v-1)*r+i, nbv)))$
00479 invstandardise_pd_schur_aloamo(r,n) := if mod(n+1,3)#0 then
00480   buildq([r], lambda([i], block([d : divide(i-1,r)+1], nbv_var(d[1], d[2]))))
00481  else
00482   buildq([r,excp:ceiling(n/2)+1,repl:2*(n+1)/3], lambda([i], block([d : divide(i-1,r)+1], nbv_var(if d[1]#excp then d[1] else repl, d[2]))))$
00483 
00484 standardise_pd_wschur_aloamo(r,n) := standardise_schur_aloamo(r,ceiling(n/2))$
00485 invstandardise_pd_wschur_aloamo(r,n) := invstandardise_schur_aloamo(r,ceiling(n/2))$
00486 
00487 standardise_symmetrictriples_aloamo(r,n) :=
00488   buildq([r], lambda([t], ev(t, nbv(t,i):=(rank_lex_permutations(t)-2)*r+i, nbv)))$
00489 invstandardise_symmetrictriples_aloamo(r,n) :=
00490   buildq([r,n], lambda([i], block([d : divide(i-1,r)+1],
00491     nbv_var(unrank_lex_permutations(d[1]+1,n), d[2]))))$
00492 
00493 
00494 /* Weak and strong standard nested translation; now r >= 1 must hold: */
00495 
00496 schur_standnest_stdfcl(r,n) :=
00497   [block([s : standardise_schur_standnest(r,n)],
00498      s(schur_standnest_fcl(r,n))),
00499    block([invs : invstandardise_schur_standnest(r,n)],
00500      create_list(invs(i), i,1,n*(r-1)))]$
00501 /* We have schur_standnest_stdfcl(r,n) =
00502    standardise_fcl(schur_standnest_fcl(r,n)).
00503 */
00504 schur_standnest_stdfcs(r,n) := block(
00505  [FF : schur_standnest_stdfcl(r,n)],
00506   [fcl2fcs(FF[1]), FF[2]])$
00507 
00508 schur_standnest_strong_stdfcl(r,n) :=
00509   [block([s : standardise_schur_standnest(r,n)],
00510      s(schur_standnest_strong_fcl(r,n))),
00511    block([invs : invstandardise_schur_standnest(r,n)],
00512      create_list(invs(i), i,1,n*(r-1)))]$
00513 /* We have schur_standnest_strong_stdfcl(r,n) =
00514    standardise_fcl(schur_standnest_strong_fcl(r,n)).
00515 */
00516 schur_standnest_strong_stdfcs(r,n) := block(
00517  [FF : schur_standnest_strong_stdfcl(r,n)],
00518   [fcl2fcs(FF[1]), FF[2]])$
00519 
00520 /* Translation functions for standardising resp. de-standardising
00521    terms resp. individual variables:
00522 */
00523 standardise_schur_standnest(r,n) :=
00524   buildq([r], lambda([t], ev(t, nbv(v,i):=(v-1)*(r-1)+i, nbv)))$
00525 invstandardise_schur_standnest(r,n) :=
00526   buildq([r], lambda([i], block([d : divide(i-1,r-1)+1],
00527     nbv_var(d[1], d[2]))))$
00528 
00529 
00530 /* Logarithmic translation; now r >= 1 must hold: */
00531 
00532 schur_logarithmic_stdfcl(r,n) :=
00533   [block([s : standardise_schur_logarithmic(r,n)],
00534      s(schur_logarithmic_fcl(r,n))),
00535    block([invs : invstandardise_schur_logarithmic(r,n)],
00536      create_list(invs(i), i,1,n*(r-1)))]$
00537 /* We have schur_logarithmic_stdfcl(r,n) =
00538    standardise_fcl(schur_logarithmic_fcl(r,n)).
00539 */
00540 schur_logarithmic_stdfcs(r,n) := block(
00541  [FF : schur_logarithmic_stdfcl(r,n)],
00542   [fcl2fcs(FF[1]), FF[2]])$
00543 
00544 /* Translation functions for standardising resp. de-standardising
00545    terms resp. individual variables:
00546 */
00547 standardise_schur_logarithmic(r,n) :=
00548   buildq([m:cld(r)], lambda([t], ev(t, nbv(v,i):=(v-1)*m+i, nbv)))$
00549 
00550 invstandardise_schur_logarithmic(r,n) :=
00551   buildq([m:cld(r)], lambda([i], block([d : divide(i-1,m)+1],
00552     nbv_var(d[1], d[2]))))$
00553 
00554 
00555 /* **********
00556    * Output *
00557    **********
00558 */
00559 
00560 /* Output the direct translation to a file: */
00561 output_schur(r,n,filename) := block(
00562  [FF : schur_aloamo_stdfcl(r,n)],
00563   output_fcl_v(
00564     sconcat("Schur problem with ", r, " parts and ", n, " elements, using the direct (strong) translation.", newline, "c ", "Created by output_schur(", r, ",", n, ",\"", filename, "\").", newline, "c ", created_by_OKlib()),
00565     FF[1],
00566     filename,
00567     FF[2]))$
00568 /* Providing a standard name: "Schur_r_n.cnf": */
00569 output_schur_stdname(r,n) := output_schur(r,n,
00570   sconcat("Schur_",r,"_",n,".cnf"))$
00571 
00572 output_pd_schur(r,n,filename) := block(
00573  [FF : pd_schur_aloamo_stdfcl(r,n)],
00574   output_fcl_v(
00575     sconcat("Palindromic Schur problem with ", r, " parts and ", n, " elements, using the direct (strong) translation.", newline, "c ", "Created by output_pd_schur(", r, ",", n, ",\"", filename, "\").", newline, "c ", created_by_OKlib()),
00576     FF[1],
00577     filename,
00578     FF[2]))$
00579 /* Providing a standard name: "Schur_pd_r_n.cnf": */
00580 output_pd_schur_stdname(r,n) := output_pd_schur(r,n,
00581   sconcat("Schur_pd_",r,"_",n,".cnf"))$
00582 
00583 output_wschur(r,n,filename) := block(
00584  [FF : wschur_aloamo_stdfcl(r,n)],
00585   output_fcl_v(
00586     sconcat("Weak Schur problem with ", r, " parts and ", n, " elements, using the direct (strong) translation.", newline, "c ", "Created by output_wschur(", r, ",", n, ",\"", filename, "\").", newline, "c ", created_by_OKlib()),
00587     FF[1],
00588     filename,
00589     FF[2]))$
00590 /* Providing a standard name: "WSchur_r_n.cnf": */
00591 output_wschur_stdname(r,n) := output_wschur(r,n,
00592   sconcat("WSchur_",r,"_",n,".cnf"))$
00593 
00594 output_pd_wschur(r,n,filename) := block(
00595  [FF : pd_wschur_aloamo_stdfcl(r,n)],
00596   output_fcl_v(
00597     sconcat("Palindromic weak Schur problem with ", r, " parts and ", n, " elements, using the direct (strong) translation.", newline, "c ", "Created by output_pd_wschur(", r, ",", n, ",\"", filename, "\").", newline, "c ", created_by_OKlib()),
00598     FF[1],
00599     filename,
00600     FF[2]))$
00601 /* Providing a standard name: "WSchur_pd_r_n.cnf": */
00602 output_pd_wschur_stdname(r,n) := output_pd_wschur(r,n,
00603   sconcat("WSchur_pd_",r,"_",n,".cnf"))$
00604 
00605 
00606 output_mschur(r,n,filename) := block(
00607  [FF : mschur_aloamo_stdfcl(r,n)],
00608   output_fcl_v(
00609     sconcat("Modular Schur problem with ", r, " parts and ", n, " elements, using the direct (strong) translation.", newline, "c ", "Created by output_mschur(", r, ",", n, ",\"", filename, "\").", newline, "c ", created_by_OKlib()),
00610     FF[1],
00611     filename,
00612     FF[2]))$
00613 /* Providing a standard name: "MSchur_r_n.cnf": */
00614 output_mschur_stdname(r,n) := output_mschur(r,n,
00615   sconcat("MSchur_",r,"_",n,".cnf"))$
00616 
00617 output_wmschur(r,n,filename) := block(
00618  [FF : wmschur_aloamo_stdfcl(r,n)],
00619   output_fcl_v(
00620     sconcat("Weak modular Schur problem with ", r, " parts and ", n, " elements, using the direct (strong) translation.", newline, "c ", "Created by output_wmschur(", r, ",", n, ",\"", filename, "\").", newline, "c ", created_by_OKlib()),
00621     FF[1],
00622     filename,
00623     FF[2]))$
00624 /* Providing a standard name: "WMSchur_r_n.cnf": */
00625 output_wmschur_stdname(r,n) := output_wmschur(r,n,
00626   sconcat("WMSchur_",r,"_",n,".cnf"))$
00627 
00628 output_symmetrictriples(r,n,filename) := block(
00629  [FF : symmetrictriples_aloamo_stdfcl(r,n)],
00630   output_fcl_v(
00631     sconcat("Symmetric-group Schur problem with ", r, " parts and ", n, " elements, using the direct (strong) translation.", newline, "c ", "Created by output_symmetrictriples(", r, ",", n, ",\"", filename, "\").", newline, "c ", created_by_OKlib()),
00632     FF[1],
00633     filename,
00634     FF[2]))$
00635 /* Providing a standard name: "SgSchur_r_n.cnf": */
00636 output_symmetrictriples_stdname(r,n) := output_symmetrictriples(r,n,
00637   sconcat("SgSchur_",r,"_",n,".cnf"))$
00638 
00639 output_wsymmetrictriples(r,n,filename) := block(
00640  [FF : wsymmetrictriples_aloamo_stdfcl(r,n)],
00641   output_fcl_v(
00642     sconcat("Weak symmetic-group Schur problem with ", r, " parts and ", n, " elements, using the direct (strong) translation.", newline, "c ", "Created by output_wsymmetrictriples(", r, ",", n, ",\"", filename, "\").", newline, "c ", created_by_OKlib()),
00643     FF[1],
00644     filename,
00645     FF[2]))$
00646 /* Providing a standard name: "WSgSchur_r_n.cnf": */
00647 output_wsymmetrictriples_stdname(r,n) := output_wsymmetrictriples(r,n,
00648   sconcat("WSgSchur_",r,"_",n,".cnf"))$
00649 
00650 
00651 output_schur_sb(r,n,filename) := block(
00652  [FF : schur_sb_aloamo_stdfcl(r,n)],
00653   output_fcl_v(
00654     sconcat("Schur problem with ", r, " parts and ", n, " elements, using the direct (strong) translation.", newline, "c Symmetry breaking by putting element 1 into part 1.", newline, "c ", "Created by output_schur_sb(", r, ",", n, ",\"", filename, "\").", newline, "c ", created_by_OKlib()),
00655     FF[1],
00656     filename,
00657     FF[2]))$
00658 /* Providing a standard name: "Schur_sb_r_n.cnf": */
00659 output_schur_sb_stdname(r,n) := output_schur_sb(r,n,
00660   sconcat("Schur_sb_",r,"_",n,".cnf"))$
00661 
00662 output_wschur_sb(r,n,filename) := block(
00663  [FF : wschur_sb_aloamo_stdfcl(r,n)],
00664   output_fcl_v(
00665     sconcat("Weak Schur problem with ", r, " parts and ", n, " elements, using the direct (strong) translation.", newline, "c Symmetry breaking by putting element 1 into part 1.", newline, "c ", "Created by output_wschur_sb(", r, ",", n, ",\"", filename, "\").", newline, "c ", created_by_OKlib()),
00666     FF[1],
00667     filename,
00668     FF[2]))$
00669 /* Providing a standard name: "WSchur_sb_r_n.cnf": */
00670 output_wschur_sb_stdname(r,n) := output_wschur_sb(r,n,
00671   sconcat("WSchur_sb_",r,"_",n,".cnf"))$
00672 
00673 output_schur_fullsb(r,n,filename) := block(
00674  [FF : schur_fullsb_aloamo_stdfcl(r,n)],
00675   output_fcl_v(
00676     sconcat("Schur problem with ", r, " parts and ", n, " elements, using the direct (strong) translation.", newline, "c Symmetry breaking by putting the following elements into parts 1, 2, ...: ", sublist(create_list(schur(i),i,0,r-1), lambda([x], is(x<=n))), ".", newline, "c ", "Created by output_schur_fullsb(", r, ",", n, ",\"", filename, "\").", newline, "c ", created_by_OKlib()),
00677     FF[1],
00678     filename,
00679     FF[2]))$
00680 /* Providing a standard name: "Schur_fullsb_r_n.cnf": */
00681 output_schur_fullsb_stdname(r,n) := output_schur_fullsb(r,n,
00682   sconcat("Schur_fullsb_",r,"_",n,".cnf"))$
00683 
00684 output_wschur_fullsb(r,n,filename) := block(
00685  [FF : wschur_fullsb_aloamo_stdfcl(r,n)],
00686   output_fcl_v(
00687     sconcat("Weak Schur problem with ", r, " parts and ", n, " elements, using the direct (strong) translation.", newline, "c Symmetry breaking by putting the following elements into parts 1, 2, ...: ", sublist(create_list(wschur(i),i,0,r-1), lambda([x], is(x<=n))), ".", newline, "c ", "Created by output_wschur_fullsb(", r, ",", n, ",\"", filename, "\").", newline, "c ", created_by_OKlib()),
00688     FF[1],
00689     filename,
00690     FF[2]))$
00691 /* Providing a standard name: "WSchur_fullsb_r_n.cnf": */
00692 output_wschur_fullsb_stdname(r,n) := output_wschur_fullsb(r,n,
00693   sconcat("WSchur_fullsb_",r,"_",n,".cnf"))$
00694 
00695 output_pd_schur_fullsb(r,n,filename) := block(
00696  [FF : pd_schur_fullsb_aloamo_stdfcl(r,n)],
00697   output_fcl_v(
00698     sconcat("Palindromic Schur problem with ", r, " parts and ", n, " elements, using the direct (strong) translation.", newline, "c Symmetry breaking by putting the following elements into parts 1, 2, ...: ", sublist(create_list(schur(i),i,0,r-1), lambda([x], is(x<=ceiling(n/2)))), ".", newline, "c ", "Created by output_pd_schur_fullsb(", r, ",", n, ",\"", filename, "\").", newline, "c ", created_by_OKlib()),
00699     FF[1],
00700     filename,
00701     FF[2]))$
00702 /* Providing a standard name: "Schur_pd_fullsb_r_n.cnf": */
00703 output_pd_schur_fullsb_stdname(r,n) := output_pd_schur_fullsb(r,n,
00704   sconcat("Schur_pd_fullsb_",r,"_",n,".cnf"))$
00705 
00706 output_pd_wschur_fullsb(r,n,filename) := block(
00707  [FF : pd_wschur_fullsb_aloamo_stdfcl(r,n)],
00708   output_fcl_v(
00709     sconcat("Palindromic weak Schur problem with ", r, " parts and ", n, " elements, using the direct (strong) translation.", newline, "c Symmetry breaking by putting the following elements into parts 1, 2, ...: ", sublist(create_list(wschur(i),i,0,r-1), lambda([x], is(x<=ceiling(n/2)))), ".", newline, "c ", "Created by output_pd_wschur_fullsb(", r, ",", n, ",\"", filename, "\").", newline, "c ", created_by_OKlib()),
00710     FF[1],
00711     filename,
00712     FF[2]))$
00713 /* Providing a standard name: "WSchur_pd_fullsb_r_n.cnf": */
00714 output_pd_wschur_fullsb_stdname(r,n) := output_pd_wschur_fullsb(r,n,
00715   sconcat("WSchur_pd_fullsb_",r,"_",n,".cnf"))$
00716 
00717 
00718 output_schur_rm(r,n,k,filename) := block(
00719  [FF : schur_rm_aloamo_stdfcl(r,n,k)],
00720   output_fcl_v(
00721     sconcat("Schur problem with ", r, " parts and ", n, " elements, using the direct (strong) translation.", newline, "c Forbidding the first ", k, " elements in part ",r,".", newline, "c ", "Created by output_schur_rm(", r, ",", n, ",", k, ",\"", filename, "\").", newline, "c ", created_by_OKlib()),
00722     FF[1],
00723     filename,
00724     FF[2]))$
00725 /* Providing a standard name: "Schur_rm_r_n-k.cnf": */
00726 output_schur_rm_stdname(r,n,k) := output_schur_rm(r,n,k,
00727   sconcat("Schur_rm_",r,"_",n,"-",k,".cnf"))$
00728 
00729 output_pd_schur_rm(r,n,k,filename) := block(
00730  [FF : pd_schur_rm_aloamo_stdfcl(r,n,k)],
00731   output_fcl_v(
00732     sconcat("Palindromic Schur problem with ", r, " parts and ", n, " elements, using the direct (strong) translation.", newline, "c Forbidding the first ", k, " elements in part ",r,".", newline, "c ", "Created by output_pd_schur_rm(", r, ",", n, ",", k, ",\"", filename, "\").", newline, "c ", created_by_OKlib()),
00733     FF[1],
00734     filename,
00735     FF[2]))$
00736 /* Providing a standard name: "Schur_pd_rm_r_n-k.cnf": */
00737 output_pd_schur_rm_stdname(r,n,k) := output_pd_schur_rm(r,n,k,
00738   sconcat("Schur_pd_rm_",r,"_",n,"-",k,".cnf"))$
00739 
00740 output_pd_schur_fullsb_rm(r,n,k,filename) := block(
00741  [FF : pd_schur_fullsb_rm_aloamo_stdfcl(r,n,k)],
00742   output_fcl_v(
00743     sconcat("Palindromic Schur problem with ", r, " parts and ", n, " elements, using the direct (strong) translation.", newline, "c Forbidding the first ", k, " elements in part ", r,".", newline, "c Symmetry breaking by putting the following elements into parts 1, 2, ...: ", sublist(create_list(wschur(i),i,0,r-1), lambda([x], is(x<=ceiling(n/2)))), ".", newline, "c ", "Created by output_pd_fullsb_rm_schur(", r, ",", n, ",", k, ",\"", filename, "\").", newline, "c ", created_by_OKlib()),
00744     FF[1],
00745     filename,
00746     FF[2]))$
00747 /* Providing a standard name: "Schur_rm_r_n-k.cnf": */
00748 output_pd_schur_fullsb_rm_stdname(r,n,k) := output_pd_schur_fullsb_rm(r,n,k,
00749   sconcat("Schur_pd_fullsb_rm_",r,"_",n,"-",k,".cnf"))$
00750 
00751 
00752 /* Output the standard nested translation to a file: */
00753 output_schur_standnest(r,n,filename) := block(
00754  [FF : schur_standnest_stdfcl(r,n)],
00755   output_fcl_v(
00756     sconcat("Schur problem with ", r, " parts and ", n, " elements, using the weak standard nested translation.", newline, "c ", "Created by output_schur_standnest(", r, ",", n, ",\"", filename, "\").", newline, "c ", created_by_OKlib()),
00757     FF[1],
00758     filename,
00759     FF[2]))$
00760 /* Providing a standard name: "Schur_N_r_n.cnf": */
00761 output_schur_standnest_stdname(r,n) := output_schur_standnest(r,n,
00762   sconcat("Schur_N_",r,"_",n,".cnf"))$
00763 
00764 output_schur_standnest_strong(r,n,filename) := block(
00765  [FF : schur_standnest_strong_stdfcl(r,n)],
00766   output_fcl_v(
00767     sconcat("Schur problem with ", r, " parts and ", n, " elements, using the strong standard nested translation.", newline, "c ", "Created by output_schur_standnest(", r, ",", n, ",\"", filename, "\").", newline, "c ", created_by_OKlib()),
00768     FF[1],
00769     filename,
00770     FF[2]))$
00771 /* Providing a standard name: "Schur_SN_r_n.cnf": */
00772 output_schur_standnest_strong_stdname(r,n) := output_schur_standnest_strong(r,n,
00773   sconcat("Schur_SN_",r,"_",n,".cnf"))$
00774 
00775 
00776 /* Output the logarithmic translation to a file: */
00777 output_schur_logarithmic(r,n,filename) := block(
00778  [FF : schur_logarithmic_stdfcl(r,n)],
00779   output_fcl_v(
00780     sconcat("Schur problem with ", r, " parts and ", n, " elements, using the logarithmic translation.", newline, "c ", "Created by output_schur_logarithmic(", r, ",", n, ",\"", filename, "\").", newline, "c ", created_by_OKlib()),
00781     FF[1],
00782     filename,
00783     FF[2]))$
00784 /* Providing a standard name: "Schur_L_r_n.cnf": */
00785 output_schur_logarithmic_stdname(r,n) := output_schur_logarithmic(r,n,
00786   sconcat("Schur_L_",r,"_",n,".cnf"))$
00787 
00788