#!/bin/sh # This is a shell archive, meaning: # 1. Remove everything above the #!/bin/sh line. # 2. Save the resulting text in a file. # 3. Execute the file with /bin/sh (not csh) to create the files: # README # chekndom.desc # chekndom.ver1.clauses # chekndom.ver1.in # chekndom.ver1.out # chekndom.ver2.clauses # chekndom.ver2.in # chekndom.ver2.out # mission.desc # mission.ver1.clauses # mission.ver1.in # mission.ver1.out # mission.ver2.clauses # mission.ver2.in # mission.ver2.out # This archive created: Tue Aug 16 11:24:01 1988 export PATH; PATH=/bin:$PATH if test -f 'README' then echo shar: over-writing existing file "'README'" fi cat << \SHAR_EOF > 'README' problem-set/puzzles/space.state/README created : 07/26/88 revised : 07/26/88 Contents of 'space.state' : --------------------------- Main File Headings ---------------------------------------------------------------------- README : You are currently here; a description of all the files in the directory problem-set/puzzles/space.state. chekndom : To solve "The Checkerboard and Dominoes Puzzle" mission : To solve "The Missionaries and Cannibals Puzzle" ---------------------------------------------------------------------- For each problem, there are several standard files, which include one probname.desc file and at least one of each of probname.ver#.in, probname.ver#.clauses, and probname.ver#.out. These contain the following: probname.desc : contains the Natural Language Description of the problem, where available, as well as complete details on each formulation and each version. probname.ver#.in : contains the problem specification, input clauses, and strategy for OTTER; this file is ready to run. probname.ver#.clauses : contains the description, commentary, and the actual clauses (including the denial of the conclusion) used for probname.ver#.in, without any strategy; note that comments always are on lines beginning with a % and that clauses terminate with periods. probname.ver#.out : contains the output from running probname.ver#.in through OTTER, with proof if one is found, and with statistics on the clauses generated and CPU time used. HOW TO RUN : ---------------------------------------------------------------------- Invoke OTTER by using the following command : otter < probname.ver#.in [ > outfile ] [ & ] NOTE : '> outfile' may be used to send all output to a file named outfile; '&' may be used to run the program in the background. SHAR_EOF if test -f 'chekndom.desc' then echo shar: over-writing existing file "'chekndom.desc'" fi cat << \SHAR_EOF > 'chekndom.desc' problem-set/puzzles/space_state/chekndom.desc created : 07/09/86 revised : 07/13/88 Natural Language Description: The Checkerboard and Dominoes Puzzle There is a checker board whose upper left and lower right squares have been removed. There is a box of dominoes that are one square by two squares in size. Can you exactly cover the checker board with dominoes? Versions: chekndom.ver1 : Procedural representation using hyper-resolution original puzzle, answer: cannot be covered. created by : L. Wos verified for ITP : 07/09/86 translated for OTTER by : K.R. verified for OTTER : 07/13/88 chekndom.ver2.in- Procedural representation using hyper-resolution variation of original puzzle, has second and third square removed from first row, answer: can be covered. created by : verified for ITP : untested translated for OTTER by : K.R. verified for OTTER : 07/13/88 SHAR_EOF if test -f 'chekndom.ver1.clauses' then echo shar: over-writing existing file "'chekndom.ver1.clauses'" fi cat << \SHAR_EOF > 'chekndom.ver1.clauses' % problem-set/puzzles/space_state/chekndom.ver1.clauses % created : 07/13/88 % revised : 07/13/88 % description: % % This run solves "The Checkerboard and Dominoes Puzzle" using % hyper-resolution. % % THE CHECKERBOARD AND DOMINOES PUZZLE % % There is a checker board whose upper left and lower right % squares have been removed. There is a box of dominoes that % are one square by two squares in size. Can you exactly cover % the checker board with dominoes? % representation: % % Procedural version: % COMMENTS : Since the clause-set is satisfiable, there is no proof by . % contradiction. % PREDICATES : % ACHIEVABLE(arg1,arg2): Gives the state of each row and the % individual squares in the row. % FUNCTIONS : % row(x): x in this function indicate the row number. % squares(): gives the state of each square in a particular % row. 'c' stands for covered, 'n' for not covered. % and 'r' for removed. % compl(x): Changes the state of a square from x to another. % For each row : If an adjacent pair of checkers are not covered then, % cover them , until every such pair in that row has been looked at.. % Place a domino horizontally, where possible -ACHIEVABLE(Row(x),Squares(n,n,y3,y4,y5,y6,y7,y8)) | ACHIEVABLE(Row(x),Squares(c,c,y3,y4,y5,y6,y7,y8)). -ACHIEVABLE(Row(x),Squares(y1,n,n,y4,y5,y6,y7,y8)) | ACHIEVABLE(Row(x),Squares(y1,c,c,y4,y5,y6,y7,y8)). -ACHIEVABLE(Row(x),Squares(y1,y2,n,n,y5,y6,y7,y8)) | ACHIEVABLE(Row(x),Squares(y1,y2,c,c,y5,y6,y7,y8)). -ACHIEVABLE(Row(x),Squares(y1,y2,y3,n,n,y6,y7,y8)) | ACHIEVABLE(Row(x),Squares(y1,y2,y3,c,c,y6,y7,y8)). -ACHIEVABLE(Row(x),Squares(y1,y2,y3,y4,n,n,y7,y8)) | ACHIEVABLE(Row(x),Squares(y1,y2,y3,y4,c,c,y7,y8)). -ACHIEVABLE(Row(x),Squares(y1,y2,y3,y4,y5,n,n,y8)) | ACHIEVABLE(Row(x),Squares(y1,y2,y3,y4,y5,c,c,y8)). -ACHIEVABLE(Row(x),Squares(y1,y2,y3,y4,y5,y6,n,n)) | ACHIEVABLE(Row(x),Squares(y1,y2,y3,y4,y5,y6,c,c)). % If the Row is complete then examine the Row directly below.. % Then depending, on the complementary function, change the state % of the squares. This may place several dominoes vertically. -ACHIEVABLE(Row(x),Squares(y1,y2,y3,y4,y5,y6,y7,y8)) | ACHIEVABLE(Row(succ(x)),Squares(compl(y1),compl(y2), compl(y3),compl(y4),compl(y5),compl(y6),compl(y7),compl(y8))). % The end condition (to stop when the 8th Row is finished) ACHIEVABLE(Row(9),Squares(y1,y2,y3,y4,y5,y6,y7,y8)). % Initial condition. ACHIEVABLE(Row(1),Squares(r,n,n,n,n,n,n,n)). % If it is possible to cover the checkerboard using dominoes then the. % resulting statement will unify with this clause giving a proof by. % contradiction. If it is not possible, the set of support will be % exhausted. -ACHIEVABLE(Row(8),Squares(c,c,c,c,c,c,c,n)). EQUAL(compl(c),n). EQUAL(compl(n),c). EQUAL(compl(r),n). EQUAL(succ(1),2). EQUAL(succ(2),3). EQUAL(succ(3),4). EQUAL(succ(4),5). EQUAL(succ(5),6). EQUAL(succ(6),7). EQUAL(succ(7),8). EQUAL(succ(8),9). SHAR_EOF if test -f 'chekndom.ver1.in' then echo shar: over-writing existing file "'chekndom.ver1.in'" fi cat << \SHAR_EOF > 'chekndom.ver1.in' % problem-set/puzzles/space_state/chekndom.ver1.in % created : 07/09/86 % revised : 07/13/88 % description: % % This run solves "The Checkerboard and Dominoes Puzzle" using % hyper-resolution. % % THE CHECKERBOARD AND DOMINOES PUZZLE % % There is a checker board whose upper left and lower right % squares have been removed. There is a box of dominoes that % are one square by two squares in size. Can you exactly cover % the checker board with dominoes? % representation: % % Procedural version: % COMMENTS : Since the clause-set is satisfiable, there is no proof by . % contradiction. % PREDICATES : % ACHIEVABLE(arg1,arg2): Gives the state of each row and the % individual squares in the row. % FUNCTIONS : % row(x): x in this function indicate the row number. % squares(): gives the state of each square in a particular % row. 'c' stands for covered, 'n' for not covered. % and 'r' for removed. % compl(x): Changes the state of a square from x to another. % For each row : If an adjacent pair of checkers are not covered then, % cover them , until every such pair in that row has been looked at.. set(hyper_res). list(axioms). % Place a domino horizontally, where possible -ACHIEVABLE(Row(x),Squares(n,n,y3,y4,y5,y6,y7,y8)) | ACHIEVABLE(Row(x),Squares(c,c,y3,y4,y5,y6,y7,y8)). -ACHIEVABLE(Row(x),Squares(y1,n,n,y4,y5,y6,y7,y8)) | ACHIEVABLE(Row(x),Squares(y1,c,c,y4,y5,y6,y7,y8)). -ACHIEVABLE(Row(x),Squares(y1,y2,n,n,y5,y6,y7,y8)) | ACHIEVABLE(Row(x),Squares(y1,y2,c,c,y5,y6,y7,y8)). -ACHIEVABLE(Row(x),Squares(y1,y2,y3,n,n,y6,y7,y8)) | ACHIEVABLE(Row(x),Squares(y1,y2,y3,c,c,y6,y7,y8)). -ACHIEVABLE(Row(x),Squares(y1,y2,y3,y4,n,n,y7,y8)) | ACHIEVABLE(Row(x),Squares(y1,y2,y3,y4,c,c,y7,y8)). -ACHIEVABLE(Row(x),Squares(y1,y2,y3,y4,y5,n,n,y8)) | ACHIEVABLE(Row(x),Squares(y1,y2,y3,y4,y5,c,c,y8)). -ACHIEVABLE(Row(x),Squares(y1,y2,y3,y4,y5,y6,n,n)) | ACHIEVABLE(Row(x),Squares(y1,y2,y3,y4,y5,y6,c,c)). % If the Row is complete then examine the Row directly below.. % Then depending, on the complementary function, change the state % of the squares. This may place several dominoes vertically. -ACHIEVABLE(Row(x),Squares(y1,y2,y3,y4,y5,y6,y7,y8)) | ACHIEVABLE(Row(succ(x)),Squares(compl(y1),compl(y2), compl(y3),compl(y4),compl(y5),compl(y6),compl(y7),compl(y8))). % The end condition (to stop when the 8th Row is finished) ACHIEVABLE(Row(9),Squares(y1,y2,y3,y4,y5,y6,y7,y8)). end_of_list. list(sos). % Initial condition. ACHIEVABLE(Row(1),Squares(r,n,n,n,n,n,n,n)). % If it is possible to cover the checkerboard using dominoes then the. % resulting statement will unify with this clause giving a proof by. % contradiction. If it is not possible, the set of support will be % exhausted. -ACHIEVABLE(Row(8),Squares(c,c,c,c,c,c,c,n)). end_of_list. list(demodulators). EQUAL(compl(c),n). EQUAL(compl(n),c). EQUAL(compl(r),n). EQUAL(succ(1),2). EQUAL(succ(2),3). EQUAL(succ(3),4). EQUAL(succ(4),5). EQUAL(succ(5),6). EQUAL(succ(6),7). EQUAL(succ(7),8). EQUAL(succ(8),9). end_of_list. SHAR_EOF if test -f 'chekndom.ver1.out' then echo shar: over-writing existing file "'chekndom.ver1.out'" fi cat << \SHAR_EOF > 'chekndom.ver1.out' problem-set/puzzles/space_state/chekndom.ver1.out created : 07/13/88 revised : 07/13/88 OTTER version 0.9, 19 May 1988. set(hyper_res). list(axioms). 1 -ACHIEVABLE(Row(x),Squares(n,n,y3,y4,y5,y6,y7,y8)) | ACHIEVABLE(Row(x),Squares(c,c,y3,y4,y5,y6,y7,y8)). 2 -ACHIEVABLE(Row(x),Squares(y1,n,n,y4,y5,y6,y7,y8)) | ACHIEVABLE(Row(x),Squares(y1,c,c,y4,y5,y6,y7,y8)). 3 -ACHIEVABLE(Row(x),Squares(y1,y2,n,n,y5,y6,y7,y8)) | ACHIEVABLE(Row(x),Squares(y1,y2,c,c,y5,y6,y7,y8)). 4 -ACHIEVABLE(Row(x),Squares(y1,y2,y3,n,n,y6,y7,y8)) | ACHIEVABLE(Row(x),Squares(y1,y2,y3,c,c,y6,y7,y8)). 5 -ACHIEVABLE(Row(x),Squares(y1,y2,y3,y4,n,n,y7,y8)) | ACHIEVABLE(Row(x),Squares(y1,y2,y3,y4,c,c,y7,y8)). 6 -ACHIEVABLE(Row(x),Squares(y1,y2,y3,y4,y5,n,n,y8)) | ACHIEVABLE(Row(x),Squares(y1,y2,y3,y4,y5,c,c,y8)). 7 -ACHIEVABLE(Row(x),Squares(y1,y2,y3,y4,y5,y6,n,n)) | ACHIEVABLE(Row(x),Squares(y1,y2,y3,y4,y5,y6,c,c)). 8 -ACHIEVABLE(Row(x),Squares(y1,y2,y3,y4,y5,y6,y7,y8)) | ACHIEVABLE(Row(succ(x)),Squares(compl(y1),compl(y2),compl(y3),compl(y4),compl(y5),compl(y6),compl(y7),compl(y8))). 9 ACHIEVABLE(Row(9),Squares(y1,y2,y3,y4,y5,y6,y7,y8)). end_of_list. list(sos). 10 ACHIEVABLE(Row(1),Squares(r,n,n,n,n,n,n,n)). 11 -ACHIEVABLE(Row(8),Squares(c,c,c,c,c,c,c,n)). end_of_list. list(demodulators). 12 EQUAL(compl(c),n). 13 EQUAL(compl(n),c). 14 EQUAL(compl(r),n). 15 EQUAL(succ(1),2). 16 EQUAL(succ(2),3). 17 EQUAL(succ(3),4). 18 EQUAL(succ(4),5). 19 EQUAL(succ(5),6). 20 EQUAL(succ(6),7). 21 EQUAL(succ(7),8). 22 EQUAL(succ(8),9). end_of_list. new given clause: 10 ACHIEVABLE(Row(1),Squares(r,n,n,n,n,n,n,n)). ** KEPT: 23 (10,8,15,14,13,13,13,13,13,13,13) ACHIEVABLE(Row(2),Squares(n,c,c,c,c,c,c,c)). ** KEPT: 24 (10,7) ACHIEVABLE(Row(1),Squares(r,n,n,n,n,n,c,c)). ** KEPT: 25 (10,6) ACHIEVABLE(Row(1),Squares(r,n,n,n,n,c,c,n)). ** KEPT: 26 (10,5) ACHIEVABLE(Row(1),Squares(r,n,n,n,c,c,n,n)). ** KEPT: 27 (10,4) ACHIEVABLE(Row(1),Squares(r,n,n,c,c,n,n,n)). ** KEPT: 28 (10,3) ACHIEVABLE(Row(1),Squares(r,n,c,c,n,n,n,n)). ** KEPT: 29 (10,2) ACHIEVABLE(Row(1),Squares(r,c,c,n,n,n,n,n)). new given clause: 11 -ACHIEVABLE(Row(8),Squares(c,c,c,c,c,c,c,n)). new given clause: 23 (10,8,15,14,13,13,13,13,13,13,13) ACHIEVABLE(Row(2),Squares(n,c,c,c,c,c,c,c)). ** KEPT: 30 (23,8,16,13,12,12,12,12,12,12,12) ACHIEVABLE(Row(3),Squares(c,n,n,n,n,n,n,n)). new given clause: 24 (10,7) ACHIEVABLE(Row(1),Squares(r,n,n,n,n,n,c,c)). ** KEPT: 31 (24,8,15,14,13,13,13,13,13,12,12) ACHIEVABLE(Row(2),Squares(n,c,c,c,c,c,n,n)). ** KEPT: 32 (24,5) ACHIEVABLE(Row(1),Squares(r,n,n,n,c,c,c,c)). ** KEPT: 33 (24,4) ACHIEVABLE(Row(1),Squares(r,n,n,c,c,n,c,c)). ** KEPT: 34 (24,3) ACHIEVABLE(Row(1),Squares(r,n,c,c,n,n,c,c)). ** KEPT: 35 (24,2) ACHIEVABLE(Row(1),Squares(r,c,c,n,n,n,c,c)). new given clause: 25 (10,6) ACHIEVABLE(Row(1),Squares(r,n,n,n,n,c,c,n)). ** KEPT: 36 (25,8,15,14,13,13,13,13,12,12,13) ACHIEVABLE(Row(2),Squares(n,c,c,c,c,n,n,c)). ** KEPT: 37 (25,4) ACHIEVABLE(Row(1),Squares(r,n,n,c,c,c,c,n)). ** KEPT: 38 (25,3) ACHIEVABLE(Row(1),Squares(r,n,c,c,n,c,c,n)). ** KEPT: 39 (25,2) ACHIEVABLE(Row(1),Squares(r,c,c,n,n,c,c,n)). new given clause: 26 (10,5) ACHIEVABLE(Row(1),Squares(r,n,n,n,c,c,n,n)). ** KEPT: 40 (26,8,15,14,13,13,13,12,12,13,13) ACHIEVABLE(Row(2),Squares(n,c,c,c,n,n,c,c)). ** KEPT: 41 (26,3) ACHIEVABLE(Row(1),Squares(r,n,c,c,c,c,n,n)). ** KEPT: 42 (26,2) ACHIEVABLE(Row(1),Squares(r,c,c,n,c,c,n,n)). new given clause: 27 (10,4) ACHIEVABLE(Row(1),Squares(r,n,n,c,c,n,n,n)). ** KEPT: 43 (27,8,15,14,13,13,12,12,13,13,13) ACHIEVABLE(Row(2),Squares(n,c,c,n,n,c,c,c)). ** KEPT: 44 (27,2) ACHIEVABLE(Row(1),Squares(r,c,c,c,c,n,n,n)). new given clause: 28 (10,3) ACHIEVABLE(Row(1),Squares(r,n,c,c,n,n,n,n)). ** KEPT: 45 (28,8,15,14,13,12,12,13,13,13,13) ACHIEVABLE(Row(2),Squares(n,c,n,n,c,c,c,c)). new given clause: 29 (10,2) ACHIEVABLE(Row(1),Squares(r,c,c,n,n,n,n,n)). ** KEPT: 46 (29,8,15,14,12,12,13,13,13,13,13) ACHIEVABLE(Row(2),Squares(n,n,n,c,c,c,c,c)). new given clause: 30 (23,8,16,13,12,12,12,12,12,12,12) ACHIEVABLE(Row(3),Squares(c,n,n,n,n,n,n,n)). ** KEPT: 47 (30,8,17,12,13,13,13,13,13,13,13) ACHIEVABLE(Row(4),Squares(n,c,c,c,c,c,c,c)). ** KEPT: 48 (30,7) ACHIEVABLE(Row(3),Squares(c,n,n,n,n,n,c,c)). ** KEPT: 49 (30,6) ACHIEVABLE(Row(3),Squares(c,n,n,n,n,c,c,n)). ** KEPT: 50 (30,5) ACHIEVABLE(Row(3),Squares(c,n,n,n,c,c,n,n)). ** KEPT: 51 (30,4) ACHIEVABLE(Row(3),Squares(c,n,n,c,c,n,n,n)). ** KEPT: 52 (30,3) ACHIEVABLE(Row(3),Squares(c,n,c,c,n,n,n,n)). ** KEPT: 53 (30,2) ACHIEVABLE(Row(3),Squares(c,c,c,n,n,n,n,n)). new given clause: 31 (24,8,15,14,13,13,13,13,13,12,12) ACHIEVABLE(Row(2),Squares(n,c,c,c,c,c,n,n)). new given clause: 32 (24,5) ACHIEVABLE(Row(1),Squares(r,n,n,n,c,c,c,c)). ** KEPT: 54 (32,8,15,14,13,13,13,12,12,12,12) ACHIEVABLE(Row(2),Squares(n,c,c,c,n,n,n,n)). ** KEPT: 55 (32,3) ACHIEVABLE(Row(1),Squares(r,n,c,c,c,c,c,c)). ** KEPT: 56 (32,2) ACHIEVABLE(Row(1),Squares(r,c,c,n,c,c,c,c)). new given clause: 33 (24,4) ACHIEVABLE(Row(1),Squares(r,n,n,c,c,n,c,c)). ** KEPT: 57 (33,8,15,14,13,13,12,12,13,12,12) ACHIEVABLE(Row(2),Squares(n,c,c,n,n,c,n,n)). ** KEPT: 58 (33,2) ACHIEVABLE(Row(1),Squares(r,c,c,c,c,n,c,c)). new given clause: 34 (24,3) ACHIEVABLE(Row(1),Squares(r,n,c,c,n,n,c,c)). ** KEPT: 59 (34,8,15,14,13,12,12,13,13,12,12) ACHIEVABLE(Row(2),Squares(n,c,n,n,c,c,n,n)). new given clause: 35 (24,2) ACHIEVABLE(Row(1),Squares(r,c,c,n,n,n,c,c)). ** KEPT: 60 (35,8,15,14,12,12,13,13,13,12,12) ACHIEVABLE(Row(2),Squares(n,n,n,c,c,c,n,n)). new given clause: 36 (25,8,15,14,13,13,13,13,12,12,13) ACHIEVABLE(Row(2),Squares(n,c,c,c,c,n,n,c)). new given clause: 37 (25,4) ACHIEVABLE(Row(1),Squares(r,n,n,c,c,c,c,n)). ** KEPT: 61 (37,8,15,14,13,13,12,12,12,12,13) ACHIEVABLE(Row(2),Squares(n,c,c,n,n,n,n,c)). ** KEPT: 62 (37,2) ACHIEVABLE(Row(1),Squares(r,c,c,c,c,c,c,n)). new given clause: 38 (25,3) ACHIEVABLE(Row(1),Squares(r,n,c,c,n,c,c,n)). ** KEPT: 63 (38,8,15,14,13,12,12,13,12,12,13) ACHIEVABLE(Row(2),Squares(n,c,n,n,c,n,n,c)). new given clause: 39 (25,2) ACHIEVABLE(Row(1),Squares(r,c,c,n,n,c,c,n)). ** KEPT: 64 (39,8,15,14,12,12,13,13,12,12,13) ACHIEVABLE(Row(2),Squares(n,n,n,c,c,n,n,c)). new given clause: 40 (26,8,15,14,13,13,13,12,12,13,13) ACHIEVABLE(Row(2),Squares(n,c,c,c,n,n,c,c)). new given clause: 41 (26,3) ACHIEVABLE(Row(1),Squares(r,n,c,c,c,c,n,n)). ** KEPT: 65 (41,8,15,14,13,12,12,12,12,13,13) ACHIEVABLE(Row(2),Squares(n,c,n,n,n,n,c,c)). new given clause: 42 (26,2) ACHIEVABLE(Row(1),Squares(r,c,c,n,c,c,n,n)). ** KEPT: 66 (42,8,15,14,12,12,13,12,12,13,13) ACHIEVABLE(Row(2),Squares(n,n,n,c,n,n,c,c)). new given clause: 43 (27,8,15,14,13,13,12,12,13,13,13) ACHIEVABLE(Row(2),Squares(n,c,c,n,n,c,c,c)). new given clause: 44 (27,2) ACHIEVABLE(Row(1),Squares(r,c,c,c,c,n,n,n)). ** KEPT: 67 (44,8,15,14,12,12,12,12,13,13,13) ACHIEVABLE(Row(2),Squares(n,n,n,n,n,c,c,c)). new given clause: 45 (28,8,15,14,13,12,12,13,13,13,13) ACHIEVABLE(Row(2),Squares(n,c,n,n,c,c,c,c)). new given clause: 46 (29,8,15,14,12,12,13,13,13,13,13) ACHIEVABLE(Row(2),Squares(n,n,n,c,c,c,c,c)). ** KEPT: 68 (46,1) ACHIEVABLE(Row(2),Squares(c,c,n,c,c,c,c,c)). new given clause: 47 (30,8,17,12,13,13,13,13,13,13,13) ACHIEVABLE(Row(4),Squares(n,c,c,c,c,c,c,c)). ** KEPT: 69 (47,8,18,13,12,12,12,12,12,12,12) ACHIEVABLE(Row(5),Squares(c,n,n,n,n,n,n,n)). new given clause: 48 (30,7) ACHIEVABLE(Row(3),Squares(c,n,n,n,n,n,c,c)). ** KEPT: 70 (48,8,17,12,13,13,13,13,13,12,12) ACHIEVABLE(Row(4),Squares(n,c,c,c,c,c,n,n)). ** KEPT: 71 (48,5) ACHIEVABLE(Row(3),Squares(c,n,n,n,c,c,c,c)). ** KEPT: 72 (48,4) ACHIEVABLE(Row(3),Squares(c,n,n,c,c,n,c,c)). ** KEPT: 73 (48,3) ACHIEVABLE(Row(3),Squares(c,n,c,c,n,n,c,c)). ** KEPT: 74 (48,2) ACHIEVABLE(Row(3),Squares(c,c,c,n,n,n,c,c)). new given clause: 49 (30,6) ACHIEVABLE(Row(3),Squares(c,n,n,n,n,c,c,n)). ** KEPT: 75 (49,8,17,12,13,13,13,13,12,12,13) ACHIEVABLE(Row(4),Squares(n,c,c,c,c,n,n,c)). ** KEPT: 76 (49,4) ACHIEVABLE(Row(3),Squares(c,n,n,c,c,c,c,n)). ** KEPT: 77 (49,3) ACHIEVABLE(Row(3),Squares(c,n,c,c,n,c,c,n)). ** KEPT: 78 (49,2) ACHIEVABLE(Row(3),Squares(c,c,c,n,n,c,c,n)). new given clause: 50 (30,5) ACHIEVABLE(Row(3),Squares(c,n,n,n,c,c,n,n)). ** KEPT: 79 (50,8,17,12,13,13,13,12,12,13,13) ACHIEVABLE(Row(4),Squares(n,c,c,c,n,n,c,c)). ** KEPT: 80 (50,3) ACHIEVABLE(Row(3),Squares(c,n,c,c,c,c,n,n)). ** KEPT: 81 (50,2) ACHIEVABLE(Row(3),Squares(c,c,c,n,c,c,n,n)). new given clause: 51 (30,4) ACHIEVABLE(Row(3),Squares(c,n,n,c,c,n,n,n)). ** KEPT: 82 (51,8,17,12,13,13,12,12,13,13,13) ACHIEVABLE(Row(4),Squares(n,c,c,n,n,c,c,c)). ** KEPT: 83 (51,2) ACHIEVABLE(Row(3),Squares(c,c,c,c,c,n,n,n)). new given clause: 52 (30,3) ACHIEVABLE(Row(3),Squares(c,n,c,c,n,n,n,n)). ** KEPT: 84 (52,8,17,12,13,12,12,13,13,13,13) ACHIEVABLE(Row(4),Squares(n,c,n,n,c,c,c,c)). new given clause: 53 (30,2) ACHIEVABLE(Row(3),Squares(c,c,c,n,n,n,n,n)). ** KEPT: 85 (53,8,17,12,12,12,13,13,13,13,13) ACHIEVABLE(Row(4),Squares(n,n,n,c,c,c,c,c)). new given clause: 54 (32,8,15,14,13,13,13,12,12,12,12) ACHIEVABLE(Row(2),Squares(n,c,c,c,n,n,n,n)). ** KEPT: 86 (54,6) ACHIEVABLE(Row(2),Squares(n,c,c,c,n,c,c,n)). new given clause: 55 (32,3) ACHIEVABLE(Row(1),Squares(r,n,c,c,c,c,c,c)). ** KEPT: 87 (55,8,15,14,13,12,12,12,12,12,12) ACHIEVABLE(Row(2),Squares(n,c,n,n,n,n,n,n)). new given clause: 56 (32,2) ACHIEVABLE(Row(1),Squares(r,c,c,n,c,c,c,c)). ** KEPT: 88 (56,8,15,14,12,12,13,12,12,12,12) ACHIEVABLE(Row(2),Squares(n,n,n,c,n,n,n,n)). new given clause: 57 (33,8,15,14,13,13,12,12,13,12,12) ACHIEVABLE(Row(2),Squares(n,c,c,n,n,c,n,n)). new given clause: 58 (33,2) ACHIEVABLE(Row(1),Squares(r,c,c,c,c,n,c,c)). ** KEPT: 89 (58,8,15,14,12,12,12,12,13,12,12) ACHIEVABLE(Row(2),Squares(n,n,n,n,n,c,n,n)). new given clause: 59 (34,8,15,14,13,12,12,13,13,12,12) ACHIEVABLE(Row(2),Squares(n,c,n,n,c,c,n,n)). new given clause: 60 (35,8,15,14,12,12,13,13,13,12,12) ACHIEVABLE(Row(2),Squares(n,n,n,c,c,c,n,n)). ** KEPT: 90 (60,1) ACHIEVABLE(Row(2),Squares(c,c,n,c,c,c,n,n)). new given clause: 61 (37,8,15,14,13,13,12,12,12,12,13) ACHIEVABLE(Row(2),Squares(n,c,c,n,n,n,n,c)). ** KEPT: 91 (61,5) ACHIEVABLE(Row(2),Squares(n,c,c,n,c,c,n,c)). new given clause: 62 (37,2) ACHIEVABLE(Row(1),Squares(r,c,c,c,c,c,c,n)). ** KEPT: 92 (62,8,15,14,12,12,12,12,12,12,13) ACHIEVABLE(Row(2),Squares(n,n,n,n,n,n,n,c)). new given clause: 63 (38,8,15,14,13,12,12,13,12,12,13) ACHIEVABLE(Row(2),Squares(n,c,n,n,c,n,n,c)). new given clause: 64 (39,8,15,14,12,12,13,13,12,12,13) ACHIEVABLE(Row(2),Squares(n,n,n,c,c,n,n,c)). ** KEPT: 93 (64,1) ACHIEVABLE(Row(2),Squares(c,c,n,c,c,n,n,c)). new given clause: 65 (41,8,15,14,13,12,12,12,12,13,13) ACHIEVABLE(Row(2),Squares(n,c,n,n,n,n,c,c)). ** KEPT: 94 (65,4) ACHIEVABLE(Row(2),Squares(n,c,n,c,c,n,c,c)). new given clause: 66 (42,8,15,14,12,12,13,12,12,13,13) ACHIEVABLE(Row(2),Squares(n,n,n,c,n,n,c,c)). ** KEPT: 95 (66,1) ACHIEVABLE(Row(2),Squares(c,c,n,c,n,n,c,c)). new given clause: 67 (44,8,15,14,12,12,12,12,13,13,13) ACHIEVABLE(Row(2),Squares(n,n,n,n,n,c,c,c)). ** KEPT: 96 (67,3) ACHIEVABLE(Row(2),Squares(n,n,c,c,n,c,c,c)). ** KEPT: 97 (67,1) ACHIEVABLE(Row(2),Squares(c,c,n,n,n,c,c,c)). new given clause: 68 (46,1) ACHIEVABLE(Row(2),Squares(c,c,n,c,c,c,c,c)). ** KEPT: 98 (68,8,16,12,12,13,12,12,12,12,12) ACHIEVABLE(Row(3),Squares(n,n,c,n,n,n,n,n)). new given clause: 69 (47,8,18,13,12,12,12,12,12,12,12) ACHIEVABLE(Row(5),Squares(c,n,n,n,n,n,n,n)). ** KEPT: 99 (69,8,19,12,13,13,13,13,13,13,13) ACHIEVABLE(Row(6),Squares(n,c,c,c,c,c,c,c)). ** KEPT: 100 (69,7) ACHIEVABLE(Row(5),Squares(c,n,n,n,n,n,c,c)). ** KEPT: 101 (69,6) ACHIEVABLE(Row(5),Squares(c,n,n,n,n,c,c,n)). ** KEPT: 102 (69,5) ACHIEVABLE(Row(5),Squares(c,n,n,n,c,c,n,n)). ** KEPT: 103 (69,4) ACHIEVABLE(Row(5),Squares(c,n,n,c,c,n,n,n)). ** KEPT: 104 (69,3) ACHIEVABLE(Row(5),Squares(c,n,c,c,n,n,n,n)). ** KEPT: 105 (69,2) ACHIEVABLE(Row(5),Squares(c,c,c,n,n,n,n,n)). new given clause: 70 (48,8,17,12,13,13,13,13,13,12,12) ACHIEVABLE(Row(4),Squares(n,c,c,c,c,c,n,n)). new given clause: 71 (48,5) ACHIEVABLE(Row(3),Squares(c,n,n,n,c,c,c,c)). ** KEPT: 106 (71,8,17,12,13,13,13,12,12,12,12) ACHIEVABLE(Row(4),Squares(n,c,c,c,n,n,n,n)). ** KEPT: 107 (71,3) ACHIEVABLE(Row(3),Squares(c,n,c,c,c,c,c,c)). ** KEPT: 108 (71,2) ACHIEVABLE(Row(3),Squares(c,c,c,n,c,c,c,c)). new given clause: 72 (48,4) ACHIEVABLE(Row(3),Squares(c,n,n,c,c,n,c,c)). ** KEPT: 109 (72,8,17,12,13,13,12,12,13,12,12) ACHIEVABLE(Row(4),Squares(n,c,c,n,n,c,n,n)). ** KEPT: 110 (72,2) ACHIEVABLE(Row(3),Squares(c,c,c,c,c,n,c,c)). new given clause: 73 (48,3) ACHIEVABLE(Row(3),Squares(c,n,c,c,n,n,c,c)). ** KEPT: 111 (73,8,17,12,13,12,12,13,13,12,12) ACHIEVABLE(Row(4),Squares(n,c,n,n,c,c,n,n)). new given clause: 74 (48,2) ACHIEVABLE(Row(3),Squares(c,c,c,n,n,n,c,c)). ** KEPT: 112 (74,8,17,12,12,12,13,13,13,12,12) ACHIEVABLE(Row(4),Squares(n,n,n,c,c,c,n,n)). new given clause: 75 (49,8,17,12,13,13,13,13,12,12,13) ACHIEVABLE(Row(4),Squares(n,c,c,c,c,n,n,c)). new given clause: 76 (49,4) ACHIEVABLE(Row(3),Squares(c,n,n,c,c,c,c,n)). ** KEPT: 113 (76,8,17,12,13,13,12,12,12,12,13) ACHIEVABLE(Row(4),Squares(n,c,c,n,n,n,n,c)). ** KEPT: 114 (76,2) ACHIEVABLE(Row(3),Squares(c,c,c,c,c,c,c,n)). new given clause: 77 (49,3) ACHIEVABLE(Row(3),Squares(c,n,c,c,n,c,c,n)). ** KEPT: 115 (77,8,17,12,13,12,12,13,12,12,13) ACHIEVABLE(Row(4),Squares(n,c,n,n,c,n,n,c)). new given clause: 78 (49,2) ACHIEVABLE(Row(3),Squares(c,c,c,n,n,c,c,n)). ** KEPT: 116 (78,8,17,12,12,12,13,13,12,12,13) ACHIEVABLE(Row(4),Squares(n,n,n,c,c,n,n,c)). new given clause: 79 (50,8,17,12,13,13,13,12,12,13,13) ACHIEVABLE(Row(4),Squares(n,c,c,c,n,n,c,c)). new given clause: 80 (50,3) ACHIEVABLE(Row(3),Squares(c,n,c,c,c,c,n,n)). ** KEPT: 117 (80,8,17,12,13,12,12,12,12,13,13) ACHIEVABLE(Row(4),Squares(n,c,n,n,n,n,c,c)). new given clause: 81 (50,2) ACHIEVABLE(Row(3),Squares(c,c,c,n,c,c,n,n)). ** KEPT: 118 (81,8,17,12,12,12,13,12,12,13,13) ACHIEVABLE(Row(4),Squares(n,n,n,c,n,n,c,c)). new given clause: 82 (51,8,17,12,13,13,12,12,13,13,13) ACHIEVABLE(Row(4),Squares(n,c,c,n,n,c,c,c)). new given clause: 83 (51,2) ACHIEVABLE(Row(3),Squares(c,c,c,c,c,n,n,n)). ** KEPT: 119 (83,8,17,12,12,12,12,12,13,13,13) ACHIEVABLE(Row(4),Squares(n,n,n,n,n,c,c,c)). new given clause: 84 (52,8,17,12,13,12,12,13,13,13,13) ACHIEVABLE(Row(4),Squares(n,c,n,n,c,c,c,c)). new given clause: 85 (53,8,17,12,12,12,13,13,13,13,13) ACHIEVABLE(Row(4),Squares(n,n,n,c,c,c,c,c)). ** KEPT: 120 (85,1) ACHIEVABLE(Row(4),Squares(c,c,n,c,c,c,c,c)). new given clause: 86 (54,6) ACHIEVABLE(Row(2),Squares(n,c,c,c,n,c,c,n)). ** KEPT: 121 (86,8,16,13,12,12,12,13,12,12,13) ACHIEVABLE(Row(3),Squares(c,n,n,n,c,n,n,c)). new given clause: 87 (55,8,15,14,13,12,12,12,12,12,12) ACHIEVABLE(Row(2),Squares(n,c,n,n,n,n,n,n)). ** KEPT: 122 (87,6) ACHIEVABLE(Row(2),Squares(n,c,n,n,n,c,c,n)). ** KEPT: 123 (87,4) ACHIEVABLE(Row(2),Squares(n,c,n,c,c,n,n,n)). new given clause: 88 (56,8,15,14,12,12,13,12,12,12,12) ACHIEVABLE(Row(2),Squares(n,n,n,c,n,n,n,n)). ** KEPT: 124 (88,6) ACHIEVABLE(Row(2),Squares(n,n,n,c,n,c,c,n)). ** KEPT: 125 (88,1) ACHIEVABLE(Row(2),Squares(c,c,n,c,n,n,n,n)). new given clause: 89 (58,8,15,14,12,12,12,12,13,12,12) ACHIEVABLE(Row(2),Squares(n,n,n,n,n,c,n,n)). ** KEPT: 126 (89,3) ACHIEVABLE(Row(2),Squares(n,n,c,c,n,c,n,n)). ** KEPT: 127 (89,1) ACHIEVABLE(Row(2),Squares(c,c,n,n,n,c,n,n)). new given clause: 90 (60,1) ACHIEVABLE(Row(2),Squares(c,c,n,c,c,c,n,n)). ** KEPT: 128 (90,8,16,12,12,13,12,12,12,13,13) ACHIEVABLE(Row(3),Squares(n,n,c,n,n,n,c,c)). new given clause: 91 (61,5) ACHIEVABLE(Row(2),Squares(n,c,c,n,c,c,n,c)). ** KEPT: 129 (91,8,16,13,12,12,13,12,12,13,12) ACHIEVABLE(Row(3),Squares(c,n,n,c,n,n,c,n)). new given clause: 92 (62,8,15,14,12,12,12,12,12,12,13) ACHIEVABLE(Row(2),Squares(n,n,n,n,n,n,n,c)). ** KEPT: 130 (92,5) ACHIEVABLE(Row(2),Squares(n,n,n,n,c,c,n,c)). ** KEPT: 131 (92,3) ACHIEVABLE(Row(2),Squares(n,n,c,c,n,n,n,c)). ** KEPT: 132 (92,1) ACHIEVABLE(Row(2),Squares(c,c,n,n,n,n,n,c)). new given clause: 93 (64,1) ACHIEVABLE(Row(2),Squares(c,c,n,c,c,n,n,c)). ** KEPT: 133 (93,8,16,12,12,13,12,12,13,13,12) ACHIEVABLE(Row(3),Squares(n,n,c,n,n,c,c,n)). new given clause: 94 (65,4) ACHIEVABLE(Row(2),Squares(n,c,n,c,c,n,c,c)). ** KEPT: 134 (94,8,16,13,12,13,12,12,13,12,12) ACHIEVABLE(Row(3),Squares(c,n,c,n,n,c,n,n)). new given clause: 95 (66,1) ACHIEVABLE(Row(2),Squares(c,c,n,c,n,n,c,c)). ** KEPT: 135 (95,8,16,12,12,13,12,13,13,12,12) ACHIEVABLE(Row(3),Squares(n,n,c,n,c,c,n,n)). new given clause: 96 (67,3) ACHIEVABLE(Row(2),Squares(n,n,c,c,n,c,c,c)). ** KEPT: 136 (96,8,16,13,13,12,12,13,12,12,12) ACHIEVABLE(Row(3),Squares(c,c,n,n,c,n,n,n)). ** KEPT: 137 (96,1) ACHIEVABLE(Row(2),Squares(c,c,c,c,n,c,c,c)). new given clause: 97 (67,1) ACHIEVABLE(Row(2),Squares(c,c,n,n,n,c,c,c)). ** KEPT: 138 (97,8,16,12,12,13,13,13,12,12,12) ACHIEVABLE(Row(3),Squares(n,n,c,c,c,n,n,n)). new given clause: 98 (68,8,16,12,12,13,12,12,12,12,12) ACHIEVABLE(Row(3),Squares(n,n,c,n,n,n,n,n)). new given clause: 99 (69,8,19,12,13,13,13,13,13,13,13) ACHIEVABLE(Row(6),Squares(n,c,c,c,c,c,c,c)). ** KEPT: 139 (99,8,20,13,12,12,12,12,12,12,12) ACHIEVABLE(Row(7),Squares(c,n,n,n,n,n,n,n)). new given clause: 100 (69,7) ACHIEVABLE(Row(5),Squares(c,n,n,n,n,n,c,c)). ** KEPT: 140 (100,8,19,12,13,13,13,13,13,12,12) ACHIEVABLE(Row(6),Squares(n,c,c,c,c,c,n,n)). ** KEPT: 141 (100,5) ACHIEVABLE(Row(5),Squares(c,n,n,n,c,c,c,c)). ** KEPT: 142 (100,4) ACHIEVABLE(Row(5),Squares(c,n,n,c,c,n,c,c)). ** KEPT: 143 (100,3) ACHIEVABLE(Row(5),Squares(c,n,c,c,n,n,c,c)). ** KEPT: 144 (100,2) ACHIEVABLE(Row(5),Squares(c,c,c,n,n,n,c,c)). new given clause: 101 (69,6) ACHIEVABLE(Row(5),Squares(c,n,n,n,n,c,c,n)). ** KEPT: 145 (101,8,19,12,13,13,13,13,12,12,13) ACHIEVABLE(Row(6),Squares(n,c,c,c,c,n,n,c)). ** KEPT: 146 (101,4) ACHIEVABLE(Row(5),Squares(c,n,n,c,c,c,c,n)). ** KEPT: 147 (101,3) ACHIEVABLE(Row(5),Squares(c,n,c,c,n,c,c,n)). ** KEPT: 148 (101,2) ACHIEVABLE(Row(5),Squares(c,c,c,n,n,c,c,n)). new given clause: 102 (69,5) ACHIEVABLE(Row(5),Squares(c,n,n,n,c,c,n,n)). ** KEPT: 149 (102,8,19,12,13,13,13,12,12,13,13) ACHIEVABLE(Row(6),Squares(n,c,c,c,n,n,c,c)). ** KEPT: 150 (102,3) ACHIEVABLE(Row(5),Squares(c,n,c,c,c,c,n,n)). ** KEPT: 151 (102,2) ACHIEVABLE(Row(5),Squares(c,c,c,n,c,c,n,n)). new given clause: 103 (69,4) ACHIEVABLE(Row(5),Squares(c,n,n,c,c,n,n,n)). ** KEPT: 152 (103,8,19,12,13,13,12,12,13,13,13) ACHIEVABLE(Row(6),Squares(n,c,c,n,n,c,c,c)). ** KEPT: 153 (103,2) ACHIEVABLE(Row(5),Squares(c,c,c,c,c,n,n,n)). new given clause: 104 (69,3) ACHIEVABLE(Row(5),Squares(c,n,c,c,n,n,n,n)). ** KEPT: 154 (104,8,19,12,13,12,12,13,13,13,13) ACHIEVABLE(Row(6),Squares(n,c,n,n,c,c,c,c)). new given clause: 105 (69,2) ACHIEVABLE(Row(5),Squares(c,c,c,n,n,n,n,n)). ** KEPT: 155 (105,8,19,12,12,12,13,13,13,13,13) ACHIEVABLE(Row(6),Squares(n,n,n,c,c,c,c,c)). new given clause: 106 (71,8,17,12,13,13,13,12,12,12,12) ACHIEVABLE(Row(4),Squares(n,c,c,c,n,n,n,n)). ** KEPT: 156 (106,6) ACHIEVABLE(Row(4),Squares(n,c,c,c,n,c,c,n)). new given clause: 107 (71,3) ACHIEVABLE(Row(3),Squares(c,n,c,c,c,c,c,c)). ** KEPT: 157 (107,8,17,12,13,12,12,12,12,12,12) ACHIEVABLE(Row(4),Squares(n,c,n,n,n,n,n,n)). new given clause: 108 (71,2) ACHIEVABLE(Row(3),Squares(c,c,c,n,c,c,c,c)). ** KEPT: 158 (108,8,17,12,12,12,13,12,12,12,12) ACHIEVABLE(Row(4),Squares(n,n,n,c,n,n,n,n)). new given clause: 109 (72,8,17,12,13,13,12,12,13,12,12) ACHIEVABLE(Row(4),Squares(n,c,c,n,n,c,n,n)). new given clause: 110 (72,2) ACHIEVABLE(Row(3),Squares(c,c,c,c,c,n,c,c)). ** KEPT: 159 (110,8,17,12,12,12,12,12,13,12,12) ACHIEVABLE(Row(4),Squares(n,n,n,n,n,c,n,n)). new given clause: 111 (73,8,17,12,13,12,12,13,13,12,12) ACHIEVABLE(Row(4),Squares(n,c,n,n,c,c,n,n)). new given clause: 112 (74,8,17,12,12,12,13,13,13,12,12) ACHIEVABLE(Row(4),Squares(n,n,n,c,c,c,n,n)). ** KEPT: 160 (112,1) ACHIEVABLE(Row(4),Squares(c,c,n,c,c,c,n,n)). new given clause: 113 (76,8,17,12,13,13,12,12,12,12,13) ACHIEVABLE(Row(4),Squares(n,c,c,n,n,n,n,c)). ** KEPT: 161 (113,5) ACHIEVABLE(Row(4),Squares(n,c,c,n,c,c,n,c)). new given clause: 114 (76,2) ACHIEVABLE(Row(3),Squares(c,c,c,c,c,c,c,n)). ** KEPT: 162 (114,8,17,12,12,12,12,12,12,12,13) ACHIEVABLE(Row(4),Squares(n,n,n,n,n,n,n,c)). new given clause: 115 (77,8,17,12,13,12,12,13,12,12,13) ACHIEVABLE(Row(4),Squares(n,c,n,n,c,n,n,c)). new given clause: 116 (78,8,17,12,12,12,13,13,12,12,13) ACHIEVABLE(Row(4),Squares(n,n,n,c,c,n,n,c)). ** KEPT: 163 (116,1) ACHIEVABLE(Row(4),Squares(c,c,n,c,c,n,n,c)). new given clause: 117 (80,8,17,12,13,12,12,12,12,13,13) ACHIEVABLE(Row(4),Squares(n,c,n,n,n,n,c,c)). ** KEPT: 164 (117,4) ACHIEVABLE(Row(4),Squares(n,c,n,c,c,n,c,c)). new given clause: 118 (81,8,17,12,12,12,13,12,12,13,13) ACHIEVABLE(Row(4),Squares(n,n,n,c,n,n,c,c)). ** KEPT: 165 (118,1) ACHIEVABLE(Row(4),Squares(c,c,n,c,n,n,c,c)). new given clause: 119 (83,8,17,12,12,12,12,12,13,13,13) ACHIEVABLE(Row(4),Squares(n,n,n,n,n,c,c,c)). ** KEPT: 166 (119,3) ACHIEVABLE(Row(4),Squares(n,n,c,c,n,c,c,c)). ** KEPT: 167 (119,1) ACHIEVABLE(Row(4),Squares(c,c,n,n,n,c,c,c)). new given clause: 120 (85,1) ACHIEVABLE(Row(4),Squares(c,c,n,c,c,c,c,c)). ** KEPT: 168 (120,8,18,12,12,13,12,12,12,12,12) ACHIEVABLE(Row(5),Squares(n,n,c,n,n,n,n,n)). new given clause: 121 (86,8,16,13,12,12,12,13,12,12,13) ACHIEVABLE(Row(3),Squares(c,n,n,n,c,n,n,c)). ** KEPT: 169 (121,3) ACHIEVABLE(Row(3),Squares(c,n,c,c,c,n,n,c)). ** KEPT: 170 (121,2) ACHIEVABLE(Row(3),Squares(c,c,c,n,c,n,n,c)). new given clause: 122 (87,6) ACHIEVABLE(Row(2),Squares(n,c,n,n,n,c,c,n)). ** KEPT: 171 (122,4) ACHIEVABLE(Row(2),Squares(n,c,n,c,c,c,c,n)). new given clause: 123 (87,4) ACHIEVABLE(Row(2),Squares(n,c,n,c,c,n,n,n)). ** KEPT: 172 (123,8,16,13,12,13,12,12,13,13,13) ACHIEVABLE(Row(3),Squares(c,n,c,n,n,c,c,c)). new given clause: 124 (88,6) ACHIEVABLE(Row(2),Squares(n,n,n,c,n,c,c,n)). ** KEPT: 173 (124,1) ACHIEVABLE(Row(2),Squares(c,c,n,c,n,c,c,n)). new given clause: 125 (88,1) ACHIEVABLE(Row(2),Squares(c,c,n,c,n,n,n,n)). ** KEPT: 174 (125,8,16,12,12,13,12,13,13,13,13) ACHIEVABLE(Row(3),Squares(n,n,c,n,c,c,c,c)). new given clause: 126 (89,3) ACHIEVABLE(Row(2),Squares(n,n,c,c,n,c,n,n)). ** KEPT: 175 (126,8,16,13,13,12,12,13,12,13,13) ACHIEVABLE(Row(3),Squares(c,c,n,n,c,n,c,c)). ** KEPT: 176 (126,1) ACHIEVABLE(Row(2),Squares(c,c,c,c,n,c,n,n)). new given clause: 127 (89,1) ACHIEVABLE(Row(2),Squares(c,c,n,n,n,c,n,n)). ** KEPT: 177 (127,8,16,12,12,13,13,13,12,13,13) ACHIEVABLE(Row(3),Squares(n,n,c,c,c,n,c,c)). new given clause: 128 (90,8,16,12,12,13,12,12,12,13,13) ACHIEVABLE(Row(3),Squares(n,n,c,n,n,n,c,c)). new given clause: 129 (91,8,16,13,12,12,13,12,12,13,12) ACHIEVABLE(Row(3),Squares(c,n,n,c,n,n,c,n)). ** KEPT: 178 (129,2) ACHIEVABLE(Row(3),Squares(c,c,c,c,n,n,c,n)). new given clause: 130 (92,5) ACHIEVABLE(Row(2),Squares(n,n,n,n,c,c,n,c)). ** KEPT: 179 (130,3) ACHIEVABLE(Row(2),Squares(n,n,c,c,c,c,n,c)). ** KEPT: 180 (130,1) ACHIEVABLE(Row(2),Squares(c,c,n,n,c,c,n,c)). new given clause: 131 (92,3) ACHIEVABLE(Row(2),Squares(n,n,c,c,n,n,n,c)). ** KEPT: 181 (131,8,16,13,13,12,12,13,13,13,12) ACHIEVABLE(Row(3),Squares(c,c,n,n,c,c,c,n)). ** KEPT: 182 (131,1) ACHIEVABLE(Row(2),Squares(c,c,c,c,n,n,n,c)). new given clause: 132 (92,1) ACHIEVABLE(Row(2),Squares(c,c,n,n,n,n,n,c)). ** KEPT: 183 (132,8,16,12,12,13,13,13,13,13,12) ACHIEVABLE(Row(3),Squares(n,n,c,c,c,c,c,n)). new given clause: 133 (93,8,16,12,12,13,12,12,13,13,12) ACHIEVABLE(Row(3),Squares(n,n,c,n,n,c,c,n)). new given clause: 134 (94,8,16,13,12,13,12,12,13,12,12) ACHIEVABLE(Row(3),Squares(c,n,c,n,n,c,n,n)). new given clause: 135 (95,8,16,12,12,13,12,13,13,12,12) ACHIEVABLE(Row(3),Squares(n,n,c,n,c,c,n,n)). new given clause: 136 (96,8,16,13,13,12,12,13,12,12,12) ACHIEVABLE(Row(3),Squares(c,c,n,n,c,n,n,n)). new given clause: 137 (96,1) ACHIEVABLE(Row(2),Squares(c,c,c,c,n,c,c,c)). ** KEPT: 184 (137,8,16,12,12,12,12,13,12,12,12) ACHIEVABLE(Row(3),Squares(n,n,n,n,c,n,n,n)). new given clause: 138 (97,8,16,12,12,13,13,13,12,12,12) ACHIEVABLE(Row(3),Squares(n,n,c,c,c,n,n,n)). new given clause: 139 (99,8,20,13,12,12,12,12,12,12,12) ACHIEVABLE(Row(7),Squares(c,n,n,n,n,n,n,n)). ** KEPT: 185 (139,8,21,12,13,13,13,13,13,13,13) ACHIEVABLE(Row(8),Squares(n,c,c,c,c,c,c,c)). ** KEPT: 186 (139,7) ACHIEVABLE(Row(7),Squares(c,n,n,n,n,n,c,c)). ** KEPT: 187 (139,6) ACHIEVABLE(Row(7),Squares(c,n,n,n,n,c,c,n)). ** KEPT: 188 (139,5) ACHIEVABLE(Row(7),Squares(c,n,n,n,c,c,n,n)). ** KEPT: 189 (139,4) ACHIEVABLE(Row(7),Squares(c,n,n,c,c,n,n,n)). ** KEPT: 190 (139,3) ACHIEVABLE(Row(7),Squares(c,n,c,c,n,n,n,n)). ** KEPT: 191 (139,2) ACHIEVABLE(Row(7),Squares(c,c,c,n,n,n,n,n)). new given clause: 140 (100,8,19,12,13,13,13,13,13,12,12) ACHIEVABLE(Row(6),Squares(n,c,c,c,c,c,n,n)). new given clause: 141 (100,5) ACHIEVABLE(Row(5),Squares(c,n,n,n,c,c,c,c)). ** KEPT: 192 (141,8,19,12,13,13,13,12,12,12,12) ACHIEVABLE(Row(6),Squares(n,c,c,c,n,n,n,n)). ** KEPT: 193 (141,3) ACHIEVABLE(Row(5),Squares(c,n,c,c,c,c,c,c)). ** KEPT: 194 (141,2) ACHIEVABLE(Row(5),Squares(c,c,c,n,c,c,c,c)). new given clause: 142 (100,4) ACHIEVABLE(Row(5),Squares(c,n,n,c,c,n,c,c)). ** KEPT: 195 (142,8,19,12,13,13,12,12,13,12,12) ACHIEVABLE(Row(6),Squares(n,c,c,n,n,c,n,n)). ** KEPT: 196 (142,2) ACHIEVABLE(Row(5),Squares(c,c,c,c,c,n,c,c)). new given clause: 143 (100,3) ACHIEVABLE(Row(5),Squares(c,n,c,c,n,n,c,c)). ** KEPT: 197 (143,8,19,12,13,12,12,13,13,12,12) ACHIEVABLE(Row(6),Squares(n,c,n,n,c,c,n,n)). new given clause: 144 (100,2) ACHIEVABLE(Row(5),Squares(c,c,c,n,n,n,c,c)). ** KEPT: 198 (144,8,19,12,12,12,13,13,13,12,12) ACHIEVABLE(Row(6),Squares(n,n,n,c,c,c,n,n)). new given clause: 145 (101,8,19,12,13,13,13,13,12,12,13) ACHIEVABLE(Row(6),Squares(n,c,c,c,c,n,n,c)). new given clause: 146 (101,4) ACHIEVABLE(Row(5),Squares(c,n,n,c,c,c,c,n)). ** KEPT: 199 (146,8,19,12,13,13,12,12,12,12,13) ACHIEVABLE(Row(6),Squares(n,c,c,n,n,n,n,c)). ** KEPT: 200 (146,2) ACHIEVABLE(Row(5),Squares(c,c,c,c,c,c,c,n)). new given clause: 147 (101,3) ACHIEVABLE(Row(5),Squares(c,n,c,c,n,c,c,n)). ** KEPT: 201 (147,8,19,12,13,12,12,13,12,12,13) ACHIEVABLE(Row(6),Squares(n,c,n,n,c,n,n,c)). new given clause: 148 (101,2) ACHIEVABLE(Row(5),Squares(c,c,c,n,n,c,c,n)). ** KEPT: 202 (148,8,19,12,12,12,13,13,12,12,13) ACHIEVABLE(Row(6),Squares(n,n,n,c,c,n,n,c)). new given clause: 149 (102,8,19,12,13,13,13,12,12,13,13) ACHIEVABLE(Row(6),Squares(n,c,c,c,n,n,c,c)). new given clause: 150 (102,3) ACHIEVABLE(Row(5),Squares(c,n,c,c,c,c,n,n)). ** KEPT: 203 (150,8,19,12,13,12,12,12,12,13,13) ACHIEVABLE(Row(6),Squares(n,c,n,n,n,n,c,c)). new given clause: 151 (102,2) ACHIEVABLE(Row(5),Squares(c,c,c,n,c,c,n,n)). ** KEPT: 204 (151,8,19,12,12,12,13,12,12,13,13) ACHIEVABLE(Row(6),Squares(n,n,n,c,n,n,c,c)). new given clause: 152 (103,8,19,12,13,13,12,12,13,13,13) ACHIEVABLE(Row(6),Squares(n,c,c,n,n,c,c,c)). new given clause: 153 (103,2) ACHIEVABLE(Row(5),Squares(c,c,c,c,c,n,n,n)). ** KEPT: 205 (153,8,19,12,12,12,12,12,13,13,13) ACHIEVABLE(Row(6),Squares(n,n,n,n,n,c,c,c)). new given clause: 154 (104,8,19,12,13,12,12,13,13,13,13) ACHIEVABLE(Row(6),Squares(n,c,n,n,c,c,c,c)). new given clause: 155 (105,8,19,12,12,12,13,13,13,13,13) ACHIEVABLE(Row(6),Squares(n,n,n,c,c,c,c,c)). ** KEPT: 206 (155,1) ACHIEVABLE(Row(6),Squares(c,c,n,c,c,c,c,c)). new given clause: 156 (106,6) ACHIEVABLE(Row(4),Squares(n,c,c,c,n,c,c,n)). ** KEPT: 207 (156,8,18,13,12,12,12,13,12,12,13) ACHIEVABLE(Row(5),Squares(c,n,n,n,c,n,n,c)). new given clause: 157 (107,8,17,12,13,12,12,12,12,12,12) ACHIEVABLE(Row(4),Squares(n,c,n,n,n,n,n,n)). ** KEPT: 208 (157,6) ACHIEVABLE(Row(4),Squares(n,c,n,n,n,c,c,n)). ** KEPT: 209 (157,4) ACHIEVABLE(Row(4),Squares(n,c,n,c,c,n,n,n)). new given clause: 158 (108,8,17,12,12,12,13,12,12,12,12) ACHIEVABLE(Row(4),Squares(n,n,n,c,n,n,n,n)). ** KEPT: 210 (158,6) ACHIEVABLE(Row(4),Squares(n,n,n,c,n,c,c,n)). ** KEPT: 211 (158,1) ACHIEVABLE(Row(4),Squares(c,c,n,c,n,n,n,n)). new given clause: 159 (110,8,17,12,12,12,12,12,13,12,12) ACHIEVABLE(Row(4),Squares(n,n,n,n,n,c,n,n)). ** KEPT: 212 (159,3) ACHIEVABLE(Row(4),Squares(n,n,c,c,n,c,n,n)). ** KEPT: 213 (159,1) ACHIEVABLE(Row(4),Squares(c,c,n,n,n,c,n,n)). new given clause: 160 (112,1) ACHIEVABLE(Row(4),Squares(c,c,n,c,c,c,n,n)). ** KEPT: 214 (160,8,18,12,12,13,12,12,12,13,13) ACHIEVABLE(Row(5),Squares(n,n,c,n,n,n,c,c)). new given clause: 161 (113,5) ACHIEVABLE(Row(4),Squares(n,c,c,n,c,c,n,c)). ** KEPT: 215 (161,8,18,13,12,12,13,12,12,13,12) ACHIEVABLE(Row(5),Squares(c,n,n,c,n,n,c,n)). new given clause: 162 (114,8,17,12,12,12,12,12,12,12,13) ACHIEVABLE(Row(4),Squares(n,n,n,n,n,n,n,c)). ** KEPT: 216 (162,5) ACHIEVABLE(Row(4),Squares(n,n,n,n,c,c,n,c)). ** KEPT: 217 (162,3) ACHIEVABLE(Row(4),Squares(n,n,c,c,n,n,n,c)). ** KEPT: 218 (162,1) ACHIEVABLE(Row(4),Squares(c,c,n,n,n,n,n,c)). new given clause: 163 (116,1) ACHIEVABLE(Row(4),Squares(c,c,n,c,c,n,n,c)). ** KEPT: 219 (163,8,18,12,12,13,12,12,13,13,12) ACHIEVABLE(Row(5),Squares(n,n,c,n,n,c,c,n)). new given clause: 164 (117,4) ACHIEVABLE(Row(4),Squares(n,c,n,c,c,n,c,c)). ** KEPT: 220 (164,8,18,13,12,13,12,12,13,12,12) ACHIEVABLE(Row(5),Squares(c,n,c,n,n,c,n,n)). new given clause: 165 (118,1) ACHIEVABLE(Row(4),Squares(c,c,n,c,n,n,c,c)). ** KEPT: 221 (165,8,18,12,12,13,12,13,13,12,12) ACHIEVABLE(Row(5),Squares(n,n,c,n,c,c,n,n)). new given clause: 166 (119,3) ACHIEVABLE(Row(4),Squares(n,n,c,c,n,c,c,c)). ** KEPT: 222 (166,8,18,13,13,12,12,13,12,12,12) ACHIEVABLE(Row(5),Squares(c,c,n,n,c,n,n,n)). ** KEPT: 223 (166,1) ACHIEVABLE(Row(4),Squares(c,c,c,c,n,c,c,c)). new given clause: 167 (119,1) ACHIEVABLE(Row(4),Squares(c,c,n,n,n,c,c,c)). ** KEPT: 224 (167,8,18,12,12,13,13,13,12,12,12) ACHIEVABLE(Row(5),Squares(n,n,c,c,c,n,n,n)). new given clause: 168 (120,8,18,12,12,13,12,12,12,12,12) ACHIEVABLE(Row(5),Squares(n,n,c,n,n,n,n,n)). new given clause: 169 (121,3) ACHIEVABLE(Row(3),Squares(c,n,c,c,c,n,n,c)). new given clause: 170 (121,2) ACHIEVABLE(Row(3),Squares(c,c,c,n,c,n,n,c)). new given clause: 171 (122,4) ACHIEVABLE(Row(2),Squares(n,c,n,c,c,c,c,n)). ** KEPT: 225 (171,8,16,13,12,13,12,12,12,12,13) ACHIEVABLE(Row(3),Squares(c,n,c,n,n,n,n,c)). new given clause: 172 (123,8,16,13,12,13,12,12,13,13,13) ACHIEVABLE(Row(3),Squares(c,n,c,n,n,c,c,c)). new given clause: 173 (124,1) ACHIEVABLE(Row(2),Squares(c,c,n,c,n,c,c,n)). ** KEPT: 226 (173,8,16,12,12,13,12,13,12,12,13) ACHIEVABLE(Row(3),Squares(n,n,c,n,c,n,n,c)). new given clause: 174 (125,8,16,12,12,13,12,13,13,13,13) ACHIEVABLE(Row(3),Squares(n,n,c,n,c,c,c,c)). new given clause: 175 (126,8,16,13,13,12,12,13,12,13,13) ACHIEVABLE(Row(3),Squares(c,c,n,n,c,n,c,c)). new given clause: 176 (126,1) ACHIEVABLE(Row(2),Squares(c,c,c,c,n,c,n,n)). ** KEPT: 227 (176,8,16,12,12,12,12,13,12,13,13) ACHIEVABLE(Row(3),Squares(n,n,n,n,c,n,c,c)). new given clause: 177 (127,8,16,12,12,13,13,13,12,13,13) ACHIEVABLE(Row(3),Squares(n,n,c,c,c,n,c,c)). new given clause: 178 (129,2) ACHIEVABLE(Row(3),Squares(c,c,c,c,n,n,c,n)). new given clause: 179 (130,3) ACHIEVABLE(Row(2),Squares(n,n,c,c,c,c,n,c)). ** KEPT: 228 (179,8,16,13,13,12,12,12,12,13,12) ACHIEVABLE(Row(3),Squares(c,c,n,n,n,n,c,n)). ** KEPT: 229 (179,1) ACHIEVABLE(Row(2),Squares(c,c,c,c,c,c,n,c)). new given clause: 180 (130,1) ACHIEVABLE(Row(2),Squares(c,c,n,n,c,c,n,c)). ** KEPT: 230 (180,8,16,12,12,13,13,12,12,13,12) ACHIEVABLE(Row(3),Squares(n,n,c,c,n,n,c,n)). new given clause: 181 (131,8,16,13,13,12,12,13,13,13,12) ACHIEVABLE(Row(3),Squares(c,c,n,n,c,c,c,n)). new given clause: 182 (131,1) ACHIEVABLE(Row(2),Squares(c,c,c,c,n,n,n,c)). ** KEPT: 231 (182,8,16,12,12,12,12,13,13,13,12) ACHIEVABLE(Row(3),Squares(n,n,n,n,c,c,c,n)). new given clause: 183 (132,8,16,12,12,13,13,13,13,13,12) ACHIEVABLE(Row(3),Squares(n,n,c,c,c,c,c,n)). new given clause: 184 (137,8,16,12,12,12,12,13,12,12,12) ACHIEVABLE(Row(3),Squares(n,n,n,n,c,n,n,n)). ** KEPT: 232 (184,2) ACHIEVABLE(Row(3),Squares(n,c,c,n,c,n,n,n)). new given clause: 185 (139,8,21,12,13,13,13,13,13,13,13) ACHIEVABLE(Row(8),Squares(n,c,c,c,c,c,c,c)). new given clause: 186 (139,7) ACHIEVABLE(Row(7),Squares(c,n,n,n,n,n,c,c)). ** KEPT: 233 (186,8,21,12,13,13,13,13,13,12,12) ACHIEVABLE(Row(8),Squares(n,c,c,c,c,c,n,n)). ** KEPT: 234 (186,5) ACHIEVABLE(Row(7),Squares(c,n,n,n,c,c,c,c)). ** KEPT: 235 (186,4) ACHIEVABLE(Row(7),Squares(c,n,n,c,c,n,c,c)). ** KEPT: 236 (186,3) ACHIEVABLE(Row(7),Squares(c,n,c,c,n,n,c,c)). ** KEPT: 237 (186,2) ACHIEVABLE(Row(7),Squares(c,c,c,n,n,n,c,c)). new given clause: 187 (139,6) ACHIEVABLE(Row(7),Squares(c,n,n,n,n,c,c,n)). ** KEPT: 238 (187,8,21,12,13,13,13,13,12,12,13) ACHIEVABLE(Row(8),Squares(n,c,c,c,c,n,n,c)). ** KEPT: 239 (187,4) ACHIEVABLE(Row(7),Squares(c,n,n,c,c,c,c,n)). ** KEPT: 240 (187,3) ACHIEVABLE(Row(7),Squares(c,n,c,c,n,c,c,n)). ** KEPT: 241 (187,2) ACHIEVABLE(Row(7),Squares(c,c,c,n,n,c,c,n)). new given clause: 188 (139,5) ACHIEVABLE(Row(7),Squares(c,n,n,n,c,c,n,n)). ** KEPT: 242 (188,8,21,12,13,13,13,12,12,13,13) ACHIEVABLE(Row(8),Squares(n,c,c,c,n,n,c,c)). ** KEPT: 243 (188,3) ACHIEVABLE(Row(7),Squares(c,n,c,c,c,c,n,n)). ** KEPT: 244 (188,2) ACHIEVABLE(Row(7),Squares(c,c,c,n,c,c,n,n)). new given clause: 189 (139,4) ACHIEVABLE(Row(7),Squares(c,n,n,c,c,n,n,n)). ** KEPT: 245 (189,8,21,12,13,13,12,12,13,13,13) ACHIEVABLE(Row(8),Squares(n,c,c,n,n,c,c,c)). ** KEPT: 246 (189,2) ACHIEVABLE(Row(7),Squares(c,c,c,c,c,n,n,n)). new given clause: 190 (139,3) ACHIEVABLE(Row(7),Squares(c,n,c,c,n,n,n,n)). ** KEPT: 247 (190,8,21,12,13,12,12,13,13,13,13) ACHIEVABLE(Row(8),Squares(n,c,n,n,c,c,c,c)). new given clause: 191 (139,2) ACHIEVABLE(Row(7),Squares(c,c,c,n,n,n,n,n)). ** KEPT: 248 (191,8,21,12,12,12,13,13,13,13,13) ACHIEVABLE(Row(8),Squares(n,n,n,c,c,c,c,c)). new given clause: 192 (141,8,19,12,13,13,13,12,12,12,12) ACHIEVABLE(Row(6),Squares(n,c,c,c,n,n,n,n)). ** KEPT: 249 (192,6) ACHIEVABLE(Row(6),Squares(n,c,c,c,n,c,c,n)). new given clause: 193 (141,3) ACHIEVABLE(Row(5),Squares(c,n,c,c,c,c,c,c)). ** KEPT: 250 (193,8,19,12,13,12,12,12,12,12,12) ACHIEVABLE(Row(6),Squares(n,c,n,n,n,n,n,n)). new given clause: 194 (141,2) ACHIEVABLE(Row(5),Squares(c,c,c,n,c,c,c,c)). ** KEPT: 251 (194,8,19,12,12,12,13,12,12,12,12) ACHIEVABLE(Row(6),Squares(n,n,n,c,n,n,n,n)). new given clause: 195 (142,8,19,12,13,13,12,12,13,12,12) ACHIEVABLE(Row(6),Squares(n,c,c,n,n,c,n,n)). new given clause: 196 (142,2) ACHIEVABLE(Row(5),Squares(c,c,c,c,c,n,c,c)). ** KEPT: 252 (196,8,19,12,12,12,12,12,13,12,12) ACHIEVABLE(Row(6),Squares(n,n,n,n,n,c,n,n)). new given clause: 197 (143,8,19,12,13,12,12,13,13,12,12) ACHIEVABLE(Row(6),Squares(n,c,n,n,c,c,n,n)). new given clause: 198 (144,8,19,12,12,12,13,13,13,12,12) ACHIEVABLE(Row(6),Squares(n,n,n,c,c,c,n,n)). ** KEPT: 253 (198,1) ACHIEVABLE(Row(6),Squares(c,c,n,c,c,c,n,n)). new given clause: 199 (146,8,19,12,13,13,12,12,12,12,13) ACHIEVABLE(Row(6),Squares(n,c,c,n,n,n,n,c)). ** KEPT: 254 (199,5) ACHIEVABLE(Row(6),Squares(n,c,c,n,c,c,n,c)). new given clause: 200 (146,2) ACHIEVABLE(Row(5),Squares(c,c,c,c,c,c,c,n)). ** KEPT: 255 (200,8,19,12,12,12,12,12,12,12,13) ACHIEVABLE(Row(6),Squares(n,n,n,n,n,n,n,c)). new given clause: 201 (147,8,19,12,13,12,12,13,12,12,13) ACHIEVABLE(Row(6),Squares(n,c,n,n,c,n,n,c)). new given clause: 202 (148,8,19,12,12,12,13,13,12,12,13) ACHIEVABLE(Row(6),Squares(n,n,n,c,c,n,n,c)). ** KEPT: 256 (202,1) ACHIEVABLE(Row(6),Squares(c,c,n,c,c,n,n,c)). new given clause: 203 (150,8,19,12,13,12,12,12,12,13,13) ACHIEVABLE(Row(6),Squares(n,c,n,n,n,n,c,c)). ** KEPT: 257 (203,4) ACHIEVABLE(Row(6),Squares(n,c,n,c,c,n,c,c)). new given clause: 204 (151,8,19,12,12,12,13,12,12,13,13) ACHIEVABLE(Row(6),Squares(n,n,n,c,n,n,c,c)). ** KEPT: 258 (204,1) ACHIEVABLE(Row(6),Squares(c,c,n,c,n,n,c,c)). new given clause: 205 (153,8,19,12,12,12,12,12,13,13,13) ACHIEVABLE(Row(6),Squares(n,n,n,n,n,c,c,c)). ** KEPT: 259 (205,3) ACHIEVABLE(Row(6),Squares(n,n,c,c,n,c,c,c)). ** KEPT: 260 (205,1) ACHIEVABLE(Row(6),Squares(c,c,n,n,n,c,c,c)). new given clause: 206 (155,1) ACHIEVABLE(Row(6),Squares(c,c,n,c,c,c,c,c)). ** KEPT: 261 (206,8,20,12,12,13,12,12,12,12,12) ACHIEVABLE(Row(7),Squares(n,n,c,n,n,n,n,n)). new given clause: 207 (156,8,18,13,12,12,12,13,12,12,13) ACHIEVABLE(Row(5),Squares(c,n,n,n,c,n,n,c)). ** KEPT: 262 (207,3) ACHIEVABLE(Row(5),Squares(c,n,c,c,c,n,n,c)). ** KEPT: 263 (207,2) ACHIEVABLE(Row(5),Squares(c,c,c,n,c,n,n,c)). new given clause: 208 (157,6) ACHIEVABLE(Row(4),Squares(n,c,n,n,n,c,c,n)). ** KEPT: 264 (208,4) ACHIEVABLE(Row(4),Squares(n,c,n,c,c,c,c,n)). new given clause: 209 (157,4) ACHIEVABLE(Row(4),Squares(n,c,n,c,c,n,n,n)). ** KEPT: 265 (209,8,18,13,12,13,12,12,13,13,13) ACHIEVABLE(Row(5),Squares(c,n,c,n,n,c,c,c)). new given clause: 210 (158,6) ACHIEVABLE(Row(4),Squares(n,n,n,c,n,c,c,n)). ** KEPT: 266 (210,1) ACHIEVABLE(Row(4),Squares(c,c,n,c,n,c,c,n)). new given clause: 211 (158,1) ACHIEVABLE(Row(4),Squares(c,c,n,c,n,n,n,n)). ** KEPT: 267 (211,8,18,12,12,13,12,13,13,13,13) ACHIEVABLE(Row(5),Squares(n,n,c,n,c,c,c,c)). new given clause: 212 (159,3) ACHIEVABLE(Row(4),Squares(n,n,c,c,n,c,n,n)). ** KEPT: 268 (212,8,18,13,13,12,12,13,12,13,13) ACHIEVABLE(Row(5),Squares(c,c,n,n,c,n,c,c)). ** KEPT: 269 (212,1) ACHIEVABLE(Row(4),Squares(c,c,c,c,n,c,n,n)). new given clause: 213 (159,1) ACHIEVABLE(Row(4),Squares(c,c,n,n,n,c,n,n)). ** KEPT: 270 (213,8,18,12,12,13,13,13,12,13,13) ACHIEVABLE(Row(5),Squares(n,n,c,c,c,n,c,c)). new given clause: 214 (160,8,18,12,12,13,12,12,12,13,13) ACHIEVABLE(Row(5),Squares(n,n,c,n,n,n,c,c)). new given clause: 215 (161,8,18,13,12,12,13,12,12,13,12) ACHIEVABLE(Row(5),Squares(c,n,n,c,n,n,c,n)). ** KEPT: 271 (215,2) ACHIEVABLE(Row(5),Squares(c,c,c,c,n,n,c,n)). new given clause: 216 (162,5) ACHIEVABLE(Row(4),Squares(n,n,n,n,c,c,n,c)). ** KEPT: 272 (216,3) ACHIEVABLE(Row(4),Squares(n,n,c,c,c,c,n,c)). ** KEPT: 273 (216,1) ACHIEVABLE(Row(4),Squares(c,c,n,n,c,c,n,c)). new given clause: 217 (162,3) ACHIEVABLE(Row(4),Squares(n,n,c,c,n,n,n,c)). ** KEPT: 274 (217,8,18,13,13,12,12,13,13,13,12) ACHIEVABLE(Row(5),Squares(c,c,n,n,c,c,c,n)). ** KEPT: 275 (217,1) ACHIEVABLE(Row(4),Squares(c,c,c,c,n,n,n,c)). new given clause: 218 (162,1) ACHIEVABLE(Row(4),Squares(c,c,n,n,n,n,n,c)). ** KEPT: 276 (218,8,18,12,12,13,13,13,13,13,12) ACHIEVABLE(Row(5),Squares(n,n,c,c,c,c,c,n)). new given clause: 219 (163,8,18,12,12,13,12,12,13,13,12) ACHIEVABLE(Row(5),Squares(n,n,c,n,n,c,c,n)). new given clause: 220 (164,8,18,13,12,13,12,12,13,12,12) ACHIEVABLE(Row(5),Squares(c,n,c,n,n,c,n,n)). new given clause: 221 (165,8,18,12,12,13,12,13,13,12,12) ACHIEVABLE(Row(5),Squares(n,n,c,n,c,c,n,n)). new given clause: 222 (166,8,18,13,13,12,12,13,12,12,12) ACHIEVABLE(Row(5),Squares(c,c,n,n,c,n,n,n)). new given clause: 223 (166,1) ACHIEVABLE(Row(4),Squares(c,c,c,c,n,c,c,c)). ** KEPT: 277 (223,8,18,12,12,12,12,13,12,12,12) ACHIEVABLE(Row(5),Squares(n,n,n,n,c,n,n,n)). new given clause: 224 (167,8,18,12,12,13,13,13,12,12,12) ACHIEVABLE(Row(5),Squares(n,n,c,c,c,n,n,n)). new given clause: 225 (171,8,16,13,12,13,12,12,12,12,13) ACHIEVABLE(Row(3),Squares(c,n,c,n,n,n,n,c)). ** KEPT: 278 (225,5) ACHIEVABLE(Row(3),Squares(c,n,c,n,c,c,n,c)). new given clause: 226 (173,8,16,12,12,13,12,13,12,12,13) ACHIEVABLE(Row(3),Squares(n,n,c,n,c,n,n,c)). new given clause: 227 (176,8,16,12,12,12,12,13,12,13,13) ACHIEVABLE(Row(3),Squares(n,n,n,n,c,n,c,c)). ** KEPT: 279 (227,2) ACHIEVABLE(Row(3),Squares(n,c,c,n,c,n,c,c)). new given clause: 228 (179,8,16,13,13,12,12,12,12,13,12) ACHIEVABLE(Row(3),Squares(c,c,n,n,n,n,c,n)). ** KEPT: 280 (228,4) ACHIEVABLE(Row(3),Squares(c,c,n,c,c,n,c,n)). new given clause: 229 (179,1) ACHIEVABLE(Row(2),Squares(c,c,c,c,c,c,n,c)). ** KEPT: 281 (229,8,16,12,12,12,12,12,12,13,12) ACHIEVABLE(Row(3),Squares(n,n,n,n,n,n,c,n)). new given clause: 230 (180,8,16,12,12,13,13,12,12,13,12) ACHIEVABLE(Row(3),Squares(n,n,c,c,n,n,c,n)). new given clause: 231 (182,8,16,12,12,12,12,13,13,13,12) ACHIEVABLE(Row(3),Squares(n,n,n,n,c,c,c,n)). ** KEPT: 282 (231,2) ACHIEVABLE(Row(3),Squares(n,c,c,n,c,c,c,n)). new given clause: 232 (184,2) ACHIEVABLE(Row(3),Squares(n,c,c,n,c,n,n,n)). ** KEPT: 283 (232,8,17,13,12,12,13,12,13,13,13) ACHIEVABLE(Row(4),Squares(c,n,n,c,n,c,c,c)). new given clause: 233 (186,8,21,12,13,13,13,13,13,12,12) ACHIEVABLE(Row(8),Squares(n,c,c,c,c,c,n,n)). new given clause: 234 (186,5) ACHIEVABLE(Row(7),Squares(c,n,n,n,c,c,c,c)). ** KEPT: 284 (234,8,21,12,13,13,13,12,12,12,12) ACHIEVABLE(Row(8),Squares(n,c,c,c,n,n,n,n)). ** KEPT: 285 (234,3) ACHIEVABLE(Row(7),Squares(c,n,c,c,c,c,c,c)). ** KEPT: 286 (234,2) ACHIEVABLE(Row(7),Squares(c,c,c,n,c,c,c,c)). new given clause: 235 (186,4) ACHIEVABLE(Row(7),Squares(c,n,n,c,c,n,c,c)). ** KEPT: 287 (235,8,21,12,13,13,12,12,13,12,12) ACHIEVABLE(Row(8),Squares(n,c,c,n,n,c,n,n)). ** KEPT: 288 (235,2) ACHIEVABLE(Row(7),Squares(c,c,c,c,c,n,c,c)). new given clause: 236 (186,3) ACHIEVABLE(Row(7),Squares(c,n,c,c,n,n,c,c)). ** KEPT: 289 (236,8,21,12,13,12,12,13,13,12,12) ACHIEVABLE(Row(8),Squares(n,c,n,n,c,c,n,n)). new given clause: 237 (186,2) ACHIEVABLE(Row(7),Squares(c,c,c,n,n,n,c,c)). ** KEPT: 290 (237,8,21,12,12,12,13,13,13,12,12) ACHIEVABLE(Row(8),Squares(n,n,n,c,c,c,n,n)). new given clause: 238 (187,8,21,12,13,13,13,13,12,12,13) ACHIEVABLE(Row(8),Squares(n,c,c,c,c,n,n,c)). new given clause: 239 (187,4) ACHIEVABLE(Row(7),Squares(c,n,n,c,c,c,c,n)). ** KEPT: 291 (239,8,21,12,13,13,12,12,12,12,13) ACHIEVABLE(Row(8),Squares(n,c,c,n,n,n,n,c)). ** KEPT: 292 (239,2) ACHIEVABLE(Row(7),Squares(c,c,c,c,c,c,c,n)). new given clause: 240 (187,3) ACHIEVABLE(Row(7),Squares(c,n,c,c,n,c,c,n)). ** KEPT: 293 (240,8,21,12,13,12,12,13,12,12,13) ACHIEVABLE(Row(8),Squares(n,c,n,n,c,n,n,c)). new given clause: 241 (187,2) ACHIEVABLE(Row(7),Squares(c,c,c,n,n,c,c,n)). ** KEPT: 294 (241,8,21,12,12,12,13,13,12,12,13) ACHIEVABLE(Row(8),Squares(n,n,n,c,c,n,n,c)). new given clause: 242 (188,8,21,12,13,13,13,12,12,13,13) ACHIEVABLE(Row(8),Squares(n,c,c,c,n,n,c,c)). new given clause: 243 (188,3) ACHIEVABLE(Row(7),Squares(c,n,c,c,c,c,n,n)). ** KEPT: 295 (243,8,21,12,13,12,12,12,12,13,13) ACHIEVABLE(Row(8),Squares(n,c,n,n,n,n,c,c)). new given clause: 244 (188,2) ACHIEVABLE(Row(7),Squares(c,c,c,n,c,c,n,n)). ** KEPT: 296 (244,8,21,12,12,12,13,12,12,13,13) ACHIEVABLE(Row(8),Squares(n,n,n,c,n,n,c,c)). new given clause: 245 (189,8,21,12,13,13,12,12,13,13,13) ACHIEVABLE(Row(8),Squares(n,c,c,n,n,c,c,c)). new given clause: 246 (189,2) ACHIEVABLE(Row(7),Squares(c,c,c,c,c,n,n,n)). ** KEPT: 297 (246,8,21,12,12,12,12,12,13,13,13) ACHIEVABLE(Row(8),Squares(n,n,n,n,n,c,c,c)). new given clause: 247 (190,8,21,12,13,12,12,13,13,13,13) ACHIEVABLE(Row(8),Squares(n,c,n,n,c,c,c,c)). new given clause: 248 (191,8,21,12,12,12,13,13,13,13,13) ACHIEVABLE(Row(8),Squares(n,n,n,c,c,c,c,c)). ** KEPT: 298 (248,1) ACHIEVABLE(Row(8),Squares(c,c,n,c,c,c,c,c)). new given clause: 249 (192,6) ACHIEVABLE(Row(6),Squares(n,c,c,c,n,c,c,n)). ** KEPT: 299 (249,8,20,13,12,12,12,13,12,12,13) ACHIEVABLE(Row(7),Squares(c,n,n,n,c,n,n,c)). new given clause: 250 (193,8,19,12,13,12,12,12,12,12,12) ACHIEVABLE(Row(6),Squares(n,c,n,n,n,n,n,n)). ** KEPT: 300 (250,6) ACHIEVABLE(Row(6),Squares(n,c,n,n,n,c,c,n)). ** KEPT: 301 (250,4) ACHIEVABLE(Row(6),Squares(n,c,n,c,c,n,n,n)). new given clause: 251 (194,8,19,12,12,12,13,12,12,12,12) ACHIEVABLE(Row(6),Squares(n,n,n,c,n,n,n,n)). ** KEPT: 302 (251,6) ACHIEVABLE(Row(6),Squares(n,n,n,c,n,c,c,n)). ** KEPT: 303 (251,1) ACHIEVABLE(Row(6),Squares(c,c,n,c,n,n,n,n)). new given clause: 252 (196,8,19,12,12,12,12,12,13,12,12) ACHIEVABLE(Row(6),Squares(n,n,n,n,n,c,n,n)). ** KEPT: 304 (252,3) ACHIEVABLE(Row(6),Squares(n,n,c,c,n,c,n,n)). ** KEPT: 305 (252,1) ACHIEVABLE(Row(6),Squares(c,c,n,n,n,c,n,n)). new given clause: 253 (198,1) ACHIEVABLE(Row(6),Squares(c,c,n,c,c,c,n,n)). ** KEPT: 306 (253,8,20,12,12,13,12,12,12,13,13) ACHIEVABLE(Row(7),Squares(n,n,c,n,n,n,c,c)). new given clause: 254 (199,5) ACHIEVABLE(Row(6),Squares(n,c,c,n,c,c,n,c)). ** KEPT: 307 (254,8,20,13,12,12,13,12,12,13,12) ACHIEVABLE(Row(7),Squares(c,n,n,c,n,n,c,n)). new given clause: 255 (200,8,19,12,12,12,12,12,12,12,13) ACHIEVABLE(Row(6),Squares(n,n,n,n,n,n,n,c)). ** KEPT: 308 (255,5) ACHIEVABLE(Row(6),Squares(n,n,n,n,c,c,n,c)). ** KEPT: 309 (255,3) ACHIEVABLE(Row(6),Squares(n,n,c,c,n,n,n,c)). ** KEPT: 310 (255,1) ACHIEVABLE(Row(6),Squares(c,c,n,n,n,n,n,c)). new given clause: 256 (202,1) ACHIEVABLE(Row(6),Squares(c,c,n,c,c,n,n,c)). ** KEPT: 311 (256,8,20,12,12,13,12,12,13,13,12) ACHIEVABLE(Row(7),Squares(n,n,c,n,n,c,c,n)). new given clause: 257 (203,4) ACHIEVABLE(Row(6),Squares(n,c,n,c,c,n,c,c)). ** KEPT: 312 (257,8,20,13,12,13,12,12,13,12,12) ACHIEVABLE(Row(7),Squares(c,n,c,n,n,c,n,n)). new given clause: 258 (204,1) ACHIEVABLE(Row(6),Squares(c,c,n,c,n,n,c,c)). ** KEPT: 313 (258,8,20,12,12,13,12,13,13,12,12) ACHIEVABLE(Row(7),Squares(n,n,c,n,c,c,n,n)). new given clause: 259 (205,3) ACHIEVABLE(Row(6),Squares(n,n,c,c,n,c,c,c)). ** KEPT: 314 (259,8,20,13,13,12,12,13,12,12,12) ACHIEVABLE(Row(7),Squares(c,c,n,n,c,n,n,n)). ** KEPT: 315 (259,1) ACHIEVABLE(Row(6),Squares(c,c,c,c,n,c,c,c)). new given clause: 260 (205,1) ACHIEVABLE(Row(6),Squares(c,c,n,n,n,c,c,c)). ** KEPT: 316 (260,8,20,12,12,13,13,13,12,12,12) ACHIEVABLE(Row(7),Squares(n,n,c,c,c,n,n,n)). new given clause: 261 (206,8,20,12,12,13,12,12,12,12,12) ACHIEVABLE(Row(7),Squares(n,n,c,n,n,n,n,n)). new given clause: 262 (207,3) ACHIEVABLE(Row(5),Squares(c,n,c,c,c,n,n,c)). new given clause: 263 (207,2) ACHIEVABLE(Row(5),Squares(c,c,c,n,c,n,n,c)). new given clause: 264 (208,4) ACHIEVABLE(Row(4),Squares(n,c,n,c,c,c,c,n)). ** KEPT: 317 (264,8,18,13,12,13,12,12,12,12,13) ACHIEVABLE(Row(5),Squares(c,n,c,n,n,n,n,c)). new given clause: 265 (209,8,18,13,12,13,12,12,13,13,13) ACHIEVABLE(Row(5),Squares(c,n,c,n,n,c,c,c)). new given clause: 266 (210,1) ACHIEVABLE(Row(4),Squares(c,c,n,c,n,c,c,n)). ** KEPT: 318 (266,8,18,12,12,13,12,13,12,12,13) ACHIEVABLE(Row(5),Squares(n,n,c,n,c,n,n,c)). new given clause: 267 (211,8,18,12,12,13,12,13,13,13,13) ACHIEVABLE(Row(5),Squares(n,n,c,n,c,c,c,c)). new given clause: 268 (212,8,18,13,13,12,12,13,12,13,13) ACHIEVABLE(Row(5),Squares(c,c,n,n,c,n,c,c)). new given clause: 269 (212,1) ACHIEVABLE(Row(4),Squares(c,c,c,c,n,c,n,n)). ** KEPT: 319 (269,8,18,12,12,12,12,13,12,13,13) ACHIEVABLE(Row(5),Squares(n,n,n,n,c,n,c,c)). new given clause: 270 (213,8,18,12,12,13,13,13,12,13,13) ACHIEVABLE(Row(5),Squares(n,n,c,c,c,n,c,c)). new given clause: 271 (215,2) ACHIEVABLE(Row(5),Squares(c,c,c,c,n,n,c,n)). new given clause: 272 (216,3) ACHIEVABLE(Row(4),Squares(n,n,c,c,c,c,n,c)). ** KEPT: 320 (272,8,18,13,13,12,12,12,12,13,12) ACHIEVABLE(Row(5),Squares(c,c,n,n,n,n,c,n)). ** KEPT: 321 (272,1) ACHIEVABLE(Row(4),Squares(c,c,c,c,c,c,n,c)). new given clause: 273 (216,1) ACHIEVABLE(Row(4),Squares(c,c,n,n,c,c,n,c)). ** KEPT: 322 (273,8,18,12,12,13,13,12,12,13,12) ACHIEVABLE(Row(5),Squares(n,n,c,c,n,n,c,n)). new given clause: 274 (217,8,18,13,13,12,12,13,13,13,12) ACHIEVABLE(Row(5),Squares(c,c,n,n,c,c,c,n)). new given clause: 275 (217,1) ACHIEVABLE(Row(4),Squares(c,c,c,c,n,n,n,c)). ** KEPT: 323 (275,8,18,12,12,12,12,13,13,13,12) ACHIEVABLE(Row(5),Squares(n,n,n,n,c,c,c,n)). new given clause: 276 (218,8,18,12,12,13,13,13,13,13,12) ACHIEVABLE(Row(5),Squares(n,n,c,c,c,c,c,n)). new given clause: 277 (223,8,18,12,12,12,12,13,12,12,12) ACHIEVABLE(Row(5),Squares(n,n,n,n,c,n,n,n)). ** KEPT: 324 (277,2) ACHIEVABLE(Row(5),Squares(n,c,c,n,c,n,n,n)). new given clause: 278 (225,5) ACHIEVABLE(Row(3),Squares(c,n,c,n,c,c,n,c)). ** KEPT: 325 (278,8,17,12,13,12,13,12,12,13,12) ACHIEVABLE(Row(4),Squares(n,c,n,c,n,n,c,n)). new given clause: 279 (227,2) ACHIEVABLE(Row(3),Squares(n,c,c,n,c,n,c,c)). ** KEPT: 326 (279,8,17,13,12,12,13,12,13,12,12) ACHIEVABLE(Row(4),Squares(c,n,n,c,n,c,n,n)). new given clause: 280 (228,4) ACHIEVABLE(Row(3),Squares(c,c,n,c,c,n,c,n)). ** KEPT: 327 (280,8,17,12,12,13,12,12,13,12,13) ACHIEVABLE(Row(4),Squares(n,n,c,n,n,c,n,c)). new given clause: 281 (229,8,16,12,12,12,12,12,12,13,12) ACHIEVABLE(Row(3),Squares(n,n,n,n,n,n,c,n)). ** KEPT: 328 (281,4) ACHIEVABLE(Row(3),Squares(n,n,n,c,c,n,c,n)). ** KEPT: 329 (281,2) ACHIEVABLE(Row(3),Squares(n,c,c,n,n,n,c,n)). new given clause: 282 (231,2) ACHIEVABLE(Row(3),Squares(n,c,c,n,c,c,c,n)). ** KEPT: 330 (282,8,17,13,12,12,13,12,12,12,13) ACHIEVABLE(Row(4),Squares(c,n,n,c,n,n,n,c)). new given clause: 283 (232,8,17,13,12,12,13,12,13,13,13) ACHIEVABLE(Row(4),Squares(c,n,n,c,n,c,c,c)). new given clause: 284 (234,8,21,12,13,13,13,12,12,12,12) ACHIEVABLE(Row(8),Squares(n,c,c,c,n,n,n,n)). ** KEPT: 331 (284,6) ACHIEVABLE(Row(8),Squares(n,c,c,c,n,c,c,n)). new given clause: 285 (234,3) ACHIEVABLE(Row(7),Squares(c,n,c,c,c,c,c,c)). ** KEPT: 332 (285,8,21,12,13,12,12,12,12,12,12) ACHIEVABLE(Row(8),Squares(n,c,n,n,n,n,n,n)). new given clause: 286 (234,2) ACHIEVABLE(Row(7),Squares(c,c,c,n,c,c,c,c)). ** KEPT: 333 (286,8,21,12,12,12,13,12,12,12,12) ACHIEVABLE(Row(8),Squares(n,n,n,c,n,n,n,n)). new given clause: 287 (235,8,21,12,13,13,12,12,13,12,12) ACHIEVABLE(Row(8),Squares(n,c,c,n,n,c,n,n)). new given clause: 288 (235,2) ACHIEVABLE(Row(7),Squares(c,c,c,c,c,n,c,c)). ** KEPT: 334 (288,8,21,12,12,12,12,12,13,12,12) ACHIEVABLE(Row(8),Squares(n,n,n,n,n,c,n,n)). new given clause: 289 (236,8,21,12,13,12,12,13,13,12,12) ACHIEVABLE(Row(8),Squares(n,c,n,n,c,c,n,n)). new given clause: 290 (237,8,21,12,12,12,13,13,13,12,12) ACHIEVABLE(Row(8),Squares(n,n,n,c,c,c,n,n)). ** KEPT: 335 (290,1) ACHIEVABLE(Row(8),Squares(c,c,n,c,c,c,n,n)). new given clause: 291 (239,8,21,12,13,13,12,12,12,12,13) ACHIEVABLE(Row(8),Squares(n,c,c,n,n,n,n,c)). ** KEPT: 336 (291,5) ACHIEVABLE(Row(8),Squares(n,c,c,n,c,c,n,c)). new given clause: 292 (239,2) ACHIEVABLE(Row(7),Squares(c,c,c,c,c,c,c,n)). ** KEPT: 337 (292,8,21,12,12,12,12,12,12,12,13) ACHIEVABLE(Row(8),Squares(n,n,n,n,n,n,n,c)). new given clause: 293 (240,8,21,12,13,12,12,13,12,12,13) ACHIEVABLE(Row(8),Squares(n,c,n,n,c,n,n,c)). new given clause: 294 (241,8,21,12,12,12,13,13,12,12,13) ACHIEVABLE(Row(8),Squares(n,n,n,c,c,n,n,c)). ** KEPT: 338 (294,1) ACHIEVABLE(Row(8),Squares(c,c,n,c,c,n,n,c)). new given clause: 295 (243,8,21,12,13,12,12,12,12,13,13) ACHIEVABLE(Row(8),Squares(n,c,n,n,n,n,c,c)). ** KEPT: 339 (295,4) ACHIEVABLE(Row(8),Squares(n,c,n,c,c,n,c,c)). new given clause: 296 (244,8,21,12,12,12,13,12,12,13,13) ACHIEVABLE(Row(8),Squares(n,n,n,c,n,n,c,c)). ** KEPT: 340 (296,1) ACHIEVABLE(Row(8),Squares(c,c,n,c,n,n,c,c)). new given clause: 297 (246,8,21,12,12,12,12,12,13,13,13) ACHIEVABLE(Row(8),Squares(n,n,n,n,n,c,c,c)). ** KEPT: 341 (297,3) ACHIEVABLE(Row(8),Squares(n,n,c,c,n,c,c,c)). ** KEPT: 342 (297,1) ACHIEVABLE(Row(8),Squares(c,c,n,n,n,c,c,c)). new given clause: 298 (248,1) ACHIEVABLE(Row(8),Squares(c,c,n,c,c,c,c,c)). new given clause: 299 (249,8,20,13,12,12,12,13,12,12,13) ACHIEVABLE(Row(7),Squares(c,n,n,n,c,n,n,c)). ** KEPT: 343 (299,3) ACHIEVABLE(Row(7),Squares(c,n,c,c,c,n,n,c)). ** KEPT: 344 (299,2) ACHIEVABLE(Row(7),Squares(c,c,c,n,c,n,n,c)). new given clause: 300 (250,6) ACHIEVABLE(Row(6),Squares(n,c,n,n,n,c,c,n)). ** KEPT: 345 (300,4) ACHIEVABLE(Row(6),Squares(n,c,n,c,c,c,c,n)). new given clause: 301 (250,4) ACHIEVABLE(Row(6),Squares(n,c,n,c,c,n,n,n)). ** KEPT: 346 (301,8,20,13,12,13,12,12,13,13,13) ACHIEVABLE(Row(7),Squares(c,n,c,n,n,c,c,c)). new given clause: 302 (251,6) ACHIEVABLE(Row(6),Squares(n,n,n,c,n,c,c,n)). ** KEPT: 347 (302,1) ACHIEVABLE(Row(6),Squares(c,c,n,c,n,c,c,n)). new given clause: 303 (251,1) ACHIEVABLE(Row(6),Squares(c,c,n,c,n,n,n,n)). ** KEPT: 348 (303,8,20,12,12,13,12,13,13,13,13) ACHIEVABLE(Row(7),Squares(n,n,c,n,c,c,c,c)). new given clause: 304 (252,3) ACHIEVABLE(Row(6),Squares(n,n,c,c,n,c,n,n)). ** KEPT: 349 (304,8,20,13,13,12,12,13,12,13,13) ACHIEVABLE(Row(7),Squares(c,c,n,n,c,n,c,c)). ** KEPT: 350 (304,1) ACHIEVABLE(Row(6),Squares(c,c,c,c,n,c,n,n)). new given clause: 305 (252,1) ACHIEVABLE(Row(6),Squares(c,c,n,n,n,c,n,n)). ** KEPT: 351 (305,8,20,12,12,13,13,13,12,13,13) ACHIEVABLE(Row(7),Squares(n,n,c,c,c,n,c,c)). new given clause: 306 (253,8,20,12,12,13,12,12,12,13,13) ACHIEVABLE(Row(7),Squares(n,n,c,n,n,n,c,c)). new given clause: 307 (254,8,20,13,12,12,13,12,12,13,12) ACHIEVABLE(Row(7),Squares(c,n,n,c,n,n,c,n)). ** KEPT: 352 (307,2) ACHIEVABLE(Row(7),Squares(c,c,c,c,n,n,c,n)). new given clause: 308 (255,5) ACHIEVABLE(Row(6),Squares(n,n,n,n,c,c,n,c)). ** KEPT: 353 (308,3) ACHIEVABLE(Row(6),Squares(n,n,c,c,c,c,n,c)). ** KEPT: 354 (308,1) ACHIEVABLE(Row(6),Squares(c,c,n,n,c,c,n,c)). new given clause: 309 (255,3) ACHIEVABLE(Row(6),Squares(n,n,c,c,n,n,n,c)). ** KEPT: 355 (309,8,20,13,13,12,12,13,13,13,12) ACHIEVABLE(Row(7),Squares(c,c,n,n,c,c,c,n)). ** KEPT: 356 (309,1) ACHIEVABLE(Row(6),Squares(c,c,c,c,n,n,n,c)). new given clause: 310 (255,1) ACHIEVABLE(Row(6),Squares(c,c,n,n,n,n,n,c)). ** KEPT: 357 (310,8,20,12,12,13,13,13,13,13,12) ACHIEVABLE(Row(7),Squares(n,n,c,c,c,c,c,n)). new given clause: 311 (256,8,20,12,12,13,12,12,13,13,12) ACHIEVABLE(Row(7),Squares(n,n,c,n,n,c,c,n)). new given clause: 312 (257,8,20,13,12,13,12,12,13,12,12) ACHIEVABLE(Row(7),Squares(c,n,c,n,n,c,n,n)). new given clause: 313 (258,8,20,12,12,13,12,13,13,12,12) ACHIEVABLE(Row(7),Squares(n,n,c,n,c,c,n,n)). new given clause: 314 (259,8,20,13,13,12,12,13,12,12,12) ACHIEVABLE(Row(7),Squares(c,c,n,n,c,n,n,n)). new given clause: 315 (259,1) ACHIEVABLE(Row(6),Squares(c,c,c,c,n,c,c,c)). ** KEPT: 358 (315,8,20,12,12,12,12,13,12,12,12) ACHIEVABLE(Row(7),Squares(n,n,n,n,c,n,n,n)). new given clause: 316 (260,8,20,12,12,13,13,13,12,12,12) ACHIEVABLE(Row(7),Squares(n,n,c,c,c,n,n,n)). new given clause: 317 (264,8,18,13,12,13,12,12,12,12,13) ACHIEVABLE(Row(5),Squares(c,n,c,n,n,n,n,c)). ** KEPT: 359 (317,5) ACHIEVABLE(Row(5),Squares(c,n,c,n,c,c,n,c)). new given clause: 318 (266,8,18,12,12,13,12,13,12,12,13) ACHIEVABLE(Row(5),Squares(n,n,c,n,c,n,n,c)). new given clause: 319 (269,8,18,12,12,12,12,13,12,13,13) ACHIEVABLE(Row(5),Squares(n,n,n,n,c,n,c,c)). ** KEPT: 360 (319,2) ACHIEVABLE(Row(5),Squares(n,c,c,n,c,n,c,c)). new given clause: 320 (272,8,18,13,13,12,12,12,12,13,12) ACHIEVABLE(Row(5),Squares(c,c,n,n,n,n,c,n)). ** KEPT: 361 (320,4) ACHIEVABLE(Row(5),Squares(c,c,n,c,c,n,c,n)). new given clause: 321 (272,1) ACHIEVABLE(Row(4),Squares(c,c,c,c,c,c,n,c)). ** KEPT: 362 (321,8,18,12,12,12,12,12,12,13,12) ACHIEVABLE(Row(5),Squares(n,n,n,n,n,n,c,n)). new given clause: 322 (273,8,18,12,12,13,13,12,12,13,12) ACHIEVABLE(Row(5),Squares(n,n,c,c,n,n,c,n)). new given clause: 323 (275,8,18,12,12,12,12,13,13,13,12) ACHIEVABLE(Row(5),Squares(n,n,n,n,c,c,c,n)). ** KEPT: 363 (323,2) ACHIEVABLE(Row(5),Squares(n,c,c,n,c,c,c,n)). new given clause: 324 (277,2) ACHIEVABLE(Row(5),Squares(n,c,c,n,c,n,n,n)). ** KEPT: 364 (324,8,19,13,12,12,13,12,13,13,13) ACHIEVABLE(Row(6),Squares(c,n,n,c,n,c,c,c)). new given clause: 325 (278,8,17,12,13,12,13,12,12,13,12) ACHIEVABLE(Row(4),Squares(n,c,n,c,n,n,c,n)). new given clause: 326 (279,8,17,13,12,12,13,12,13,12,12) ACHIEVABLE(Row(4),Squares(c,n,n,c,n,c,n,n)). new given clause: 327 (280,8,17,12,12,13,12,12,13,12,13) ACHIEVABLE(Row(4),Squares(n,n,c,n,n,c,n,c)). ** KEPT: 365 (327,1) ACHIEVABLE(Row(4),Squares(c,c,c,n,n,c,n,c)). new given clause: 328 (281,4) ACHIEVABLE(Row(3),Squares(n,n,n,c,c,n,c,n)). ** KEPT: 366 (328,2) ACHIEVABLE(Row(3),Squares(n,c,c,c,c,n,c,n)). new given clause: 329 (281,2) ACHIEVABLE(Row(3),Squares(n,c,c,n,n,n,c,n)). ** KEPT: 367 (329,8,17,13,12,12,13,13,13,12,13) ACHIEVABLE(Row(4),Squares(c,n,n,c,c,c,n,c)). new given clause: 330 (282,8,17,13,12,12,13,12,12,12,13) ACHIEVABLE(Row(4),Squares(c,n,n,c,n,n,n,c)). new given clause: 331 (284,6) ACHIEVABLE(Row(8),Squares(n,c,c,c,n,c,c,n)). new given clause: 332 (285,8,21,12,13,12,12,12,12,12,12) ACHIEVABLE(Row(8),Squares(n,c,n,n,n,n,n,n)). ** KEPT: 368 (332,6) ACHIEVABLE(Row(8),Squares(n,c,n,n,n,c,c,n)). ** KEPT: 369 (332,4) ACHIEVABLE(Row(8),Squares(n,c,n,c,c,n,n,n)). new given clause: 333 (286,8,21,12,12,12,13,12,12,12,12) ACHIEVABLE(Row(8),Squares(n,n,n,c,n,n,n,n)). ** KEPT: 370 (333,6) ACHIEVABLE(Row(8),Squares(n,n,n,c,n,c,c,n)). ** KEPT: 371 (333,1) ACHIEVABLE(Row(8),Squares(c,c,n,c,n,n,n,n)). new given clause: 334 (288,8,21,12,12,12,12,12,13,12,12) ACHIEVABLE(Row(8),Squares(n,n,n,n,n,c,n,n)). ** KEPT: 372 (334,3) ACHIEVABLE(Row(8),Squares(n,n,c,c,n,c,n,n)). ** KEPT: 373 (334,1) ACHIEVABLE(Row(8),Squares(c,c,n,n,n,c,n,n)). new given clause: 335 (290,1) ACHIEVABLE(Row(8),Squares(c,c,n,c,c,c,n,n)). new given clause: 336 (291,5) ACHIEVABLE(Row(8),Squares(n,c,c,n,c,c,n,c)). new given clause: 337 (292,8,21,12,12,12,12,12,12,12,13) ACHIEVABLE(Row(8),Squares(n,n,n,n,n,n,n,c)). ** KEPT: 374 (337,5) ACHIEVABLE(Row(8),Squares(n,n,n,n,c,c,n,c)). ** KEPT: 375 (337,3) ACHIEVABLE(Row(8),Squares(n,n,c,c,n,n,n,c)). ** KEPT: 376 (337,1) ACHIEVABLE(Row(8),Squares(c,c,n,n,n,n,n,c)). new given clause: 338 (294,1) ACHIEVABLE(Row(8),Squares(c,c,n,c,c,n,n,c)). new given clause: 339 (295,4) ACHIEVABLE(Row(8),Squares(n,c,n,c,c,n,c,c)). new given clause: 340 (296,1) ACHIEVABLE(Row(8),Squares(c,c,n,c,n,n,c,c)). new given clause: 341 (297,3) ACHIEVABLE(Row(8),Squares(n,n,c,c,n,c,c,c)). ** KEPT: 377 (341,1) ACHIEVABLE(Row(8),Squares(c,c,c,c,n,c,c,c)). new given clause: 342 (297,1) ACHIEVABLE(Row(8),Squares(c,c,n,n,n,c,c,c)). new given clause: 343 (299,3) ACHIEVABLE(Row(7),Squares(c,n,c,c,c,n,n,c)). new given clause: 344 (299,2) ACHIEVABLE(Row(7),Squares(c,c,c,n,c,n,n,c)). new given clause: 345 (300,4) ACHIEVABLE(Row(6),Squares(n,c,n,c,c,c,c,n)). ** KEPT: 378 (345,8,20,13,12,13,12,12,12,12,13) ACHIEVABLE(Row(7),Squares(c,n,c,n,n,n,n,c)). new given clause: 346 (301,8,20,13,12,13,12,12,13,13,13) ACHIEVABLE(Row(7),Squares(c,n,c,n,n,c,c,c)). new given clause: 347 (302,1) ACHIEVABLE(Row(6),Squares(c,c,n,c,n,c,c,n)). ** KEPT: 379 (347,8,20,12,12,13,12,13,12,12,13) ACHIEVABLE(Row(7),Squares(n,n,c,n,c,n,n,c)). new given clause: 348 (303,8,20,12,12,13,12,13,13,13,13) ACHIEVABLE(Row(7),Squares(n,n,c,n,c,c,c,c)). new given clause: 349 (304,8,20,13,13,12,12,13,12,13,13) ACHIEVABLE(Row(7),Squares(c,c,n,n,c,n,c,c)). new given clause: 350 (304,1) ACHIEVABLE(Row(6),Squares(c,c,c,c,n,c,n,n)). ** KEPT: 380 (350,8,20,12,12,12,12,13,12,13,13) ACHIEVABLE(Row(7),Squares(n,n,n,n,c,n,c,c)). new given clause: 351 (305,8,20,12,12,13,13,13,12,13,13) ACHIEVABLE(Row(7),Squares(n,n,c,c,c,n,c,c)). new given clause: 352 (307,2) ACHIEVABLE(Row(7),Squares(c,c,c,c,n,n,c,n)). new given clause: 353 (308,3) ACHIEVABLE(Row(6),Squares(n,n,c,c,c,c,n,c)). ** KEPT: 381 (353,8,20,13,13,12,12,12,12,13,12) ACHIEVABLE(Row(7),Squares(c,c,n,n,n,n,c,n)). ** KEPT: 382 (353,1) ACHIEVABLE(Row(6),Squares(c,c,c,c,c,c,n,c)). new given clause: 354 (308,1) ACHIEVABLE(Row(6),Squares(c,c,n,n,c,c,n,c)). ** KEPT: 383 (354,8,20,12,12,13,13,12,12,13,12) ACHIEVABLE(Row(7),Squares(n,n,c,c,n,n,c,n)). new given clause: 355 (309,8,20,13,13,12,12,13,13,13,12) ACHIEVABLE(Row(7),Squares(c,c,n,n,c,c,c,n)). new given clause: 356 (309,1) ACHIEVABLE(Row(6),Squares(c,c,c,c,n,n,n,c)). ** KEPT: 384 (356,8,20,12,12,12,12,13,13,13,12) ACHIEVABLE(Row(7),Squares(n,n,n,n,c,c,c,n)). new given clause: 357 (310,8,20,12,12,13,13,13,13,13,12) ACHIEVABLE(Row(7),Squares(n,n,c,c,c,c,c,n)). new given clause: 358 (315,8,20,12,12,12,12,13,12,12,12) ACHIEVABLE(Row(7),Squares(n,n,n,n,c,n,n,n)). ** KEPT: 385 (358,2) ACHIEVABLE(Row(7),Squares(n,c,c,n,c,n,n,n)). new given clause: 359 (317,5) ACHIEVABLE(Row(5),Squares(c,n,c,n,c,c,n,c)). ** KEPT: 386 (359,8,19,12,13,12,13,12,12,13,12) ACHIEVABLE(Row(6),Squares(n,c,n,c,n,n,c,n)). new given clause: 360 (319,2) ACHIEVABLE(Row(5),Squares(n,c,c,n,c,n,c,c)). ** KEPT: 387 (360,8,19,13,12,12,13,12,13,12,12) ACHIEVABLE(Row(6),Squares(c,n,n,c,n,c,n,n)). new given clause: 361 (320,4) ACHIEVABLE(Row(5),Squares(c,c,n,c,c,n,c,n)). ** KEPT: 388 (361,8,19,12,12,13,12,12,13,12,13) ACHIEVABLE(Row(6),Squares(n,n,c,n,n,c,n,c)). new given clause: 362 (321,8,18,12,12,12,12,12,12,13,12) ACHIEVABLE(Row(5),Squares(n,n,n,n,n,n,c,n)). ** KEPT: 389 (362,4) ACHIEVABLE(Row(5),Squares(n,n,n,c,c,n,c,n)). ** KEPT: 390 (362,2) ACHIEVABLE(Row(5),Squares(n,c,c,n,n,n,c,n)). new given clause: 363 (323,2) ACHIEVABLE(Row(5),Squares(n,c,c,n,c,c,c,n)). ** KEPT: 391 (363,8,19,13,12,12,13,12,12,12,13) ACHIEVABLE(Row(6),Squares(c,n,n,c,n,n,n,c)). new given clause: 364 (324,8,19,13,12,12,13,12,13,13,13) ACHIEVABLE(Row(6),Squares(c,n,n,c,n,c,c,c)). new given clause: 365 (327,1) ACHIEVABLE(Row(4),Squares(c,c,c,n,n,c,n,c)). new given clause: 366 (328,2) ACHIEVABLE(Row(3),Squares(n,c,c,c,c,n,c,n)). ** KEPT: 392 (366,8,17,13,12,12,12,12,13,12,13) ACHIEVABLE(Row(4),Squares(c,n,n,n,n,c,n,c)). new given clause: 367 (329,8,17,13,12,12,13,13,13,12,13) ACHIEVABLE(Row(4),Squares(c,n,n,c,c,c,n,c)). new given clause: 368 (332,6) ACHIEVABLE(Row(8),Squares(n,c,n,n,n,c,c,n)). ** KEPT: 393 (368,4) ACHIEVABLE(Row(8),Squares(n,c,n,c,c,c,c,n)). new given clause: 369 (332,4) ACHIEVABLE(Row(8),Squares(n,c,n,c,c,n,n,n)). new given clause: 370 (333,6) ACHIEVABLE(Row(8),Squares(n,n,n,c,n,c,c,n)). ** KEPT: 394 (370,1) ACHIEVABLE(Row(8),Squares(c,c,n,c,n,c,c,n)). new given clause: 371 (333,1) ACHIEVABLE(Row(8),Squares(c,c,n,c,n,n,n,n)). new given clause: 372 (334,3) ACHIEVABLE(Row(8),Squares(n,n,c,c,n,c,n,n)). ** KEPT: 395 (372,1) ACHIEVABLE(Row(8),Squares(c,c,c,c,n,c,n,n)). new given clause: 373 (334,1) ACHIEVABLE(Row(8),Squares(c,c,n,n,n,c,n,n)). new given clause: 374 (337,5) ACHIEVABLE(Row(8),Squares(n,n,n,n,c,c,n,c)). ** KEPT: 396 (374,3) ACHIEVABLE(Row(8),Squares(n,n,c,c,c,c,n,c)). ** KEPT: 397 (374,1) ACHIEVABLE(Row(8),Squares(c,c,n,n,c,c,n,c)). new given clause: 375 (337,3) ACHIEVABLE(Row(8),Squares(n,n,c,c,n,n,n,c)). ** KEPT: 398 (375,1) ACHIEVABLE(Row(8),Squares(c,c,c,c,n,n,n,c)). new given clause: 376 (337,1) ACHIEVABLE(Row(8),Squares(c,c,n,n,n,n,n,c)). new given clause: 377 (341,1) ACHIEVABLE(Row(8),Squares(c,c,c,c,n,c,c,c)). new given clause: 378 (345,8,20,13,12,13,12,12,12,12,13) ACHIEVABLE(Row(7),Squares(c,n,c,n,n,n,n,c)). ** KEPT: 399 (378,5) ACHIEVABLE(Row(7),Squares(c,n,c,n,c,c,n,c)). new given clause: 379 (347,8,20,12,12,13,12,13,12,12,13) ACHIEVABLE(Row(7),Squares(n,n,c,n,c,n,n,c)). new given clause: 380 (350,8,20,12,12,12,12,13,12,13,13) ACHIEVABLE(Row(7),Squares(n,n,n,n,c,n,c,c)). ** KEPT: 400 (380,2) ACHIEVABLE(Row(7),Squares(n,c,c,n,c,n,c,c)). new given clause: 381 (353,8,20,13,13,12,12,12,12,13,12) ACHIEVABLE(Row(7),Squares(c,c,n,n,n,n,c,n)). ** KEPT: 401 (381,4) ACHIEVABLE(Row(7),Squares(c,c,n,c,c,n,c,n)). new given clause: 382 (353,1) ACHIEVABLE(Row(6),Squares(c,c,c,c,c,c,n,c)). ** KEPT: 402 (382,8,20,12,12,12,12,12,12,13,12) ACHIEVABLE(Row(7),Squares(n,n,n,n,n,n,c,n)). new given clause: 383 (354,8,20,12,12,13,13,12,12,13,12) ACHIEVABLE(Row(7),Squares(n,n,c,c,n,n,c,n)). new given clause: 384 (356,8,20,12,12,12,12,13,13,13,12) ACHIEVABLE(Row(7),Squares(n,n,n,n,c,c,c,n)). ** KEPT: 403 (384,2) ACHIEVABLE(Row(7),Squares(n,c,c,n,c,c,c,n)). new given clause: 385 (358,2) ACHIEVABLE(Row(7),Squares(n,c,c,n,c,n,n,n)). ** KEPT: 404 (385,8,21,13,12,12,13,12,13,13,13) ACHIEVABLE(Row(8),Squares(c,n,n,c,n,c,c,c)). new given clause: 386 (359,8,19,12,13,12,13,12,12,13,12) ACHIEVABLE(Row(6),Squares(n,c,n,c,n,n,c,n)). new given clause: 387 (360,8,19,13,12,12,13,12,13,12,12) ACHIEVABLE(Row(6),Squares(c,n,n,c,n,c,n,n)). new given clause: 388 (361,8,19,12,12,13,12,12,13,12,13) ACHIEVABLE(Row(6),Squares(n,n,c,n,n,c,n,c)). ** KEPT: 405 (388,1) ACHIEVABLE(Row(6),Squares(c,c,c,n,n,c,n,c)). new given clause: 389 (362,4) ACHIEVABLE(Row(5),Squares(n,n,n,c,c,n,c,n)). ** KEPT: 406 (389,2) ACHIEVABLE(Row(5),Squares(n,c,c,c,c,n,c,n)). new given clause: 390 (362,2) ACHIEVABLE(Row(5),Squares(n,c,c,n,n,n,c,n)). ** KEPT: 407 (390,8,19,13,12,12,13,13,13,12,13) ACHIEVABLE(Row(6),Squares(c,n,n,c,c,c,n,c)). new given clause: 391 (363,8,19,13,12,12,13,12,12,12,13) ACHIEVABLE(Row(6),Squares(c,n,n,c,n,n,n,c)). new given clause: 392 (366,8,17,13,12,12,12,12,13,12,13) ACHIEVABLE(Row(4),Squares(c,n,n,n,n,c,n,c)). ** KEPT: 408 (392,3) ACHIEVABLE(Row(4),Squares(c,n,c,c,n,c,n,c)). new given clause: 393 (368,4) ACHIEVABLE(Row(8),Squares(n,c,n,c,c,c,c,n)). new given clause: 394 (370,1) ACHIEVABLE(Row(8),Squares(c,c,n,c,n,c,c,n)). new given clause: 395 (372,1) ACHIEVABLE(Row(8),Squares(c,c,c,c,n,c,n,n)). new given clause: 396 (374,3) ACHIEVABLE(Row(8),Squares(n,n,c,c,c,c,n,c)). ** KEPT: 409 (396,1) ACHIEVABLE(Row(8),Squares(c,c,c,c,c,c,n,c)). new given clause: 397 (374,1) ACHIEVABLE(Row(8),Squares(c,c,n,n,c,c,n,c)). new given clause: 398 (375,1) ACHIEVABLE(Row(8),Squares(c,c,c,c,n,n,n,c)). new given clause: 399 (378,5) ACHIEVABLE(Row(7),Squares(c,n,c,n,c,c,n,c)). ** KEPT: 410 (399,8,21,12,13,12,13,12,12,13,12) ACHIEVABLE(Row(8),Squares(n,c,n,c,n,n,c,n)). new given clause: 400 (380,2) ACHIEVABLE(Row(7),Squares(n,c,c,n,c,n,c,c)). ** KEPT: 411 (400,8,21,13,12,12,13,12,13,12,12) ACHIEVABLE(Row(8),Squares(c,n,n,c,n,c,n,n)). new given clause: 401 (381,4) ACHIEVABLE(Row(7),Squares(c,c,n,c,c,n,c,n)). ** KEPT: 412 (401,8,21,12,12,13,12,12,13,12,13) ACHIEVABLE(Row(8),Squares(n,n,c,n,n,c,n,c)). new given clause: 402 (382,8,20,12,12,12,12,12,12,13,12) ACHIEVABLE(Row(7),Squares(n,n,n,n,n,n,c,n)). ** KEPT: 413 (402,4) ACHIEVABLE(Row(7),Squares(n,n,n,c,c,n,c,n)). ** KEPT: 414 (402,2) ACHIEVABLE(Row(7),Squares(n,c,c,n,n,n,c,n)). new given clause: 403 (384,2) ACHIEVABLE(Row(7),Squares(n,c,c,n,c,c,c,n)). ** KEPT: 415 (403,8,21,13,12,12,13,12,12,12,13) ACHIEVABLE(Row(8),Squares(c,n,n,c,n,n,n,c)). new given clause: 404 (385,8,21,13,12,12,13,12,13,13,13) ACHIEVABLE(Row(8),Squares(c,n,n,c,n,c,c,c)). new given clause: 405 (388,1) ACHIEVABLE(Row(6),Squares(c,c,c,n,n,c,n,c)). new given clause: 406 (389,2) ACHIEVABLE(Row(5),Squares(n,c,c,c,c,n,c,n)). ** KEPT: 416 (406,8,19,13,12,12,12,12,13,12,13) ACHIEVABLE(Row(6),Squares(c,n,n,n,n,c,n,c)). new given clause: 407 (390,8,19,13,12,12,13,13,13,12,13) ACHIEVABLE(Row(6),Squares(c,n,n,c,c,c,n,c)). new given clause: 408 (392,3) ACHIEVABLE(Row(4),Squares(c,n,c,c,n,c,n,c)). ** KEPT: 417 (408,8,18,12,13,12,12,13,12,13,12) ACHIEVABLE(Row(5),Squares(n,c,n,n,c,n,c,n)). new given clause: 409 (396,1) ACHIEVABLE(Row(8),Squares(c,c,c,c,c,c,n,c)). new given clause: 410 (399,8,21,12,13,12,13,12,12,13,12) ACHIEVABLE(Row(8),Squares(n,c,n,c,n,n,c,n)). new given clause: 411 (400,8,21,13,12,12,13,12,13,12,12) ACHIEVABLE(Row(8),Squares(c,n,n,c,n,c,n,n)). new given clause: 412 (401,8,21,12,12,13,12,12,13,12,13) ACHIEVABLE(Row(8),Squares(n,n,c,n,n,c,n,c)). ** KEPT: 418 (412,1) ACHIEVABLE(Row(8),Squares(c,c,c,n,n,c,n,c)). new given clause: 413 (402,4) ACHIEVABLE(Row(7),Squares(n,n,n,c,c,n,c,n)). ** KEPT: 419 (413,2) ACHIEVABLE(Row(7),Squares(n,c,c,c,c,n,c,n)). new given clause: 414 (402,2) ACHIEVABLE(Row(7),Squares(n,c,c,n,n,n,c,n)). ** KEPT: 420 (414,8,21,13,12,12,13,13,13,12,13) ACHIEVABLE(Row(8),Squares(c,n,n,c,c,c,n,c)). new given clause: 415 (403,8,21,13,12,12,13,12,12,12,13) ACHIEVABLE(Row(8),Squares(c,n,n,c,n,n,n,c)). new given clause: 416 (406,8,19,13,12,12,12,12,13,12,13) ACHIEVABLE(Row(6),Squares(c,n,n,n,n,c,n,c)). ** KEPT: 421 (416,3) ACHIEVABLE(Row(6),Squares(c,n,c,c,n,c,n,c)). new given clause: 417 (408,8,18,12,13,12,12,13,12,13,12) ACHIEVABLE(Row(5),Squares(n,c,n,n,c,n,c,n)). new given clause: 418 (412,1) ACHIEVABLE(Row(8),Squares(c,c,c,n,n,c,n,c)). new given clause: 419 (413,2) ACHIEVABLE(Row(7),Squares(n,c,c,c,c,n,c,n)). ** KEPT: 422 (419,8,21,13,12,12,12,12,13,12,13) ACHIEVABLE(Row(8),Squares(c,n,n,n,n,c,n,c)). new given clause: 420 (414,8,21,13,12,12,13,13,13,12,13) ACHIEVABLE(Row(8),Squares(c,n,n,c,c,c,n,c)). new given clause: 421 (416,3) ACHIEVABLE(Row(6),Squares(c,n,c,c,n,c,n,c)). ** KEPT: 423 (421,8,20,12,13,12,12,13,12,13,12) ACHIEVABLE(Row(7),Squares(n,c,n,n,c,n,c,n)). new given clause: 422 (419,8,21,13,12,12,12,12,13,12,13) ACHIEVABLE(Row(8),Squares(c,n,n,n,n,c,n,c)). ** KEPT: 424 (422,3) ACHIEVABLE(Row(8),Squares(c,n,c,c,n,c,n,c)). new given clause: 423 (421,8,20,12,13,12,12,13,12,13,12) ACHIEVABLE(Row(7),Squares(n,c,n,n,c,n,c,n)). new given clause: 424 (422,3) ACHIEVABLE(Row(8),Squares(c,n,c,c,n,c,n,c)). ------------ END OF SEARCH ------------ sos empty. --------------- options --------------- set(hyper_res). set(demod_hist). set(for_sub). set(print_kept). set(back_sub). set(print_back_sub). set(print_given). set(check_arity). clear(binary_res). clear(UR_res). clear(para_from). clear(para_into). clear(demod_inf). clear(para_from_left). clear(para_from_right). clear(para_into_vars). clear(para_from_vars). clear(para_all). clear(para_ones_rule). clear(no_para_into_left). clear(no_para_into_right). clear(demod_linear). clear(print_gen). clear(sort_literals). clear(Unit_deletion). clear(factor). clear(print_weight). clear(sos_fifo). clear(bird_print). clear(atom_wt_max_args). clear(print_lists_at_end). clear(free_all_mem). clear(for_sub_fpa). clear(no_fapl). clear(no_fanl). assign(report, 0). assign(max_seconds, 0). assign(max_given, 0). assign(max_kept, 0). assign(max_gen, 0). assign(max_mem, 0). assign(max_weight, 0). assign(max_literals, 0). assign(fpa_literals, 4). assign(fpa_terms, 4). assign(demod_limit, 100). assign(max_proofs, 1). assign(neg_weight, 0). -------------- statistics ------------- clauses input 22 clauses given 404 clauses generated 1161 demodulation rewrites 3627 clauses wt or lit delete 0 tautologies deleted 0 clauses forward subsumed 759 (clauses subsumed by sos) 333 unit deletions 0 clauses kept 402 empty clauses 0 factors generated 0 clauses back subsumed 0 clauses not processed 0 ----------- times (seconds) ----------- run time 17.34 input time 0.26 binary_res time 0.00 hyper_res time 3.40 UR_res time 0.00 para_into time 0.00 para_from time 0.00 pre_process time 6.30 demod time 1.74 weigh time 0.04 for_sub time 2.36 unit_del time 0.00 post_process time 5.78 back_sub time 4.16 conflict time 1.58 factor time 0.00 FPA build time 0.90 IS build time 0.22 print_cl time 1.48 cl integrate time 0.34 window time 0.00 SHAR_EOF if test -f 'chekndom.ver2.clauses' then echo shar: over-writing existing file "'chekndom.ver2.clauses'" fi cat << \SHAR_EOF > 'chekndom.ver2.clauses' % problem-set/puzzles/space_state/chekndom.ver1.clauses % created : 07/13/88 % revised : 07/13/88 % description: % % This run solves a variation of "The Checkerboard and Dominoes Puzzle" % using hyper-resolution. % % THE CHECKERBOARD AND DOMINOES PUZZLE % % There is a checker board whose upper left and lower right % squares have been removed. There is a box of dominoes that % are one square by two squares in size. Can you exactly cover % the checker board with dominoes? % % VARIATION: % Only the second and third squares of the first row have been % removed. % representation: % % Procedural version: % COMMENTS : Since the clause-set is satisfiable, there is no proof by . % contradiction. % PREDICATES : % ACHIEVABLE(arg1,arg2): Gives the state of each row and the % individual squares in the row. % FUNCTIONS : % row(x): x in this function indicate the row number. % squares(): gives the state of each square in a particular % row. 'c' stands for covered, 'n' for not covered. % and 'r' for removed. % compl(x): Changes the state of a square from x to another. % For each row : If an adjacent pair of checkers are not covered then, % cover them , until every such pair in that row has been looked at.. % Place a domino horizontally, where possible -ACHIEVABLE(Row(x),Squares(n,n,y3,y4,y5,y6,y7,y8)) | ACHIEVABLE(Row(x),Squares(c,c,y3,y4,y5,y6,y7,y8)). -ACHIEVABLE(Row(x),Squares(y1,n,n,y4,y5,y6,y7,y8)) | ACHIEVABLE(Row(x),Squares(y1,c,c,y4,y5,y6,y7,y8)). -ACHIEVABLE(Row(x),Squares(y1,y2,n,n,y5,y6,y7,y8)) | ACHIEVABLE(Row(x),Squares(y1,y2,c,c,y5,y6,y7,y8)). -ACHIEVABLE(Row(x),Squares(y1,y2,y3,n,n,y6,y7,y8)) | ACHIEVABLE(Row(x),Squares(y1,y2,y3,c,c,y6,y7,y8)). -ACHIEVABLE(Row(x),Squares(y1,y2,y3,y4,n,n,y7,y8)) | ACHIEVABLE(Row(x),Squares(y1,y2,y3,y4,c,c,y7,y8)). -ACHIEVABLE(Row(x),Squares(y1,y2,y3,y4,y5,n,n,y8)) | ACHIEVABLE(Row(x),Squares(y1,y2,y3,y4,y5,c,c,y8)). -ACHIEVABLE(Row(x),Squares(y1,y2,y3,y4,y5,y6,n,n)) | ACHIEVABLE(Row(x),Squares(y1,y2,y3,y4,y5,y6,c,c)). % If the Row is complete then examine the Row directly below.. % Then depending, on the complementary function, change the state % of the squares. This may place several dominoes vertically. -ACHIEVABLE(Row(x),Squares(y1,y2,y3,y4,y5,y6,y7,y8)) | ACHIEVABLE(Row(succ(x)),Squares(compl(y1),compl(y2), compl(y3),compl(y4),compl(y5),compl(y6),compl(y7),compl(y8))). % The end condition (to stop when the 8th Row is finished) ACHIEVABLE(Row(9),Squares(y1,y2,y3,y4,y5,y6,y7,y8)). % Initial condition. ACHIEVABLE(Row(1),Squares(n,r,r,n,n,n,n,n)). % If it is possible to cover the checkerboard using dominoes then the. % resulting statement will unify with this clause giving a proof by. % contradiction. If it is not possible, the set of support will be % exhausted. -ACHIEVABLE(Row(8),Squares(c,c,c,c,c,c,c,c)). EQUAL(compl(c),n). EQUAL(compl(n),c). EQUAL(compl(r),n). EQUAL(succ(1),2). EQUAL(succ(2),3). EQUAL(succ(3),4). EQUAL(succ(4),5). EQUAL(succ(5),6). EQUAL(succ(6),7). EQUAL(succ(7),8). EQUAL(succ(8),9). SHAR_EOF if test -f 'chekndom.ver2.in' then echo shar: over-writing existing file "'chekndom.ver2.in'" fi cat << \SHAR_EOF > 'chekndom.ver2.in' % problem-set/puzzles/space_state/chekndom.ver1.in % created: 07/13/88 % revised: 07/13/88 % description: % % This run solves a variation of "The Checkerboard and Dominoes Puzzle" % using hyper-resolution. % % THE CHECKERBOARD AND DOMINOES PUZZLE % % There is a checker board whose upper left and lower right % squares have been removed. There is a box of dominoes that % are one square by two squares in size. Can you exactly cover % the checker board with dominoes? % % VARIATION: % Only the second and third squares of the first row have been % removed. % representation: % % Procedural version: % COMMENTS : Since the clause-set is satisfiable, there is no proof by . % contradiction. % PREDICATES : % ACHIEVABLE(arg1,arg2): Gives the state of each row and the % individual squares in the row. % FUNCTIONS : % row(x): x in this function indicate the row number. % squares(): gives the state of each square in a particular % row. 'c' stands for covered, 'n' for not covered. % and 'r' for removed. % compl(x): Changes the state of a square from x to another. % For each row : If an adjacent pair of checkers are not covered then, % cover them , until every such pair in that row has been looked at.. set(hyper_res). list(axioms). % Place a domino horizontally, where possible -ACHIEVABLE(Row(x),Squares(n,n,y3,y4,y5,y6,y7,y8)) | ACHIEVABLE(Row(x),Squares(c,c,y3,y4,y5,y6,y7,y8)). -ACHIEVABLE(Row(x),Squares(y1,n,n,y4,y5,y6,y7,y8)) | ACHIEVABLE(Row(x),Squares(y1,c,c,y4,y5,y6,y7,y8)). -ACHIEVABLE(Row(x),Squares(y1,y2,n,n,y5,y6,y7,y8)) | ACHIEVABLE(Row(x),Squares(y1,y2,c,c,y5,y6,y7,y8)). -ACHIEVABLE(Row(x),Squares(y1,y2,y3,n,n,y6,y7,y8)) | ACHIEVABLE(Row(x),Squares(y1,y2,y3,c,c,y6,y7,y8)). -ACHIEVABLE(Row(x),Squares(y1,y2,y3,y4,n,n,y7,y8)) | ACHIEVABLE(Row(x),Squares(y1,y2,y3,y4,c,c,y7,y8)). -ACHIEVABLE(Row(x),Squares(y1,y2,y3,y4,y5,n,n,y8)) | ACHIEVABLE(Row(x),Squares(y1,y2,y3,y4,y5,c,c,y8)). -ACHIEVABLE(Row(x),Squares(y1,y2,y3,y4,y5,y6,n,n)) | ACHIEVABLE(Row(x),Squares(y1,y2,y3,y4,y5,y6,c,c)). % If the Row is complete then examine the Row directly below.. % Then depending, on the complementary function, change the state % of the squares. This may place several dominoes vertically. -ACHIEVABLE(Row(x),Squares(y1,y2,y3,y4,y5,y6,y7,y8)) | ACHIEVABLE(Row(succ(x)),Squares(compl(y1),compl(y2), compl(y3),compl(y4),compl(y5),compl(y6),compl(y7),compl(y8))). % The end condition (to stop when the 8th Row is finished) ACHIEVABLE(Row(9),Squares(y1,y2,y3,y4,y5,y6,y7,y8)). end_of_list. list(sos). % Initial condition. ACHIEVABLE(Row(1),Squares(n,r,r,n,n,n,n,n)). % If it is possible to cover the checkerboard using dominoes then the. % resulting statement will unify with this clause giving a proof by. % contradiction. If it is not possible, the set of support will be % exhausted. -ACHIEVABLE(Row(8),Squares(c,c,c,c,c,c,c,c)). end_of_list. list(demodulators). EQUAL(compl(c),n). EQUAL(compl(n),c). EQUAL(compl(r),n). EQUAL(succ(1),2). EQUAL(succ(2),3). EQUAL(succ(3),4). EQUAL(succ(4),5). EQUAL(succ(5),6). EQUAL(succ(6),7). EQUAL(succ(7),8). EQUAL(succ(8),9). end_of_list. SHAR_EOF if test -f 'chekndom.ver2.out' then echo shar: over-writing existing file "'chekndom.ver2.out'" fi cat << \SHAR_EOF > 'chekndom.ver2.out' problem-set/puzzles/space_state/chekndom.ver2.out created : 07/13/88 revised : 07/13/88 OTTER version 0.9, 19 May 1988. set(hyper_res). list(axioms). 1 -ACHIEVABLE(Row(x),Squares(n,n,y3,y4,y5,y6,y7,y8)) | ACHIEVABLE(Row(x),Squares(c,c,y3,y4,y5,y6,y7,y8)). 2 -ACHIEVABLE(Row(x),Squares(y1,n,n,y4,y5,y6,y7,y8)) | ACHIEVABLE(Row(x),Squares(y1,c,c,y4,y5,y6,y7,y8)). 3 -ACHIEVABLE(Row(x),Squares(y1,y2,n,n,y5,y6,y7,y8)) | ACHIEVABLE(Row(x),Squares(y1,y2,c,c,y5,y6,y7,y8)). 4 -ACHIEVABLE(Row(x),Squares(y1,y2,y3,n,n,y6,y7,y8)) | ACHIEVABLE(Row(x),Squares(y1,y2,y3,c,c,y6,y7,y8)). 5 -ACHIEVABLE(Row(x),Squares(y1,y2,y3,y4,n,n,y7,y8)) | ACHIEVABLE(Row(x),Squares(y1,y2,y3,y4,c,c,y7,y8)). 6 -ACHIEVABLE(Row(x),Squares(y1,y2,y3,y4,y5,n,n,y8)) | ACHIEVABLE(Row(x),Squares(y1,y2,y3,y4,y5,c,c,y8)). 7 -ACHIEVABLE(Row(x),Squares(y1,y2,y3,y4,y5,y6,n,n)) | ACHIEVABLE(Row(x),Squares(y1,y2,y3,y4,y5,y6,c,c)). 8 -ACHIEVABLE(Row(x),Squares(y1,y2,y3,y4,y5,y6,y7,y8)) | ACHIEVABLE(Row(succ(x)),Squares(compl(y1),compl(y2),compl(y3),compl(y4),compl(y5),compl(y6),compl(y7),compl(y8))). 9 ACHIEVABLE(Row(9),Squares(y1,y2,y3,y4,y5,y6,y7,y8)). end_of_list. list(sos). 10 ACHIEVABLE(Row(1),Squares(n,r,r,n,n,n,n,n)). 11 -ACHIEVABLE(Row(8),Squares(c,c,c,c,c,c,c,c)). end_of_list. list(demodulators). 12 EQUAL(compl(c),n). 13 EQUAL(compl(n),c). 14 EQUAL(compl(r),n). 15 EQUAL(succ(1),2). 16 EQUAL(succ(2),3). 17 EQUAL(succ(3),4). 18 EQUAL(succ(4),5). 19 EQUAL(succ(5),6). 20 EQUAL(succ(6),7). 21 EQUAL(succ(7),8). 22 EQUAL(succ(8),9). end_of_list. ---------------- PROOF ---------------- 2 -ACHIEVABLE(Row(x),Squares(y1,n,n,y4,y5,y6,y7,y8)) | ACHIEVABLE(Row(x),Squares(y1,c,c,y4,y5,y6,y7,y8)). 8 -ACHIEVABLE(Row(x),Squares(y1,y2,y3,y4,y5,y6,y7,y8)) | ACHIEVABLE(Row(succ(x)),Squares(compl(y1),compl(y2),compl(y3),compl(y4),compl(y5),compl(y6),compl(y7),compl(y8))). 10 ACHIEVABLE(Row(1),Squares(n,r,r,n,n,n,n,n)). 11 -ACHIEVABLE(Row(8),Squares(c,c,c,c,c,c,c,c)). 12 EQUAL(compl(c),n). 13 EQUAL(compl(n),c). 14 EQUAL(compl(r),n). 15 EQUAL(succ(1),2). 16 EQUAL(succ(2),3). 17 EQUAL(succ(3),4). 18 EQUAL(succ(4),5). 19 EQUAL(succ(5),6). 20 EQUAL(succ(6),7). 21 EQUAL(succ(7),8). 23 (10,8,15,13,14,14,13,13,13,13,13) ACHIEVABLE(Row(2),Squares(c,n,n,c,c,c,c,c)). 28 (23,8,16,12,13,13,12,12,12,12,12) ACHIEVABLE(Row(3),Squares(n,c,c,n,n,n,n,n)). 37 (28,8,17,13,12,12,13,13,13,13,13) ACHIEVABLE(Row(4),Squares(c,n,n,c,c,c,c,c)). 51 (37,8,18,12,13,13,12,12,12,12,12) ACHIEVABLE(Row(5),Squares(n,c,c,n,n,n,n,n)). 74 (51,8,19,13,12,12,13,13,13,13,13) ACHIEVABLE(Row(6),Squares(c,n,n,c,c,c,c,c)). 108 (74,8,20,12,13,13,12,12,12,12,12) ACHIEVABLE(Row(7),Squares(n,c,c,n,n,n,n,n)). 149 (108,8,21,13,12,12,13,13,13,13,13) ACHIEVABLE(Row(8),Squares(c,n,n,c,c,c,c,c)). 197 (149,2) ACHIEVABLE(Row(8),Squares(c,c,c,c,c,c,c,c)). 198 (197,11) . --------------- options --------------- set(hyper_res). set(demod_hist). set(for_sub). set(print_kept). set(back_sub). set(print_back_sub). set(print_given). set(check_arity). clear(binary_res). clear(UR_res). clear(para_from). clear(para_into). clear(demod_inf). clear(para_from_left). clear(para_from_right). clear(para_into_vars). clear(para_from_vars). clear(para_all). clear(para_ones_rule). clear(no_para_into_left). clear(no_para_into_right). clear(demod_linear). clear(print_gen). clear(sort_literals). clear(Unit_deletion). clear(factor). clear(print_weight). clear(sos_fifo). clear(bird_print). clear(atom_wt_max_args). clear(print_lists_at_end). clear(free_all_mem). clear(for_sub_fpa). clear(no_fapl). clear(no_fanl). assign(report, 0). assign(max_seconds, 0). assign(max_given, 0). assign(max_kept, 0). assign(max_gen, 0). assign(max_mem, 0). assign(max_weight, 0). assign(max_literals, 0). assign(fpa_literals, 4). assign(fpa_terms, 4). assign(demod_limit, 100). assign(max_proofs, 1). assign(neg_weight, 0). -------------- statistics ------------- clauses input 22 clauses given 129 clauses generated 390 demodulation rewrites 1152 clauses wt or lit delete 0 tautologies deleted 0 clauses forward subsumed 214 (clauses subsumed by sos) 122 unit deletions 0 clauses kept 176 empty clauses 1 factors generated 0 clauses back subsumed 0 clauses not processed 2 ----------- times (seconds) ----------- run time 6.20 input time 0.28 binary_res time 0.00 hyper_res time 1.32 UR_res time 0.00 para_into time 0.00 para_from time 0.00 pre_process time 2.34 demod time 0.54 weigh time 0.02 for_sub time 0.86 unit_del time 0.00 post_process time 1.72 back_sub time 0.82 conflict time 0.84 factor time 0.00 FPA build time 0.32 IS build time 0.02 print_cl time 0.70 cl integrate time 0.20 window time 0.00 SHAR_EOF if test -f 'mission.desc' then echo shar: over-writing existing file "'mission.desc'" fi cat << \SHAR_EOF > 'mission.desc' problem-set/puzzles/space_state/mission.desc created : 07/09/86 revised : 07/13/88 Natural Language Description: The Missionaries and Cannibals Puzzle There are three missionaries and three cannibals on the west bank of a river. There is a boat on the east bank. But they have a problem: If on either bank the cannibals ever outnumber the missionaries, the outnumbered will be eaten. Is there a way for the missionaries to get their wish - to get to the east bank without losing anyone? Versions: mission.ver1 : Declarative representation, using hyper-resolution created by : L. Wos verified for ITP : 07/09/86 translated for OTTER by : K.R. verified for OTTER : 07/13/88 mission.ver2.in- Procedural representation, using hyper-resolution created by : E. Lusk verified for ITP : 06/30/86 translated for OTTER by : K.R. verified for OTTER : 07/13/88 SHAR_EOF if test -f 'mission.ver1.clauses' then echo shar: over-writing existing file "'mission.ver1.clauses'" fi cat << \SHAR_EOF > 'mission.ver1.clauses' % problem-set/puzzles/space_state/mission.ver1.clauses % created : 07/13/88 % revised : 07/13/88 % description: % % This run solves "The Missionaries and Cannibals Puzzle" using % UR-resolution. % % The Missionaries and Cannibals Puzzle % % There are three missionaries and three cannibals on the west % bank of a river. There is a boat on the east bank. But they % have a problem: If on either bank the cannibals ever outnumber % the missionaries, the outnumbered will be eaten. Is there a % way for the missionaries to get their wish - to get to the % east bank without losing anyone? % representation: % % PREDICATES : % ACHEIVABLE - The puzzle starts with an 'acheivable' arrangement % and deduces other states. The arguements of this % predicate, represented as lists, indicate the number % of missionaries and cannibals on the west and East % bank and the position of the boat. % FUNCTIONS : % West(x,y) :Indicates that there are x number of % missionaries and y number of cannibals on the west bank. % East(mx,cy):Indicates that there are x number of % missionaries and y number of cannibals on the East bank. % s(x) :gives successor of x,ie.,s(0) =1, etc % m(s(x)) :there are s(x) number of missionaries % c(s(x)) :there are s(x) number of cannibals. % Take one cannibal from the west bank to the East bank . This % automatically implies that the number of cannibals on the west % bank is reduced by one. % The number of cannibals on the East bank should now be increased by one. -ACHIEVABLE(West(m(x),c(s(y))),boatonwest,East(m(z),c(w))) |ACHIEVABLE(West(m(x),c(y)),boatoneast,East(m(z),c(s(w)))). -ACHIEVABLE(West(m(x),c(y)),boatoneast,East(m(z),c(s(w)))) |ACHIEVABLE(West(m(x),c(s(y))),boatonwest,East(m(z),c(w))). % Two missionaries are taken from the west bank to the East. -ACHIEVABLE(West(m(s(s(x))),c(y)),boatonwest,East(m(z),c(w))) |ACHIEVABLE(West(m(x),c(y)),boatoneast,East(m(s(s(z))),c(w))). % Two missionaries from East to west. -ACHIEVABLE(West(m(x),c(y)),boatoneast,East(m(s(s(z))),c(w))) |ACHIEVABLE(West(m(s(s(x))),c(y)),boatonwest,East(m(z),c(w))). % One missionary and one cannibal from west to East. -ACHIEVABLE(West(m(s(x)),c(s(y))),boatonwest,East(m(z),c(w))) |ACHIEVABLE(West(m(x),c(y)),boatoneast,East(m(s(z)),c(s(w)))). % One missionary and one cannibal from East to west. -ACHIEVABLE(West(m(x),c(y)),boatoneast,East(m(s(z)),c(s(w)))) |ACHIEVABLE(West(m(s(x)),c(s(y))),boatonwest,East(m(z),c(w))). % One missionary from west to East. -ACHIEVABLE(West(m(s(x)),c(y)),boatonwest,East(m(z),c(w))) |ACHIEVABLE(West(m(x),c(y)),boatoneast,East(m(s(z)),c(w))). % One missionary from East to west . -ACHIEVABLE(West(m(x),c(y)),boatoneast,East(m(s(z)),c(w))) |ACHIEVABLE(West(m(s(x)),c(y)),boatonwest,East(m(z),c(w))). % Two cannibals from west to East. -ACHIEVABLE(West(m(x),c(s(s(y)))),boatonwest,East(m(z),c(w))) |ACHIEVABLE(West(m(x),c(y)),boatoneast,East(m(z),c(s(s(w))))). % Two cannibals from East to west. -ACHIEVABLE(West(m(x),c(y)),boatoneast,East(m(z),c(s(s(w))))) |ACHIEVABLE(West(m(x),c(s(s(y)))),boatonwest,East(m(z),c(w))). % The possible combinations of the missionaries and the cannibals on % either banks may be characterised by the differance their number % (of one or two). This idea is captured in the following. ACHIEVABLE(West(m(s(x)),c(s(s(x)))),y,East(z,w)). ACHIEVABLE(West(m(s(x)),c(s(s(s(x))))),y,East(z,w)). ACHIEVABLE(West(x,y),z,East(m(s(w)),c(s(s(w))))). ACHIEVABLE(West(x,y),z,East(m(s(w)),c(s(s(s(w)))))). % Corresponds to the unachievable state that corresponds to assuming % the puzzle unsolvable. ACHIEVABLE(West(m(s(s(s(0)))),c(s(s(s(0))))),boatonwest, East(m(0),c(0))). -ACHIEVABLE(West(m(0),c(0)),x,East(m(s(s(s(0)))),c(s(s(s(0)))))). SHAR_EOF if test -f 'mission.ver1.in' then echo shar: over-writing existing file "'mission.ver1.in'" fi cat << \SHAR_EOF > 'mission.ver1.in' % problem-set/puzzles/space_state/mission.ver1.in % created : 07/09/86 % revised : 07/13/88 % description: % % This run solves "The Missionaries and Cannibals Puzzle" using % UR-resolution. % % The Missionaries and Cannibals Puzzle % % There are three missionaries and three cannibals on the west % bank of a river. There is a boat on the east bank. But they % have a problem: If on either bank the cannibals ever outnumber % the missionaries, the outnumbered will be eaten. Is there a % way for the missionaries to get their wish - to get to the % east bank without losing anyone? % representation: % % Declarative version % PREDICATES : % ACHEIVABLE - The puzzle starts with an 'acheivable' arrangement % and deduces other states. The arguements of this % predicate, represented as lists, indicate the number % of missionaries and cannibals on the west and East % bank and the position of the boat. % FUNCTIONS : % West(x,y) :Indicates that there are x number of % missionaries and y number of cannibals on the west bank. % East(mx,cy):Indicates that there are x number of % missionaries and y number of cannibals on the East bank. % s(x) :gives successor of x,ie.,s(0) =1, etc % m(s(x)) :there are s(x) number of missionaries % c(s(x)) :there are s(x) number of cannibals. set(hyper_res). list(axioms). % Take one cannibal from the west bank to the East bank . This % automatically implies that the number of cannibals on the west % bank is reduced by one. % The number of cannibals on the East bank should now be increased by one. -ACHIEVABLE(West(m(x),c(s(y))),boatonwest,East(m(z),c(w))) |ACHIEVABLE(West(m(x),c(y)),boatoneast,East(m(z),c(s(w)))). -ACHIEVABLE(West(m(x),c(y)),boatoneast,East(m(z),c(s(w)))) |ACHIEVABLE(West(m(x),c(s(y))),boatonwest,East(m(z),c(w))). % Two missionaries are taken from the west bank to the East. -ACHIEVABLE(West(m(s(s(x))),c(y)),boatonwest,East(m(z),c(w))) |ACHIEVABLE(West(m(x),c(y)),boatoneast,East(m(s(s(z))),c(w))). % Two missionaries from East to west. -ACHIEVABLE(West(m(x),c(y)),boatoneast,East(m(s(s(z))),c(w))) |ACHIEVABLE(West(m(s(s(x))),c(y)),boatonwest,East(m(z),c(w))). % One missionary and one cannibal from west to East. -ACHIEVABLE(West(m(s(x)),c(s(y))),boatonwest,East(m(z),c(w))) |ACHIEVABLE(West(m(x),c(y)),boatoneast,East(m(s(z)),c(s(w)))). % One missionary and one cannibal from East to west. -ACHIEVABLE(West(m(x),c(y)),boatoneast,East(m(s(z)),c(s(w)))) |ACHIEVABLE(West(m(s(x)),c(s(y))),boatonwest,East(m(z),c(w))). % One missionary from west to East. -ACHIEVABLE(West(m(s(x)),c(y)),boatonwest,East(m(z),c(w))) |ACHIEVABLE(West(m(x),c(y)),boatoneast,East(m(s(z)),c(w))). % One missionary from East to west . -ACHIEVABLE(West(m(x),c(y)),boatoneast,East(m(s(z)),c(w))) |ACHIEVABLE(West(m(s(x)),c(y)),boatonwest,East(m(z),c(w))). % Two cannibals from west to East. -ACHIEVABLE(West(m(x),c(s(s(y)))),boatonwest,East(m(z),c(w))) |ACHIEVABLE(West(m(x),c(y)),boatoneast,East(m(z),c(s(s(w))))). % Two cannibals from East to west. -ACHIEVABLE(West(m(x),c(y)),boatoneast,East(m(z),c(s(s(w))))) |ACHIEVABLE(West(m(x),c(s(s(y)))),boatonwest,East(m(z),c(w))). % The possible combinations of the missionaries and the cannibals on % either banks may be characterised by the differance their number % (of one or two). This idea is captured in the following. ACHIEVABLE(West(m(s(x)),c(s(s(x)))),y,East(z,w)). ACHIEVABLE(West(m(s(x)),c(s(s(s(x))))),y,East(z,w)). ACHIEVABLE(West(x,y),z,East(m(s(w)),c(s(s(w))))). ACHIEVABLE(West(x,y),z,East(m(s(w)),c(s(s(s(w)))))). end_of_list. list(sos). % Corresponds to the unachievable state that corresponds to assuming % the puzzle unsolvable. ACHIEVABLE(West(m(s(s(s(0)))),c(s(s(s(0))))),boatonwest, East(m(0),c(0))). -ACHIEVABLE(West(m(0),c(0)),x,East(m(s(s(s(0)))),c(s(s(s(0)))))). end_of_list. SHAR_EOF if test -f 'mission.ver1.out' then echo shar: over-writing existing file "'mission.ver1.out'" fi cat << \SHAR_EOF > 'mission.ver1.out' problem-set/puzzles/space_state/mission.ver1.out created : 07/13/88 revised : 07/13/88 OTTER version 0.9, 19 May 1988. set(hyper_res). list(axioms). 1 -ACHIEVABLE(West(m(x),c(s(y))),boatonwest,East(m(z),c(w))) | ACHIEVABLE(West(m(x),c(y)),boatoneast,East(m(z),c(s(w)))). 2 -ACHIEVABLE(West(m(x),c(y)),boatoneast,East(m(z),c(s(w)))) | ACHIEVABLE(West(m(x),c(s(y))),boatonwest,East(m(z),c(w))). 3 -ACHIEVABLE(West(m(s(s(x))),c(y)),boatonwest,East(m(z),c(w))) | ACHIEVABLE(West(m(x),c(y)),boatoneast,East(m(s(s(z))),c(w))). 4 -ACHIEVABLE(West(m(x),c(y)),boatoneast,East(m(s(s(z))),c(w))) | ACHIEVABLE(West(m(s(s(x))),c(y)),boatonwest,East(m(z),c(w))). 5 -ACHIEVABLE(West(m(s(x)),c(s(y))),boatonwest,East(m(z),c(w))) | ACHIEVABLE(West(m(x),c(y)),boatoneast,East(m(s(z)),c(s(w)))). 6 -ACHIEVABLE(West(m(x),c(y)),boatoneast,East(m(s(z)),c(s(w)))) | ACHIEVABLE(West(m(s(x)),c(s(y))),boatonwest,East(m(z),c(w))). 7 -ACHIEVABLE(West(m(s(x)),c(y)),boatonwest,East(m(z),c(w))) | ACHIEVABLE(West(m(x),c(y)),boatoneast,East(m(s(z)),c(w))). 8 -ACHIEVABLE(West(m(x),c(y)),boatoneast,East(m(s(z)),c(w))) | ACHIEVABLE(West(m(s(x)),c(y)),boatonwest,East(m(z),c(w))). 9 -ACHIEVABLE(West(m(x),c(s(s(y)))),boatonwest,East(m(z),c(w))) | ACHIEVABLE(West(m(x),c(y)),boatoneast,East(m(z),c(s(s(w))))). 10 -ACHIEVABLE(West(m(x),c(y)),boatoneast,East(m(z),c(s(s(w))))) | ACHIEVABLE(West(m(x),c(s(s(y)))),boatonwest,East(m(z),c(w))). 11 ACHIEVABLE(West(m(s(x)),c(s(s(x)))),y,East(z,w)). 12 ACHIEVABLE(West(m(s(x)),c(s(s(s(x))))),y,East(z,w)). 13 ACHIEVABLE(West(x,y),z,East(m(s(w)),c(s(s(w))))). 14 ACHIEVABLE(West(x,y),z,East(m(s(w)),c(s(s(s(w)))))). end_of_list. list(sos). 15 ACHIEVABLE(West(m(s(s(s(0)))),c(s(s(s(0))))),boatonwest,East(m(0),c(0))). 16 -ACHIEVABLE(West(m(0),c(0)),x,East(m(s(s(s(0)))),c(s(s(s(0)))))). end_of_list. ---------------- PROOF ---------------- 2 -ACHIEVABLE(West(m(x),c(y)),boatoneast,East(m(z),c(s(w)))) | ACHIEVABLE(West(m(x),c(s(y))),boatonwest,East(m(z),c(w))). 3 -ACHIEVABLE(West(m(s(s(x))),c(y)),boatonwest,East(m(z),c(w))) | ACHIEVABLE(West(m(x),c(y)),boatoneast,East(m(s(s(z))),c(w))). 5 -ACHIEVABLE(West(m(s(x)),c(s(y))),boatonwest,East(m(z),c(w))) | ACHIEVABLE(West(m(x),c(y)),boatoneast,East(m(s(z)),c(s(w)))). 6 -ACHIEVABLE(West(m(x),c(y)),boatoneast,East(m(s(z)),c(s(w)))) | ACHIEVABLE(West(m(s(x)),c(s(y))),boatonwest,East(m(z),c(w))). 8 -ACHIEVABLE(West(m(x),c(y)),boatoneast,East(m(s(z)),c(w))) | ACHIEVABLE(West(m(s(x)),c(y)),boatonwest,East(m(z),c(w))). 9 -ACHIEVABLE(West(m(x),c(s(s(y)))),boatonwest,East(m(z),c(w))) | ACHIEVABLE(West(m(x),c(y)),boatoneast,East(m(z),c(s(s(w))))). 15 ACHIEVABLE(West(m(s(s(s(0)))),c(s(s(s(0))))),boatonwest,East(m(0),c(0))). 16 -ACHIEVABLE(West(m(0),c(0)),x,East(m(s(s(s(0)))),c(s(s(s(0)))))). 17 (15,9) ACHIEVABLE(West(m(s(s(s(0)))),c(s(0))),boatoneast,East(m(0),c(s(s(0))))). 20 (17,2) ACHIEVABLE(West(m(s(s(s(0)))),c(s(s(0)))),boatonwest,East(m(0),c(s(0)))). 21 (20,9) ACHIEVABLE(West(m(s(s(s(0)))),c(0)),boatoneast,East(m(0),c(s(s(s(0)))))). 22 (21,2) ACHIEVABLE(West(m(s(s(s(0)))),c(s(0))),boatonwest,East(m(0),c(s(s(0))))). 23 (22,3) ACHIEVABLE(West(m(s(0)),c(s(0))),boatoneast,East(m(s(s(0))),c(s(s(0))))). 24 (23,6) ACHIEVABLE(West(m(s(s(0))),c(s(s(0)))),boatonwest,East(m(s(0)),c(s(0)))). 25 (24,3) ACHIEVABLE(West(m(0),c(s(s(0)))),boatoneast,East(m(s(s(s(0)))),c(s(0)))). 26 (25,2) ACHIEVABLE(West(m(0),c(s(s(s(0))))),boatonwest,East(m(s(s(s(0)))),c(0))). 27 (26,9) ACHIEVABLE(West(m(0),c(s(0))),boatoneast,East(m(s(s(s(0)))),c(s(s(0))))). 28 (27,8) ACHIEVABLE(West(m(s(0)),c(s(0))),boatonwest,East(m(s(s(0))),c(s(s(0))))). 30 (28,5) ACHIEVABLE(West(m(0),c(0)),boatoneast,East(m(s(s(s(0)))),c(s(s(s(0)))))). 31 (30,16) . --------------- options --------------- set(hyper_res). set(demod_hist). set(for_sub). set(print_kept). set(back_sub). set(print_back_sub). set(print_given). set(check_arity). clear(binary_res). clear(UR_res). clear(para_from). clear(para_into). clear(demod_inf). clear(para_from_left). clear(para_from_right). clear(para_into_vars). clear(para_from_vars). clear(para_all). clear(para_ones_rule). clear(no_para_into_left). clear(no_para_into_right). clear(demod_linear). clear(print_gen). clear(sort_literals). clear(Unit_deletion). clear(factor). clear(print_weight). clear(sos_fifo). clear(bird_print). clear(atom_wt_max_args). clear(print_lists_at_end). clear(free_all_mem). clear(for_sub_fpa). clear(no_fapl). clear(no_fanl). assign(report, 0). assign(max_seconds, 0). assign(max_given, 0). assign(max_kept, 0). assign(max_gen, 0). assign(max_mem, 0). assign(max_weight, 0). assign(max_literals, 0). assign(fpa_literals, 4). assign(fpa_terms, 4). assign(demod_limit, 100). assign(max_proofs, 1). assign(neg_weight, 0). -------------- statistics ------------- clauses input 16 clauses given 14 clauses generated 47 demodulation rewrites 0 clauses wt or lit delete 0 tautologies deleted 0 clauses forward subsumed 32 (clauses subsumed by sos) 1 unit deletions 0 clauses kept 15 empty clauses 1 factors generated 0 clauses back subsumed 0 clauses not processed 2 ----------- times (seconds) ----------- run time 1.02 input time 0.36 binary_res time 0.00 hyper_res time 0.10 UR_res time 0.00 para_into time 0.00 para_from time 0.00 pre_process time 0.30 demod time 0.00 weigh time 0.00 for_sub time 0.10 unit_del time 0.00 post_process time 0.10 back_sub time 0.02 conflict time 0.08 factor time 0.00 FPA build time 0.08 IS build time 0.04 print_cl time 0.28 cl integrate time 0.06 window time 0.00 SHAR_EOF if test -f 'mission.ver2.clauses' then echo shar: over-writing existing file "'mission.ver2.clauses'" fi cat << \SHAR_EOF > 'mission.ver2.clauses' % problem-set/puzzles/space_state/mission.ver2.clauses % created : 07/13/88. % revised : 07/13/88. % description: % % This run solves "The Missionaries and Cannibals Puzzle" using % hyper-resolution. % % The Missionaries and Cannibals Puzzle % % There are three missionaries and three cannibals on the west % bank of a river. There is a boat on the east bank. But they % have a problem: If on either bank the cannibals ever outnumber % the missionaries, the outnumbered will be eaten. Is there a % way for the missionaries to get their wish - to get to the % east bank without losing anyone? % representation: % % Procedural version -Config(Left(M(3),C(3)),Right(M(0),C(0)),BoatOnLeft) | Config(Left(M(3),C(1)),Right(M(0),C(2)),BoatOnRight). -Config(Left(M(3),C(3)),Right(M(0),C(0)),BoatOnLeft) | Config(Left(M(2),C(2)),Right(M(1),C(1)),BoatOnRight). -Config(Left(M(3),C(2)),Right(M(0),C(1)),BoatOnLeft) | Config(Left(M(3),C(0)),Right(M(0),C(3)),BoatOnRight). -Config(Left(M(3),C(2)),Right(M(0),C(1)),BoatOnLeft) | Config(Left(M(3),C(1)),Right(M(0),C(2)),BoatOnRight). -Config(Left(M(3),C(2)),Right(M(0),C(1)),BoatOnLeft) | Config(Left(M(2),C(2)),Right(M(1),C(1)),BoatOnRight). -Config(Left(M(3),C(1)),Right(M(0),C(2)),BoatOnLeft) | Config(Left(M(1),C(1)),Right(M(2),C(2)),BoatOnRight). -Config(Left(M(3),C(1)),Right(M(0),C(2)),BoatOnLeft) | Config(Left(M(3),C(0)),Right(M(0),C(3)),BoatOnRight). -Config(Left(M(2),C(2)),Right(M(1),C(1)),BoatOnLeft) | Config(Left(M(1),C(1)),Right(M(2),C(2)),BoatOnRight). -Config(Left(M(2),C(2)),Right(M(1),C(1)),BoatOnLeft) | Config(Left(M(0),C(2)),Right(M(3),C(1)),BoatOnRight). -Config(Left(M(1),C(1)),Right(M(2),C(2)),BoatOnLeft) | Config(Left(M(0),C(0)),Right(M(3),C(3)),BoatOnRight). -Config(Left(M(1),C(1)),Right(M(2),C(2)),BoatOnLeft) | Config(Left(M(0),C(1)),Right(M(3),C(2)),BoatOnRight). -Config(Left(M(0),C(3)),Right(M(3),C(0)),BoatOnLeft) | Config(Left(M(0),C(1)),Right(M(3),C(2)),BoatOnRight). -Config(Left(M(0),C(3)),Right(M(3),C(0)),BoatOnLeft) | Config(Left(M(0),C(2)),Right(M(3),C(1)),BoatOnRight). -Config(Left(M(0),C(2)),Right(M(3),C(1)),BoatOnLeft) | Config(Left(M(0),C(0)),Right(M(3),C(3)),BoatOnRight). -Config(Left(M(0),C(2)),Right(M(3),C(1)),BoatOnLeft) | Config(Left(M(0),C(1)),Right(M(3),C(2)),BoatOnRight). -Config(Left(M(0),C(1)),Right(M(3),C(2)),BoatOnLeft) | Config(Left(M(0),C(0)),Right(M(3),C(3)),BoatOnRight). -Config(Left(M(0),C(1)),Right(M(3),C(2)),BoatOnRight) | Config(Left(M(0),C(3)),Right(M(3),C(0)),BoatOnLeft). -Config(Left(M(0),C(1)),Right(M(3),C(2)),BoatOnRight) | Config(Left(M(0),C(2)),Right(M(3),C(1)),BoatOnLeft). -Config(Left(M(0),C(1)),Right(M(3),C(2)),BoatOnRight) | Config(Left(M(1),C(1)),Right(M(2),C(2)),BoatOnLeft). -Config(Left(M(0),C(2)),Right(M(3),C(1)),BoatOnRight) | Config(Left(M(2),C(2)),Right(M(1),C(1)),BoatOnLeft). -Config(Left(M(0),C(2)),Right(M(3),C(1)),BoatOnRight) | Config(Left(M(0),C(3)),Right(M(3),C(0)),BoatOnLeft). -Config(Left(M(1),C(1)),Right(M(2),C(2)),BoatOnRight) | Config(Left(M(2),C(2)),Right(M(1),C(1)),BoatOnLeft). -Config(Left(M(1),C(1)),Right(M(2),C(2)),BoatOnRight) | Config(Left(M(3),C(1)),Right(M(0),C(2)),BoatOnLeft). -Config(Left(M(2),C(2)),Right(M(1),C(1)),BoatOnRight) | Config(Left(M(3),C(3)),Right(M(0),C(0)),BoatOnLeft). -Config(Left(M(2),C(2)),Right(M(1),C(1)),BoatOnRight) | Config(Left(M(3),C(2)),Right(M(0),C(1)),BoatOnLeft). -Config(Left(M(3),C(0)),Right(M(0),C(3)),BoatOnRight) | Config(Left(M(3),C(2)),Right(M(0),C(1)),BoatOnLeft). -Config(Left(M(3),C(0)),Right(M(0),C(3)),BoatOnRight) | Config(Left(M(3),C(1)),Right(M(0),C(2)),BoatOnLeft). -Config(Left(M(3),C(1)),Right(M(0),C(2)),BoatOnRight) | Config(Left(M(3),C(3)),Right(M(0),C(0)),BoatOnLeft). -Config(Left(M(3),C(1)),Right(M(0),C(2)),BoatOnRight) | Config(Left(M(3),C(2)),Right(M(0),C(1)),BoatOnLeft). -Config(Left(M(3),C(2)),Right(M(0),C(1)),BoatOnRight) | Config(Left(M(3),C(3)),Right(M(0),C(0)),BoatOnLeft). Config(Left(M(3),C(3)),Right(M(0),C(0)),BoatOnLeft). -Config(Left(M(0),C(0)),Right(M(3),C(3)),BoatOnRight). SHAR_EOF if test -f 'mission.ver2.in' then echo shar: over-writing existing file "'mission.ver2.in'" fi cat << \SHAR_EOF > 'mission.ver2.in' % problem-set/puzzles/space_state/mission.ver2.in % created : 07/09/86. % revised : 07/13/88. % description: % % This run solves "The Missionaries and Cannibals Puzzle" using % hyper-resolution. % % The Missionaries and Cannibals Puzzle % % There are three missionaries and three cannibals on the west % bank of a river. There is a boat on the east bank. But they % have a problem: If on either bank the cannibals ever outnumber % the missionaries, the outnumbered will be eaten. Is there a % way for the missionaries to get their wish - to get to the % east bank without losing anyone? % % representation: % % Procedural version set(hyper_res). list(axioms). -Config(Left(M(3),C(3)),Right(M(0),C(0)),BoatOnLeft) | Config(Left(M(3),C(1)),Right(M(0),C(2)),BoatOnRight). -Config(Left(M(3),C(3)),Right(M(0),C(0)),BoatOnLeft) | Config(Left(M(2),C(2)),Right(M(1),C(1)),BoatOnRight). -Config(Left(M(3),C(2)),Right(M(0),C(1)),BoatOnLeft) | Config(Left(M(3),C(0)),Right(M(0),C(3)),BoatOnRight). -Config(Left(M(3),C(2)),Right(M(0),C(1)),BoatOnLeft) | Config(Left(M(3),C(1)),Right(M(0),C(2)),BoatOnRight). -Config(Left(M(3),C(2)),Right(M(0),C(1)),BoatOnLeft) | Config(Left(M(2),C(2)),Right(M(1),C(1)),BoatOnRight). -Config(Left(M(3),C(1)),Right(M(0),C(2)),BoatOnLeft) | Config(Left(M(1),C(1)),Right(M(2),C(2)),BoatOnRight). -Config(Left(M(3),C(1)),Right(M(0),C(2)),BoatOnLeft) | Config(Left(M(3),C(0)),Right(M(0),C(3)),BoatOnRight). -Config(Left(M(2),C(2)),Right(M(1),C(1)),BoatOnLeft) | Config(Left(M(1),C(1)),Right(M(2),C(2)),BoatOnRight). -Config(Left(M(2),C(2)),Right(M(1),C(1)),BoatOnLeft) | Config(Left(M(0),C(2)),Right(M(3),C(1)),BoatOnRight). -Config(Left(M(1),C(1)),Right(M(2),C(2)),BoatOnLeft) | Config(Left(M(0),C(0)),Right(M(3),C(3)),BoatOnRight). -Config(Left(M(1),C(1)),Right(M(2),C(2)),BoatOnLeft) | Config(Left(M(0),C(1)),Right(M(3),C(2)),BoatOnRight). -Config(Left(M(0),C(3)),Right(M(3),C(0)),BoatOnLeft) | Config(Left(M(0),C(1)),Right(M(3),C(2)),BoatOnRight). -Config(Left(M(0),C(3)),Right(M(3),C(0)),BoatOnLeft) | Config(Left(M(0),C(2)),Right(M(3),C(1)),BoatOnRight). -Config(Left(M(0),C(2)),Right(M(3),C(1)),BoatOnLeft) | Config(Left(M(0),C(0)),Right(M(3),C(3)),BoatOnRight). -Config(Left(M(0),C(2)),Right(M(3),C(1)),BoatOnLeft) | Config(Left(M(0),C(1)),Right(M(3),C(2)),BoatOnRight). -Config(Left(M(0),C(1)),Right(M(3),C(2)),BoatOnLeft) | Config(Left(M(0),C(0)),Right(M(3),C(3)),BoatOnRight). -Config(Left(M(0),C(1)),Right(M(3),C(2)),BoatOnRight) | Config(Left(M(0),C(3)),Right(M(3),C(0)),BoatOnLeft). -Config(Left(M(0),C(1)),Right(M(3),C(2)),BoatOnRight) | Config(Left(M(0),C(2)),Right(M(3),C(1)),BoatOnLeft). -Config(Left(M(0),C(1)),Right(M(3),C(2)),BoatOnRight) | Config(Left(M(1),C(1)),Right(M(2),C(2)),BoatOnLeft). -Config(Left(M(0),C(2)),Right(M(3),C(1)),BoatOnRight) | Config(Left(M(2),C(2)),Right(M(1),C(1)),BoatOnLeft). -Config(Left(M(0),C(2)),Right(M(3),C(1)),BoatOnRight) | Config(Left(M(0),C(3)),Right(M(3),C(0)),BoatOnLeft). -Config(Left(M(1),C(1)),Right(M(2),C(2)),BoatOnRight) | Config(Left(M(2),C(2)),Right(M(1),C(1)),BoatOnLeft). -Config(Left(M(1),C(1)),Right(M(2),C(2)),BoatOnRight) | Config(Left(M(3),C(1)),Right(M(0),C(2)),BoatOnLeft). -Config(Left(M(2),C(2)),Right(M(1),C(1)),BoatOnRight) | Config(Left(M(3),C(3)),Right(M(0),C(0)),BoatOnLeft). -Config(Left(M(2),C(2)),Right(M(1),C(1)),BoatOnRight) | Config(Left(M(3),C(2)),Right(M(0),C(1)),BoatOnLeft). -Config(Left(M(3),C(0)),Right(M(0),C(3)),BoatOnRight) | Config(Left(M(3),C(2)),Right(M(0),C(1)),BoatOnLeft). -Config(Left(M(3),C(0)),Right(M(0),C(3)),BoatOnRight) | Config(Left(M(3),C(1)),Right(M(0),C(2)),BoatOnLeft). -Config(Left(M(3),C(1)),Right(M(0),C(2)),BoatOnRight) | Config(Left(M(3),C(3)),Right(M(0),C(0)),BoatOnLeft). -Config(Left(M(3),C(1)),Right(M(0),C(2)),BoatOnRight) | Config(Left(M(3),C(2)),Right(M(0),C(1)),BoatOnLeft). -Config(Left(M(3),C(2)),Right(M(0),C(1)),BoatOnRight) | Config(Left(M(3),C(3)),Right(M(0),C(0)),BoatOnLeft). end_of_list. list(sos). Config(Left(M(3),C(3)),Right(M(0),C(0)),BoatOnLeft). -Config(Left(M(0),C(0)),Right(M(3),C(3)),BoatOnRight). end_of_list. SHAR_EOF if test -f 'mission.ver2.out' then echo shar: over-writing existing file "'mission.ver2.out'" fi cat << \SHAR_EOF > 'mission.ver2.out' problem-set/puzzles/space_state/mission.ver2.out created : 07/13/88 revised : 07/13/88 OTTER version 0.9, 19 May 1988. set(hyper_res). list(axioms). 1 -Config(Left(M(3),C(3)),Right(M(0),C(0)),BoatOnLeft) | Config(Left(M(3),C(1)),Right(M(0),C(2)),BoatOnRight). 2 -Config(Left(M(3),C(3)),Right(M(0),C(0)),BoatOnLeft) | Config(Left(M(2),C(2)),Right(M(1),C(1)),BoatOnRight). 3 -Config(Left(M(3),C(2)),Right(M(0),C(1)),BoatOnLeft) | Config(Left(M(3),C(0)),Right(M(0),C(3)),BoatOnRight). 4 -Config(Left(M(3),C(2)),Right(M(0),C(1)),BoatOnLeft) | Config(Left(M(3),C(1)),Right(M(0),C(2)),BoatOnRight). 5 -Config(Left(M(3),C(2)),Right(M(0),C(1)),BoatOnLeft) | Config(Left(M(2),C(2)),Right(M(1),C(1)),BoatOnRight). 6 -Config(Left(M(3),C(1)),Right(M(0),C(2)),BoatOnLeft) | Config(Left(M(1),C(1)),Right(M(2),C(2)),BoatOnRight). 7 -Config(Left(M(3),C(1)),Right(M(0),C(2)),BoatOnLeft) | Config(Left(M(3),C(0)),Right(M(0),C(3)),BoatOnRight). 8 -Config(Left(M(2),C(2)),Right(M(1),C(1)),BoatOnLeft) | Config(Left(M(1),C(1)),Right(M(2),C(2)),BoatOnRight). 9 -Config(Left(M(2),C(2)),Right(M(1),C(1)),BoatOnLeft) | Config(Left(M(0),C(2)),Right(M(3),C(1)),BoatOnRight). 10 -Config(Left(M(1),C(1)),Right(M(2),C(2)),BoatOnLeft) | Config(Left(M(0),C(0)),Right(M(3),C(3)),BoatOnRight). 11 -Config(Left(M(1),C(1)),Right(M(2),C(2)),BoatOnLeft) | Config(Left(M(0),C(1)),Right(M(3),C(2)),BoatOnRight). 12 -Config(Left(M(0),C(3)),Right(M(3),C(0)),BoatOnLeft) | Config(Left(M(0),C(1)),Right(M(3),C(2)),BoatOnRight). 13 -Config(Left(M(0),C(3)),Right(M(3),C(0)),BoatOnLeft) | Config(Left(M(0),C(2)),Right(M(3),C(1)),BoatOnRight). 14 -Config(Left(M(0),C(2)),Right(M(3),C(1)),BoatOnLeft) | Config(Left(M(0),C(0)),Right(M(3),C(3)),BoatOnRight). 15 -Config(Left(M(0),C(2)),Right(M(3),C(1)),BoatOnLeft) | Config(Left(M(0),C(1)),Right(M(3),C(2)),BoatOnRight). 16 -Config(Left(M(0),C(1)),Right(M(3),C(2)),BoatOnLeft) | Config(Left(M(0),C(0)),Right(M(3),C(3)),BoatOnRight). 17 -Config(Left(M(0),C(1)),Right(M(3),C(2)),BoatOnRight) | Config(Left(M(0),C(3)),Right(M(3),C(0)),BoatOnLeft). 18 -Config(Left(M(0),C(1)),Right(M(3),C(2)),BoatOnRight) | Config(Left(M(0),C(2)),Right(M(3),C(1)),BoatOnLeft). 19 -Config(Left(M(0),C(1)),Right(M(3),C(2)),BoatOnRight) | Config(Left(M(1),C(1)),Right(M(2),C(2)),BoatOnLeft). 20 -Config(Left(M(0),C(2)),Right(M(3),C(1)),BoatOnRight) | Config(Left(M(2),C(2)),Right(M(1),C(1)),BoatOnLeft). 21 -Config(Left(M(0),C(2)),Right(M(3),C(1)),BoatOnRight) | Config(Left(M(0),C(3)),Right(M(3),C(0)),BoatOnLeft). 22 -Config(Left(M(1),C(1)),Right(M(2),C(2)),BoatOnRight) | Config(Left(M(2),C(2)),Right(M(1),C(1)),BoatOnLeft). 23 -Config(Left(M(1),C(1)),Right(M(2),C(2)),BoatOnRight) | Config(Left(M(3),C(1)),Right(M(0),C(2)),BoatOnLeft). 24 -Config(Left(M(2),C(2)),Right(M(1),C(1)),BoatOnRight) | Config(Left(M(3),C(3)),Right(M(0),C(0)),BoatOnLeft). 25 -Config(Left(M(2),C(2)),Right(M(1),C(1)),BoatOnRight) | Config(Left(M(3),C(2)),Right(M(0),C(1)),BoatOnLeft). 26 -Config(Left(M(3),C(0)),Right(M(0),C(3)),BoatOnRight) | Config(Left(M(3),C(2)),Right(M(0),C(1)),BoatOnLeft). 27 -Config(Left(M(3),C(0)),Right(M(0),C(3)),BoatOnRight) | Config(Left(M(3),C(1)),Right(M(0),C(2)),BoatOnLeft). 28 -Config(Left(M(3),C(1)),Right(M(0),C(2)),BoatOnRight) | Config(Left(M(3),C(3)),Right(M(0),C(0)),BoatOnLeft). 29 -Config(Left(M(3),C(1)),Right(M(0),C(2)),BoatOnRight) | Config(Left(M(3),C(2)),Right(M(0),C(1)),BoatOnLeft). 30 -Config(Left(M(3),C(2)),Right(M(0),C(1)),BoatOnRight) | Config(Left(M(3),C(3)),Right(M(0),C(0)),BoatOnLeft). end_of_list. list(sos). 31 Config(Left(M(3),C(3)),Right(M(0),C(0)),BoatOnLeft). 32 -Config(Left(M(0),C(0)),Right(M(3),C(3)),BoatOnRight). end_of_list. ---------------- PROOF ---------------- 2 -Config(Left(M(3),C(3)),Right(M(0),C(0)),BoatOnLeft) | Config(Left(M(2),C(2)),Right(M(1),C(1)),BoatOnRight). 3 -Config(Left(M(3),C(2)),Right(M(0),C(1)),BoatOnLeft) | Config(Left(M(3),C(0)),Right(M(0),C(3)),BoatOnRight). 6 -Config(Left(M(3),C(1)),Right(M(0),C(2)),BoatOnLeft) | Config(Left(M(1),C(1)),Right(M(2),C(2)),BoatOnRight). 9 -Config(Left(M(2),C(2)),Right(M(1),C(1)),BoatOnLeft) | Config(Left(M(0),C(2)),Right(M(3),C(1)),BoatOnRight). 10 -Config(Left(M(1),C(1)),Right(M(2),C(2)),BoatOnLeft) | Config(Left(M(0),C(0)),Right(M(3),C(3)),BoatOnRight). 12 -Config(Left(M(0),C(3)),Right(M(3),C(0)),BoatOnLeft) | Config(Left(M(0),C(1)),Right(M(3),C(2)),BoatOnRight). 19 -Config(Left(M(0),C(1)),Right(M(3),C(2)),BoatOnRight) | Config(Left(M(1),C(1)),Right(M(2),C(2)),BoatOnLeft). 21 -Config(Left(M(0),C(2)),Right(M(3),C(1)),BoatOnRight) | Config(Left(M(0),C(3)),Right(M(3),C(0)),BoatOnLeft). 22 -Config(Left(M(1),C(1)),Right(M(2),C(2)),BoatOnRight) | Config(Left(M(2),C(2)),Right(M(1),C(1)),BoatOnLeft). 25 -Config(Left(M(2),C(2)),Right(M(1),C(1)),BoatOnRight) | Config(Left(M(3),C(2)),Right(M(0),C(1)),BoatOnLeft). 27 -Config(Left(M(3),C(0)),Right(M(0),C(3)),BoatOnRight) | Config(Left(M(3),C(1)),Right(M(0),C(2)),BoatOnLeft). 31 Config(Left(M(3),C(3)),Right(M(0),C(0)),BoatOnLeft). 32 -Config(Left(M(0),C(0)),Right(M(3),C(3)),BoatOnRight). 33 (31,2) Config(Left(M(2),C(2)),Right(M(1),C(1)),BoatOnRight). 35 (33,25) Config(Left(M(3),C(2)),Right(M(0),C(1)),BoatOnLeft). 36 (35,3) Config(Left(M(3),C(0)),Right(M(0),C(3)),BoatOnRight). 37 (36,27) Config(Left(M(3),C(1)),Right(M(0),C(2)),BoatOnLeft). 38 (37,6) Config(Left(M(1),C(1)),Right(M(2),C(2)),BoatOnRight). 39 (38,22) Config(Left(M(2),C(2)),Right(M(1),C(1)),BoatOnLeft). 40 (39,9) Config(Left(M(0),C(2)),Right(M(3),C(1)),BoatOnRight). 41 (40,21) Config(Left(M(0),C(3)),Right(M(3),C(0)),BoatOnLeft). 42 (41,12) Config(Left(M(0),C(1)),Right(M(3),C(2)),BoatOnRight). 43 (42,19) Config(Left(M(1),C(1)),Right(M(2),C(2)),BoatOnLeft). 45 (43,10) Config(Left(M(0),C(0)),Right(M(3),C(3)),BoatOnRight). 46 (45,32) . --------------- options --------------- set(hyper_res). set(demod_hist). set(for_sub). set(print_kept). set(back_sub). set(print_back_sub). set(print_given). set(check_arity). clear(binary_res). clear(UR_res). clear(para_from). clear(para_into). clear(demod_inf). clear(para_from_left). clear(para_from_right). clear(para_into_vars). clear(para_from_vars). clear(para_all). clear(para_ones_rule). clear(no_para_into_left). clear(no_para_into_right). clear(demod_linear). clear(print_gen). clear(sort_literals). clear(Unit_deletion). clear(factor). clear(print_weight). clear(sos_fifo). clear(bird_print). clear(atom_wt_max_args). clear(print_lists_at_end). clear(free_all_mem). clear(for_sub_fpa). clear(no_fapl). clear(no_fanl). assign(report, 0). assign(max_seconds, 0). assign(max_given, 0). assign(max_kept, 0). assign(max_gen, 0). assign(max_mem, 0). assign(max_weight, 0). assign(max_literals, 0). assign(fpa_literals, 4). assign(fpa_terms, 4). assign(demod_limit, 100). assign(max_proofs, 1). assign(neg_weight, 0). -------------- statistics ------------- clauses input 32 clauses given 13 clauses generated 16 demodulation rewrites 0 clauses wt or lit delete 0 tautologies deleted 0 clauses forward subsumed 2 (clauses subsumed by sos) 0 unit deletions 0 clauses kept 14 empty clauses 1 factors generated 0 clauses back subsumed 24 clauses not processed 2 ----------- times (seconds) ----------- run time 1.60 input time 0.82 binary_res time 0.00 hyper_res time 0.10 UR_res time 0.00 para_into time 0.00 para_from time 0.00 pre_process time 0.08 demod time 0.00 weigh time 0.00 for_sub time 0.00 unit_del time 0.00 post_process time 0.42 back_sub time 0.12 conflict time 0.04 factor time 0.00 FPA build time 0.16 IS build time 0.06 print_cl time 0.34 cl integrate time 0.12 window time 0.00 SHAR_EOF # End of shell archive exit 0