----- Mace4 (32) Oct-2005-work, Oct 2005 ----- Built with library LADR Oct-2005-work, Oct 2005. The process was started by mccune on cleo.thornwood, Wed Nov 9 11:31:16 2005 The command was "../mace4 -m -1 -f example.in". The process ID is 19175. % Reading from file example.in assign(domain_size,9). assign(max_seconds,2). set(print_models_portable). formulas(sudoko_rules). (all x all y1 all y2 (f(x,y1) = f(x,y2) -> y1 = y2)). (all x1 all x2 all y (f(x1,y) = f(x2,y) -> x1 = x2)). (all x (same_interval(x,x))). (all x all y (same_interval(x,y) -> same_interval(y,x))). (all x all y all z (same_interval(x,y) & same_interval(y,z) -> same_interval(x,z))). same_interval(0,1). same_interval(1,2). same_interval(3,4). same_interval(4,5). same_interval(6,7). same_interval(7,8). - same_interval(0,3). - same_interval(3,6). - same_interval(0,6). (all x1 all y1 all x2 all y2 (same_interval(x1,x2) & same_interval(y1,y2) & f(x1,y1) = f(x2,y2) -> x1 = x2 & y1 = y2)). (all x all z exists y (f(x,y) = z)). (all y all z exists x (f(x,y) = z)). end_of_list. formulas(sample_puzzle). f(0,0) = 1. f(0,3) = 2. f(0,6) = 3. f(1,1) = 2. f(1,4) = 3. f(1,7) = 4. f(2,2) = 3. f(2,5) = 4. f(2,8) = 5. f(3,0) = 6. f(3,3) = 4. f(3,6) = 5. f(4,1) = 7. f(4,4) = 5. f(4,7) = 6. f(5,2) = 8. f(5,5) = 6. f(5,8) = 7. f(6,0) = 8. f(6,3) = 0. f(6,6) = 7. f(7,1) = 0. f(7,4) = 1. f(7,7) = 8. f(8,2) = 1. f(8,5) = 2. f(8,8) = 4. end_of_list. % Finished reading the input. % From the command line: assign(max_models, -1). % The maximum domain element in the input is 8. === Starting model search for domain size 9. === -------- Model 1 at 0.03 seconds -------- interpretation( 9, [ function(f(_,_), [1,4,5,2,8,0,3,7,6, 7,2,6,5,3,1,8,4,0, 0,8,3,7,6,4,1,2,5, 6,1,0,4,2,7,5,3,8, 3,7,4,1,5,8,0,6,2, 2,5,8,3,0,6,4,1,7, 8,6,2,0,4,3,7,5,1, 4,0,7,6,1,5,2,8,3, 5,3,1,8,7,2,6,0,4]), function($f1(_,_), [5,0,3,6,1,2,8,7,4, 8,5,1,4,7,3,2,0,6, 0,6,7,2,5,8,4,3,1, 2,1,4,7,3,6,0,5,8, 6,3,8,0,2,4,7,1,5, 4,7,0,3,6,1,5,8,2, 3,8,2,5,4,7,1,6,0, 1,4,6,8,0,5,3,2,7, 7,2,5,1,8,0,6,4,3]), function($f2(_,_), [2,0,5,4,7,8,3,1,6, 7,3,1,8,0,5,6,4,2, 3,8,6,2,4,0,1,7,5, 6,4,0,5,3,1,7,2,8, 5,7,3,1,6,4,2,8,0, 0,1,8,6,2,7,5,3,4, 4,2,7,0,5,3,8,6,1, 8,5,2,3,1,6,4,0,7, 1,6,4,7,8,2,0,5,3]), relation(same_interval(_,_), [1,1,1,0,0,0,0,0,0, 1,1,1,0,0,0,0,0,0, 1,1,1,0,0,0,0,0,0, 0,0,0,1,1,1,0,0,0, 0,0,0,1,1,1,0,0,0, 0,0,0,1,1,1,0,0,0, 0,0,0,0,0,0,1,1,1, 0,0,0,0,0,0,1,1,1, 0,0,0,0,0,0,1,1,1]) ]). -------- end of model -------- User_CPU=0.03, System_CPU=0.01, Wall_clock=0. Exiting with 1 model. Process 19175 exit (all_models) Wed Nov 9 11:31:16 2005 The process finished Wed Nov 9 11:31:16 2005