Solve Sudoku Puzzle #2

This solver uses a totally different approach. It uses logical theorem proving. For example, the assertion "square(1,1,3)" means there is a 3 in the top left corner. And "-square(x,y,1) | -square(x,y,2)" means you cannot have a 1 and 2 in the same cell. It uses a theorem prover called "prover9" to do the logical inferencing. And it also relies on another program to communicate with prover9 (not listed here).

Initial state
(4x4): 3 . | . . . . | . 1 -----+----- 2 . | . 4 . . | . .
Final state
(4x4): 3 1 | 4 2 4 2 | 3 1 -----+----- 2 3 | 1 4 1 4 | 2 3

Initial state (9x9):
 .  3  .  |  4  .  .  |  .  9  5
 .  .  4  |  .  5  2  |  .  .  .
 8  .  .  |  .  .  .  |  7  .  .
 ----------+-----------+----------
 .  .  .  |  .  1  .  |  9  4  .
 2  .  .  |  .  .  .  |  .  .  7
 .  5  3  |  .  6  .  |  .  .  .
 ----------+-----------+----------
 .  .  2  |  .  .  .  |  .  .  6
 .  .  .  |  6  3  .  |  4  .  .
 3  4  .  |  .  .  7  |  .  8  .
Final state (9x9):
 6  3  1  |  4  7  8  |  2  9  5
 9  7  4  |  3  5  2  |  1  6  8
 8  2  5  |  1  9  6  |  7  3  4
 ----------+-----------+----------
 7  6  8  |  2  1  5  |  9  4  3
 2  1  9  |  8  4  3  |  6  5  7
 4  5  3  |  7  6  9  |  8  1  2
 ----------+-----------+----------
 1  9  2  |  5  8  4  |  3  7  6
 5  8  7  |  6  3  1  |  4  2  9
 3  4  6  |  9  2  7  |  5  8  1

src/sudoku.c - 4x4 solver

   1: #include <stdio.h>
   2: 
   3: #include "../inc/split_stdin.h"
   4: 
   5: int side = 2;
   6: int size = 4;
   7: 
   8: char state[9][9];	// '0' = blank, else '1', etc
   9: int possible[9][9][9];	// Only meaningful if state = '0'
  10: 
  11: int num_fields;
  12: char **response;
  13: 
  14: void initial_rules() {
  15:     int i, j, k, l;
  16: 
  17:     // Every square contains a 1, 2, 3 ... size.
  18:     printf("tell square(x,y,1)");
  19:     for (i=2; i<=size; i++) {
  20: 	printf(" | square(x,y,%d)", i);
  21:     }
  22:     printf("\n");
  23: 
  24:     for (i=1; i<size; i++) {
  25: 	for (j=i+1; j<=size; j++) {
  26: 	    // A square cannot contain more than 1 number.
  27:             printf("tell -square(x,y,%d) | -square(x,y,%d)\n", i, j);
  28: 
  29: 	    // A row cannot have duplicate numbers in any column.
  30:             printf("tell -square(x,%d,z) | -square(x,%d,z)\n", i, j);
  31: 
  32: 	    // A column cannot have duplicate numbers in any row.
  33:             printf("tell -square(%d,y,z) | -square(%d,y,z)\n", i, j);
  34: 	}
  35:     }
  36: 
  37:     // Pretty nasty code here, sorry. i,j are the blocks
  38:     // in the puzzle. k,l are each square inside the block.
  39:     for (i=0; i<size; i+=side) {
  40: 	for (j=0; j<size; j+=side) {
  41: 	    for (k=0; k<size; k++) {
  42: 		for (l=k+1; l<size; l++) {
  43: 		    // Each block cannot have duplicate values.
  44: 		    printf("tell -square(%d,%d,z) | -square(%d,%d,z)\n",
  45: 			    i+(k/side)+1, j+(k%side)+1,
  46: 			    i+(l/side)+1, j+(l%side)+1);
  47: 		}
  48: 	    }
  49: 	}
  50:     }
  51: 
  52:     fflush(stdout);
  53: }
  54: 
  55: // void prt(char *ttl) {
  56: //     int row, col;
  57: //     char ch;
  58: // 
  59: //     fprintf(stderr, "%s\n", ttl);
  60: //     for (row=1; row<=size; row++) {
  61: // 	for (col=1; col<=size; col++) {
  62: // 	    ch = state[row-1][col-1];
  63: // 	    if (ch == '0') ch = '.';
  64: // 	    fprintf(stderr, " %c", ch);
  65: // 	    if (col == 2 && col < size) fprintf(stderr, " |");
  66: // 	}
  67: // 	fprintf(stderr, "\n");
  68: // 	if (row == 2 && row < size) {
  69: // 	    fprintf(stderr, "-----");
  70: // 	    for (col=1; col<side; col++) {
  71: // 		fprintf(stderr, "+-----");
  72: // 	    }
  73: // 	    fprintf(stderr, "\n");
  74: // 	}
  75: //     }
  76: //     fflush(stderr);
  77: // }
  78: 
  79: // Return codes for 'try'
  80: #define TRY_WON 0
  81: #define TRY_LOST 1
  82: #define TRY_WORKED 2
  83: #define TRY_FAILED 3
  84: 
  85: int try(int row, int col, int val) {
  86:     int ret = TRY_FAILED;
  87: 
  88:     printf("ask square(%d,%d,%d)\n", row, col, val);
  89:     fflush(stdout);
  90:     // fprintf(stderr, "**** ask square(%d,%d,%d)\n", row, col, val);
  91:     // fflush(stderr);
  92: 
  93:     response = split_stdin(" ", &num_fields);
  94:     // fprintf(stderr, "**** response = %s\n", response[1]);
  95:     // fflush(stderr);
  96:     if (num_fields >= 2 && strcmp(response[1], "true") == 0) {
  97: 	state[row-1][col-1] = val + '0';
  98: 	printf("tell square(%d,%d,%d)\n", row, col, val);
  99: 	fflush(stdout);
 100: 
 101: 	// See if we finished
 102: 	printf("%d %d %d\n", row, col, val);
 103: 	fflush(stdout);
 104: 	free_split_stdin(response, num_fields);
 105: 	response = split_stdin(" ", &num_fields);
 106: 	if (strcmp(response[0], "win") == 0) {
 107: 	    ret = TRY_WON;
 108: 	}
 109: 	else if (strcmp(response[0], "correct") == 0) {
 110: 	    ret = TRY_WORKED;
 111: 	}
 112: 	else if (strcmp(response[0], "lose") == 0) {
 113: 	    ret = TRY_LOST;
 114: 	}
 115: 	else {
 116: 	    fprintf(stderr, "Invalid response in try: %s\n", response[0]);
 117: 	    fflush(stderr);
 118: 	    ret = TRY_LOST;
 119: 	}
 120: 
 121: 	// prt("State:");
 122:     }
 123:     else if (num_fields >= 2 && strcmp(response[1], "false") == 0) {
 124: 	// Don't keep asking the same impossible choice
 125: 	possible[row-1][col-1][val-1] = 0;
 126: 	ret = TRY_FAILED;
 127:     }
 128:     free_split_stdin(response, num_fields);
 129: 
 130:     return ret;
 131: }
 132: 
 133: int main(int argc, char *argv[]) {
 134:     int row, col;
 135:     char ch;
 136:     int val;
 137:     int more;
 138:     int ret;
 139:     int done;
 140: 
 141:     // See if we are doing a 9 x 9 puzzle
 142:     if (argc == 2 && strcmp(argv[1], "9") == 0) {
 143: 	size = 9;
 144: 	side = 3;
 145:     }
 146: 
 147:     response = split_stdin(" ", &num_fields);
 148:     if (num_fields != size*size) {
 149: 	fprintf(stderr, "\nNumber of fields must be %d, not %d (%s)\n",
 150: 		size*size, num_fields, response[0]);
 151: 	fflush(stderr);
 152: 	exit(1);
 153:     }
 154: 
 155:     // Set up Sudoku game rules
 156:     initial_rules();
 157: 
 158:     // Read initial state
 159:     for (col=1; col<=size; col++) {
 160: 	for (row=1; row<=size; row++) {
 161: 	    ch = *response[size*(row-1)+col-1];
 162: 	    if (ch >= '1' && ch <= ('0'+size)) {
 163: 		printf("tell square(%d,%d,%c)\n", row, col, ch);
 164: 		fflush(stdout);
 165: 	    }
 166: 	    else if (ch == '0') {
 167: 		for (val=1; val<=size; val++) {
 168: 		    possible[row-1][col-1][val-1] = 1;
 169: 		}
 170: 	    }
 171: 	    else {
 172: 		fprintf(stderr, "Invalid code, row=%d col=%d code=%d\n",
 173: 			row, col, ch);
 174: 		fflush(stderr);
 175: 	    }
 176: 	    state[row-1][col-1] = ch;
 177: 	}
 178:     }
 179:     free_split_stdin(response, num_fields);
 180:     
 181:     // Look for possible moves
 182:     more = 1;
 183:     done = 0;
 184:     while (more && !done) {
 185: 	more = 0;
 186: 	for (row=1; row<=size; row++) {
 187: 	    for (col=1; col<=size; col++) {
 188: 		if (state[row-1][col-1] == '0') {
 189: 		    for (val=1; val<=size; val++) {
 190: 			if (possible[row-1][col-1][val-1]) {
 191: 			    ret = try(row, col, val);
 192: 			    if (ret == TRY_LOST || ret == TRY_WON) {
 193: 				done = 1;
 194: 				break;
 195: 			    }
 196: 			    else if (ret == TRY_WORKED) {
 197: 				more = 1;
 198: 			    }
 199: 			}
 200: 		    }
 201: 		}
 202: 		if (done) break;
 203: 	    }
 204: 	    if (done) break;
 205: 	}
 206:     }
 207: 
 208:     if (done && ret == TRY_WON) fprintf(stderr, "*** WON ***\n");
 209:     else if (done && ret == TRY_LOST) fprintf(stderr, "*** LOST ***\n");
 210:     else fprintf(stderr, "Unable to find a valid solution.\n");
 211:     fflush(stderr);
 212:     
 213:     // prt("Final State");
 214:     exit(0);
 215: }
 216: 

