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.