/usr/share/doc/prover9-doc/examples/kenken6.in is in prover9-doc 0.0.200902a-2.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 | set(arithmetic).
% KenKen is a puzzle similar in some ways to Sudoku.
% Solutions are Latin squares (each row and each column
% is a permuatation of the domain). The grid is partitioned
% into blocks of various sizes and shapes, and an arithmetic
% relation is specified for each block; for example, the
% sum of the members is 8, or the difference (for a block of
% size 2) is 3.
%
% See the Wikipedia Web page on KenKen.
%
% Ordinarily, KenKen uses {1,...,n}, but we use {0,...,n-1}.
assign(domain_size, 6). % domain is {0,1,2,3,4,5}
assign(max_models, -1). % find all models
formulas(assumptions).
% Latin Square
f(x,y1) = f(x,y2) -> y1=y2.
f(x1,y) = f(x2,y) -> x1=x2.
% Clues for the blocks.
f(0,1) * f(0,2) = 0.
f(0,0) + f(1,0) = 5.
f(0,3) * f(1,3) = 20.
f(0,4) * f(0,5) * f(1,5) * f(2,5) = 6.
f(1,4) + f(2,4) = 2.
abs(f(1,1) + -f(1,2)) = 3.
f(2,0) * f(2,1) * f(3,0) * f(3,1) = 240.
f(2,2) * f(2,3) = 6.
f(3,2) * f(4,2) = 0.
f(3,3) + f(4,3) + f(4,4) = 7.
f(3,4) * f(3,5) = 0.
f(4,0) * f(4,1) = 6.
abs(f(4,5) + -f(5,5)) = 1.
f(5,0) + f(5,1) + f(5,2) = 8.
f(5,3) + f(5,4) = 3.
end_of_list.
|