src/sudoku9.c - 9x9 solver

   1: #include <stdio.h>
   2: 
   3: #include "../inc/split_stdin.h"
   4: 
   5: int state[9][9];
   6: int blanks = 0;
   7: int rows = 0;
   8: 
   9: int num_fields;
  10: char **response;
  11: 
  12: void addRow(char *row) {
  13:     int j;
  14:     char ch;
  15: 
  16:     for (j=0; j<9; j++) {
  17: 	ch = row[j];
  18: 	if (ch == '.') {
  19: 	    state[rows][j] = 0;
  20: 	    blanks++;
  21: 	}
  22: 	else state[rows][j] = ch - '0';
  23:     }
  24:     rows++;
  25: }
  26: 
  27: void prt() {
  28:     int row, col;
  29: 
  30:     for (row=0; row<9; row++) {
  31: 	for (col=0; col<9; col++) {
  32: 	    if (state[row][col] == 0) fprintf(stderr, " .");
  33: 	    else fprintf(stderr, " %d", state[row][col]);
  34: 	    if (col == 2 || col == 5) fprintf(stderr, " |");
  35: 	}
  36: 	fprintf(stderr, "\n");
  37: 	if (row == 2 || row == 5) fprintf(stderr, "-------+-------+-------\n");
  38:     }
  39:     fprintf(stderr, "\n");
  40:     fflush(stderr);
  41: }
  42: 
  43: int main(int argc, char *argv[]) {
  44:     int which = 1;
  45:     int row, col, val;
  46: 
  47:     if (argc == 2) which = *argv[1] - '0';
  48:     fprintf(stderr, "Sample = %d\n", which);
  49: 
  50:     switch (which) {
  51: 	default :
  52: 	case 1 :
  53: 	    addRow("96..23..."); addRow("1.7.8...6"); addRow(".....6752");
  54: 	    addRow("......419"); addRow("8.31.25.."); addRow("7.16.4...");
  55: 	    addRow(".3....698"); addRow(".1824...."); addRow("...36..2.");
  56: 	    break;
  57: 	case 2 :
  58: 	    addRow("..4...918"); addRow("...4....."); addRow("1..2..3..");
  59: 	    addRow("8.762...."); addRow(".31...65."); addRow("....378.2");
  60: 	    addRow("..3..4..5"); addRow(".....2..."); addRow("562...1..");
  61: 	    break;
  62: 	case 3 :
  63: 	    addRow(".3.4...95"); addRow("..4.52..."); addRow("8.....7..");
  64: 	    addRow("....1.94."); addRow("2.......7"); addRow(".53.6....");
  65: 	    addRow("..2.....6"); addRow("...63.4.."); addRow("34...7.8.");
  66: 	    break;
  67: 	case 4 :
  68: 	    addRow("4.586...."); addRow("36....9.."); addRow("..9..3...");
  69: 	    addRow("...3....4"); addRow(".7..1..5."); addRow("6....5...");
  70: 	    addRow("...6..5.."); addRow("..1....92"); addRow("....971.3");
  71: 	    break;
  72:     }
  73:     prt();
  74: 
  75:     // Initial state -- send to agent
  76:     for (row=0; row<9; row++) {
  77: 	for (col=0; col<9; col++) {
  78: 	    printf(" %d", state[row][col]);
  79: 	}
  80:     }
  81:     printf("\n");
  82:     fflush(stdout);
  83: 
  84:     while (blanks > 0) {
  85: 	response = split_stdin(" ", &num_fields);
  86: 	if (num_fields != 3) {
  87: 	    fprintf(stderr, "Invalid input. Should have 3 values\n");
  88: 	    exit(1);
  89: 	}
  90: 	row = atoi(response[0]) - 1;
  91: 	col = atoi(response[1]) - 1;
  92: 	val = atoi(response[2]);
  93: 	if (state[row][col] != 0) {
  94: 	    printf("lose\n");
  95: 	}
  96: 	else {
  97: 	    state[row][col] = val;
  98: 	    prt();
  99: 	    blanks--;
 100: 	    if (blanks == 0) printf("win\n");
 101: 	    else printf("correct\n");
 102: 	}
 103: 	fflush(stdout);
 104: 	free_split_stdin(response, num_fields);
 105:     }
 106: 
 107:     exit(0);
 108: }
 109: 

