% mace4 -f sudoku-mace4.in ============================== Mace4 ================================= Mace4 (32) version Oct-2007, Oct 2007. Process 7808 was started by hiro on monad, Tue Mar 3 08:04:05 2009 The command was "mace4 -f sudoku-mace4.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file sudoku-mace4.in set(prolog_style_variables). formulas(assumptions). (all X (X = 1 | X = 2 | X = 3 | X = 4 | X = 5 | X = 6 | X = 7 | X = 8 | X = 9)). 1 != 2 & 1 != 3 & 1 != 4 & 1 != 5 & 1 != 6 & 1 != 7 & 1 != 8 & 1 != 9 & 2 != 3 & 2 != 4 & 2 != 5 & 2 != 6 & 2 != 7 & 2 != 8 & 2 != 9 & 3 != 4 & 3 != 5 & 3 != 6 & 3 != 7 & 3 != 8 & 3 != 9 & 4 != 5 & 4 != 6 & 4 != 7 & 4 != 8 & 4 != 9 & 5 != 6 & 5 != 7 & 5 != 8 & 5 != 9 & 6 != 7 & 6 != 8 & 6 != 9 & 7 != 8 & 7 != 9 & 8 != 9. (all X (r1(X) <-> X = 1 | X = 2 | X = 3)). (all X (r2(X) <-> X = 4 | X = 5 | X = 6)). (all X (r3(X) <-> X = 7 | X = 8 | X = 9)). (all N all X exists Y N = a(X,Y)). (all N all Y exists X N = a(X,Y)). (all N ((exists X exists Y (r1(X) & r1(Y) & N = a(X,Y))) & (exists X exists Y (r1(X) & r2(Y) & N = a(X,Y))) & (exists X exists Y (r1(X) & r3(Y) & N = a(X,Y))) & (exists X exists Y (r2(X) & r1(Y) & N = a(X,Y))) & (exists X exists Y (r2(X) & r2(Y) & N = a(X,Y))) & (exists X exists Y (r2(X) & r3(Y) & N = a(X,Y))) & (exists X exists Y (r3(X) & r1(Y) & N = a(X,Y))) & (exists X exists Y (r3(X) & r2(Y) & N = a(X,Y))) & (exists X exists Y (r3(X) & r3(Y) & N = a(X,Y))))). (all X all Y all Z (a(X,Y) = a(X,Z) -> Y = Z)). (all X all Y all Z (a(X,Y) = a(Z,Y) -> X = Z)). (all X all Y all Z all W ((r1(X) & r1(Y) & r1(Z) & r1(W) & a(X,Y) = a(Z,W) -> X = Z & Y = W) & (r1(X) & r2(Y) & r1(Z) & r2(W) & a(X,Y) = a(Z,W) -> X = Z & Y = W) & (r1(X) & r3(Y) & r1(Z) & r3(W) & a(X,Y) = a(Z,W) -> X = Z & Y = W) & (r2(X) & r1(Y) & r2(Z) & r1(W) & a(X,Y) = a(Z,W) -> X = Z & Y = W) & (r2(X) & r2(Y) & r2(Z) & r2(W) & a(X,Y) = a(Z,W) -> X = Z & Y = W) & (r2(X) & r3(Y) & r2(Z) & r3(W) & a(X,Y) = a(Z,W) -> X = Z & Y = W) & (r3(X) & r1(Y) & r3(Z) & r1(W) & a(X,Y) = a(Z,W) -> X = Z & Y = W) & (r3(X) & r2(Y) & r3(Z) & r2(W) & a(X,Y) = a(Z,W) -> X = Z & Y = W) & (r3(X) & r3(Y) & r3(Z) & r3(W) & a(X,Y) = a(Z,W) -> X = Z & Y = W))). a(1,1) = 1 & a(1,4) = 2 & a(1,7) = 3 & a(2,2) = 2 & a(2,5) = 3 & a(2,8) = 4 & a(3,3) = 3 & a(3,6) = 4 & a(3,9) = 5 & a(4,1) = 6 & a(4,4) = 4 & a(4,7) = 5 & a(5,2) = 7 & a(5,5) = 5 & a(5,8) = 6 & a(6,3) = 8 & a(6,6) = 6 & a(6,9) = 7 & a(7,1) = 8 & a(7,4) = 9 & a(7,7) = 7 & a(8,2) = 9 & a(8,5) = 1 & a(8,8) = 8 & a(9,3) = 1 & a(9,6) = 2 & a(9,9) = 4. end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 (all X (X = 1 | X = 2 | X = 3 | X = 4 | X = 5 | X = 6 | X = 7 | X = 8 | X = 9)) # label(non_clause). [assumption]. 2 1 != 2 & 1 != 3 & 1 != 4 & 1 != 5 & 1 != 6 & 1 != 7 & 1 != 8 & 1 != 9 & 2 != 3 & 2 != 4 & 2 != 5 & 2 != 6 & 2 != 7 & 2 != 8 & 2 != 9 & 3 != 4 & 3 != 5 & 3 != 6 & 3 != 7 & 3 != 8 & 3 != 9 & 4 != 5 & 4 != 6 & 4 != 7 & 4 != 8 & 4 != 9 & 5 != 6 & 5 != 7 & 5 != 8 & 5 != 9 & 6 != 7 & 6 != 8 & 6 != 9 & 7 != 8 & 7 != 9 & 8 != 9 # label(non_clause). [assumption]. 3 (all X (r1(X) <-> X = 1 | X = 2 | X = 3)) # label(non_clause). [assumption]. 4 (all X (r2(X) <-> X = 4 | X = 5 | X = 6)) # label(non_clause). [assumption]. 5 (all X (r3(X) <-> X = 7 | X = 8 | X = 9)) # label(non_clause). [assumption]. 6 (all N all X exists Y N = a(X,Y)) # label(non_clause). [assumption]. 7 (all N all Y exists X N = a(X,Y)) # label(non_clause). [assumption]. 8 (all N ((exists X exists Y (r1(X) & r1(Y) & N = a(X,Y))) & (exists X exists Y (r1(X) & r2(Y) & N = a(X,Y))) & (exists X exists Y (r1(X) & r3(Y) & N = a(X,Y))) & (exists X exists Y (r2(X) & r1(Y) & N = a(X,Y))) & (exists X exists Y (r2(X) & r2(Y) & N = a(X,Y))) & (exists X exists Y (r2(X) & r3(Y) & N = a(X,Y))) & (exists X exists Y (r3(X) & r1(Y) & N = a(X,Y))) & (exists X exists Y (r3(X) & r2(Y) & N = a(X,Y))) & (exists X exists Y (r3(X) & r3(Y) & N = a(X,Y))))) # label(non_clause). [assumption]. 9 (all X all Y all Z (a(X,Y) = a(X,Z) -> Y = Z)) # label(non_clause). [assumption]. 10 (all X all Y all Z (a(X,Y) = a(Z,Y) -> X = Z)) # label(non_clause). [assumption]. 11 (all X all Y all Z all W ((r1(X) & r1(Y) & r1(Z) & r1(W) & a(X,Y) = a(Z,W) -> X = Z & Y = W) & (r1(X) & r2(Y) & r1(Z) & r2(W) & a(X,Y) = a(Z,W) -> X = Z & Y = W) & (r1(X) & r3(Y) & r1(Z) & r3(W) & a(X,Y) = a(Z,W) -> X = Z & Y = W) & (r2(X) & r1(Y) & r2(Z) & r1(W) & a(X,Y) = a(Z,W) -> X = Z & Y = W) & (r2(X) & r2(Y) & r2(Z) & r2(W) & a(X,Y) = a(Z,W) -> X = Z & Y = W) & (r2(X) & r3(Y) & r2(Z) & r3(W) & a(X,Y) = a(Z,W) -> X = Z & Y = W) & (r3(X) & r1(Y) & r3(Z) & r1(W) & a(X,Y) = a(Z,W) -> X = Z & Y = W) & (r3(X) & r2(Y) & r3(Z) & r2(W) & a(X,Y) = a(Z,W) -> X = Z & Y = W) & (r3(X) & r3(Y) & r3(Z) & r3(W) & a(X,Y) = a(Z,W) -> X = Z & Y = W))) # label(non_clause). [assumption]. 12 a(1,1) = 1 & a(1,4) = 2 & a(1,7) = 3 & a(2,2) = 2 & a(2,5) = 3 & a(2,8) = 4 & a(3,3) = 3 & a(3,6) = 4 & a(3,9) = 5 & a(4,1) = 6 & a(4,4) = 4 & a(4,7) = 5 & a(5,2) = 7 & a(5,5) = 5 & a(5,8) = 6 & a(6,3) = 8 & a(6,6) = 6 & a(6,9) = 7 & a(7,1) = 8 & a(7,4) = 9 & a(7,7) = 7 & a(8,2) = 9 & a(8,5) = 1 & a(8,8) = 8 & a(9,3) = 1 & a(9,6) = 2 & a(9,9) = 4 # label(non_clause). [assumption]. ============================== end of process non-clausal formulas === ============================== CLAUSES FOR SEARCH ==================== formulas(mace4_clauses). 1 = A | 2 = A | 3 = A | 4 = A | 5 = A | 6 = A | 7 = A | 8 = A | 9 = A. 2 != 1. 3 != 1. 4 != 1. 5 != 1. 6 != 1. 7 != 1. 8 != 1. 9 != 1. 3 != 2. 4 != 2. 5 != 2. 6 != 2. 7 != 2. 8 != 2. 9 != 2. 4 != 3. 5 != 3. 6 != 3. 7 != 3. 8 != 3. 9 != 3. 5 != 4. 6 != 4. 7 != 4. 8 != 4. 9 != 4. 6 != 5. 7 != 5. 8 != 5. 9 != 5. 7 != 6. 8 != 6. 9 != 6. 8 != 7. 9 != 7. 9 != 8. -r1(A) | 1 = A | 2 = A | 3 = A. r1(A) | 1 != A. r1(A) | 2 != A. r1(A) | 3 != A. -r2(A) | 4 = A | 5 = A | 6 = A. r2(A) | 4 != A. r2(A) | 5 != A. r2(A) | 6 != A. -r3(A) | 7 = A | 8 = A | 9 = A. r3(A) | 7 != A. r3(A) | 8 != A. r3(A) | 9 != A. a(A,f1(B,A)) = B. a(f2(A,B),B) = A. r1(f3(A)). r1(f4(A)). a(f3(A),f4(A)) = A. r1(f5(A)). r2(f6(A)). a(f5(A),f6(A)) = A. r1(f7(A)). r3(f8(A)). a(f7(A),f8(A)) = A. r2(f9(A)). r1(f10(A)). a(f9(A),f10(A)) = A. r2(f11(A)). r2(f12(A)). a(f11(A),f12(A)) = A. r2(f13(A)). r3(f14(A)). a(f13(A),f14(A)) = A. r3(f15(A)). r1(f16(A)). a(f15(A),f16(A)) = A. r3(f17(A)). r2(f18(A)). a(f17(A),f18(A)) = A. r3(f19(A)). r3(f20(A)). a(f19(A),f20(A)) = A. a(A,B) != a(A,C) | B = C. a(A,B) != a(C,B) | A = C. -r1(A) | -r1(B) | -r1(C) | -r1(D) | a(C,D) != a(A,B) | C = A. -r1(A) | -r1(B) | -r1(C) | -r1(D) | a(C,D) != a(A,B) | D = B. -r1(A) | -r2(B) | -r1(C) | -r2(D) | a(C,D) != a(A,B) | C = A. -r1(A) | -r2(B) | -r1(C) | -r2(D) | a(C,D) != a(A,B) | D = B. -r1(A) | -r3(B) | -r1(C) | -r3(D) | a(C,D) != a(A,B) | C = A. -r1(A) | -r3(B) | -r1(C) | -r3(D) | a(C,D) != a(A,B) | D = B. -r2(A) | -r1(B) | -r2(C) | -r1(D) | a(C,D) != a(A,B) | C = A. -r2(A) | -r1(B) | -r2(C) | -r1(D) | a(C,D) != a(A,B) | D = B. -r2(A) | -r2(B) | -r2(C) | -r2(D) | a(C,D) != a(A,B) | C = A. -r2(A) | -r2(B) | -r2(C) | -r2(D) | a(C,D) != a(A,B) | D = B. -r2(A) | -r3(B) | -r2(C) | -r3(D) | a(C,D) != a(A,B) | C = A. -r2(A) | -r3(B) | -r2(C) | -r3(D) | a(C,D) != a(A,B) | D = B. -r3(A) | -r1(B) | -r3(C) | -r1(D) | a(C,D) != a(A,B) | C = A. -r3(A) | -r1(B) | -r3(C) | -r1(D) | a(C,D) != a(A,B) | D = B. -r3(A) | -r2(B) | -r3(C) | -r2(D) | a(C,D) != a(A,B) | C = A. -r3(A) | -r2(B) | -r3(C) | -r2(D) | a(C,D) != a(A,B) | D = B. -r3(A) | -r3(B) | -r3(C) | -r3(D) | a(C,D) != a(A,B) | C = A. -r3(A) | -r3(B) | -r3(C) | -r3(D) | a(C,D) != a(A,B) | D = B. a(1,1) = 1. a(1,4) = 2. a(1,7) = 3. a(2,2) = 2. a(2,5) = 3. a(2,8) = 4. a(3,3) = 3. a(3,6) = 4. a(3,9) = 5. a(4,1) = 6. a(4,4) = 4. a(4,7) = 5. a(5,2) = 7. a(5,5) = 5. a(5,8) = 6. a(6,3) = 8. a(6,6) = 6. a(6,9) = 7. a(7,1) = 8. a(7,4) = 9. a(7,7) = 7. a(8,2) = 9. a(8,5) = 1. a(8,8) = 8. a(9,3) = 1. a(9,6) = 2. a(9,9) = 4. end_of_list. ============================== end of clauses for search ============= % The maximum domain element in the input is 9. ============================== DOMAIN SIZE 2 ========================= === Mace4 starting on domain size 2. === Fatal error: mace4: domain_element too big Fatal error: mace4: domain_element too big %