% 数の定義 (Paradoxは数をサポートしていないので、単に項として扱う)
fof( dom1, axiom, ![X] : (X=1 | X=2 | X=3 | X=4 | X=5 | X=6 | X=7 | X=8 | X=9) ).
fof( dom2, axiom,
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
).

% 範囲の定義
fof( r1, axiom, ![X] : (r1(X) <=> (X=1 | X=2 | X=3))).
fof( r2, axiom, ![X] : (r2(X) <=> (X=4 | X=5 | X=6))).
fof( r3, axiom, ![X] : (r3(X) <=> (X=7 | X=8 | X=9))).

% 全ての数が全ての行および列に存在する
fof( rule1, axiom, ![N,X] : ?[Y] : N=a(X,Y) ).
fof( rule2, axiom, ![N,Y] : ?[X] : N=a(X,Y) ).
% 全ての数が任意のブロックに存在する
fof( rule3, axiom, ![N] : (
(?[X,Y] : (r1(X) & r1(Y) & N=a(X,Y))) &
(?[X,Y] : (r1(X) & r2(Y) & N=a(X,Y))) &
(?[X,Y] : (r1(X) & r3(Y) & N=a(X,Y))) &
(?[X,Y] : (r2(X) & r1(Y) & N=a(X,Y))) &
(?[X,Y] : (r2(X) & r2(Y) & N=a(X,Y))) &
(?[X,Y] : (r2(X) & r3(Y) & N=a(X,Y))) &
(?[X,Y] : (r3(X) & r1(Y) & N=a(X,Y))) &
(?[X,Y] : (r3(X) & r2(Y) & N=a(X,Y))) &
(?[X,Y] : (r3(X) & r3(Y) & N=a(X,Y)))
)).

% 枝刈り用の規則
fof( rule1b, axiom, ![X,Y,Z] : (a(X,Y)=a(X,Z) => Y=Z) ).
fof( rule2b, axiom, ![X,Y,Z] : (a(X,Y)=a(Z,Y) => X=Z) ).
fof( rule3b, axiom, ![X,Y,Z,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))
)).

% 既知の数字の定義
fof( given, axiom,
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
).