src/split_stdin.c - line reader

   1: #include <stdio.h>
   2: #include <stdlib.h>
   3: #include <string.h>
   4: 
   5: #include "../inc/split_stdin.h"
   6: 
   7: /* splits a line from stdin into several strings.
   8: * A line is assumed to consist of several fields separated by
   9: * characters from separators.
  10: * num_fields is set to the number of strings.
  11: * num_fields is -1 if EOF before any strings are found.
  12: */
  13: 
  14: char **split_stdin(char *separators, int *num_fields) {
  15:     int c, nfields, nchars, clen, flen;
  16:     char *current;
  17:     char **fields;
  18:     current = (char *) calloc(10, sizeof(char));
  19:     clen = 10;
  20:     nchars = 0;
  21:     fields = (char **) calloc(10, sizeof(char *));
  22:     flen = 10;
  23:     nfields = 0;
  24:     do {
  25:         c = getc(stdin);
  26:         if (NULL == strchr(separators,c) && '\n' != c && EOF != c) {
  27:             if (nchars == clen) {
  28:                 clen += clen;
  29:                 current = (char *) realloc(current, clen * sizeof(char));
  30:             }
  31:             current[nchars] = c;
  32:             nchars++;
  33:         }
  34:         else if (nchars > 0) {
  35:             current = (char *) realloc(current, (nchars+1) * sizeof(char));
  36:             current[nchars] = '\0';
  37:             if (nfields == flen) {
  38:                 flen += flen;
  39:                 fields = (char **) realloc(fields, flen * sizeof(char *));
  40:             }
  41:             fields[nfields] = current;
  42:             nfields++;
  43:             current = (char *) calloc(10, sizeof(char));
  44:             clen = 10;
  45:             nchars = 0;
  46:         }
  47:     }
  48:     while ('\n' != c && EOF != c);
  49: 
  50:     free(current);
  51:     fields = (char **) realloc(fields, nfields * sizeof(char *));
  52:     if (EOF == c && nfields == 0) nfields = -1;
  53:     *num_fields = nfields;
  54:     return fields;
  55: }
  56: 
  57: /* Free up memory allocated by by split_stdin.
  58: * response is the data returned by a call to split_stdin.
  59: * num_fields is the number of strings in response.
  60: */
  61: 
  62: void free_split_stdin(char **response, int num_fields) {
  63:     int i;
  64:     for (i = 0; i < num_fields; i++) free(response[i]);
  65:     free(response);
  66: }
  67: 

inc/split_stdin.h - line reader

   1: /* split_stdin.h */
   2: 
   3: char **split_stdin(char *separators, int *num_fields);
   4: 
   5: void free_split_stdin(char **response, int num_fields);
   6: 

Makefile - make file

   1: all : lab2 sudoku9
   2: 
   3: lab2 : src/sudoku.c src/split_stdin.c
   4: 	gcc src/sudoku.c src/split_stdin.c -o lab2
   5: 
   6: sudoku9 : src/sudoku9.c src/split_stdin.c
   7: 	gcc src/sudoku9.c src/split_stdin.c -o sudoku9
   8: 
   9: 

sudoku4.out - detailed 4x4 output

   1: 
   2:  3 . | . .
   3:  . . | . 1
   4: -----+-----
   5:  2 . | . 4
   6:  . . | . .
   7: 
   8: sudoku4 -v:  3 0 0 0 0 0 0 1 2 0 0 4 0 0 0 0
   9: ./lab2: tell square(x,y,1) | square(x,y,2) | square(x,y,3) | square(x,y,4)
  10: ./lab2: tell -square(x,y,1) | -square(x,y,2)
  11: ./lab2: tell -square(x,1,z) | -square(x,2,z)
  12: ./lab2: tell -square(1,y,z) | -square(2,y,z)
  13: ./lab2: tell -square(x,y,1) | -square(x,y,3)
  14: ./lab2: tell -square(x,1,z) | -square(x,3,z)
  15: ./lab2: tell -square(1,y,z) | -square(3,y,z)
  16: ./lab2: tell -square(x,y,1) | -square(x,y,4)
  17: ./lab2: tell -square(x,1,z) | -square(x,4,z)
  18: ./lab2: tell -square(1,y,z) | -square(4,y,z)
  19: ./lab2: tell -square(x,y,2) | -square(x,y,3)
  20: ./lab2: tell -square(x,2,z) | -square(x,3,z)
  21: ./lab2: tell -square(2,y,z) | -square(3,y,z)
  22: ./lab2: tell -square(x,y,2) | -square(x,y,4)
  23: ./lab2: tell -square(x,2,z) | -square(x,4,z)
  24: ./lab2: tell -square(2,y,z) | -square(4,y,z)
  25: ./lab2: tell -square(x,y,3) | -square(x,y,4)
  26: ./lab2: tell -square(x,3,z) | -square(x,4,z)
  27: ./lab2: tell -square(3,y,z) | -square(4,y,z)
  28: ./lab2: tell -square(1,1,z) | -square(1,2,z)
  29: ./lab2: tell -square(1,1,z) | -square(2,1,z)
  30: ./lab2: tell -square(1,1,z) | -square(2,2,z)
  31: ./lab2: tell -square(1,2,z) | -square(2,1,z)
  32: ./lab2: tell -square(1,2,z) | -square(2,2,z)
  33: ./lab2: tell -square(2,1,z) | -square(2,2,z)
  34: ./lab2: tell -square(1,3,z) | -square(1,4,z)
  35: ./lab2: tell -square(1,3,z) | -square(2,3,z)
  36: ./lab2: tell -square(1,3,z) | -square(2,4,z)
  37: ./lab2: tell -square(1,4,z) | -square(2,3,z)
  38: ./lab2: tell -square(1,4,z) | -square(2,4,z)
  39: ./lab2: tell -square(2,3,z) | -square(2,4,z)
  40: ./lab2: tell -square(3,1,z) | -square(3,2,z)
  41: ./lab2: tell -square(3,1,z) | -square(4,1,z)
  42: ./lab2: tell -square(3,1,z) | -square(4,2,z)
  43: ./lab2: tell -square(3,2,z) | -square(4,1,z)
  44: ./lab2: tell -square(3,2,z) | -square(4,2,z)
  45: ./lab2: tell -square(4,1,z) | -square(4,2,z)
  46: ./lab2: tell -square(3,3,z) | -square(3,4,z)
  47: ./lab2: tell -square(3,3,z) | -square(4,3,z)
  48: ./lab2: tell -square(3,3,z) | -square(4,4,z)
  49: ./lab2: tell -square(3,4,z) | -square(4,3,z)
  50: ./lab2: tell -square(3,4,z) | -square(4,4,z)
  51: ./lab2: tell -square(4,3,z) | -square(4,4,z)
  52: ./lab2: tell square(1,1,3)
  53: ./lab2: tell square(3,1,2)
  54: ./lab2: tell square(2,4,1)
  55: ./lab2: tell square(3,4,4)
  56: ./lab2: ask square(1,2,1)
  57: prover9: answer true
  58: ./lab2: tell square(1,2,1)
  59: ./lab2: 1 2 1
  60: 
  61:  3 1 | . .
  62:  . . | . 1
  63: -----+-----
  64:  2 . | . 4
  65:  . . | . .
  66: 
  67: sudoku4 -v: correct
  68: ./lab2: ask square(1,2,2)
  69: prover9: answer false
  70: ./lab2: ask square(1,2,3)
  71: prover9: answer false
  72: ./lab2: ask square(1,2,4)
  73: prover9: answer false
  74: ./lab2: ask square(1,3,1)
  75: prover9: answer false
  76: ./lab2: ask square(1,3,2)
  77: prover9: answer false
  78: ./lab2: ask square(1,3,3)
  79: prover9: answer false
  80: ./lab2: ask square(1,3,4)
  81: prover9: answer true
  82: ./lab2: tell square(1,3,4)
  83: ./lab2: 1 3 4
  84: 
  85:  3 1 | 4 .
  86:  . . | . 1
  87: -----+-----
  88:  2 . | . 4
  89:  . . | . .
  90: 
  91: sudoku4 -v: correct
  92: ./lab2: ask square(1,4,1)
  93: prover9: answer false
  94: ./lab2: ask square(1,4,2)
  95: prover9: answer true
  96: ./lab2: tell square(1,4,2)
  97: ./lab2: 1 4 2
  98: 
  99:  3 1 | 4 2
 100:  . . | . 1
 101: -----+-----
 102:  2 . | . 4
 103:  . . | . .
 104: 
 105: sudoku4 -v: correct
 106: ./lab2: ask square(1,4,3)
 107: prover9: answer false
 108: ./lab2: ask square(1,4,4)
 109: prover9: answer false
 110: ./lab2: ask square(2,1,1)
 111: prover9: answer false
 112: ./lab2: ask square(2,1,2)
 113: prover9: answer false
 114: ./lab2: ask square(2,1,3)
 115: prover9: answer false
 116: ./lab2: ask square(2,1,4)
 117: prover9: answer true
 118: ./lab2: tell square(2,1,4)
 119: ./lab2: 2 1 4
 120: 
 121:  3 1 | 4 2
 122:  4 . | . 1
 123: -----+-----
 124:  2 . | . 4
 125:  . . | . .
 126: 
 127: sudoku4 -v: correct
 128: ./lab2: ask square(2,2,1)
 129: prover9: answer false
 130: ./lab2: ask square(2,2,2)
 131: prover9: answer true
 132: ./lab2: tell square(2,2,2)
 133: ./lab2: 2 2 2
 134: 
 135:  3 1 | 4 2
 136:  4 2 | . 1
 137: -----+-----
 138:  2 . | . 4
 139:  . . | . .
 140: 
 141: sudoku4 -v: correct
 142: ./lab2: ask square(2,2,3)
 143: prover9: answer false
 144: ./lab2: ask square(2,2,4)
 145: prover9: answer false
 146: ./lab2: ask square(2,3,1)
 147: prover9: answer false
 148: ./lab2: ask square(2,3,2)
 149: prover9: answer false
 150: ./lab2: ask square(2,3,3)
 151: prover9: answer true
 152: ./lab2: tell square(2,3,3)
 153: ./lab2: 2 3 3
 154: 
 155:  3 1 | 4 2
 156:  4 2 | 3 1
 157: -----+-----
 158:  2 . | . 4
 159:  . . | . .
 160: 
 161: sudoku4 -v: correct
 162: ./lab2: ask square(2,3,4)
 163: prover9: answer false
 164: ./lab2: ask square(3,2,1)
 165: prover9: answer false
 166: ./lab2: ask square(3,2,2)
 167: prover9: answer false
 168: ./lab2: ask square(3,2,3)
 169: prover9: answer true
 170: ./lab2: tell square(3,2,3)
 171: ./lab2: 3 2 3
 172: 
 173:  3 1 | 4 2
 174:  4 2 | 3 1
 175: -----+-----
 176:  2 3 | . 4
 177:  . . | . .
 178: 
 179: sudoku4 -v: correct
 180: ./lab2: ask square(3,2,4)
 181: prover9: answer false
 182: ./lab2: ask square(3,3,1)
 183: prover9: answer true
 184: ./lab2: tell square(3,3,1)
 185: ./lab2: 3 3 1
 186: 
 187:  3 1 | 4 2
 188:  4 2 | 3 1
 189: -----+-----
 190:  2 3 | 1 4
 191:  . . | . .
 192: 
 193: sudoku4 -v: correct
 194: ./lab2: ask square(3,3,2)
 195: prover9: answer false
 196: ./lab2: ask square(3,3,3)
 197: prover9: answer false
 198: ./lab2: ask square(3,3,4)
 199: prover9: answer false
 200: ./lab2: ask square(4,1,1)
 201: prover9: answer true
 202: ./lab2: tell square(4,1,1)
 203: ./lab2: 4 1 1
 204: 
 205:  3 1 | 4 2
 206:  4 2 | 3 1
 207: -----+-----
 208:  2 3 | 1 4
 209:  1 . | . .
 210: 
 211: sudoku4 -v: correct
 212: ./lab2: ask square(4,1,2)
 213: prover9: answer false
 214: ./lab2: ask square(4,1,3)
 215: prover9: answer false
 216: ./lab2: ask square(4,1,4)
 217: prover9: answer false
 218: ./lab2: ask square(4,2,1)
 219: prover9: answer false
 220: ./lab2: ask square(4,2,2)
 221: prover9: answer false
 222: ./lab2: ask square(4,2,3)
 223: prover9: answer false
 224: ./lab2: ask square(4,2,4)
 225: prover9: answer true
 226: ./lab2: tell square(4,2,4)
 227: ./lab2: 4 2 4
 228: 
 229:  3 1 | 4 2
 230:  4 2 | 3 1
 231: -----+-----
 232:  2 3 | 1 4
 233:  1 4 | . .
 234: 
 235: sudoku4 -v: correct
 236: ./lab2: ask square(4,3,1)
 237: prover9: answer false
 238: ./lab2: ask square(4,3,2)
 239: prover9: answer true
 240: ./lab2: tell square(4,3,2)
 241: ./lab2: 4 3 2
 242: 
 243:  3 1 | 4 2
 244:  4 2 | 3 1
 245: -----+-----
 246:  2 3 | 1 4
 247:  1 4 | 2 .
 248: 
 249: sudoku4 -v: correct
 250: ./lab2: ask square(4,3,3)
 251: prover9: answer false
 252: ./lab2: ask square(4,3,4)
 253: prover9: answer false
 254: ./lab2: ask square(4,4,1)
 255: prover9: answer false
 256: ./lab2: ask square(4,4,2)
 257: prover9: answer false
 258: ./lab2: ask square(4,4,3)
 259: prover9: answer true
 260: ./lab2: tell square(4,4,3)
 261: ./lab2: 4 4 3
 262: 
 263:  3 1 | 4 2
 264:  4 2 | 3 1
 265: -----+-----
 266:  2 3 | 1 4
 267:  1 4 | 2 3
 268: 
 269: sudoku4 -v: win
 270: *** WON ***
 271: 

