1/* Bongard dataset from
    2L. De Raedt and W. Van Laer. Inductive constraint logic. 
    3In Klaus P. Jantke, Takeshi Shinohara, and Thomas Zeugmann, editors, 
    4Proceedings of the Sixth International Workshop on Algorithmic
    5Learning Theory, volume 997 of Lecture Notes in Artificial Intelligence, 
    6pages 80-94. SpringerVerlag, 1995.
    7
    8Downloaded from 
    9https://dtai.cs.kuleuven.be/static/ACE/doc/
   10
   11     Arnaud Nguembang Fadja and Fabrizio Riguzzi. 
   12      Hierachical probabilistic logic programs
   13*/

   23:-use_module(library(phil)).   24:- if(current_predicate(use_rendering/1)).   25:- use_rendering(c3).   26:- use_rendering(lpad).   27:- endif.   28
   29:-phil.   30
   31
   32:- set_hplp(neg_ex,given).   33:- set_hplp(verbosity,1).   34% Structure learning settings
   35:- set_hplp(megaex_bottom,10). % max number of mega examples to considered in the generation of bottoms clauses
   36:- set_hplp(initial_clauses_per_megaex,1).   37:- set_hplp(rate,1.0). % defines the probabilityu for going from the first layer to the second layer
   38:- set_hplp(max_layer,-1). % Define the max number of layer: -1 for the maximum depth possible 
   39:- set_hplp(min_probability,0.00001).  % threshold value of the probability under which a clauses is dropped out
   40
   41% Parameter learning settings
   42:- set_hplp(algorithmType,dphil). % parameter learning algorithm dphil or emphil
   43% Maximun iteration and other stop conditions.
   44:- set_hplp(maxIter_phil,1000).  
   45:- set_hplp(epsilon_deep,0.0001). 
   46:- set_hplp(epsilon_deep_fraction,0.00001).   47
   48% regularization parameters 
   49:- set_hplp(regularized,no). % yes to enable regularization and no otherwise 
   50:- set_hplp(regularizationType,0). % 1 for L1, 2 for L2 and 3 for L3. L3 available only for emphil. If set to 0 no regularization is done
   51:- set_hplp(gamma,10). % regularization strength
   52:- set_hplp(gammaCount,0). 
   53
   54% Adam parameter for dphil algorithm
   55:- set_hplp(adam_params,[0.1,0.9,0.999,1e-8]). % adam(Eta,Beta1,Beta2,Epsilon_adam_hat)
   56% Gradient descent strategy and the corresponding batch size
   57:- set_hplp(batch_strategy,minibatch(50)).   58%:- set_hplp(batch_strategy,stoch_minibatch(10)).
   59%:- set_hplp(batch_strategy,batch).
   60
   61
   62
   63
   64
   65start :-
   66  induce_hplp([train],P),
   67  open("Program",write, Stream),
   68  write(Stream,P),
   69  close(Stream),
   70  trace,
   71  test_hplp(P,[test],LL,AUCROC,_,AUCPR,_),
   72  format("LL=~g, AUCROC=~g, AUCPR=~g", [LL, AUCROC, AUCPR]).
   73
   74bg([]).
   75
   76
   77in([
   78(
   79  pos:0.197575 :-
   80  	circle(A),
   81	in(B,A)),
   82(
   83  pos:0.000303421 :-
   84	circle(A),
   85	triangle(B)), 
   86(
   87pos:0.000448807 :-
   88	triangle(A),
   89	circle(B)
   90)]).
   91
   92
   93fold(train,[2,3,5,6,9,12,14,15,17,20,24,25,28,29,31,36,37,40,41,50,52,55,56,57,
   94  59,62,63,65,66,67,69,74,76,77,79,83,93,95,99,101,103,104,105,106,107,109,110,
   95  111,112,117,120,121,125,126,127,128,131,135,137,140,143,144,151,154,155,156,
   96  159,167,168,169,172,175,176,177,178,181,184,188,190,192,193,194,196,198,202,
   97  206,208,209,211,214,219,222,223,224,225,227,230,231,233,238,241,243,244,248,
   98  249,250,256,258,260,268,270,273,280,282,286,287,288,289,290,295,300,301,303,
   99  304,307,309,314,316,319,321,324,326,327,328,329,331,334,337,343,345,348,352,
  100  353,355,358,366,369,370,373,375,376,378,379,381,382,390,393,402,404,408,411,
  101  412,416,417,419,420,421,424,425,427,428,431,432,433,437,444,445,447,453,456,
  102  457,459,462,463,464,465,468,470,473,474,476,477,479,481,482,483,485,488,489]).
  103
  104fold(test,
  105  [490,491,494,497,499,500,512,513,516,517,520,521,527,529,531,533,534,539,540,
  106  542,543,544,546,550,552,553,555,559,565,567,568,572,578,582,583,591,595,597,
  107  600,602,609,612,614,615,616,617,622,625,628,634,635,637,639,640,641,642,647,
  108  648,649,650,654,656,657,658,662,667,669,671,679,682,683,685,686,691,693,698,
  109  700,701,705,708,709,710,719,722,723,725,728,732,734,737,740,741,743,744,745,
  110  747,748,750,751,753,754,755,765,766,768,769,772,773,777,779,780,781,787,794,
  111  795,797,803,805,807,814,815,816,818,819,822,829,832,833,835,836,837,838,841,
  112  844,845,846,847,848,849,856,859,862,864,867,872,874,876,880,882,887,890,892,
  113  893,897,899,900,904,909,910,912,915,917,926,927,929,930,931,932,933,938,939,
  114  940,941,944,945,946,947,955,957,961,971,973,974,975,977,978,979,984,989,991,
  115  995,997,1000]).
  116
  117fold(all,F):-
  118  fold(train,FTr),
  119  fold(test,FTe),
  120  append(FTr,FTe,F).
  121
  122
  123output(pos/0).
  124
  125input(triangle/1).
  126input(square/1).
  127input(circle/1).
  128input(in/2).
  129input(config/2).
  130
  131determination(pos/0,triangle/1).
  132determination(pos/0,square/1).
  133determination(pos/0,circle/1).
  134determination(pos/0,in/2).
  135determination(pos/0,config/2).
  136
  137modeh(*,pos).
  138modeb(*,triangle(-obj)).
  139modeb(*,square(-obj)).
  140modeb(*,circle(-obj)).
  141modeb(*,in(+obj,-obj)).
  142modeb(*,in(-obj,+obj)).
  143modeb(*,config(+obj,-#dir)).
  144
  145begin(model(2)).
  146pos.
  147triangle(o5).
  148config(o5,up).
  149square(o4).
  150in(o4,o5).
  151circle(o3).
  152triangle(o2).
  153config(o2,up).
  154in(o2,o3).
  155triangle(o1).
  156config(o1,up).
  157end(model(2)).
  158
  159begin(model(3)).
  160neg(pos).
  161circle(o4).
  162circle(o3).
  163in(o3,o4).
  164square(o2).
  165circle(o1).
  166in(o1,o2).
  167end(model(3)).
  168
  169begin(model(5)).
  170neg(pos).
  171square(o3).
  172square(o2).
  173in(o2,o3).
  174square(o1).
  175end(model(5)).
  176
  177begin(model(6)).
  178pos.
  179triangle(o5).
  180config(o5,down).
  181triangle(o4).
  182config(o4,up).
  183in(o4,o5).
  184circle(o3).
  185square(o2).
  186in(o2,o3).
  187triangle(o1).
  188config(o1,up).
  189end(model(6)).
  190
  191begin(model(9)).
  192pos.
  193circle(o4).
  194triangle(o3).
  195config(o3,up).
  196in(o3,o4).
  197triangle(o2).
  198config(o2,down).
  199square(o1).
  200in(o1,o2).
  201end(model(9)).
  202
  203begin(model(12)).
  204neg(pos).
  205triangle(o5).
  206config(o5,down).
  207square(o4).
  208in(o4,o5).
  209circle(o3).
  210circle(o2).
  211in(o2,o3).
  212triangle(o1).
  213config(o1,down).
  214end(model(12)).
  215
  216begin(model(14)).
  217neg(pos).
  218triangle(o3).
  219config(o3,down).
  220circle(o2).
  221in(o2,o3).
  222triangle(o1).
  223config(o1,down).
  224end(model(14)).
  225
  226begin(model(15)).
  227neg(pos).
  228triangle(o4).
  229config(o4,down).
  230circle(o3).
  231in(o3,o4).
  232triangle(o2).
  233config(o2,up).
  234circle(o1).
  235in(o1,o2).
  236end(model(15)).
  237
  238begin(model(17)).
  239pos.
  240triangle(o2).
  241config(o2,down).
  242triangle(o1).
  243config(o1,down).
  244in(o1,o2).
  245end(model(17)).
  246
  247begin(model(20)).
  248pos.
  249triangle(o6).
  250config(o6,up).
  251triangle(o5).
  252config(o5,up).
  253in(o5,o6).
  254square(o4).
  255triangle(o3).
  256config(o3,up).
  257in(o3,o4).
  258square(o2).
  259triangle(o1).
  260config(o1,up).
  261in(o1,o2).
  262end(model(20)).
  263
  264begin(model(24)).
  265pos.
  266triangle(o4).
  267config(o4,up).
  268circle(o3).
  269in(o3,o4).
  270triangle(o2).
  271config(o2,up).
  272triangle(o1).
  273config(o1,up).
  274in(o1,o2).
  275end(model(24)).
  276
  277begin(model(25)).
  278neg(pos).
  279square(o2).
  280square(o1).
  281in(o1,o2).
  282end(model(25)).
  283
  284begin(model(28)).
  285neg(pos).
  286square(o5).
  287square(o4).
  288in(o4,o5).
  289circle(o3).
  290circle(o2).
  291in(o2,o3).
  292triangle(o1).
  293config(o1,up).
  294end(model(28)).
  295
  296begin(model(29)).
  297neg(pos).
  298triangle(o2).
  299config(o2,up).
  300square(o1).
  301in(o1,o2).
  302end(model(29)).
  303
  304begin(model(31)).
  305neg(pos).
  306circle(o4).
  307square(o3).
  308in(o3,o4).
  309square(o2).
  310circle(o1).
  311in(o1,o2).
  312end(model(31)).
  313
  314begin(model(36)).
  315neg(pos).
  316triangle(o3).
  317config(o3,up).
  318circle(o2).
  319in(o2,o3).
  320circle(o1).
  321end(model(36)).
  322
  323begin(model(37)).
  324neg(pos).
  325square(o6).
  326circle(o5).
  327in(o5,o6).
  328square(o4).
  329circle(o3).
  330in(o3,o4).
  331square(o2).
  332triangle(o1).
  333config(o1,down).
  334in(o1,o2).
  335end(model(37)).
  336
  337begin(model(40)).
  338neg(pos).
  339circle(o4).
  340square(o3).
  341in(o3,o4).
  342square(o2).
  343circle(o1).
  344in(o1,o2).
  345end(model(40)).
  346
  347begin(model(41)).
  348neg(pos).
  349square(o3).
  350circle(o2).
  351in(o2,o3).
  352triangle(o1).
  353config(o1,down).
  354end(model(41)).
  355
  356begin(model(50)).
  357pos.
  358triangle(o6).
  359config(o6,up).
  360square(o5).
  361in(o5,o6).
  362triangle(o4).
  363config(o4,down).
  364circle(o3).
  365in(o3,o4).
  366triangle(o2).
  367config(o2,up).
  368triangle(o1).
  369config(o1,down).
  370in(o1,o2).
  371end(model(50)).
  372
  373begin(model(52)).
  374neg(pos).
  375square(o3).
  376circle(o2).
  377in(o2,o3).
  378circle(o1).
  379end(model(52)).
  380
  381begin(model(55)).
  382neg(pos).
  383triangle(o2).
  384config(o2,down).
  385square(o1).
  386in(o1,o2).
  387end(model(55)).
  388
  389begin(model(56)).
  390neg(pos).
  391circle(o5).
  392circle(o4).
  393in(o4,o5).
  394circle(o3).
  395circle(o2).
  396in(o2,o3).
  397circle(o1).
  398end(model(56)).
  399
  400begin(model(57)).
  401neg(pos).
  402circle(o4).
  403circle(o3).
  404in(o3,o4).
  405square(o2).
  406triangle(o1).
  407config(o1,up).
  408in(o1,o2).
  409end(model(57)).
  410
  411begin(model(59)).
  412neg(pos).
  413square(o5).
  414triangle(o4).
  415config(o4,up).
  416in(o4,o5).
  417triangle(o3).
  418config(o3,down).
  419circle(o2).
  420in(o2,o3).
  421circle(o1).
  422end(model(59)).
  423
  424begin(model(62)).
  425pos.
  426triangle(o5).
  427config(o5,up).
  428triangle(o4).
  429config(o4,down).
  430in(o4,o5).
  431triangle(o3).
  432config(o3,up).
  433square(o2).
  434in(o2,o3).
  435triangle(o1).
  436config(o1,down).
  437end(model(62)).
  438
  439begin(model(63)).
  440neg(pos).
  441triangle(o2).
  442config(o2,up).
  443square(o1).
  444in(o1,o2).
  445end(model(63)).
  446
  447begin(model(65)).
  448neg(pos).
  449circle(o6).
  450circle(o5).
  451in(o5,o6).
  452circle(o4).
  453circle(o3).
  454in(o3,o4).
  455square(o2).
  456square(o1).
  457in(o1,o2).
  458end(model(65)).
  459
  460begin(model(66)).
  461neg(pos).
  462triangle(o2).
  463config(o2,up).
  464circle(o1).
  465in(o1,o2).
  466end(model(66)).
  467
  468begin(model(67)).
  469neg(pos).
  470circle(o4).
  471circle(o3).
  472in(o3,o4).
  473square(o2).
  474triangle(o1).
  475config(o1,down).
  476in(o1,o2).
  477end(model(67)).
  478
  479begin(model(69)).
  480pos.
  481circle(o3).
  482triangle(o2).
  483config(o2,up).
  484in(o2,o3).
  485triangle(o1).
  486config(o1,down).
  487end(model(69)).
  488
  489begin(model(74)).
  490pos.
  491circle(o6).
  492triangle(o5).
  493config(o5,up).
  494in(o5,o6).
  495triangle(o4).
  496config(o4,down).
  497square(o3).
  498in(o3,o4).
  499triangle(o2).
  500config(o2,down).
  501triangle(o1).
  502config(o1,down).
  503in(o1,o2).
  504end(model(74)).
  505
  506begin(model(76)).
  507pos.
  508square(o6).
  509square(o5).
  510in(o5,o6).
  511triangle(o4).
  512config(o4,up).
  513square(o3).
  514in(o3,o4).
  515triangle(o2).
  516config(o2,up).
  517triangle(o1).
  518config(o1,down).
  519in(o1,o2).
  520end(model(76)).
  521
  522begin(model(77)).
  523neg(pos).
  524square(o3).
  525triangle(o2).
  526config(o2,up).
  527in(o2,o3).
  528square(o1).
  529end(model(77)).
  530
  531begin(model(79)).
  532pos.
  533triangle(o5).
  534config(o5,up).
  535triangle(o4).
  536config(o4,down).
  537in(o4,o5).
  538triangle(o3).
  539config(o3,down).
  540triangle(o2).
  541config(o2,up).
  542in(o2,o3).
  543square(o1).
  544end(model(79)).
  545
  546begin(model(83)).
  547pos.
  548triangle(o3).
  549config(o3,up).
  550triangle(o2).
  551config(o2,down).
  552in(o2,o3).
  553square(o1).
  554end(model(83)).
  555
  556begin(model(93)).
  557neg(pos).
  558square(o4).
  559triangle(o3).
  560config(o3,up).
  561in(o3,o4).
  562circle(o2).
  563circle(o1).
  564in(o1,o2).
  565end(model(93)).
  566
  567begin(model(95)).
  568pos.
  569circle(o6).
  570square(o5).
  571in(o5,o6).
  572square(o4).
  573triangle(o3).
  574config(o3,up).
  575in(o3,o4).
  576square(o2).
  577triangle(o1).
  578config(o1,down).
  579in(o1,o2).
  580end(model(95)).
  581
  582begin(model(99)).
  583neg(pos).
  584triangle(o4).
  585config(o4,down).
  586square(o3).
  587in(o3,o4).
  588square(o2).
  589circle(o1).
  590in(o1,o2).
  591end(model(99)).
  592
  593begin(model(101)).
  594neg(pos).
  595square(o6).
  596square(o5).
  597in(o5,o6).
  598triangle(o4).
  599config(o4,down).
  600circle(o3).
  601in(o3,o4).
  602triangle(o2).
  603config(o2,down).
  604circle(o1).
  605in(o1,o2).
  606end(model(101)).
  607
  608begin(model(103)).
  609pos.
  610circle(o4).
  611square(o3).
  612in(o3,o4).
  613square(o2).
  614triangle(o1).
  615config(o1,up).
  616in(o1,o2).
  617end(model(103)).
  618
  619begin(model(104)).
  620pos.
  621circle(o5).
  622triangle(o4).
  623config(o4,up).
  624in(o4,o5).
  625circle(o3).
  626square(o2).
  627in(o2,o3).
  628circle(o1).
  629end(model(104)).
  630
  631begin(model(105)).
  632neg(pos).
  633triangle(o2).
  634config(o2,up).
  635square(o1).
  636in(o1,o2).
  637end(model(105)).
  638
  639begin(model(106)).
  640pos.
  641triangle(o5).
  642config(o5,up).
  643triangle(o4).
  644config(o4,up).
  645in(o4,o5).
  646circle(o3).
  647circle(o2).
  648in(o2,o3).
  649square(o1).
  650end(model(106)).
  651
  652begin(model(107)).
  653pos.
  654square(o4).
  655triangle(o3).
  656config(o3,up).
  657in(o3,o4).
  658circle(o2).
  659square(o1).
  660in(o1,o2).
  661end(model(107)).
  662
  663begin(model(109)).
  664neg(pos).
  665square(o4).
  666circle(o3).
  667in(o3,o4).
  668square(o2).
  669triangle(o1).
  670config(o1,up).
  671in(o1,o2).
  672end(model(109)).
  673
  674begin(model(110)).
  675neg(pos).
  676triangle(o3).
  677config(o3,up).
  678circle(o2).
  679in(o2,o3).
  680triangle(o1).
  681config(o1,up).
  682end(model(110)).
  683
  684begin(model(111)).
  685neg(pos).
  686square(o6).
  687circle(o5).
  688in(o5,o6).
  689square(o4).
  690square(o3).
  691in(o3,o4).
  692triangle(o2).
  693config(o2,up).
  694square(o1).
  695in(o1,o2).
  696end(model(111)).
  697
  698begin(model(112)).
  699neg(pos).
  700square(o4).
  701circle(o3).
  702in(o3,o4).
  703square(o2).
  704circle(o1).
  705in(o1,o2).
  706end(model(112)).
  707
  708begin(model(117)).
  709neg(pos).
  710square(o2).
  711square(o1).
  712in(o1,o2).
  713end(model(117)).
  714
  715begin(model(120)).
  716pos.
  717circle(o3).
  718square(o2).
  719in(o2,o3).
  720triangle(o1).
  721config(o1,down).
  722end(model(120)).
  723
  724begin(model(121)).
  725neg(pos).
  726triangle(o3).
  727config(o3,down).
  728square(o2).
  729in(o2,o3).
  730triangle(o1).
  731config(o1,down).
  732end(model(121)).
  733
  734begin(model(125)).
  735neg(pos).
  736circle(o4).
  737circle(o3).
  738in(o3,o4).
  739square(o2).
  740square(o1).
  741in(o1,o2).
  742end(model(125)).
  743
  744begin(model(126)).
  745neg(pos).
  746circle(o3).
  747circle(o2).
  748in(o2,o3).
  749square(o1).
  750end(model(126)).
  751
  752begin(model(127)).
  753neg(pos).
  754triangle(o3).
  755config(o3,up).
  756square(o2).
  757in(o2,o3).
  758square(o1).
  759end(model(127)).
  760
  761begin(model(128)).
  762neg(pos).
  763circle(o3).
  764circle(o2).
  765in(o2,o3).
  766square(o1).
  767end(model(128)).
  768
  769begin(model(131)).
  770neg(pos).
  771circle(o2).
  772circle(o1).
  773in(o1,o2).
  774end(model(131)).
  775
  776begin(model(135)).
  777pos.
  778triangle(o5).
  779config(o5,down).
  780triangle(o4).
  781config(o4,up).
  782in(o4,o5).
  783triangle(o3).
  784config(o3,down).
  785square(o2).
  786in(o2,o3).
  787square(o1).
  788end(model(135)).
  789
  790begin(model(137)).
  791neg(pos).
  792square(o6).
  793circle(o5).
  794in(o5,o6).
  795circle(o4).
  796circle(o3).
  797in(o3,o4).
  798circle(o2).
  799circle(o1).
  800in(o1,o2).
  801end(model(137)).
  802
  803begin(model(140)).
  804neg(pos).
  805square(o3).
  806triangle(o2).
  807config(o2,down).
  808in(o2,o3).
  809triangle(o1).
  810config(o1,down).
  811end(model(140)).
  812
  813begin(model(143)).
  814neg(pos).
  815circle(o4).
  816triangle(o3).
  817config(o3,down).
  818in(o3,o4).
  819circle(o2).
  820circle(o1).
  821in(o1,o2).
  822end(model(143)).
  823
  824begin(model(144)).
  825neg(pos).
  826triangle(o5).
  827config(o5,down).
  828circle(o4).
  829in(o4,o5).
  830square(o3).
  831square(o2).
  832in(o2,o3).
  833square(o1).
  834end(model(144)).
  835
  836begin(model(151)).
  837neg(pos).
  838circle(o3).
  839circle(o2).
  840in(o2,o3).
  841square(o1).
  842end(model(151)).
  843
  844begin(model(154)).
  845neg(pos).
  846circle(o4).
  847square(o3).
  848in(o3,o4).
  849circle(o2).
  850circle(o1).
  851in(o1,o2).
  852end(model(154)).
  853
  854begin(model(155)).
  855neg(pos).
  856square(o3).
  857circle(o2).
  858in(o2,o3).
  859square(o1).
  860end(model(155)).
  861
  862begin(model(156)).
  863neg(pos).
  864square(o6).
  865square(o5).
  866in(o5,o6).
  867triangle(o4).
  868config(o4,down).
  869square(o3).
  870in(o3,o4).
  871circle(o2).
  872circle(o1).
  873in(o1,o2).
  874end(model(156)).
  875
  876begin(model(159)).
  877neg(pos).
  878triangle(o6).
  879config(o6,up).
  880square(o5).
  881in(o5,o6).
  882triangle(o4).
  883config(o4,down).
  884square(o3).
  885in(o3,o4).
  886square(o2).
  887triangle(o1).
  888config(o1,up).
  889in(o1,o2).
  890end(model(159)).
  891
  892begin(model(167)).
  893pos.
  894circle(o4).
  895circle(o3).
  896in(o3,o4).
  897triangle(o2).
  898config(o2,up).
  899triangle(o1).
  900config(o1,down).
  901in(o1,o2).
  902end(model(167)).
  903
  904begin(model(168)).
  905pos.
  906triangle(o4).
  907config(o4,up).
  908triangle(o3).
  909config(o3,down).
  910in(o3,o4).
  911square(o2).
  912triangle(o1).
  913config(o1,down).
  914in(o1,o2).
  915end(model(168)).
  916
  917begin(model(169)).
  918neg(pos).
  919triangle(o6).
  920config(o6,up).
  921square(o5).
  922in(o5,o6).
  923circle(o4).
  924triangle(o3).
  925config(o3,down).
  926in(o3,o4).
  927circle(o2).
  928circle(o1).
  929in(o1,o2).
  930end(model(169)).
  931
  932begin(model(172)).
  933neg(pos).
  934square(o4).
  935circle(o3).
  936in(o3,o4).
  937triangle(o2).
  938config(o2,up).
  939circle(o1).
  940in(o1,o2).
  941end(model(172)).
  942
  943begin(model(175)).
  944neg(pos).
  945circle(o2).
  946circle(o1).
  947in(o1,o2).
  948end(model(175)).
  949
  950begin(model(176)).
  951neg(pos).
  952circle(o5).
  953circle(o4).
  954in(o4,o5).
  955circle(o3).
  956square(o2).
  957in(o2,o3).
  958circle(o1).
  959end(model(176)).
  960
  961begin(model(177)).
  962neg(pos).
  963circle(o4).
  964circle(o3).
  965in(o3,o4).
  966square(o2).
  967circle(o1).
  968in(o1,o2).
  969end(model(177)).
  970
  971begin(model(178)).
  972pos.
  973triangle(o4).
  974config(o4,up).
  975triangle(o3).
  976config(o3,up).
  977in(o3,o4).
  978triangle(o2).
  979config(o2,up).
  980square(o1).
  981in(o1,o2).
  982end(model(178)).
  983
  984begin(model(181)).
  985neg(pos).
  986triangle(o2).
  987config(o2,up).
  988circle(o1).
  989in(o1,o2).
  990end(model(181)).
  991
  992begin(model(184)).
  993neg(pos).
  994square(o2).
  995circle(o1).
  996in(o1,o2).
  997end(model(184)).
  998
  999begin(model(188)).
 1000neg(pos).
 1001circle(o2).
 1002circle(o1).
 1003in(o1,o2).
 1004end(model(188)).
 1005
 1006begin(model(190)).
 1007neg(pos).
 1008square(o2).
 1009triangle(o1).
 1010config(o1,up).
 1011in(o1,o2).
 1012end(model(190)).
 1013
 1014begin(model(192)).
 1015pos.
 1016circle(o3).
 1017square(o2).
 1018in(o2,o3).
 1019triangle(o1).
 1020config(o1,down).
 1021end(model(192)).
 1022
 1023begin(model(193)).
 1024neg(pos).
 1025triangle(o4).
 1026config(o4,up).
 1027circle(o3).
 1028in(o3,o4).
 1029square(o2).
 1030circle(o1).
 1031in(o1,o2).
 1032end(model(193)).
 1033
 1034begin(model(194)).
 1035neg(pos).
 1036circle(o4).
 1037square(o3).
 1038in(o3,o4).
 1039circle(o2).
 1040circle(o1).
 1041in(o1,o2).
 1042end(model(194)).
 1043
 1044begin(model(196)).
 1045neg(pos).
 1046square(o3).
 1047circle(o2).
 1048in(o2,o3).
 1049triangle(o1).
 1050config(o1,up).
 1051end(model(196)).
 1052
 1053begin(model(198)).
 1054pos.
 1055triangle(o3).
 1056config(o3,down).
 1057triangle(o2).
 1058config(o2,down).
 1059in(o2,o3).
 1060square(o1).
 1061end(model(198)).
 1062
 1063begin(model(202)).
 1064neg(pos).
 1065circle(o5).
 1066circle(o4).
 1067in(o4,o5).
 1068square(o3).
 1069square(o2).
 1070in(o2,o3).
 1071triangle(o1).
 1072config(o1,down).
 1073end(model(202)).
 1074
 1075begin(model(206)).
 1076neg(pos).
 1077circle(o3).
 1078circle(o2).
 1079in(o2,o3).
 1080circle(o1).
 1081end(model(206)).
 1082
 1083begin(model(208)).
 1084neg(pos).
 1085square(o4).
 1086square(o3).
 1087in(o3,o4).
 1088triangle(o2).
 1089config(o2,down).
 1090circle(o1).
 1091in(o1,o2).
 1092end(model(208)).
 1093
 1094begin(model(209)).
 1095neg(pos).
 1096square(o5).
 1097square(o4).
 1098in(o4,o5).
 1099circle(o3).
 1100circle(o2).
 1101in(o2,o3).
 1102circle(o1).
 1103end(model(209)).
 1104
 1105begin(model(211)).
 1106pos.
 1107triangle(o2).
 1108config(o2,down).
 1109triangle(o1).
 1110config(o1,down).
 1111in(o1,o2).
 1112end(model(211)).
 1113
 1114begin(model(214)).
 1115pos.
 1116triangle(o5).
 1117config(o5,down).
 1118square(o4).
 1119in(o4,o5).
 1120circle(o3).
 1121square(o2).
 1122in(o2,o3).
 1123square(o1).
 1124end(model(214)).
 1125
 1126begin(model(219)).
 1127pos.
 1128square(o4).
 1129triangle(o3).
 1130config(o3,up).
 1131in(o3,o4).
 1132triangle(o2).
 1133config(o2,up).
 1134triangle(o1).
 1135config(o1,down).
 1136in(o1,o2).
 1137end(model(219)).
 1138
 1139begin(model(222)).
 1140pos.
 1141triangle(o4).
 1142config(o4,up).
 1143square(o3).
 1144in(o3,o4).
 1145triangle(o2).
 1146config(o2,down).
 1147triangle(o1).
 1148config(o1,down).
 1149in(o1,o2).
 1150end(model(222)).
 1151
 1152begin(model(223)).
 1153pos.
 1154circle(o6).
 1155circle(o5).
 1156in(o5,o6).
 1157circle(o4).
 1158circle(o3).
 1159in(o3,o4).
 1160triangle(o2).
 1161config(o2,up).
 1162triangle(o1).
 1163config(o1,down).
 1164in(o1,o2).
 1165end(model(223)).
 1166
 1167begin(model(224)).
 1168pos.
 1169circle(o6).
 1170square(o5).
 1171in(o5,o6).
 1172square(o4).
 1173square(o3).
 1174in(o3,o4).
 1175triangle(o2).
 1176config(o2,up).
 1177square(o1).
 1178in(o1,o2).
 1179end(model(224)).
 1180
 1181begin(model(225)).
 1182pos.
 1183circle(o3).
 1184triangle(o2).
 1185config(o2,up).
 1186in(o2,o3).
 1187triangle(o1).
 1188config(o1,up).
 1189end(model(225)).
 1190
 1191begin(model(227)).
 1192pos.
 1193circle(o3).
 1194triangle(o2).
 1195config(o2,up).
 1196in(o2,o3).
 1197circle(o1).
 1198end(model(227)).
 1199
 1200begin(model(230)).
 1201neg(pos).
 1202square(o5).
 1203square(o4).
 1204in(o4,o5).
 1205square(o3).
 1206triangle(o2).
 1207config(o2,up).
 1208in(o2,o3).
 1209triangle(o1).
 1210config(o1,down).
 1211end(model(230)).
 1212
 1213begin(model(231)).
 1214pos.
 1215triangle(o2).
 1216config(o2,up).
 1217triangle(o1).
 1218config(o1,down).
 1219in(o1,o2).
 1220end(model(231)).
 1221
 1222begin(model(233)).
 1223neg(pos).
 1224square(o2).
 1225circle(o1).
 1226in(o1,o2).
 1227end(model(233)).
 1228
 1229begin(model(238)).
 1230pos.
 1231triangle(o5).
 1232config(o5,up).
 1233triangle(o4).
 1234config(o4,down).
 1235in(o4,o5).
 1236triangle(o3).
 1237config(o3,down).
 1238triangle(o2).
 1239config(o2,up).
 1240in(o2,o3).
 1241circle(o1).
 1242end(model(238)).
 1243
 1244begin(model(241)).
 1245neg(pos).
 1246triangle(o5).
 1247config(o5,up).
 1248circle(o4).
 1249in(o4,o5).
 1250square(o3).
 1251circle(o2).
 1252in(o2,o3).
 1253triangle(o1).
 1254config(o1,down).
 1255end(model(241)).
 1256
 1257begin(model(243)).
 1258neg(pos).
 1259circle(o2).
 1260circle(o1).
 1261in(o1,o2).
 1262end(model(243)).
 1263
 1264begin(model(244)).
 1265pos.
 1266square(o5).
 1267square(o4).
 1268in(o4,o5).
 1269triangle(o3).
 1270config(o3,down).
 1271triangle(o2).
 1272config(o2,down).
 1273in(o2,o3).
 1274square(o1).
 1275end(model(244)).
 1276
 1277begin(model(248)).
 1278pos.
 1279circle(o3).
 1280triangle(o2).
 1281config(o2,up).
 1282in(o2,o3).
 1283triangle(o1).
 1284config(o1,down).
 1285end(model(248)).
 1286
 1287begin(model(249)).
 1288neg(pos).
 1289circle(o5).
 1290circle(o4).
 1291in(o4,o5).
 1292square(o3).
 1293circle(o2).
 1294in(o2,o3).
 1295triangle(o1).
 1296config(o1,down).
 1297end(model(249)).
 1298
 1299begin(model(250)).
 1300neg(pos).
 1301square(o6).
 1302circle(o5).
 1303in(o5,o6).
 1304circle(o4).
 1305square(o3).
 1306in(o3,o4).
 1307circle(o2).
 1308square(o1).
 1309in(o1,o2).
 1310end(model(250)).
 1311
 1312begin(model(256)).
 1313pos.
 1314circle(o4).
 1315triangle(o3).
 1316config(o3,up).
 1317in(o3,o4).
 1318triangle(o2).
 1319config(o2,up).
 1320triangle(o1).
 1321config(o1,down).
 1322in(o1,o2).
 1323end(model(256)).
 1324
 1325begin(model(258)).
 1326pos.
 1327triangle(o4).
 1328config(o4,up).
 1329triangle(o3).
 1330config(o3,down).
 1331in(o3,o4).
 1332circle(o2).
 1333triangle(o1).
 1334config(o1,down).
 1335in(o1,o2).
 1336end(model(258)).
 1337
 1338begin(model(260)).
 1339pos.
 1340square(o4).
 1341triangle(o3).
 1342config(o3,down).
 1343in(o3,o4).
 1344triangle(o2).
 1345config(o2,up).
 1346triangle(o1).
 1347config(o1,up).
 1348in(o1,o2).
 1349end(model(260)).
 1350
 1351begin(model(268)).
 1352neg(pos).
 1353square(o5).
 1354circle(o4).
 1355in(o4,o5).
 1356circle(o3).
 1357square(o2).
 1358in(o2,o3).
 1359square(o1).
 1360end(model(268)).
 1361
 1362begin(model(270)).
 1363pos.
 1364circle(o4).
 1365triangle(o3).
 1366config(o3,up).
 1367in(o3,o4).
 1368square(o2).
 1369triangle(o1).
 1370config(o1,down).
 1371in(o1,o2).
 1372end(model(270)).
 1373
 1374begin(model(273)).
 1375neg(pos).
 1376square(o4).
 1377triangle(o3).
 1378config(o3,down).
 1379in(o3,o4).
 1380square(o2).
 1381square(o1).
 1382in(o1,o2).
 1383end(model(273)).
 1384
 1385begin(model(280)).
 1386neg(pos).
 1387square(o3).
 1388square(o2).
 1389in(o2,o3).
 1390square(o1).
 1391end(model(280)).
 1392
 1393begin(model(282)).
 1394pos.
 1395triangle(o2).
 1396config(o2,up).
 1397triangle(o1).
 1398config(o1,up).
 1399in(o1,o2).
 1400end(model(282)).
 1401
 1402begin(model(286)).
 1403neg(pos).
 1404triangle(o4).
 1405config(o4,down).
 1406circle(o3).
 1407in(o3,o4).
 1408triangle(o2).
 1409config(o2,down).
 1410square(o1).
 1411in(o1,o2).
 1412end(model(286)).
 1413
 1414begin(model(287)).
 1415neg(pos).
 1416triangle(o4).
 1417config(o4,up).
 1418square(o3).
 1419in(o3,o4).
 1420triangle(o2).
 1421config(o2,down).
 1422circle(o1).
 1423in(o1,o2).
 1424end(model(287)).
 1425
 1426begin(model(288)).
 1427pos.
 1428circle(o5).
 1429triangle(o4).
 1430config(o4,up).
 1431in(o4,o5).
 1432circle(o3).
 1433square(o2).
 1434in(o2,o3).
 1435square(o1).
 1436end(model(288)).
 1437
 1438begin(model(289)).
 1439neg(pos).
 1440triangle(o6).
 1441config(o6,up).
 1442square(o5).
 1443in(o5,o6).
 1444triangle(o4).
 1445config(o4,up).
 1446square(o3).
 1447in(o3,o4).
 1448square(o2).
 1449circle(o1).
 1450in(o1,o2).
 1451end(model(289)).
 1452
 1453begin(model(290)).
 1454neg(pos).
 1455triangle(o5).
 1456config(o5,down).
 1457circle(o4).
 1458in(o4,o5).
 1459triangle(o3).
 1460config(o3,up).
 1461circle(o2).
 1462in(o2,o3).
 1463square(o1).
 1464end(model(290)).
 1465
 1466begin(model(295)).
 1467pos.
 1468circle(o6).
 1469triangle(o5).
 1470config(o5,down).
 1471in(o5,o6).
 1472triangle(o4).
 1473config(o4,down).
 1474triangle(o3).
 1475config(o3,down).
 1476in(o3,o4).
 1477circle(o2).
 1478triangle(o1).
 1479config(o1,up).
 1480in(o1,o2).
 1481end(model(295)).
 1482
 1483begin(model(300)).
 1484neg(pos).
 1485square(o3).
 1486triangle(o2).
 1487config(o2,down).
 1488in(o2,o3).
 1489triangle(o1).
 1490config(o1,down).
 1491end(model(300)).
 1492
 1493begin(model(301)).
 1494neg(pos).
 1495square(o6).
 1496triangle(o5).
 1497config(o5,up).
 1498in(o5,o6).
 1499square(o4).
 1500square(o3).
 1501in(o3,o4).
 1502triangle(o2).
 1503config(o2,up).
 1504circle(o1).
 1505in(o1,o2).
 1506end(model(301)).
 1507
 1508begin(model(303)).
 1509neg(pos).
 1510circle(o3).
 1511circle(o2).
 1512in(o2,o3).
 1513triangle(o1).
 1514config(o1,up).
 1515end(model(303)).
 1516
 1517begin(model(304)).
 1518neg(pos).
 1519square(o3).
 1520square(o2).
 1521in(o2,o3).
 1522triangle(o1).
 1523config(o1,up).
 1524end(model(304)).
 1525
 1526begin(model(307)).
 1527neg(pos).
 1528square(o3).
 1529circle(o2).
 1530in(o2,o3).
 1531square(o1).
 1532end(model(307)).
 1533
 1534begin(model(309)).
 1535neg(pos).
 1536triangle(o3).
 1537config(o3,down).
 1538circle(o2).
 1539in(o2,o3).
 1540circle(o1).
 1541end(model(309)).
 1542
 1543begin(model(314)).
 1544pos.
 1545square(o5).
 1546triangle(o4).
 1547config(o4,down).
 1548in(o4,o5).
 1549triangle(o3).
 1550config(o3,down).
 1551triangle(o2).
 1552config(o2,down).
 1553in(o2,o3).
 1554circle(o1).
 1555end(model(314)).
 1556
 1557begin(model(316)).
 1558neg(pos).
 1559square(o4).
 1560triangle(o3).
 1561config(o3,up).
 1562in(o3,o4).
 1563triangle(o2).
 1564config(o2,up).
 1565circle(o1).
 1566in(o1,o2).
 1567end(model(316)).
 1568
 1569begin(model(319)).
 1570pos.
 1571triangle(o5).
 1572config(o5,down).
 1573triangle(o4).
 1574config(o4,down).
 1575in(o4,o5).
 1576square(o3).
 1577square(o2).
 1578in(o2,o3).
 1579circle(o1).
 1580end(model(319)).
 1581
 1582begin(model(321)).
 1583neg(pos).
 1584triangle(o2).
 1585config(o2,down).
 1586circle(o1).
 1587in(o1,o2).
 1588end(model(321)).
 1589
 1590begin(model(324)).
 1591neg(pos).
 1592square(o5).
 1593square(o4).
 1594in(o4,o5).
 1595triangle(o3).
 1596config(o3,down).
 1597square(o2).
 1598in(o2,o3).
 1599square(o1).
 1600end(model(324)).
 1601
 1602begin(model(326)).
 1603neg(pos).
 1604square(o6).
 1605circle(o5).
 1606in(o5,o6).
 1607circle(o4).
 1608square(o3).
 1609in(o3,o4).
 1610square(o2).
 1611circle(o1).
 1612in(o1,o2).
 1613end(model(326)).
 1614
 1615begin(model(327)).
 1616neg(pos).
 1617square(o2).
 1618circle(o1).
 1619in(o1,o2).
 1620end(model(327)).
 1621
 1622begin(model(328)).
 1623neg(pos).
 1624square(o2).
 1625circle(o1).
 1626in(o1,o2).
 1627end(model(328)).
 1628
 1629begin(model(329)).
 1630neg(pos).
 1631triangle(o3).
 1632config(o3,up).
 1633circle(o2).
 1634in(o2,o3).
 1635square(o1).
 1636end(model(329)).
 1637
 1638begin(model(331)).
 1639pos.
 1640triangle(o4).
 1641config(o4,up).
 1642triangle(o3).
 1643config(o3,up).
 1644in(o3,o4).
 1645triangle(o2).
 1646config(o2,down).
 1647triangle(o1).
 1648config(o1,down).
 1649in(o1,o2).
 1650end(model(331)).
 1651
 1652begin(model(334)).
 1653neg(pos).
 1654triangle(o4).
 1655config(o4,up).
 1656circle(o3).
 1657in(o3,o4).
 1658square(o2).
 1659square(o1).
 1660in(o1,o2).
 1661end(model(334)).
 1662
 1663begin(model(337)).
 1664neg(pos).
 1665circle(o4).
 1666circle(o3).
 1667in(o3,o4).
 1668triangle(o2).
 1669config(o2,down).
 1670square(o1).
 1671in(o1,o2).
 1672end(model(337)).
 1673
 1674begin(model(343)).
 1675pos.
 1676triangle(o6).
 1677config(o6,down).
 1678triangle(o5).
 1679config(o5,up).
 1680in(o5,o6).
 1681square(o4).
 1682square(o3).
 1683in(o3,o4).
 1684square(o2).
 1685circle(o1).
 1686in(o1,o2).
 1687end(model(343)).
 1688
 1689begin(model(345)).
 1690pos.
 1691circle(o5).
 1692triangle(o4).
 1693config(o4,up).
 1694in(o4,o5).
 1695circle(o3).
 1696triangle(o2).
 1697config(o2,up).
 1698in(o2,o3).
 1699square(o1).
 1700end(model(345)).
 1701
 1702begin(model(348)).
 1703neg(pos).
 1704square(o4).
 1705square(o3).
 1706in(o3,o4).
 1707square(o2).
 1708circle(o1).
 1709in(o1,o2).
 1710end(model(348)).
 1711
 1712begin(model(352)).
 1713neg(pos).
 1714triangle(o6).
 1715config(o6,down).
 1716circle(o5).
 1717in(o5,o6).
 1718triangle(o4).
 1719config(o4,up).
 1720circle(o3).
 1721in(o3,o4).
 1722square(o2).
 1723square(o1).
 1724in(o1,o2).
 1725end(model(352)).
 1726
 1727begin(model(353)).
 1728neg(pos).
 1729square(o2).
 1730square(o1).
 1731in(o1,o2).
 1732end(model(353)).
 1733
 1734begin(model(355)).
 1735neg(pos).
 1736square(o2).
 1737triangle(o1).
 1738config(o1,up).
 1739in(o1,o2).
 1740end(model(355)).
 1741
 1742begin(model(358)).
 1743pos.
 1744circle(o6).
 1745square(o5).
 1746in(o5,o6).
 1747circle(o4).
 1748triangle(o3).
 1749config(o3,up).
 1750in(o3,o4).
 1751triangle(o2).
 1752config(o2,up).
 1753triangle(o1).
 1754config(o1,down).
 1755in(o1,o2).
 1756end(model(358)).
 1757
 1758begin(model(366)).
 1759pos.
 1760square(o6).
 1761triangle(o5).
 1762config(o5,down).
 1763in(o5,o6).
 1764circle(o4).
 1765triangle(o3).
 1766config(o3,down).
 1767in(o3,o4).
 1768triangle(o2).
 1769config(o2,down).
 1770triangle(o1).
 1771config(o1,up).
 1772in(o1,o2).
 1773end(model(366)).
 1774
 1775begin(model(369)).
 1776neg(pos).
 1777triangle(o6).
 1778config(o6,down).
 1779circle(o5).
 1780in(o5,o6).
 1781square(o4).
 1782square(o3).
 1783in(o3,o4).
 1784triangle(o2).
 1785config(o2,up).
 1786square(o1).
 1787in(o1,o2).
 1788end(model(369)).
 1789
 1790begin(model(370)).
 1791neg(pos).
 1792circle(o6).
 1793circle(o5).
 1794in(o5,o6).
 1795square(o4).
 1796triangle(o3).
 1797config(o3,down).
 1798in(o3,o4).
 1799square(o2).
 1800square(o1).
 1801in(o1,o2).
 1802end(model(370)).
 1803
 1804begin(model(373)).
 1805pos.
 1806triangle(o3).
 1807config(o3,up).
 1808triangle(o2).
 1809config(o2,down).
 1810in(o2,o3).
 1811square(o1).
 1812end(model(373)).
 1813
 1814begin(model(375)).
 1815pos.
 1816triangle(o4).
 1817config(o4,down).
 1818circle(o3).
 1819in(o3,o4).
 1820triangle(o2).
 1821config(o2,up).
 1822triangle(o1).
 1823config(o1,up).
 1824in(o1,o2).
 1825end(model(375)).
 1826
 1827begin(model(376)).
 1828neg(pos).
 1829square(o4).
 1830triangle(o3).
 1831config(o3,down).
 1832in(o3,o4).
 1833square(o2).
 1834square(o1).
 1835in(o1,o2).
 1836end(model(376)).
 1837
 1838begin(model(378)).
 1839neg(pos).
 1840square(o3).
 1841circle(o2).
 1842in(o2,o3).
 1843square(o1).
 1844end(model(378)).
 1845
 1846begin(model(379)).
 1847pos.
 1848triangle(o3).
 1849config(o3,up).
 1850triangle(o2).
 1851config(o2,up).
 1852in(o2,o3).
 1853triangle(o1).
 1854config(o1,up).
 1855end(model(379)).
 1856
 1857begin(model(381)).
 1858pos.
 1859circle(o5).
 1860square(o4).
 1861in(o4,o5).
 1862square(o3).
 1863triangle(o2).
 1864config(o2,down).
 1865in(o2,o3).
 1866triangle(o1).
 1867config(o1,up).
 1868end(model(381)).
 1869
 1870begin(model(382)).
 1871pos.
 1872circle(o4).
 1873triangle(o3).
 1874config(o3,up).
 1875in(o3,o4).
 1876square(o2).
 1877square(o1).
 1878in(o1,o2).
 1879end(model(382)).
 1880
 1881begin(model(390)).
 1882pos.
 1883triangle(o4).
 1884config(o4,down).
 1885circle(o3).
 1886in(o3,o4).
 1887triangle(o2).
 1888config(o2,down).
 1889triangle(o1).
 1890config(o1,down).
 1891in(o1,o2).
 1892end(model(390)).
 1893
 1894begin(model(393)).
 1895neg(pos).
 1896triangle(o3).
 1897config(o3,up).
 1898square(o2).
 1899in(o2,o3).
 1900square(o1).
 1901end(model(393)).
 1902
 1903begin(model(402)).
 1904pos.
 1905triangle(o5).
 1906config(o5,down).
 1907square(o4).
 1908in(o4,o5).
 1909triangle(o3).
 1910config(o3,down).
 1911triangle(o2).
 1912config(o2,up).
 1913in(o2,o3).
 1914circle(o1).
 1915end(model(402)).
 1916
 1917begin(model(404)).
 1918neg(pos).
 1919square(o3).
 1920circle(o2).
 1921in(o2,o3).
 1922circle(o1).
 1923end(model(404)).
 1924
 1925begin(model(408)).
 1926neg(pos).
 1927square(o2).
 1928square(o1).
 1929in(o1,o2).
 1930end(model(408)).
 1931
 1932begin(model(411)).
 1933neg(pos).
 1934circle(o5).
 1935triangle(o4).
 1936config(o4,down).
 1937in(o4,o5).
 1938circle(o3).
 1939circle(o2).
 1940in(o2,o3).
 1941square(o1).
 1942end(model(411)).
 1943
 1944begin(model(412)).
 1945neg(pos).
 1946circle(o6).
 1947circle(o5).
 1948in(o5,o6).
 1949square(o4).
 1950circle(o3).
 1951in(o3,o4).
 1952circle(o2).
 1953square(o1).
 1954in(o1,o2).
 1955end(model(412)).
 1956
 1957begin(model(416)).
 1958neg(pos).
 1959circle(o4).
 1960square(o3).
 1961in(o3,o4).
 1962square(o2).
 1963circle(o1).
 1964in(o1,o2).
 1965end(model(416)).
 1966
 1967begin(model(417)).
 1968neg(pos).
 1969triangle(o6).
 1970config(o6,up).
 1971square(o5).
 1972in(o5,o6).
 1973square(o4).
 1974circle(o3).
 1975in(o3,o4).
 1976triangle(o2).
 1977config(o2,up).
 1978square(o1).
 1979in(o1,o2).
 1980end(model(417)).
 1981
 1982begin(model(419)).
 1983neg(pos).
 1984square(o2).
 1985circle(o1).
 1986in(o1,o2).
 1987end(model(419)).
 1988
 1989begin(model(420)).
 1990pos.
 1991triangle(o4).
 1992config(o4,up).
 1993triangle(o3).
 1994config(o3,up).
 1995in(o3,o4).
 1996triangle(o2).
 1997config(o2,up).
 1998triangle(o1).
 1999config(o1,down).
 2000in(o1,o2).
 2001end(model(420)).
 2002
 2003begin(model(421)).
 2004neg(pos).
 2005square(o2).
 2006triangle(o1).
 2007config(o1,up).
 2008in(o1,o2).
 2009end(model(421)).
 2010
 2011begin(model(424)).
 2012neg(pos).
 2013square(o2).
 2014circle(o1).
 2015in(o1,o2).
 2016end(model(424)).
 2017
 2018begin(model(425)).
 2019neg(pos).
 2020triangle(o3).
 2021config(o3,up).
 2022circle(o2).
 2023in(o2,o3).
 2024square(o1).
 2025end(model(425)).
 2026
 2027begin(model(427)).
 2028pos.
 2029square(o6).
 2030circle(o5).
 2031in(o5,o6).
 2032square(o4).
 2033square(o3).
 2034in(o3,o4).
 2035triangle(o2).
 2036config(o2,up).
 2037triangle(o1).
 2038config(o1,up).
 2039in(o1,o2).
 2040end(model(427)).
 2041
 2042begin(model(428)).
 2043pos.
 2044circle(o4).
 2045square(o3).
 2046in(o3,o4).
 2047square(o2).
 2048triangle(o1).
 2049config(o1,down).
 2050in(o1,o2).
 2051end(model(428)).
 2052
 2053begin(model(431)).
 2054neg(pos).
 2055square(o2).
 2056triangle(o1).
 2057config(o1,up).
 2058in(o1,o2).
 2059end(model(431)).
 2060
 2061begin(model(432)).
 2062neg(pos).
 2063square(o3).
 2064circle(o2).
 2065in(o2,o3).
 2066circle(o1).
 2067end(model(432)).
 2068
 2069begin(model(433)).
 2070pos.
 2071triangle(o6).
 2072config(o6,down).
 2073square(o5).
 2074in(o5,o6).
 2075circle(o4).
 2076square(o3).
 2077in(o3,o4).
 2078circle(o2).
 2079square(o1).
 2080in(o1,o2).
 2081end(model(433)).
 2082
 2083begin(model(437)).
 2084neg(pos).
 2085triangle(o2).
 2086config(o2,up).
 2087circle(o1).
 2088in(o1,o2).
 2089end(model(437)).
 2090
 2091begin(model(444)).
 2092neg(pos).
 2093triangle(o3).
 2094config(o3,down).
 2095circle(o2).
 2096in(o2,o3).
 2097triangle(o1).
 2098config(o1,up).
 2099end(model(444)).
 2100
 2101begin(model(445)).
 2102neg(pos).
 2103square(o5).
 2104triangle(o4).
 2105config(o4,up).
 2106in(o4,o5).
 2107triangle(o3).
 2108config(o3,down).
 2109square(o2).
 2110in(o2,o3).
 2111square(o1).
 2112end(model(445)).
 2113
 2114begin(model(447)).
 2115neg(pos).
 2116square(o5).
 2117square(o4).
 2118in(o4,o5).
 2119square(o3).
 2120triangle(o2).
 2121config(o2,up).
 2122in(o2,o3).
 2123triangle(o1).
 2124config(o1,down).
 2125end(model(447)).
 2126
 2127begin(model(453)).
 2128pos.
 2129circle(o6).
 2130triangle(o5).
 2131config(o5,down).
 2132in(o5,o6).
 2133triangle(o4).
 2134config(o4,down).
 2135triangle(o3).
 2136config(o3,up).
 2137in(o3,o4).
 2138triangle(o2).
 2139config(o2,up).
 2140triangle(o1).
 2141config(o1,up).
 2142in(o1,o2).
 2143end(model(453)).
 2144
 2145begin(model(456)).
 2146pos.
 2147triangle(o3).
 2148config(o3,up).
 2149triangle(o2).
 2150config(o2,up).
 2151in(o2,o3).
 2152square(o1).
 2153end(model(456)).
 2154
 2155begin(model(457)).
 2156neg(pos).
 2157square(o4).
 2158triangle(o3).
 2159config(o3,up).
 2160in(o3,o4).
 2161triangle(o2).
 2162config(o2,up).
 2163square(o1).
 2164in(o1,o2).
 2165end(model(457)).
 2166
 2167begin(model(459)).
 2168pos.
 2169triangle(o6).
 2170config(o6,down).
 2171triangle(o5).
 2172config(o5,up).
 2173in(o5,o6).
 2174circle(o4).
 2175circle(o3).
 2176in(o3,o4).
 2177triangle(o2).
 2178config(o2,down).
 2179circle(o1).
 2180in(o1,o2).
 2181end(model(459)).
 2182
 2183begin(model(462)).
 2184neg(pos).
 2185square(o2).
 2186triangle(o1).
 2187config(o1,down).
 2188in(o1,o2).
 2189end(model(462)).
 2190
 2191begin(model(463)).
 2192pos.
 2193square(o6).
 2194triangle(o5).
 2195config(o5,down).
 2196in(o5,o6).
 2197square(o4).
 2198square(o3).
 2199in(o3,o4).
 2200circle(o2).
 2201square(o1).
 2202in(o1,o2).
 2203end(model(463)).
 2204
 2205begin(model(464)).
 2206pos.
 2207triangle(o4).
 2208config(o4,down).
 2209square(o3).
 2210in(o3,o4).
 2211triangle(o2).
 2212config(o2,up).
 2213triangle(o1).
 2214config(o1,up).
 2215in(o1,o2).
 2216end(model(464)).
 2217
 2218begin(model(465)).
 2219pos.
 2220triangle(o3).
 2221config(o3,down).
 2222triangle(o2).
 2223config(o2,down).
 2224in(o2,o3).
 2225square(o1).
 2226end(model(465)).
 2227
 2228begin(model(468)).
 2229neg(pos).
 2230circle(o2).
 2231circle(o1).
 2232in(o1,o2).
 2233end(model(468)).
 2234
 2235begin(model(470)).
 2236neg(pos).
 2237triangle(o4).
 2238config(o4,down).
 2239square(o3).
 2240in(o3,o4).
 2241circle(o2).
 2242circle(o1).
 2243in(o1,o2).
 2244end(model(470)).
 2245
 2246begin(model(473)).
 2247neg(pos).
 2248square(o4).
 2249triangle(o3).
 2250config(o3,up).
 2251in(o3,o4).
 2252square(o2).
 2253circle(o1).
 2254in(o1,o2).
 2255end(model(473)).
 2256
 2257begin(model(474)).
 2258neg(pos).
 2259triangle(o6).
 2260config(o6,up).
 2261square(o5).
 2262in(o5,o6).
 2263square(o4).
 2264circle(o3).
 2265in(o3,o4).
 2266square(o2).
 2267circle(o1).
 2268in(o1,o2).
 2269end(model(474)).
 2270
 2271begin(model(476)).
 2272neg(pos).
 2273triangle(o5).
 2274config(o5,down).
 2275square(o4).
 2276in(o4,o5).
 2277circle(o3).
 2278circle(o2).
 2279in(o2,o3).
 2280square(o1).
 2281end(model(476)).
 2282
 2283begin(model(477)).
 2284neg(pos).
 2285square(o4).
 2286triangle(o3).
 2287config(o3,up).
 2288in(o3,o4).
 2289square(o2).
 2290triangle(o1).
 2291config(o1,up).
 2292in(o1,o2).
 2293end(model(477)).
 2294
 2295begin(model(479)).
 2296pos.
 2297circle(o2).
 2298triangle(o1).
 2299config(o1,up).
 2300in(o1,o2).
 2301end(model(479)).
 2302
 2303begin(model(481)).
 2304neg(pos).
 2305triangle(o2).
 2306config(o2,down).
 2307circle(o1).
 2308in(o1,o2).
 2309end(model(481)).
 2310
 2311begin(model(482)).
 2312pos.
 2313triangle(o4).
 2314config(o4,up).
 2315triangle(o3).
 2316config(o3,up).
 2317in(o3,o4).
 2318circle(o2).
 2319triangle(o1).
 2320config(o1,up).
 2321in(o1,o2).
 2322end(model(482)).
 2323
 2324begin(model(483)).
 2325neg(pos).
 2326circle(o4).
 2327circle(o3).
 2328in(o3,o4).
 2329square(o2).
 2330square(o1).
 2331in(o1,o2).
 2332end(model(483)).
 2333
 2334begin(model(485)).
 2335neg(pos).
 2336triangle(o2).
 2337config(o2,down).
 2338circle(o1).
 2339in(o1,o2).
 2340end(model(485)).
 2341
 2342begin(model(488)).
 2343neg(pos).
 2344triangle(o4).
 2345config(o4,down).
 2346circle(o3).
 2347in(o3,o4).
 2348square(o2).
 2349circle(o1).
 2350in(o1,o2).
 2351end(model(488)).
 2352
 2353begin(model(489)).
 2354neg(pos).
 2355triangle(o3).
 2356config(o3,down).
 2357square(o2).
 2358in(o2,o3).
 2359square(o1).
 2360end(model(489)).
 2361
 2362begin(model(490)).
 2363neg(pos).
 2364triangle(o5).
 2365config(o5,down).
 2366circle(o4).
 2367in(o4,o5).
 2368circle(o3).
 2369circle(o2).
 2370in(o2,o3).
 2371square(o1).
 2372end(model(490)).
 2373
 2374begin(model(491)).
 2375neg(pos).
 2376triangle(o2).
 2377config(o2,up).
 2378square(o1).
 2379in(o1,o2).
 2380end(model(491)).
 2381
 2382begin(model(494)).
 2383neg(pos).
 2384triangle(o2).
 2385config(o2,up).
 2386square(o1).
 2387in(o1,o2).
 2388end(model(494)).
 2389
 2390begin(model(497)).
 2391neg(pos).
 2392triangle(o2).
 2393config(o2,up).
 2394square(o1).
 2395in(o1,o2).
 2396end(model(497)).
 2397
 2398begin(model(499)).
 2399neg(pos).
 2400square(o5).
 2401triangle(o4).
 2402config(o4,down).
 2403in(o4,o5).
 2404square(o3).
 2405square(o2).
 2406in(o2,o3).
 2407square(o1).
 2408end(model(499)).
 2409
 2410begin(model(500)).
 2411neg(pos).
 2412circle(o3).
 2413circle(o2).
 2414in(o2,o3).
 2415square(o1).
 2416end(model(500)).
 2417
 2418begin(model(512)).
 2419neg(pos).
 2420square(o2).
 2421triangle(o1).
 2422config(o1,down).
 2423in(o1,o2).
 2424end(model(512)).
 2425
 2426begin(model(513)).
 2427neg(pos).
 2428triangle(o6).
 2429config(o6,up).
 2430square(o5).
 2431in(o5,o6).
 2432square(o4).
 2433triangle(o3).
 2434config(o3,up).
 2435in(o3,o4).
 2436triangle(o2).
 2437config(o2,up).
 2438square(o1).
 2439in(o1,o2).
 2440end(model(513)).
 2441
 2442begin(model(516)).
 2443pos.
 2444circle(o4).
 2445square(o3).
 2446in(o3,o4).
 2447circle(o2).
 2448triangle(o1).
 2449config(o1,down).
 2450in(o1,o2).
 2451end(model(516)).
 2452
 2453begin(model(517)).
 2454neg(pos).
 2455square(o5).
 2456square(o4).
 2457in(o4,o5).
 2458triangle(o3).
 2459config(o3,down).
 2460square(o2).
 2461in(o2,o3).
 2462square(o1).
 2463end(model(517)).
 2464
 2465begin(model(520)).
 2466pos.
 2467triangle(o2).
 2468config(o2,down).
 2469triangle(o1).
 2470config(o1,down).
 2471in(o1,o2).
 2472end(model(520)).
 2473
 2474begin(model(521)).
 2475neg(pos).
 2476circle(o6).
 2477circle(o5).
 2478in(o5,o6).
 2479square(o4).
 2480square(o3).
 2481in(o3,o4).
 2482circle(o2).
 2483square(o1).
 2484in(o1,o2).
 2485end(model(521)).
 2486
 2487begin(model(527)).
 2488pos.
 2489circle(o5).
 2490triangle(o4).
 2491config(o4,up).
 2492in(o4,o5).
 2493circle(o3).
 2494square(o2).
 2495in(o2,o3).
 2496triangle(o1).
 2497config(o1,up).
 2498end(model(527)).
 2499
 2500begin(model(529)).
 2501neg(pos).
 2502square(o4).
 2503triangle(o3).
 2504config(o3,up).
 2505in(o3,o4).
 2506square(o2).
 2507circle(o1).
 2508in(o1,o2).
 2509end(model(529)).
 2510
 2511begin(model(531)).
 2512neg(pos).
 2513circle(o2).
 2514circle(o1).
 2515in(o1,o2).
 2516end(model(531)).
 2517
 2518begin(model(533)).
 2519neg(pos).
 2520triangle(o4).
 2521config(o4,up).
 2522square(o3).
 2523in(o3,o4).
 2524square(o2).
 2525square(o1).
 2526in(o1,o2).
 2527end(model(533)).
 2528
 2529begin(model(534)).
 2530neg(pos).
 2531circle(o2).
 2532circle(o1).
 2533in(o1,o2).
 2534end(model(534)).
 2535
 2536begin(model(539)).
 2537pos.
 2538square(o6).
 2539triangle(o5).
 2540config(o5,down).
 2541in(o5,o6).
 2542circle(o4).
 2543square(o3).
 2544in(o3,o4).
 2545square(o2).
 2546square(o1).
 2547in(o1,o2).
 2548end(model(539)).
 2549
 2550begin(model(540)).
 2551neg(pos).
 2552circle(o2).
 2553circle(o1).
 2554in(o1,o2).
 2555end(model(540)).
 2556
 2557begin(model(542)).
 2558neg(pos).
 2559square(o5).
 2560square(o4).
 2561in(o4,o5).
 2562triangle(o3).
 2563config(o3,up).
 2564circle(o2).
 2565in(o2,o3).
 2566triangle(o1).
 2567config(o1,down).
 2568end(model(542)).
 2569
 2570begin(model(543)).
 2571neg(pos).
 2572triangle(o4).
 2573config(o4,up).
 2574square(o3).
 2575in(o3,o4).
 2576circle(o2).
 2577circle(o1).
 2578in(o1,o2).
 2579end(model(543)).
 2580
 2581begin(model(544)).
 2582neg(pos).
 2583circle(o6).
 2584circle(o5).
 2585in(o5,o6).
 2586square(o4).
 2587circle(o3).
 2588in(o3,o4).
 2589circle(o2).
 2590square(o1).
 2591in(o1,o2).
 2592end(model(544)).
 2593
 2594begin(model(546)).
 2595neg(pos).
 2596square(o3).
 2597circle(o2).
 2598in(o2,o3).
 2599circle(o1).
 2600end(model(546)).
 2601
 2602begin(model(550)).
 2603pos.
 2604triangle(o4).
 2605config(o4,up).
 2606square(o3).
 2607in(o3,o4).
 2608circle(o2).
 2609square(o1).
 2610in(o1,o2).
 2611end(model(550)).
 2612
 2613begin(model(552)).
 2614pos.
 2615circle(o4).
 2616triangle(o3).
 2617config(o3,down).
 2618in(o3,o4).
 2619circle(o2).
 2620triangle(o1).
 2621config(o1,up).
 2622in(o1,o2).
 2623end(model(552)).
 2624
 2625begin(model(553)).
 2626neg(pos).
 2627circle(o2).
 2628circle(o1).
 2629in(o1,o2).
 2630end(model(553)).
 2631
 2632begin(model(555)).
 2633neg(pos).
 2634square(o4).
 2635triangle(o3).
 2636config(o3,down).
 2637in(o3,o4).
 2638square(o2).
 2639circle(o1).
 2640in(o1,o2).
 2641end(model(555)).
 2642
 2643begin(model(559)).
 2644neg(pos).
 2645square(o3).
 2646circle(o2).
 2647in(o2,o3).
 2648triangle(o1).
 2649config(o1,up).
 2650end(model(559)).
 2651
 2652begin(model(565)).
 2653pos.
 2654triangle(o6).
 2655config(o6,down).
 2656triangle(o5).
 2657config(o5,up).
 2658in(o5,o6).
 2659circle(o4).
 2660square(o3).
 2661in(o3,o4).
 2662triangle(o2).
 2663config(o2,up).
 2664circle(o1).
 2665in(o1,o2).
 2666end(model(565)).
 2667
 2668begin(model(567)).
 2669pos.
 2670circle(o3).
 2671square(o2).
 2672in(o2,o3).
 2673triangle(o1).
 2674config(o1,down).
 2675end(model(567)).
 2676
 2677begin(model(568)).
 2678pos.
 2679square(o6).
 2680square(o5).
 2681in(o5,o6).
 2682square(o4).
 2683triangle(o3).
 2684config(o3,up).
 2685in(o3,o4).
 2686circle(o2).
 2687triangle(o1).
 2688config(o1,up).
 2689in(o1,o2).
 2690end(model(568)).
 2691
 2692begin(model(572)).
 2693pos.
 2694triangle(o4).
 2695config(o4,down).
 2696triangle(o3).
 2697config(o3,down).
 2698in(o3,o4).
 2699square(o2).
 2700triangle(o1).
 2701config(o1,up).
 2702in(o1,o2).
 2703end(model(572)).
 2704
 2705begin(model(578)).
 2706neg(pos).
 2707square(o2).
 2708triangle(o1).
 2709config(o1,up).
 2710in(o1,o2).
 2711end(model(578)).
 2712
 2713begin(model(582)).
 2714pos.
 2715triangle(o4).
 2716config(o4,down).
 2717triangle(o3).
 2718config(o3,up).
 2719in(o3,o4).
 2720circle(o2).
 2721triangle(o1).
 2722config(o1,down).
 2723in(o1,o2).
 2724end(model(582)).
 2725
 2726begin(model(583)).
 2727neg(pos).
 2728square(o3).
 2729circle(o2).
 2730in(o2,o3).
 2731square(o1).
 2732end(model(583)).
 2733
 2734begin(model(591)).
 2735neg(pos).
 2736square(o2).
 2737triangle(o1).
 2738config(o1,up).
 2739in(o1,o2).
 2740end(model(591)).
 2741
 2742begin(model(595)).
 2743pos.
 2744square(o4).
 2745triangle(o3).
 2746config(o3,down).
 2747in(o3,o4).
 2748triangle(o2).
 2749config(o2,down).
 2750triangle(o1).
 2751config(o1,up).
 2752in(o1,o2).
 2753end(model(595)).
 2754
 2755begin(model(597)).
 2756pos.
 2757circle(o4).
 2758square(o3).
 2759in(o3,o4).
 2760triangle(o2).
 2761config(o2,up).
 2762square(o1).
 2763in(o1,o2).
 2764end(model(597)).
 2765
 2766begin(model(600)).
 2767neg(pos).
 2768square(o2).
 2769square(o1).
 2770in(o1,o2).
 2771end(model(600)).
 2772
 2773begin(model(602)).
 2774pos.
 2775circle(o5).
 2776triangle(o4).
 2777config(o4,down).
 2778in(o4,o5).
 2779circle(o3).
 2780triangle(o2).
 2781config(o2,up).
 2782in(o2,o3).
 2783circle(o1).
 2784end(model(602)).
 2785
 2786begin(model(609)).
 2787neg(pos).
 2788circle(o2).
 2789circle(o1).
 2790in(o1,o2).
 2791end(model(609)).
 2792
 2793begin(model(612)).
 2794neg(pos).
 2795triangle(o5).
 2796config(o5,down).
 2797circle(o4).
 2798in(o4,o5).
 2799square(o3).
 2800square(o2).
 2801in(o2,o3).
 2802square(o1).
 2803end(model(612)).
 2804
 2805begin(model(614)).
 2806neg(pos).
 2807triangle(o3).
 2808config(o3,up).
 2809square(o2).
 2810in(o2,o3).
 2811square(o1).
 2812end(model(614)).
 2813
 2814begin(model(615)).
 2815neg(pos).
 2816square(o2).
 2817triangle(o1).
 2818config(o1,up).
 2819in(o1,o2).
 2820end(model(615)).
 2821
 2822begin(model(616)).
 2823neg(pos).
 2824circle(o2).
 2825circle(o1).
 2826in(o1,o2).
 2827end(model(616)).
 2828
 2829begin(model(617)).
 2830neg(pos).
 2831square(o5).
 2832triangle(o4).
 2833config(o4,down).
 2834in(o4,o5).
 2835square(o3).
 2836square(o2).
 2837in(o2,o3).
 2838square(o1).
 2839end(model(617)).
 2840
 2841begin(model(622)).
 2842pos.
 2843triangle(o2).
 2844config(o2,down).
 2845triangle(o1).
 2846config(o1,down).
 2847in(o1,o2).
 2848end(model(622)).
 2849
 2850begin(model(625)).
 2851neg(pos).
 2852circle(o2).
 2853circle(o1).
 2854in(o1,o2).
 2855end(model(625)).
 2856
 2857begin(model(628)).
 2858neg(pos).
 2859triangle(o5).
 2860config(o5,down).
 2861circle(o4).
 2862in(o4,o5).
 2863square(o3).
 2864square(o2).
 2865in(o2,o3).
 2866square(o1).
 2867end(model(628)).
 2868
 2869begin(model(634)).
 2870pos.
 2871square(o6).
 2872triangle(o5).
 2873config(o5,up).
 2874in(o5,o6).
 2875triangle(o4).
 2876config(o4,down).
 2877triangle(o3).
 2878config(o3,up).
 2879in(o3,o4).
 2880circle(o2).
 2881square(o1).
 2882in(o1,o2).
 2883end(model(634)).
 2884
 2885begin(model(635)).
 2886neg(pos).
 2887triangle(o5).
 2888config(o5,down).
 2889circle(o4).
 2890in(o4,o5).
 2891triangle(o3).
 2892config(o3,up).
 2893square(o2).
 2894in(o2,o3).
 2895circle(o1).
 2896end(model(635)).
 2897
 2898begin(model(637)).
 2899neg(pos).
 2900square(o2).
 2901triangle(o1).
 2902config(o1,up).
 2903in(o1,o2).
 2904end(model(637)).
 2905
 2906begin(model(639)).
 2907pos.
 2908triangle(o5).
 2909config(o5,up).
 2910square(o4).
 2911in(o4,o5).
 2912circle(o3).
 2913square(o2).
 2914in(o2,o3).
 2915triangle(o1).
 2916config(o1,up).
 2917end(model(639)).
 2918
 2919begin(model(640)).
 2920pos.
 2921circle(o6).
 2922square(o5).
 2923in(o5,o6).
 2924triangle(o4).
 2925config(o4,up).
 2926triangle(o3).
 2927config(o3,down).
 2928in(o3,o4).
 2929triangle(o2).
 2930config(o2,down).
 2931square(o1).
 2932in(o1,o2).
 2933end(model(640)).
 2934
 2935begin(model(641)).
 2936pos.
 2937circle(o2).
 2938triangle(o1).
 2939config(o1,up).
 2940in(o1,o2).
 2941end(model(641)).
 2942
 2943begin(model(642)).
 2944pos.
 2945circle(o6).
 2946square(o5).
 2947in(o5,o6).
 2948triangle(o4).
 2949config(o4,up).
 2950square(o3).
 2951in(o3,o4).
 2952circle(o2).
 2953square(o1).
 2954in(o1,o2).
 2955end(model(642)).
 2956
 2957begin(model(647)).
 2958pos.
 2959triangle(o4).
 2960config(o4,up).
 2961triangle(o3).
 2962config(o3,down).
 2963in(o3,o4).
 2964square(o2).
 2965square(o1).
 2966in(o1,o2).
 2967end(model(647)).
 2968
 2969begin(model(648)).
 2970pos.
 2971triangle(o6).
 2972config(o6,down).
 2973triangle(o5).
 2974config(o5,down).
 2975in(o5,o6).
 2976square(o4).
 2977circle(o3).
 2978in(o3,o4).
 2979circle(o2).
 2980circle(o1).
 2981in(o1,o2).
 2982end(model(648)).
 2983
 2984begin(model(649)).
 2985pos.
 2986square(o4).
 2987triangle(o3).
 2988config(o3,up).
 2989in(o3,o4).
 2990circle(o2).
 2991square(o1).
 2992in(o1,o2).
 2993end(model(649)).
 2994
 2995begin(model(650)).
 2996pos.
 2997circle(o4).
 2998square(o3).
 2999in(o3,o4).
 3000square(o2).
 3001triangle(o1).
 3002config(o1,up).
 3003in(o1,o2).
 3004end(model(650)).
 3005
 3006begin(model(654)).
 3007neg(pos).
 3008triangle(o4).
 3009config(o4,up).
 3010circle(o3).
 3011in(o3,o4).
 3012circle(o2).
 3013circle(o1).
 3014in(o1,o2).
 3015end(model(654)).
 3016
 3017begin(model(656)).
 3018neg(pos).
 3019square(o2).
 3020triangle(o1).
 3021config(o1,down).
 3022in(o1,o2).
 3023end(model(656)).
 3024
 3025begin(model(657)).
 3026pos.
 3027circle(o3).
 3028triangle(o2).
 3029config(o2,up).
 3030in(o2,o3).
 3031square(o1).
 3032end(model(657)).
 3033
 3034begin(model(658)).
 3035neg(pos).
 3036square(o4).
 3037circle(o3).
 3038in(o3,o4).
 3039square(o2).
 3040circle(o1).
 3041in(o1,o2).
 3042end(model(658)).
 3043
 3044begin(model(662)).
 3045neg(pos).
 3046square(o3).
 3047circle(o2).
 3048in(o2,o3).
 3049circle(o1).
 3050end(model(662)).
 3051
 3052begin(model(667)).
 3053pos.
 3054circle(o6).
 3055circle(o5).
 3056in(o5,o6).
 3057triangle(o4).
 3058config(o4,down).
 3059circle(o3).
 3060in(o3,o4).
 3061triangle(o2).
 3062config(o2,up).
 3063triangle(o1).
 3064config(o1,down).
 3065in(o1,o2).
 3066end(model(667)).
 3067
 3068begin(model(669)).
 3069neg(pos).
 3070square(o4).
 3071square(o3).
 3072in(o3,o4).
 3073square(o2).
 3074triangle(o1).
 3075config(o1,down).
 3076in(o1,o2).
 3077end(model(669)).
 3078
 3079begin(model(671)).
 3080neg(pos).
 3081square(o5).
 3082square(o4).
 3083in(o4,o5).
 3084triangle(o3).
 3085config(o3,up).
 3086circle(o2).
 3087in(o2,o3).
 3088square(o1).
 3089end(model(671)).
 3090
 3091begin(model(679)).
 3092neg(pos).
 3093triangle(o2).
 3094config(o2,up).
 3095square(o1).
 3096in(o1,o2).
 3097end(model(679)).
 3098
 3099begin(model(682)).
 3100neg(pos).
 3101triangle(o4).
 3102config(o4,up).
 3103square(o3).
 3104in(o3,o4).
 3105triangle(o2).
 3106config(o2,up).
 3107square(o1).
 3108in(o1,o2).
 3109end(model(682)).
 3110
 3111begin(model(683)).
 3112neg(pos).
 3113square(o4).
 3114circle(o3).
 3115in(o3,o4).
 3116triangle(o2).
 3117config(o2,down).
 3118circle(o1).
 3119in(o1,o2).
 3120end(model(683)).
 3121
 3122begin(model(685)).
 3123pos.
 3124square(o6).
 3125circle(o5).
 3126in(o5,o6).
 3127circle(o4).
 3128circle(o3).
 3129in(o3,o4).
 3130triangle(o2).
 3131config(o2,up).
 3132triangle(o1).
 3133config(o1,up).
 3134in(o1,o2).
 3135end(model(685)).
 3136
 3137begin(model(686)).
 3138pos.
 3139circle(o4).
 3140triangle(o3).
 3141config(o3,up).
 3142in(o3,o4).
 3143square(o2).
 3144triangle(o1).
 3145config(o1,down).
 3146in(o1,o2).
 3147end(model(686)).
 3148
 3149begin(model(691)).
 3150neg(pos).
 3151square(o5).
 3152circle(o4).
 3153in(o4,o5).
 3154triangle(o3).
 3155config(o3,up).
 3156square(o2).
 3157in(o2,o3).
 3158circle(o1).
 3159end(model(691)).
 3160
 3161begin(model(693)).
 3162neg(pos).
 3163triangle(o6).
 3164config(o6,up).
 3165square(o5).
 3166in(o5,o6).
 3167square(o4).
 3168circle(o3).
 3169in(o3,o4).
 3170square(o2).
 3171triangle(o1).
 3172config(o1,down).
 3173in(o1,o2).
 3174end(model(693)).
 3175
 3176begin(model(698)).
 3177neg(pos).
 3178triangle(o6).
 3179config(o6,up).
 3180circle(o5).
 3181in(o5,o6).
 3182square(o4).
 3183square(o3).
 3184in(o3,o4).
 3185square(o2).
 3186square(o1).
 3187in(o1,o2).
 3188end(model(698)).
 3189
 3190begin(model(700)).
 3191neg(pos).
 3192triangle(o2).
 3193config(o2,down).
 3194circle(o1).
 3195in(o1,o2).
 3196end(model(700)).
 3197
 3198begin(model(701)).
 3199neg(pos).
 3200circle(o5).
 3201square(o4).
 3202in(o4,o5).
 3203circle(o3).
 3204circle(o2).
 3205in(o2,o3).
 3206circle(o1).
 3207end(model(701)).
 3208
 3209begin(model(705)).
 3210neg(pos).
 3211circle(o5).
 3212circle(o4).
 3213in(o4,o5).
 3214triangle(o3).
 3215config(o3,up).
 3216circle(o2).
 3217in(o2,o3).
 3218circle(o1).
 3219end(model(705)).
 3220
 3221begin(model(708)).
 3222neg(pos).
 3223triangle(o5).
 3224config(o5,up).
 3225square(o4).
 3226in(o4,o5).
 3227circle(o3).
 3228circle(o2).
 3229in(o2,o3).
 3230square(o1).
 3231end(model(708)).
 3232
 3233begin(model(709)).
 3234neg(pos).
 3235circle(o5).
 3236circle(o4).
 3237in(o4,o5).
 3238triangle(o3).
 3239config(o3,down).
 3240circle(o2).
 3241in(o2,o3).
 3242square(o1).
 3243end(model(709)).
 3244
 3245begin(model(710)).
 3246neg(pos).
 3247square(o4).
 3248triangle(o3).
 3249config(o3,down).
 3250in(o3,o4).
 3251square(o2).
 3252triangle(o1).
 3253config(o1,down).
 3254in(o1,o2).
 3255end(model(710)).
 3256
 3257begin(model(719)).
 3258neg(pos).
 3259square(o4).
 3260square(o3).
 3261in(o3,o4).
 3262triangle(o2).
 3263config(o2,down).
 3264circle(o1).
 3265in(o1,o2).
 3266end(model(719)).
 3267
 3268begin(model(722)).
 3269neg(pos).
 3270triangle(o4).
 3271config(o4,down).
 3272square(o3).
 3273in(o3,o4).
 3274triangle(o2).
 3275config(o2,up).
 3276square(o1).
 3277in(o1,o2).
 3278end(model(722)).
 3279
 3280begin(model(723)).
 3281neg(pos).
 3282circle(o4).
 3283circle(o3).
 3284in(o3,o4).
 3285triangle(o2).
 3286config(o2,down).
 3287circle(o1).
 3288in(o1,o2).
 3289end(model(723)).
 3290
 3291begin(model(725)).
 3292pos.
 3293triangle(o2).
 3294config(o2,down).
 3295triangle(o1).
 3296config(o1,down).
 3297in(o1,o2).
 3298end(model(725)).
 3299
 3300begin(model(728)).
 3301neg(pos).
 3302circle(o4).
 3303circle(o3).
 3304in(o3,o4).
 3305square(o2).
 3306circle(o1).
 3307in(o1,o2).
 3308end(model(728)).
 3309
 3310begin(model(732)).
 3311neg(pos).
 3312circle(o5).
 3313triangle(o4).
 3314config(o4,down).
 3315in(o4,o5).
 3316triangle(o3).
 3317config(o3,up).
 3318circle(o2).
 3319in(o2,o3).
 3320circle(o1).
 3321end(model(732)).
 3322
 3323begin(model(734)).
 3324neg(pos).
 3325square(o4).
 3326circle(o3).
 3327in(o3,o4).
 3328triangle(o2).
 3329config(o2,down).
 3330circle(o1).
 3331in(o1,o2).
 3332end(model(734)).
 3333
 3334begin(model(737)).
 3335neg(pos).
 3336square(o4).
 3337circle(o3).
 3338in(o3,o4).
 3339square(o2).
 3340triangle(o1).
 3341config(o1,down).
 3342in(o1,o2).
 3343end(model(737)).
 3344
 3345begin(model(740)).
 3346neg(pos).
 3347square(o2).
 3348square(o1).
 3349in(o1,o2).
 3350end(model(740)).
 3351
 3352begin(model(741)).
 3353neg(pos).
 3354triangle(o5).
 3355config(o5,up).
 3356circle(o4).
 3357in(o4,o5).
 3358square(o3).
 3359circle(o2).
 3360in(o2,o3).
 3361triangle(o1).
 3362config(o1,down).
 3363end(model(741)).
 3364
 3365begin(model(743)).
 3366neg(pos).
 3367triangle(o2).
 3368config(o2,down).
 3369square(o1).
 3370in(o1,o2).
 3371end(model(743)).
 3372
 3373begin(model(744)).
 3374neg(pos).
 3375triangle(o5).
 3376config(o5,down).
 3377square(o4).
 3378in(o4,o5).
 3379triangle(o3).
 3380config(o3,down).
 3381square(o2).
 3382in(o2,o3).
 3383triangle(o1).
 3384config(o1,down).
 3385end(model(744)).
 3386
 3387begin(model(745)).
 3388pos.
 3389circle(o3).
 3390square(o2).
 3391in(o2,o3).
 3392triangle(o1).
 3393config(o1,up).
 3394end(model(745)).
 3395
 3396begin(model(747)).
 3397neg(pos).
 3398square(o2).
 3399square(o1).
 3400in(o1,o2).
 3401end(model(747)).
 3402
 3403begin(model(748)).
 3404neg(pos).
 3405square(o5).
 3406circle(o4).
 3407in(o4,o5).
 3408triangle(o3).
 3409config(o3,down).
 3410circle(o2).
 3411in(o2,o3).
 3412triangle(o1).
 3413config(o1,up).
 3414end(model(748)).
 3415
 3416begin(model(750)).
 3417neg(pos).
 3418square(o4).
 3419triangle(o3).
 3420config(o3,up).
 3421in(o3,o4).
 3422triangle(o2).
 3423config(o2,up).
 3424square(o1).
 3425in(o1,o2).
 3426end(model(750)).
 3427
 3428begin(model(751)).
 3429neg(pos).
 3430triangle(o2).
 3431config(o2,down).
 3432square(o1).
 3433in(o1,o2).
 3434end(model(751)).
 3435
 3436begin(model(753)).
 3437pos.
 3438circle(o6).
 3439triangle(o5).
 3440config(o5,up).
 3441in(o5,o6).
 3442square(o4).
 3443square(o3).
 3444in(o3,o4).
 3445square(o2).
 3446square(o1).
 3447in(o1,o2).
 3448end(model(753)).
 3449
 3450begin(model(754)).
 3451neg(pos).
 3452square(o3).
 3453triangle(o2).
 3454config(o2,up).
 3455in(o2,o3).
 3456triangle(o1).
 3457config(o1,up).
 3458end(model(754)).
 3459
 3460begin(model(755)).
 3461neg(pos).
 3462triangle(o2).
 3463config(o2,up).
 3464circle(o1).
 3465in(o1,o2).
 3466end(model(755)).
 3467
 3468begin(model(765)).
 3469neg(pos).
 3470triangle(o2).
 3471config(o2,down).
 3472square(o1).
 3473in(o1,o2).
 3474end(model(765)).
 3475
 3476begin(model(766)).
 3477neg(pos).
 3478triangle(o3).
 3479config(o3,up).
 3480square(o2).
 3481in(o2,o3).
 3482triangle(o1).
 3483config(o1,down).
 3484end(model(766)).
 3485
 3486begin(model(768)).
 3487pos.
 3488square(o6).
 3489square(o5).
 3490in(o5,o6).
 3491circle(o4).
 3492triangle(o3).
 3493config(o3,down).
 3494in(o3,o4).
 3495triangle(o2).
 3496config(o2,down).
 3497triangle(o1).
 3498config(o1,up).
 3499in(o1,o2).
 3500end(model(768)).
 3501
 3502begin(model(769)).
 3503neg(pos).
 3504circle(o2).
 3505circle(o1).
 3506in(o1,o2).
 3507end(model(769)).
 3508
 3509begin(model(772)).
 3510neg(pos).
 3511square(o5).
 3512circle(o4).
 3513in(o4,o5).
 3514square(o3).
 3515triangle(o2).
 3516config(o2,down).
 3517in(o2,o3).
 3518triangle(o1).
 3519config(o1,down).
 3520end(model(772)).
 3521
 3522begin(model(773)).
 3523neg(pos).
 3524square(o5).
 3525triangle(o4).
 3526config(o4,up).
 3527in(o4,o5).
 3528square(o3).
 3529circle(o2).
 3530in(o2,o3).
 3531square(o1).
 3532end(model(773)).
 3533
 3534begin(model(777)).
 3535neg(pos).
 3536triangle(o3).
 3537config(o3,up).
 3538circle(o2).
 3539in(o2,o3).
 3540circle(o1).
 3541end(model(777)).
 3542
 3543begin(model(779)).
 3544neg(pos).
 3545square(o5).
 3546triangle(o4).
 3547config(o4,down).
 3548in(o4,o5).
 3549triangle(o3).
 3550config(o3,up).
 3551square(o2).
 3552in(o2,o3).
 3553square(o1).
 3554end(model(779)).
 3555
 3556begin(model(780)).
 3557neg(pos).
 3558square(o5).
 3559square(o4).
 3560in(o4,o5).
 3561circle(o3).
 3562circle(o2).
 3563in(o2,o3).
 3564circle(o1).
 3565end(model(780)).
 3566
 3567begin(model(781)).
 3568neg(pos).
 3569triangle(o6).
 3570config(o6,up).
 3571square(o5).
 3572in(o5,o6).
 3573square(o4).
 3574triangle(o3).
 3575config(o3,up).
 3576in(o3,o4).
 3577triangle(o2).
 3578config(o2,up).
 3579circle(o1).
 3580in(o1,o2).
 3581end(model(781)).
 3582
 3583begin(model(787)).
 3584pos.
 3585square(o6).
 3586triangle(o5).
 3587config(o5,down).
 3588in(o5,o6).
 3589triangle(o4).
 3590config(o4,down).
 3591square(o3).
 3592in(o3,o4).
 3593circle(o2).
 3594square(o1).
 3595in(o1,o2).
 3596end(model(787)).
 3597
 3598begin(model(794)).
 3599neg(pos).
 3600triangle(o3).
 3601config(o3,up).
 3602square(o2).
 3603in(o2,o3).
 3604triangle(o1).
 3605config(o1,down).
 3606end(model(794)).
 3607
 3608begin(model(795)).
 3609neg(pos).
 3610triangle(o3).
 3611config(o3,down).
 3612circle(o2).
 3613in(o2,o3).
 3614triangle(o1).
 3615config(o1,up).
 3616end(model(795)).
 3617
 3618begin(model(797)).
 3619neg(pos).
 3620circle(o5).
 3621circle(o4).
 3622in(o4,o5).
 3623circle(o3).
 3624square(o2).
 3625in(o2,o3).
 3626circle(o1).
 3627end(model(797)).
 3628
 3629begin(model(803)).
 3630neg(pos).
 3631triangle(o4).
 3632config(o4,up).
 3633circle(o3).
 3634in(o3,o4).
 3635square(o2).
 3636square(o1).
 3637in(o1,o2).
 3638end(model(803)).
 3639
 3640begin(model(805)).
 3641pos.
 3642circle(o6).
 3643triangle(o5).
 3644config(o5,down).
 3645in(o5,o6).
 3646square(o4).
 3647triangle(o3).
 3648config(o3,down).
 3649in(o3,o4).
 3650triangle(o2).
 3651config(o2,up).
 3652triangle(o1).
 3653config(o1,up).
 3654in(o1,o2).
 3655end(model(805)).
 3656
 3657begin(model(807)).
 3658neg(pos).
 3659square(o5).
 3660triangle(o4).
 3661config(o4,up).
 3662in(o4,o5).
 3663triangle(o3).
 3664config(o3,down).
 3665circle(o2).
 3666in(o2,o3).
 3667circle(o1).
 3668end(model(807)).
 3669
 3670begin(model(814)).
 3671neg(pos).
 3672square(o2).
 3673square(o1).
 3674in(o1,o2).
 3675end(model(814)).
 3676
 3677begin(model(815)).
 3678neg(pos).
 3679circle(o5).
 3680circle(o4).
 3681in(o4,o5).
 3682square(o3).
 3683circle(o2).
 3684in(o2,o3).
 3685square(o1).
 3686end(model(815)).
 3687
 3688begin(model(816)).
 3689pos.
 3690triangle(o6).
 3691config(o6,up).
 3692triangle(o5).
 3693config(o5,down).
 3694in(o5,o6).
 3695triangle(o4).
 3696config(o4,up).
 3697circle(o3).
 3698in(o3,o4).
 3699square(o2).
 3700triangle(o1).
 3701config(o1,up).
 3702in(o1,o2).
 3703end(model(816)).
 3704
 3705begin(model(818)).
 3706neg(pos).
 3707square(o2).
 3708triangle(o1).
 3709config(o1,up).
 3710in(o1,o2).
 3711end(model(818)).
 3712
 3713begin(model(819)).
 3714neg(pos).
 3715circle(o5).
 3716circle(o4).
 3717in(o4,o5).
 3718square(o3).
 3719square(o2).
 3720in(o2,o3).
 3721circle(o1).
 3722end(model(819)).
 3723
 3724begin(model(822)).
 3725neg(pos).
 3726square(o3).
 3727square(o2).
 3728in(o2,o3).
 3729square(o1).
 3730end(model(822)).
 3731
 3732begin(model(829)).
 3733neg(pos).
 3734square(o3).
 3735square(o2).
 3736in(o2,o3).
 3737triangle(o1).
 3738config(o1,down).
 3739end(model(829)).
 3740
 3741begin(model(832)).
 3742neg(pos).
 3743square(o5).
 3744circle(o4).
 3745in(o4,o5).
 3746triangle(o3).
 3747config(o3,down).
 3748circle(o2).
 3749in(o2,o3).
 3750square(o1).
 3751end(model(832)).
 3752
 3753begin(model(833)).
 3754neg(pos).
 3755triangle(o3).
 3756config(o3,up).
 3757circle(o2).
 3758in(o2,o3).
 3759circle(o1).
 3760end(model(833)).
 3761
 3762begin(model(835)).
 3763pos.
 3764triangle(o6).
 3765config(o6,down).
 3766square(o5).
 3767in(o5,o6).
 3768triangle(o4).
 3769config(o4,up).
 3770triangle(o3).
 3771config(o3,up).
 3772in(o3,o4).
 3773circle(o2).
 3774triangle(o1).
 3775config(o1,down).
 3776in(o1,o2).
 3777end(model(835)).
 3778
 3779begin(model(836)).
 3780neg(pos).
 3781square(o6).
 3782square(o5).
 3783in(o5,o6).
 3784circle(o4).
 3785square(o3).
 3786in(o3,o4).
 3787square(o2).
 3788circle(o1).
 3789in(o1,o2).
 3790end(model(836)).
 3791
 3792begin(model(837)).
 3793pos.
 3794triangle(o5).
 3795config(o5,down).
 3796triangle(o4).
 3797config(o4,down).
 3798in(o4,o5).
 3799square(o3).
 3800triangle(o2).
 3801config(o2,down).
 3802in(o2,o3).
 3803square(o1).
 3804end(model(837)).
 3805
 3806begin(model(838)).
 3807neg(pos).
 3808square(o4).
 3809triangle(o3).
 3810config(o3,up).
 3811in(o3,o4).
 3812triangle(o2).
 3813config(o2,up).
 3814square(o1).
 3815in(o1,o2).
 3816end(model(838)).
 3817
 3818begin(model(841)).
 3819pos.
 3820triangle(o5).
 3821config(o5,down).
 3822triangle(o4).
 3823config(o4,down).
 3824in(o4,o5).
 3825square(o3).
 3826circle(o2).
 3827in(o2,o3).
 3828circle(o1).
 3829end(model(841)).
 3830
 3831begin(model(844)).
 3832pos.
 3833square(o6).
 3834square(o5).
 3835in(o5,o6).
 3836circle(o4).
 3837triangle(o3).
 3838config(o3,up).
 3839in(o3,o4).
 3840circle(o2).
 3841square(o1).
 3842in(o1,o2).
 3843end(model(844)).
 3844
 3845begin(model(845)).
 3846neg(pos).
 3847triangle(o4).
 3848config(o4,up).
 3849circle(o3).
 3850in(o3,o4).
 3851triangle(o2).
 3852config(o2,down).
 3853circle(o1).
 3854in(o1,o2).
 3855end(model(845)).
 3856
 3857begin(model(846)).
 3858neg(pos).
 3859square(o5).
 3860square(o4).
 3861in(o4,o5).
 3862square(o3).
 3863square(o2).
 3864in(o2,o3).
 3865square(o1).
 3866end(model(846)).
 3867
 3868begin(model(847)).
 3869neg(pos).
 3870circle(o6).
 3871circle(o5).
 3872in(o5,o6).
 3873circle(o4).
 3874square(o3).
 3875in(o3,o4).
 3876circle(o2).
 3877square(o1).
 3878in(o1,o2).
 3879end(model(847)).
 3880
 3881begin(model(848)).
 3882neg(pos).
 3883triangle(o3).
 3884config(o3,down).
 3885circle(o2).
 3886in(o2,o3).
 3887triangle(o1).
 3888config(o1,down).
 3889end(model(848)).
 3890
 3891begin(model(849)).
 3892pos.
 3893triangle(o5).
 3894config(o5,down).
 3895triangle(o4).
 3896config(o4,up).
 3897in(o4,o5).
 3898circle(o3).
 3899triangle(o2).
 3900config(o2,up).
 3901in(o2,o3).
 3902square(o1).
 3903end(model(849)).
 3904
 3905begin(model(856)).
 3906neg(pos).
 3907triangle(o2).
 3908config(o2,down).
 3909square(o1).
 3910in(o1,o2).
 3911end(model(856)).
 3912
 3913begin(model(859)).
 3914neg(pos).
 3915square(o2).
 3916circle(o1).
 3917in(o1,o2).
 3918end(model(859)).
 3919
 3920begin(model(862)).
 3921neg(pos).
 3922square(o3).
 3923triangle(o2).
 3924config(o2,down).
 3925in(o2,o3).
 3926square(o1).
 3927end(model(862)).
 3928
 3929begin(model(864)).
 3930pos.
 3931circle(o3).
 3932triangle(o2).
 3933config(o2,up).
 3934in(o2,o3).
 3935square(o1).
 3936end(model(864)).
 3937
 3938begin(model(867)).
 3939neg(pos).
 3940circle(o5).
 3941circle(o4).
 3942in(o4,o5).
 3943square(o3).
 3944triangle(o2).
 3945config(o2,up).
 3946in(o2,o3).
 3947circle(o1).
 3948end(model(867)).
 3949
 3950begin(model(872)).
 3951neg(pos).
 3952square(o3).
 3953circle(o2).
 3954in(o2,o3).
 3955circle(o1).
 3956end(model(872)).
 3957
 3958begin(model(874)).
 3959pos.
 3960triangle(o3).
 3961config(o3,down).
 3962triangle(o2).
 3963config(o2,down).
 3964in(o2,o3).
 3965square(o1).
 3966end(model(874)).
 3967
 3968begin(model(876)).
 3969neg(pos).
 3970square(o2).
 3971circle(o1).
 3972in(o1,o2).
 3973end(model(876)).
 3974
 3975begin(model(880)).
 3976pos.
 3977circle(o6).
 3978circle(o5).
 3979in(o5,o6).
 3980triangle(o4).
 3981config(o4,up).
 3982triangle(o3).
 3983config(o3,up).
 3984in(o3,o4).
 3985circle(o2).
 3986circle(o1).
 3987in(o1,o2).
 3988end(model(880)).
 3989
 3990begin(model(882)).
 3991neg(pos).
 3992triangle(o4).
 3993config(o4,down).
 3994circle(o3).
 3995in(o3,o4).
 3996circle(o2).
 3997circle(o1).
 3998in(o1,o2).
 3999end(model(882)).
 4000
 4001begin(model(887)).
 4002neg(pos).
 4003triangle(o4).
 4004config(o4,down).
 4005square(o3).
 4006in(o3,o4).
 4007triangle(o2).
 4008config(o2,up).
 4009square(o1).
 4010in(o1,o2).
 4011end(model(887)).
 4012
 4013begin(model(890)).
 4014neg(pos).
 4015triangle(o3).
 4016config(o3,down).
 4017square(o2).
 4018in(o2,o3).
 4019square(o1).
 4020end(model(890)).
 4021
 4022begin(model(892)).
 4023neg(pos).
 4024triangle(o5).
 4025config(o5,down).
 4026circle(o4).
 4027in(o4,o5).
 4028square(o3).
 4029triangle(o2).
 4030config(o2,up).
 4031in(o2,o3).
 4032square(o1).
 4033end(model(892)).
 4034
 4035begin(model(893)).
 4036pos.
 4037triangle(o2).
 4038config(o2,up).
 4039triangle(o1).
 4040config(o1,down).
 4041in(o1,o2).
 4042end(model(893)).
 4043
 4044begin(model(897)).
 4045neg(pos).
 4046square(o6).
 4047square(o5).
 4048in(o5,o6).
 4049triangle(o4).
 4050config(o4,up).
 4051square(o3).
 4052in(o3,o4).
 4053triangle(o2).
 4054config(o2,up).
 4055square(o1).
 4056in(o1,o2).
 4057end(model(897)).
 4058
 4059begin(model(899)).
 4060neg(pos).
 4061circle(o2).
 4062circle(o1).
 4063in(o1,o2).
 4064end(model(899)).
 4065
 4066begin(model(900)).
 4067neg(pos).
 4068square(o6).
 4069triangle(o5).
 4070config(o5,down).
 4071in(o5,o6).
 4072square(o4).
 4073triangle(o3).
 4074config(o3,up).
 4075in(o3,o4).
 4076square(o2).
 4077square(o1).
 4078in(o1,o2).
 4079end(model(900)).
 4080
 4081begin(model(904)).
 4082neg(pos).
 4083circle(o5).
 4084circle(o4).
 4085in(o4,o5).
 4086square(o3).
 4087circle(o2).
 4088in(o2,o3).
 4089circle(o1).
 4090end(model(904)).
 4091
 4092begin(model(909)).
 4093pos.
 4094circle(o6).
 4095square(o5).
 4096in(o5,o6).
 4097triangle(o4).
 4098config(o4,up).
 4099triangle(o3).
 4100config(o3,up).
 4101in(o3,o4).
 4102square(o2).
 4103circle(o1).
 4104in(o1,o2).
 4105end(model(909)).
 4106
 4107begin(model(910)).
 4108pos.
 4109triangle(o4).
 4110config(o4,down).
 4111square(o3).
 4112in(o3,o4).
 4113circle(o2).
 4114square(o1).
 4115in(o1,o2).
 4116end(model(910)).
 4117
 4118begin(model(912)).
 4119neg(pos).
 4120circle(o6).
 4121triangle(o5).
 4122config(o5,down).
 4123in(o5,o6).
 4124triangle(o4).
 4125config(o4,up).
 4126square(o3).
 4127in(o3,o4).
 4128triangle(o2).
 4129config(o2,up).
 4130circle(o1).
 4131in(o1,o2).
 4132end(model(912)).
 4133
 4134begin(model(915)).
 4135neg(pos).
 4136triangle(o5).
 4137config(o5,up).
 4138square(o4).
 4139in(o4,o5).
 4140triangle(o3).
 4141config(o3,down).
 4142circle(o2).
 4143in(o2,o3).
 4144circle(o1).
 4145end(model(915)).
 4146
 4147begin(model(917)).
 4148neg(pos).
 4149triangle(o3).
 4150config(o3,up).
 4151square(o2).
 4152in(o2,o3).
 4153triangle(o1).
 4154config(o1,up).
 4155end(model(917)).
 4156
 4157begin(model(926)).
 4158neg(pos).
 4159square(o4).
 4160square(o3).
 4161in(o3,o4).
 4162square(o2).
 4163circle(o1).
 4164in(o1,o2).
 4165end(model(926)).
 4166
 4167begin(model(927)).
 4168neg(pos).
 4169triangle(o5).
 4170config(o5,down).
 4171circle(o4).
 4172in(o4,o5).
 4173triangle(o3).
 4174config(o3,up).
 4175circle(o2).
 4176in(o2,o3).
 4177circle(o1).
 4178end(model(927)).
 4179
 4180begin(model(929)).
 4181neg(pos).
 4182square(o2).
 4183circle(o1).
 4184in(o1,o2).
 4185end(model(929)).
 4186
 4187begin(model(930)).
 4188pos.
 4189triangle(o3).
 4190config(o3,up).
 4191triangle(o2).
 4192config(o2,up).
 4193in(o2,o3).
 4194square(o1).
 4195end(model(930)).
 4196
 4197begin(model(931)).
 4198neg(pos).
 4199square(o2).
 4200triangle(o1).
 4201config(o1,up).
 4202in(o1,o2).
 4203end(model(931)).
 4204
 4205begin(model(932)).
 4206pos.
 4207triangle(o5).
 4208config(o5,down).
 4209square(o4).
 4210in(o4,o5).
 4211triangle(o3).
 4212config(o3,down).
 4213triangle(o2).
 4214config(o2,up).
 4215in(o2,o3).
 4216circle(o1).
 4217end(model(932)).
 4218
 4219begin(model(933)).
 4220neg(pos).
 4221square(o3).
 4222square(o2).
 4223in(o2,o3).
 4224triangle(o1).
 4225config(o1,down).
 4226end(model(933)).
 4227
 4228begin(model(938)).
 4229pos.
 4230circle(o6).
 4231circle(o5).
 4232in(o5,o6).
 4233triangle(o4).
 4234config(o4,down).
 4235triangle(o3).
 4236config(o3,up).
 4237in(o3,o4).
 4238square(o2).
 4239triangle(o1).
 4240config(o1,down).
 4241in(o1,o2).
 4242end(model(938)).
 4243
 4244begin(model(939)).
 4245neg(pos).
 4246triangle(o2).
 4247config(o2,up).
 4248square(o1).
 4249in(o1,o2).
 4250end(model(939)).
 4251
 4252begin(model(940)).
 4253pos.
 4254triangle(o4).
 4255config(o4,down).
 4256triangle(o3).
 4257config(o3,up).
 4258in(o3,o4).
 4259circle(o2).
 4260triangle(o1).
 4261config(o1,up).
 4262in(o1,o2).
 4263end(model(940)).
 4264
 4265begin(model(941)).
 4266neg(pos).
 4267triangle(o3).
 4268config(o3,down).
 4269circle(o2).
 4270in(o2,o3).
 4271square(o1).
 4272end(model(941)).
 4273
 4274begin(model(944)).
 4275neg(pos).
 4276circle(o4).
 4277circle(o3).
 4278in(o3,o4).
 4279circle(o2).
 4280triangle(o1).
 4281config(o1,down).
 4282in(o1,o2).
 4283end(model(944)).
 4284
 4285begin(model(945)).
 4286neg(pos).
 4287square(o5).
 4288square(o4).
 4289in(o4,o5).
 4290square(o3).
 4291circle(o2).
 4292in(o2,o3).
 4293triangle(o1).
 4294config(o1,down).
 4295end(model(945)).
 4296
 4297begin(model(946)).
 4298pos.
 4299triangle(o5).
 4300config(o5,up).
 4301circle(o4).
 4302in(o4,o5).
 4303triangle(o3).
 4304config(o3,down).
 4305triangle(o2).
 4306config(o2,down).
 4307in(o2,o3).
 4308circle(o1).
 4309end(model(946)).
 4310
 4311begin(model(947)).
 4312pos.
 4313circle(o5).
 4314circle(o4).
 4315in(o4,o5).
 4316triangle(o3).
 4317config(o3,down).
 4318triangle(o2).
 4319config(o2,down).
 4320in(o2,o3).
 4321circle(o1).
 4322end(model(947)).
 4323
 4324begin(model(955)).
 4325neg(pos).
 4326circle(o6).
 4327triangle(o5).
 4328config(o5,down).
 4329in(o5,o6).
 4330square(o4).
 4331triangle(o3).
 4332config(o3,up).
 4333in(o3,o4).
 4334square(o2).
 4335circle(o1).
 4336in(o1,o2).
 4337end(model(955)).
 4338
 4339begin(model(957)).
 4340pos.
 4341triangle(o6).
 4342config(o6,down).
 4343circle(o5).
 4344in(o5,o6).
 4345circle(o4).
 4346square(o3).
 4347in(o3,o4).
 4348triangle(o2).
 4349config(o2,up).
 4350triangle(o1).
 4351config(o1,up).
 4352in(o1,o2).
 4353end(model(957)).
 4354
 4355begin(model(961)).
 4356neg(pos).
 4357square(o4).
 4358circle(o3).
 4359in(o3,o4).
 4360circle(o2).
 4361circle(o1).
 4362in(o1,o2).
 4363end(model(961)).
 4364
 4365begin(model(971)).
 4366pos.
 4367circle(o5).
 4368triangle(o4).
 4369config(o4,down).
 4370in(o4,o5).
 4371triangle(o3).
 4372config(o3,up).
 4373triangle(o2).
 4374config(o2,down).
 4375in(o2,o3).
 4376square(o1).
 4377end(model(971)).
 4378
 4379begin(model(973)).
 4380neg(pos).
 4381square(o4).
 4382circle(o3).
 4383in(o3,o4).
 4384triangle(o2).
 4385config(o2,down).
 4386circle(o1).
 4387in(o1,o2).
 4388end(model(973)).
 4389
 4390begin(model(974)).
 4391neg(pos).
 4392circle(o6).
 4393circle(o5).
 4394in(o5,o6).
 4395square(o4).
 4396circle(o3).
 4397in(o3,o4).
 4398circle(o2).
 4399circle(o1).
 4400in(o1,o2).
 4401end(model(974)).
 4402
 4403begin(model(975)).
 4404neg(pos).
 4405square(o3).
 4406triangle(o2).
 4407config(o2,down).
 4408in(o2,o3).
 4409triangle(o1).
 4410config(o1,up).
 4411end(model(975)).
 4412
 4413begin(model(977)).
 4414neg(pos).
 4415circle(o2).
 4416circle(o1).
 4417in(o1,o2).
 4418end(model(977)).
 4419
 4420begin(model(978)).
 4421pos.
 4422triangle(o2).
 4423config(o2,down).
 4424triangle(o1).
 4425config(o1,up).
 4426in(o1,o2).
 4427end(model(978)).
 4428
 4429begin(model(979)).
 4430pos.
 4431circle(o2).
 4432triangle(o1).
 4433config(o1,up).
 4434in(o1,o2).
 4435end(model(979)).
 4436
 4437begin(model(984)).
 4438neg(pos).
 4439square(o2).
 4440circle(o1).
 4441in(o1,o2).
 4442end(model(984)).
 4443
 4444begin(model(989)).
 4445neg(pos).
 4446triangle(o2).
 4447config(o2,up).
 4448circle(o1).
 4449in(o1,o2).
 4450end(model(989)).
 4451
 4452begin(model(991)).
 4453pos.
 4454circle(o6).
 4455square(o5).
 4456in(o5,o6).
 4457triangle(o4).
 4458config(o4,down).
 4459square(o3).
 4460in(o3,o4).
 4461triangle(o2).
 4462config(o2,up).
 4463triangle(o1).
 4464config(o1,down).
 4465in(o1,o2).
 4466end(model(991)).
 4467
 4468begin(model(995)).
 4469pos.
 4470triangle(o6).
 4471config(o6,up).
 4472triangle(o5).
 4473config(o5,up).
 4474in(o5,o6).
 4475square(o4).
 4476square(o3).
 4477in(o3,o4).
 4478circle(o2).
 4479circle(o1).
 4480in(o1,o2).
 4481end(model(995)).
 4482
 4483begin(model(997)).
 4484neg(pos).
 4485square(o3).
 4486square(o2).
 4487in(o2,o3).
 4488triangle(o1).
 4489config(o1,down).
 4490end(model(997)).
 4491
 4492begin(model(1000)).
 4493neg(pos).
 4494square(o6).
 4495triangle(o5).
 4496config(o5,up).
 4497in(o5,o6).
 4498triangle(o4).
 4499config(o4,up).
 4500circle(o3).
 4501in(o3,o4).
 4502triangle(o2).
 4503config(o2,down).
 4504circle(o1).
 4505in(o1,o2).
 4506end(model(1000))