% time mace4 -f sudoku-mace4-2.in ============================== Mace4 ================================= Mace4 (32) version Oct-2007, Oct 2007. Process 6812 was started by hiro on monad, Sat Mar 7 22:52:08 2009 The command was "mace4 -f sudoku-mace4-2.in". ============================== end of head =========================== ============================== INPUT ================================= % Reading from file sudoku-mace4-2.in assign(domain_size,9). set(prolog_style_variables). formulas(assumptions). (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 = 0)). (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,0) = 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,0) = 7. a(7,1) = 8. a(7,4) = 0. a(7,7) = 7. a(8,2) = 0. a(8,5) = 1. a(8,8) = 8. a(0,3) = 1. a(0,6) = 2. a(0,0) = 4. end_of_list. ============================== end of input ========================== ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 (all X (r1(X) <-> X = 1 | X = 2 | X = 3)) # label(non_clause). [assumption]. 2 (all X (r2(X) <-> X = 4 | X = 5 | X = 6)) # label(non_clause). [assumption]. 3 (all X (r3(X) <-> X = 7 | X = 8 | X = 0)) # label(non_clause). [assumption]. 4 (all N all X exists Y N = a(X,Y)) # label(non_clause). [assumption]. 5 (all N all Y exists X N = a(X,Y)) # label(non_clause). [assumption]. 6 (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]. 7 (all X all Y all Z (a(X,Y) = a(X,Z) -> Y = Z)) # label(non_clause). [assumption]. 8 (all X all Y all Z (a(X,Y) = a(Z,Y) -> X = Z)) # label(non_clause). [assumption]. 9 (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]. ============================== end of process non-clausal formulas === ============================== CLAUSES FOR SEARCH ==================== formulas(mace4_clauses). -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 | 0 = A. r3(A) | 7 != A. r3(A) | 8 != A. r3(A) | 0 != 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,0) = 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,0) = 7. a(7,1) = 8. a(7,4) = 0. a(7,7) = 7. a(8,2) = 0. a(8,5) = 1. a(8,8) = 8. a(0,3) = 1. a(0,6) = 2. a(0,0) = 4. end_of_list. ============================== end of clauses for search ============= % The maximum domain element in the input is 8. ============================== DOMAIN SIZE 9 ========================= === Mace4 starting on domain size 9. === ============================== MODEL ================================= interpretation( 9, [number=1, seconds=0], [ function(f3(_), [ 3, 1, 2, 3, 1, 1, 2, 2, 3 ]), function(f4(_), [ 1, 1, 2, 3, 2, 3, 3, 1, 2 ]), function(f5(_), [ 1, 2, 1, 2, 3, 2, 3, 3, 1 ]), function(f6(_), [ 6, 6, 4, 5, 6, 4, 5, 4, 5 ]), function(f7(_), [ 2, 3, 3, 1, 2, 3, 1, 1, 2 ]), function(f8(_), [ 0, 7, 8, 7, 8, 0, 0, 8, 7 ]), function(f9(_), [ 4, 4, 6, 5, 5, 6, 4, 5, 6 ]), function(f10(_), [ 3, 2, 1, 1, 3, 2, 1, 2, 3 ]), function(f11(_), [ 6, 5, 4, 6, 4, 5, 6, 4, 5 ]), function(f12(_), [ 5, 4, 5, 4, 4, 5, 6, 6, 6 ]), function(f13(_), [ 5, 6, 5, 4, 6, 4, 5, 6, 4 ]), function(f14(_), [ 7, 8, 0, 8, 7, 7, 8, 0, 0 ]), function(f15(_), [ 8, 0, 7, 0, 8, 0, 7, 8, 7 ]), function(f16(_), [ 2, 3, 3, 2, 1, 1, 2, 3, 1 ]), function(f17(_), [ 7, 8, 0, 7, 7, 8, 8, 0, 0 ]), function(f18(_), [ 4, 5, 6, 6, 5, 6, 4, 5, 4 ]), function(f19(_), [ 0, 7, 8, 8, 0, 7, 0, 7, 8 ]), function(f20(_), [ 8, 0, 7, 0, 0, 8, 7, 7, 8 ]), function(a(_,_), [ 4, 5, 3, 1, 8, 7, 2, 6, 0, 6, 1, 4, 5, 2, 8, 0, 3, 7, 0, 7, 2, 6, 5, 3, 1, 8, 4, 5, 0, 8, 3, 7, 6, 4, 1, 2, 8, 6, 1, 0, 4, 2, 7, 5, 3, 2, 3, 7, 4, 1, 5, 8, 0, 6, 7, 2, 5, 8, 3, 0, 6, 4, 1, 1, 8, 6, 2, 0, 4, 3, 7, 5, 3, 4, 0, 7, 6, 1, 5, 2, 8 ]), function(f1(_,_), [ 8, 6, 0, 1, 3, 7, 5, 4, 2, 3, 1, 6, 7, 2, 4, 8, 0, 5, 6, 4, 2, 8, 5, 0, 1, 3, 7, 2, 7, 5, 3, 8, 1, 4, 6, 0, 0, 2, 8, 6, 4, 3, 7, 5, 1, 1, 3, 4, 0, 7, 5, 2, 8, 6, 7, 0, 3, 5, 1, 8, 6, 2, 4, 5, 8, 1, 4, 6, 2, 0, 7, 3, 4, 5, 7, 2, 0, 6, 3, 1, 8 ]), function(f2(_,_), [ 2, 3, 8, 4, 7, 6, 1, 5, 0, 7, 1, 4, 0, 5, 8, 2, 3, 6, 5, 6, 2, 7, 1, 4, 0, 8, 3, 8, 5, 0, 3, 6, 2, 7, 1, 4, 0, 8, 1, 5, 4, 7, 3, 6, 2, 3, 0, 6, 1, 2, 5, 8, 4, 7, 1, 4, 7, 2, 8, 3, 6, 0, 5, 6, 2, 5, 8, 3, 0, 4, 7, 1, 4, 7, 3, 6, 0, 1, 5, 2, 8 ]), relation(r1(_), [ 0, 1, 1, 1, 0, 0, 0, 0, 0 ]), relation(r2(_), [ 0, 0, 0, 0, 1, 1, 1, 0, 0 ]), relation(r3(_), [ 1, 0, 0, 0, 0, 0, 0, 1, 1 ]) ]). ============================== end of model ========================== ============================== STATISTICS ============================ For domain size 9. Current CPU time: 0.00 seconds (total CPU time: 0.59 seconds). Ground clauses: seen=120096, kept=2727. Selections=88, assignments=468, propagations=796, current_models=1. Rewrite_terms=13783, rewrite_bools=7424, indexes=101. Rules_from_neg_clauses=641, cross_offs=4184. ============================== end of statistics ===================== ------ process 6812 exit (max_models) ------ User_CPU=0.59, System_CPU=0.11, Wall_clock=1. Exiting with 1 model. Process 6812 exit (max_models) Sat Mar 7 22:52:09 2009 The process finished Sat Mar 7 22:52:09 2009 mace4 -f sudoku-mace4-2.in 0.59s user 0.15s system 92% cpu 0.806 total %