sudoku9.out - brief 9x9 output

   1: Sample = 3
   2:  . 3 . | 4 . . | . 9 5
   3:  . . 4 | . 5 2 | . . .
   4:  8 . . | . . . | 7 . .
   5: -------+-------+-------
   6:  . . . | . 1 . | 9 4 .
   7:  2 . . | . . . | . . 7
   8:  . 5 3 | . 6 . | . . .
   9: -------+-------+-------
  10:  . . 2 | . . . | . . 6
  11:  . . . | 6 3 . | 4 . .
  12:  3 4 . | . . 7 | . 8 .
  13: 
  14:  . 3 . | 4 7 . | . 9 5
  15:  . . 4 | . 5 2 | . . .
  16:  8 . . | . . . | 7 . .
  17: -------+-------+-------
  18:  . . . | . 1 . | 9 4 .
  19:  2 . . | . . . | . . 7
  20:  . 5 3 | . 6 . | . . .
  21: -------+-------+-------
  22:  . . 2 | . . . | . . 6
  23:  . . . | 6 3 . | 4 . .
  24:  3 4 . | . . 7 | . 8 .
  25: 
  26:  . 3 . | 4 7 8 | . 9 5
  27:  . . 4 | . 5 2 | . . .
  28:  8 . . | . . . | 7 . .
  29: -------+-------+-------
  30:  . . . | . 1 . | 9 4 .
  31:  2 . . | . . . | . . 7
  32:  . 5 3 | . 6 . | . . .
  33: -------+-------+-------
  34:  . . 2 | . . . | . . 6
  35:  . . . | 6 3 . | 4 . .
  36:  3 4 . | . . 7 | . 8 .
  37: 
  38:  . 3 . | 4 7 8 | 2 9 5
  39:  . . 4 | . 5 2 | . . .
  40:  8 . . | . . . | 7 . .
  41: -------+-------+-------
  42:  . . . | . 1 . | 9 4 .
  43:  2 . . | . . . | . . 7
  44:  . 5 3 | . 6 . | . . .
  45: -------+-------+-------
  46:  . . 2 | . . . | . . 6
  47:  . . . | 6 3 . | 4 . .
  48:  3 4 . | . . 7 | . 8 .
  49: 
  50:  . 3 . | 4 7 8 | 2 9 5
  51:  . . 4 | . 5 2 | . . .
  52:  8 2 . | . . . | 7 . .
  53: -------+-------+-------
  54:  . . . | . 1 . | 9 4 .
  55:  2 . . | . . . | . . 7
  56:  . 5 3 | . 6 . | . . .
  57: -------+-------+-------
  58:  . . 2 | . . . | . . 6
  59:  . . . | 6 3 . | 4 . .
  60:  3 4 . | . . 7 | . 8 .
  61: 
  62:  . 3 . | 4 7 8 | 2 9 5
  63:  . . 4 | . 5 2 | . . .
  64:  8 2 5 | . . . | 7 . .
  65: -------+-------+-------
  66:  . . . | . 1 . | 9 4 .
  67:  2 . . | . . . | . . 7
  68:  . 5 3 | . 6 . | . . .
  69: -------+-------+-------
  70:  . . 2 | . . . | . . 6
  71:  . . . | 6 3 . | 4 . .
  72:  3 4 . | . . 7 | . 8 .
  73: 
  74:  . 3 . | 4 7 8 | 2 9 5
  75:  . . 4 | . 5 2 | . . .
  76:  8 2 5 | . 9 . | 7 . .
  77: -------+-------+-------
  78:  . . . | . 1 . | 9 4 .
  79:  2 . . | . . . | . . 7
  80:  . 5 3 | . 6 . | . . .
  81: -------+-------+-------
  82:  . . 2 | . . . | . . 6
  83:  . . . | 6 3 . | 4 . .
  84:  3 4 . | . . 7 | . 8 .
  85: 
  86:  . 3 . | 4 7 8 | 2 9 5
  87:  . . 4 | . 5 2 | . . .
  88:  8 2 5 | . 9 6 | 7 . .
  89: -------+-------+-------
  90:  . . . | . 1 . | 9 4 .
  91:  2 . . | . . . | . . 7
  92:  . 5 3 | . 6 . | . . .
  93: -------+-------+-------
  94:  . . 2 | . . . | . . 6
  95:  . . . | 6 3 . | 4 . .
  96:  3 4 . | . . 7 | . 8 .
  97: 
  98:  . 3 . | 4 7 8 | 2 9 5
  99:  . . 4 | . 5 2 | . . .
 100:  8 2 5 | . 9 6 | 7 . 4
 101: -------+-------+-------
 102:  . . . | . 1 . | 9 4 .
 103:  2 . . | . . . | . . 7
 104:  . 5 3 | . 6 . | . . .
 105: -------+-------+-------
 106:  . . 2 | . . . | . . 6
 107:  . . . | 6 3 . | 4 . .
 108:  3 4 . | . . 7 | . 8 .
 109: 
 110:  . 3 . | 4 7 8 | 2 9 5
 111:  . . 4 | . 5 2 | . . .
 112:  8 2 5 | . 9 6 | 7 . 4
 113: -------+-------+-------
 114:  7 . . | . 1 . | 9 4 .
 115:  2 . . | . . . | . . 7
 116:  . 5 3 | . 6 . | . . .
 117: -------+-------+-------
 118:  . . 2 | . . . | . . 6
 119:  . . . | 6 3 . | 4 . .
 120:  3 4 . | . . 7 | . 8 .
 121: 
 122:  . 3 . | 4 7 8 | 2 9 5
 123:  . . 4 | . 5 2 | . . .
 124:  8 2 5 | . 9 6 | 7 . 4
 125: -------+-------+-------
 126:  7 6 . | . 1 . | 9 4 .
 127:  2 . . | . . . | . . 7
 128:  . 5 3 | . 6 . | . . .
 129: -------+-------+-------
 130:  . . 2 | . . . | . . 6
 131:  . . . | 6 3 . | 4 . .
 132:  3 4 . | . . 7 | . 8 .
 133: 
 134:  . 3 . | 4 7 8 | 2 9 5
 135:  . . 4 | . 5 2 | . . .
 136:  8 2 5 | . 9 6 | 7 . 4
 137: -------+-------+-------
 138:  7 6 8 | . 1 . | 9 4 .
 139:  2 . . | . . . | . . 7
 140:  . 5 3 | . 6 . | . . .
 141: -------+-------+-------
 142:  . . 2 | . . . | . . 6
 143:  . . . | 6 3 . | 4 . .
 144:  3 4 . | . . 7 | . 8 .
 145: 
 146:  . 3 . | 4 7 8 | 2 9 5
 147:  . . 4 | . 5 2 | . . .
 148:  8 2 5 | . 9 6 | 7 . 4
 149: -------+-------+-------
 150:  7 6 8 | 2 1 . | 9 4 .
 151:  2 . . | . . . | . . 7
 152:  . 5 3 | . 6 . | . . .
 153: -------+-------+-------
 154:  . . 2 | . . . | . . 6
 155:  . . . | 6 3 . | 4 . .
 156:  3 4 . | . . 7 | . 8 .
 157: 
 158:  . 3 . | 4 7 8 | 2 9 5
 159:  . . 4 | . 5 2 | . . .
 160:  8 2 5 | . 9 6 | 7 . 4
 161: -------+-------+-------
 162:  7 6 8 | 2 1 5 | 9 4 .
 163:  2 . . | . . . | . . 7
 164:  . 5 3 | . 6 . | . . .
 165: -------+-------+-------
 166:  . . 2 | . . . | . . 6
 167:  . . . | 6 3 . | 4 . .
 168:  3 4 . | . . 7 | . 8 .
 169: 
 170:  . 3 . | 4 7 8 | 2 9 5
 171:  . . 4 | . 5 2 | . . .
 172:  8 2 5 | . 9 6 | 7 . 4
 173: -------+-------+-------
 174:  7 6 8 | 2 1 5 | 9 4 3
 175:  2 . . | . . . | . . 7
 176:  . 5 3 | . 6 . | . . .
 177: -------+-------+-------
 178:  . . 2 | . . . | . . 6
 179:  . . . | 6 3 . | 4 . .
 180:  3 4 . | . . 7 | . 8 .
 181: 
 182:  . 3 . | 4 7 8 | 2 9 5
 183:  . . 4 | . 5 2 | . . .
 184:  8 2 5 | . 9 6 | 7 . 4
 185: -------+-------+-------
 186:  7 6 8 | 2 1 5 | 9 4 3
 187:  2 . . | 8 . . | . . 7
 188:  . 5 3 | . 6 . | . . .
 189: -------+-------+-------
 190:  . . 2 | . . . | . . 6
 191:  . . . | 6 3 . | 4 . .
 192:  3 4 . | . . 7 | . 8 .
 193: 
 194:  . 3 . | 4 7 8 | 2 9 5
 195:  . . 4 | . 5 2 | . . .
 196:  8 2 5 | . 9 6 | 7 . 4
 197: -------+-------+-------
 198:  7 6 8 | 2 1 5 | 9 4 3
 199:  2 . . | 8 4 . | . . 7
 200:  . 5 3 | . 6 . | . . .
 201: -------+-------+-------
 202:  . . 2 | . . . | . . 6
 203:  . . . | 6 3 . | 4 . .
 204:  3 4 . | . . 7 | . 8 .
 205: 
 206:  . 3 . | 4 7 8 | 2 9 5
 207:  . . 4 | . 5 2 | . . .
 208:  8 2 5 | . 9 6 | 7 . 4
 209: -------+-------+-------
 210:  7 6 8 | 2 1 5 | 9 4 3
 211:  2 . . | 8 4 3 | . . 7
 212:  . 5 3 | . 6 . | . . .
 213: -------+-------+-------
 214:  . . 2 | . . . | . . 6
 215:  . . . | 6 3 . | 4 . .
 216:  3 4 . | . . 7 | . 8 .
 217: 
 218:  . 3 . | 4 7 8 | 2 9 5
 219:  . . 4 | . 5 2 | . . .
 220:  8 2 5 | . 9 6 | 7 . 4
 221: -------+-------+-------
 222:  7 6 8 | 2 1 5 | 9 4 3
 223:  2 . . | 8 4 3 | . . 7
 224:  4 5 3 | . 6 . | . . .
 225: -------+-------+-------
 226:  . . 2 | . . . | . . 6
 227:  . . . | 6 3 . | 4 . .
 228:  3 4 . | . . 7 | . 8 .
 229: 
 230:  . 3 . | 4 7 8 | 2 9 5
 231:  . . 4 | . 5 2 | . . .
 232:  8 2 5 | . 9 6 | 7 . 4
 233: -------+-------+-------
 234:  7 6 8 | 2 1 5 | 9 4 3
 235:  2 . . | 8 4 3 | . . 7
 236:  4 5 3 | 7 6 . | . . .
 237: -------+-------+-------
 238:  . . 2 | . . . | . . 6
 239:  . . . | 6 3 . | 4 . .
 240:  3 4 . | . . 7 | . 8 .
 241: 
 242:  . 3 . | 4 7 8 | 2 9 5
 243:  . . 4 | . 5 2 | . . .
 244:  8 2 5 | . 9 6 | 7 . 4
 245: -------+-------+-------
 246:  7 6 8 | 2 1 5 | 9 4 3
 247:  2 . . | 8 4 3 | . . 7
 248:  4 5 3 | 7 6 9 | . . .
 249: -------+-------+-------
 250:  . . 2 | . . . | . . 6
 251:  . . . | 6 3 . | 4 . .
 252:  3 4 . | . . 7 | . 8 .
 253: 
 254:  . 3 . | 4 7 8 | 2 9 5
 255:  . . 4 | . 5 2 | . . .
 256:  8 2 5 | . 9 6 | 7 . 4
 257: -------+-------+-------
 258:  7 6 8 | 2 1 5 | 9 4 3
 259:  2 . . | 8 4 3 | . . 7
 260:  4 5 3 | 7 6 9 | . . .
 261: -------+-------+-------
 262:  . . 2 | . 8 . | . . 6
 263:  . . . | 6 3 . | 4 . .
 264:  3 4 . | . . 7 | . 8 .
 265: 
 266:  . 3 . | 4 7 8 | 2 9 5
 267:  . . 4 | . 5 2 | . . .
 268:  8 2 5 | . 9 6 | 7 . 4
 269: -------+-------+-------
 270:  7 6 8 | 2 1 5 | 9 4 3
 271:  2 . . | 8 4 3 | . . 7
 272:  4 5 3 | 7 6 9 | . . .
 273: -------+-------+-------
 274:  . . 2 | . 8 4 | . . 6
 275:  . . . | 6 3 . | 4 . .
 276:  3 4 . | . . 7 | . 8 .
 277: 
 278:  . 3 . | 4 7 8 | 2 9 5
 279:  . . 4 | . 5 2 | . . .
 280:  8 2 5 | . 9 6 | 7 . 4
 281: -------+-------+-------
 282:  7 6 8 | 2 1 5 | 9 4 3
 283:  2 . . | 8 4 3 | . . 7
 284:  4 5 3 | 7 6 9 | . . .
 285: -------+-------+-------
 286:  . . 2 | . 8 4 | . . 6
 287:  . . . | 6 3 1 | 4 . .
 288:  3 4 . | . . 7 | . 8 .
 289: 
 290:  . 3 . | 4 7 8 | 2 9 5
 291:  . . 4 | . 5 2 | . . .
 292:  8 2 5 | . 9 6 | 7 . 4
 293: -------+-------+-------
 294:  7 6 8 | 2 1 5 | 9 4 3
 295:  2 . . | 8 4 3 | . . 7
 296:  4 5 3 | 7 6 9 | . . .
 297: -------+-------+-------
 298:  . . 2 | . 8 4 | . . 6
 299:  . . . | 6 3 1 | 4 . .
 300:  3 4 . | . 2 7 | . 8 .
 301: 
 302:  . 3 . | 4 7 8 | 2 9 5
 303:  . . 4 | . 5 2 | . . .
 304:  8 2 5 | . 9 6 | 7 . 4
 305: -------+-------+-------
 306:  7 6 8 | 2 1 5 | 9 4 3
 307:  2 . . | 8 4 3 | . . 7
 308:  4 5 3 | 7 6 9 | . . .
 309: -------+-------+-------
 310:  . . 2 | . 8 4 | . . 6
 311:  . . . | 6 3 1 | 4 . .
 312:  3 4 . | . 2 7 | . 8 1
 313: 
 314:  6 3 . | 4 7 8 | 2 9 5
 315:  . . 4 | . 5 2 | . . .
 316:  8 2 5 | . 9 6 | 7 . 4
 317: -------+-------+-------
 318:  7 6 8 | 2 1 5 | 9 4 3
 319:  2 . . | 8 4 3 | . . 7
 320:  4 5 3 | 7 6 9 | . . .
 321: -------+-------+-------
 322:  . . 2 | . 8 4 | . . 6
 323:  . . . | 6 3 1 | 4 . .
 324:  3 4 . | . 2 7 | . 8 1
 325: 
 326:  6 3 1 | 4 7 8 | 2 9 5
 327:  . . 4 | . 5 2 | . . .
 328:  8 2 5 | . 9 6 | 7 . 4
 329: -------+-------+-------
 330:  7 6 8 | 2 1 5 | 9 4 3
 331:  2 . . | 8 4 3 | . . 7
 332:  4 5 3 | 7 6 9 | . . .
 333: -------+-------+-------
 334:  . . 2 | . 8 4 | . . 6
 335:  . . . | 6 3 1 | 4 . .
 336:  3 4 . | . 2 7 | . 8 1
 337: 
 338:  6 3 1 | 4 7 8 | 2 9 5
 339:  9 . 4 | . 5 2 | . . .
 340:  8 2 5 | . 9 6 | 7 . 4
 341: -------+-------+-------
 342:  7 6 8 | 2 1 5 | 9 4 3
 343:  2 . . | 8 4 3 | . . 7
 344:  4 5 3 | 7 6 9 | . . .
 345: -------+-------+-------
 346:  . . 2 | . 8 4 | . . 6
 347:  . . . | 6 3 1 | 4 . .
 348:  3 4 . | . 2 7 | . 8 1
 349: 
 350:  6 3 1 | 4 7 8 | 2 9 5
 351:  9 7 4 | . 5 2 | . . .
 352:  8 2 5 | . 9 6 | 7 . 4
 353: -------+-------+-------
 354:  7 6 8 | 2 1 5 | 9 4 3
 355:  2 . . | 8 4 3 | . . 7
 356:  4 5 3 | 7 6 9 | . . .
 357: -------+-------+-------
 358:  . . 2 | . 8 4 | . . 6
 359:  . . . | 6 3 1 | 4 . .
 360:  3 4 . | . 2 7 | . 8 1
 361: 
 362:  6 3 1 | 4 7 8 | 2 9 5
 363:  9 7 4 | 3 5 2 | . . .
 364:  8 2 5 | . 9 6 | 7 . 4
 365: -------+-------+-------
 366:  7 6 8 | 2 1 5 | 9 4 3
 367:  2 . . | 8 4 3 | . . 7
 368:  4 5 3 | 7 6 9 | . . .
 369: -------+-------+-------
 370:  . . 2 | . 8 4 | . . 6
 371:  . . . | 6 3 1 | 4 . .
 372:  3 4 . | . 2 7 | . 8 1
 373: 
 374:  6 3 1 | 4 7 8 | 2 9 5
 375:  9 7 4 | 3 5 2 | 1 . .
 376:  8 2 5 | . 9 6 | 7 . 4
 377: -------+-------+-------
 378:  7 6 8 | 2 1 5 | 9 4 3
 379:  2 . . | 8 4 3 | . . 7
 380:  4 5 3 | 7 6 9 | . . .
 381: -------+-------+-------
 382:  . . 2 | . 8 4 | . . 6
 383:  . . . | 6 3 1 | 4 . .
 384:  3 4 . | . 2 7 | . 8 1
 385: 
 386:  6 3 1 | 4 7 8 | 2 9 5
 387:  9 7 4 | 3 5 2 | 1 6 .
 388:  8 2 5 | . 9 6 | 7 . 4
 389: -------+-------+-------
 390:  7 6 8 | 2 1 5 | 9 4 3
 391:  2 . . | 8 4 3 | . . 7
 392:  4 5 3 | 7 6 9 | . . .
 393: -------+-------+-------
 394:  . . 2 | . 8 4 | . . 6
 395:  . . . | 6 3 1 | 4 . .
 396:  3 4 . | . 2 7 | . 8 1
 397: 
 398:  6 3 1 | 4 7 8 | 2 9 5
 399:  9 7 4 | 3 5 2 | 1 6 8
 400:  8 2 5 | . 9 6 | 7 . 4
 401: -------+-------+-------
 402:  7 6 8 | 2 1 5 | 9 4 3
 403:  2 . . | 8 4 3 | . . 7
 404:  4 5 3 | 7 6 9 | . . .
 405: -------+-------+-------
 406:  . . 2 | . 8 4 | . . 6
 407:  . . . | 6 3 1 | 4 . .
 408:  3 4 . | . 2 7 | . 8 1
 409: 
 410:  6 3 1 | 4 7 8 | 2 9 5
 411:  9 7 4 | 3 5 2 | 1 6 8
 412:  8 2 5 | 1 9 6 | 7 . 4
 413: -------+-------+-------
 414:  7 6 8 | 2 1 5 | 9 4 3
 415:  2 . . | 8 4 3 | . . 7
 416:  4 5 3 | 7 6 9 | . . .
 417: -------+-------+-------
 418:  . . 2 | . 8 4 | . . 6
 419:  . . . | 6 3 1 | 4 . .
 420:  3 4 . | . 2 7 | . 8 1
 421: 
 422:  6 3 1 | 4 7 8 | 2 9 5
 423:  9 7 4 | 3 5 2 | 1 6 8
 424:  8 2 5 | 1 9 6 | 7 3 4
 425: -------+-------+-------
 426:  7 6 8 | 2 1 5 | 9 4 3
 427:  2 . . | 8 4 3 | . . 7
 428:  4 5 3 | 7 6 9 | . . .
 429: -------+-------+-------
 430:  . . 2 | . 8 4 | . . 6
 431:  . . . | 6 3 1 | 4 . .
 432:  3 4 . | . 2 7 | . 8 1
 433: 
 434:  6 3 1 | 4 7 8 | 2 9 5
 435:  9 7 4 | 3 5 2 | 1 6 8
 436:  8 2 5 | 1 9 6 | 7 3 4
 437: -------+-------+-------
 438:  7 6 8 | 2 1 5 | 9 4 3
 439:  2 1 . | 8 4 3 | . . 7
 440:  4 5 3 | 7 6 9 | . . .
 441: -------+-------+-------
 442:  . . 2 | . 8 4 | . . 6
 443:  . . . | 6 3 1 | 4 . .
 444:  3 4 . | . 2 7 | . 8 1
 445: 
 446:  6 3 1 | 4 7 8 | 2 9 5
 447:  9 7 4 | 3 5 2 | 1 6 8
 448:  8 2 5 | 1 9 6 | 7 3 4
 449: -------+-------+-------
 450:  7 6 8 | 2 1 5 | 9 4 3
 451:  2 1 9 | 8 4 3 | . . 7
 452:  4 5 3 | 7 6 9 | . . .
 453: -------+-------+-------
 454:  . . 2 | . 8 4 | . . 6
 455:  . . . | 6 3 1 | 4 . .
 456:  3 4 . | . 2 7 | . 8 1
 457: 
 458:  6 3 1 | 4 7 8 | 2 9 5
 459:  9 7 4 | 3 5 2 | 1 6 8
 460:  8 2 5 | 1 9 6 | 7 3 4
 461: -------+-------+-------
 462:  7 6 8 | 2 1 5 | 9 4 3
 463:  2 1 9 | 8 4 3 | 6 . 7
 464:  4 5 3 | 7 6 9 | . . .
 465: -------+-------+-------
 466:  . . 2 | . 8 4 | . . 6
 467:  . . . | 6 3 1 | 4 . .
 468:  3 4 . | . 2 7 | . 8 1
 469: 
 470:  6 3 1 | 4 7 8 | 2 9 5
 471:  9 7 4 | 3 5 2 | 1 6 8
 472:  8 2 5 | 1 9 6 | 7 3 4
 473: -------+-------+-------
 474:  7 6 8 | 2 1 5 | 9 4 3
 475:  2 1 9 | 8 4 3 | 6 5 7
 476:  4 5 3 | 7 6 9 | . . .
 477: -------+-------+-------
 478:  . . 2 | . 8 4 | . . 6
 479:  . . . | 6 3 1 | 4 . .
 480:  3 4 . | . 2 7 | . 8 1
 481: 
 482:  6 3 1 | 4 7 8 | 2 9 5
 483:  9 7 4 | 3 5 2 | 1 6 8
 484:  8 2 5 | 1 9 6 | 7 3 4
 485: -------+-------+-------
 486:  7 6 8 | 2 1 5 | 9 4 3
 487:  2 1 9 | 8 4 3 | 6 5 7
 488:  4 5 3 | 7 6 9 | 8 . .
 489: -------+-------+-------
 490:  . . 2 | . 8 4 | . . 6
 491:  . . . | 6 3 1 | 4 . .
 492:  3 4 . | . 2 7 | . 8 1
 493: 
 494:  6 3 1 | 4 7 8 | 2 9 5
 495:  9 7 4 | 3 5 2 | 1 6 8
 496:  8 2 5 | 1 9 6 | 7 3 4
 497: -------+-------+-------
 498:  7 6 8 | 2 1 5 | 9 4 3
 499:  2 1 9 | 8 4 3 | 6 5 7
 500:  4 5 3 | 7 6 9 | 8 1 .
 501: -------+-------+-------
 502:  . . 2 | . 8 4 | . . 6
 503:  . . . | 6 3 1 | 4 . .
 504:  3 4 . | . 2 7 | . 8 1
 505: 
 506:  6 3 1 | 4 7 8 | 2 9 5
 507:  9 7 4 | 3 5 2 | 1 6 8
 508:  8 2 5 | 1 9 6 | 7 3 4
 509: -------+-------+-------
 510:  7 6 8 | 2 1 5 | 9 4 3
 511:  2 1 9 | 8 4 3 | 6 5 7
 512:  4 5 3 | 7 6 9 | 8 1 2
 513: -------+-------+-------
 514:  . . 2 | . 8 4 | . . 6
 515:  . . . | 6 3 1 | 4 . .
 516:  3 4 . | . 2 7 | . 8 1
 517: 
 518:  6 3 1 | 4 7 8 | 2 9 5
 519:  9 7 4 | 3 5 2 | 1 6 8
 520:  8 2 5 | 1 9 6 | 7 3 4
 521: -------+-------+-------
 522:  7 6 8 | 2 1 5 | 9 4 3
 523:  2 1 9 | 8 4 3 | 6 5 7
 524:  4 5 3 | 7 6 9 | 8 1 2
 525: -------+-------+-------
 526:  1 . 2 | . 8 4 | . . 6
 527:  . . . | 6 3 1 | 4 . .
 528:  3 4 . | . 2 7 | . 8 1
 529: 
 530:  6 3 1 | 4 7 8 | 2 9 5
 531:  9 7 4 | 3 5 2 | 1 6 8
 532:  8 2 5 | 1 9 6 | 7 3 4
 533: -------+-------+-------
 534:  7 6 8 | 2 1 5 | 9 4 3
 535:  2 1 9 | 8 4 3 | 6 5 7
 536:  4 5 3 | 7 6 9 | 8 1 2
 537: -------+-------+-------
 538:  1 9 2 | . 8 4 | . . 6
 539:  . . . | 6 3 1 | 4 . .
 540:  3 4 . | . 2 7 | . 8 1
 541: 
 542:  6 3 1 | 4 7 8 | 2 9 5
 543:  9 7 4 | 3 5 2 | 1 6 8
 544:  8 2 5 | 1 9 6 | 7 3 4
 545: -------+-------+-------
 546:  7 6 8 | 2 1 5 | 9 4 3
 547:  2 1 9 | 8 4 3 | 6 5 7
 548:  4 5 3 | 7 6 9 | 8 1 2
 549: -------+-------+-------
 550:  1 9 2 | 5 8 4 | . . 6
 551:  . . . | 6 3 1 | 4 . .
 552:  3 4 . | . 2 7 | . 8 1
 553: 
 554:  6 3 1 | 4 7 8 | 2 9 5
 555:  9 7 4 | 3 5 2 | 1 6 8
 556:  8 2 5 | 1 9 6 | 7 3 4
 557: -------+-------+-------
 558:  7 6 8 | 2 1 5 | 9 4 3
 559:  2 1 9 | 8 4 3 | 6 5 7
 560:  4 5 3 | 7 6 9 | 8 1 2
 561: -------+-------+-------
 562:  1 9 2 | 5 8 4 | 3 . 6
 563:  . . . | 6 3 1 | 4 . .
 564:  3 4 . | . 2 7 | . 8 1
 565: 
 566:  6 3 1 | 4 7 8 | 2 9 5
 567:  9 7 4 | 3 5 2 | 1 6 8
 568:  8 2 5 | 1 9 6 | 7 3 4
 569: -------+-------+-------
 570:  7 6 8 | 2 1 5 | 9 4 3
 571:  2 1 9 | 8 4 3 | 6 5 7
 572:  4 5 3 | 7 6 9 | 8 1 2
 573: -------+-------+-------
 574:  1 9 2 | 5 8 4 | 3 7 6
 575:  . . . | 6 3 1 | 4 . .
 576:  3 4 . | . 2 7 | . 8 1
 577: 
 578:  6 3 1 | 4 7 8 | 2 9 5
 579:  9 7 4 | 3 5 2 | 1 6 8
 580:  8 2 5 | 1 9 6 | 7 3 4
 581: -------+-------+-------
 582:  7 6 8 | 2 1 5 | 9 4 3
 583:  2 1 9 | 8 4 3 | 6 5 7
 584:  4 5 3 | 7 6 9 | 8 1 2
 585: -------+-------+-------
 586:  1 9 2 | 5 8 4 | 3 7 6
 587:  5 . . | 6 3 1 | 4 . .
 588:  3 4 . | . 2 7 | . 8 1
 589: 
 590:  6 3 1 | 4 7 8 | 2 9 5
 591:  9 7 4 | 3 5 2 | 1 6 8
 592:  8 2 5 | 1 9 6 | 7 3 4
 593: -------+-------+-------
 594:  7 6 8 | 2 1 5 | 9 4 3
 595:  2 1 9 | 8 4 3 | 6 5 7
 596:  4 5 3 | 7 6 9 | 8 1 2
 597: -------+-------+-------
 598:  1 9 2 | 5 8 4 | 3 7 6
 599:  5 8 . | 6 3 1 | 4 . .
 600:  3 4 . | . 2 7 | . 8 1
 601: 
 602:  6 3 1 | 4 7 8 | 2 9 5
 603:  9 7 4 | 3 5 2 | 1 6 8
 604:  8 2 5 | 1 9 6 | 7 3 4
 605: -------+-------+-------
 606:  7 6 8 | 2 1 5 | 9 4 3
 607:  2 1 9 | 8 4 3 | 6 5 7
 608:  4 5 3 | 7 6 9 | 8 1 2
 609: -------+-------+-------
 610:  1 9 2 | 5 8 4 | 3 7 6
 611:  5 8 7 | 6 3 1 | 4 . .
 612:  3 4 . | . 2 7 | . 8 1
 613: 
 614:  6 3 1 | 4 7 8 | 2 9 5
 615:  9 7 4 | 3 5 2 | 1 6 8
 616:  8 2 5 | 1 9 6 | 7 3 4
 617: -------+-------+-------
 618:  7 6 8 | 2 1 5 | 9 4 3
 619:  2 1 9 | 8 4 3 | 6 5 7
 620:  4 5 3 | 7 6 9 | 8 1 2
 621: -------+-------+-------
 622:  1 9 2 | 5 8 4 | 3 7 6
 623:  5 8 7 | 6 3 1 | 4 2 .
 624:  3 4 . | . 2 7 | . 8 1
 625: 
 626:  6 3 1 | 4 7 8 | 2 9 5
 627:  9 7 4 | 3 5 2 | 1 6 8
 628:  8 2 5 | 1 9 6 | 7 3 4
 629: -------+-------+-------
 630:  7 6 8 | 2 1 5 | 9 4 3
 631:  2 1 9 | 8 4 3 | 6 5 7
 632:  4 5 3 | 7 6 9 | 8 1 2
 633: -------+-------+-------
 634:  1 9 2 | 5 8 4 | 3 7 6
 635:  5 8 7 | 6 3 1 | 4 2 9
 636:  3 4 . | . 2 7 | . 8 1
 637: 
 638:  6 3 1 | 4 7 8 | 2 9 5
 639:  9 7 4 | 3 5 2 | 1 6 8
 640:  8 2 5 | 1 9 6 | 7 3 4
 641: -------+-------+-------
 642:  7 6 8 | 2 1 5 | 9 4 3
 643:  2 1 9 | 8 4 3 | 6 5 7
 644:  4 5 3 | 7 6 9 | 8 1 2
 645: -------+-------+-------
 646:  1 9 2 | 5 8 4 | 3 7 6
 647:  5 8 7 | 6 3 1 | 4 2 9
 648:  3 4 6 | . 2 7 | . 8 1
 649: 
 650:  6 3 1 | 4 7 8 | 2 9 5
 651:  9 7 4 | 3 5 2 | 1 6 8
 652:  8 2 5 | 1 9 6 | 7 3 4
 653: -------+-------+-------
 654:  7 6 8 | 2 1 5 | 9 4 3
 655:  2 1 9 | 8 4 3 | 6 5 7
 656:  4 5 3 | 7 6 9 | 8 1 2
 657: -------+-------+-------
 658:  1 9 2 | 5 8 4 | 3 7 6
 659:  5 8 7 | 6 3 1 | 4 2 9
 660:  3 4 6 | 9 2 7 | . 8 1
 661: 
 662:  6 3 1 | 4 7 8 | 2 9 5
 663:  9 7 4 | 3 5 2 | 1 6 8
 664:  8 2 5 | 1 9 6 | 7 3 4
 665: -------+-------+-------
 666:  7 6 8 | 2 1 5 | 9 4 3
 667:  2 1 9 | 8 4 3 | 6 5 7
 668:  4 5 3 | 7 6 9 | 8 1 2
 669: -------+-------+-------
 670:  1 9 2 | 5 8 4 | 3 7 6
 671:  5 8 7 | 6 3 1 | 4 2 9
 672:  3 4 6 | 9 2 7 | 5 8 1
 673: 
 674: *** WON ***
 675: 
Email: steve@oharasteve.com