% 数の定義
fof( dom1, axiom, ![X] : (X=n1 | X=n2 | X=n3 | X=n4 | X=n5 | X=n6 | X=n7 | X=n8 | X=n9) ).
fof( dom2, axiom,
n1!=n2 & n1!=n3 & n1!=n4 & n1!=n5 & n1!=n6 & n1!=n7 & n1!=n8 & n1!=n9 &
n2!=n3 & n2!=n4 & n2!=n5 & n2!=n6 & n2!=n7 & n2!=n8 & n2!=n9 &
n3!=n4 & n3!=n5 & n3!=n6 & n3!=n7 & n3!=n8 & n3!=n9 &
n4!=n5 & n4!=n6 & n4!=n7 & n4!=n8 & n4!=n9 &
n5!=n6 & n5!=n7 & n5!=n8 & n5!=n9 &
n6!=n7 & n6!=n8 & n6!=n9 &
n7!=n8 & n7!=n9 &
n8!=n9
).

% 範囲の定義
fof( r1, axiom, ![X] : (r1(X) <=> (X=n1 | X=n2 | X=n3))).
fof( r2, axiom, ![X] : (r2(X) <=> (X=n4 | X=n5 | X=n6))).
fof( r3, axiom, ![X] : (r3(X) <=> (X=n7 | X=n8 | X=n9))).

% 全ての数が全ての行および列に存在する
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(n1,n1)=n1 & a(n1,n4)=n2 & a(n1,n7)=n3 & 
a(n2,n2)=n2 & a(n2,n5)=n3 & a(n2,n8)=n4 & 
a(n3,n3)=n3 & a(n3,n6)=n4 & a(n3,n9)=n5 & 
a(n4,n1)=n6 & a(n4,n4)=n4 & a(n4,n7)=n5 & 
a(n5,n2)=n7 & a(n5,n5)=n5 & a(n5,n8)=n6 & 
a(n6,n3)=n8 & a(n6,n6)=n6 & a(n6,n9)=n7 & 
a(n7,n1)=n8 & a(n7,n4)=n9 & a(n7,n7)=n7 &
a(n8,n2)=n9 & a(n8,n5)=n1 & a(n8,n8)=n8 & 
a(n9,n3)=n1 & a(n9,n6)=n2 & a(n9,n9)=n4 
).