-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathsudoku9x9.tptp
155 lines (151 loc) · 7.56 KB
/
sudoku9x9.tptp
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
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
%fof(problem,axiom,(
% ! [ X12,X13,X14, X16,X17, X19,
% X23 ,X25,X26,X27,X28,X29,
% X31,X32, X35,X36, X38,
% X42,X43,X44,X45, X48,
% X51, X53,X54,X55,X56,X57, X59,
% X62, X65,X66,X67,X68,
% X72, X74,X75, X78,X79,
% X81,X82,X83,X84,X85, X87,
% X91, X93,X94, X96,X97,X98 ] :
% problem("1",X12,X13,X14,"7",X16,X17,"3",X19,
% "8","3",X23,"6",X25,X26,X27,X28,X29,
% X31,X32,"2","9",X35,X36,"6",X38,"8",
% "6",X42,X43,X44,X45,"4","9",X48,"7",
% X51,"9",X53,X54,X55,X56,X57,"5",X59,
% "3",X62,"7","5",X65,X66,X67,X68,"4",
% "2",X72,"3",X74,X75,"9","1",X78,X79,
% X81,X82,X83,X84,X85,"2",X87,"4","3",
% X91,"4",X93,X94,"8",X96,X97,X98,"9") )).
fof(solutionSequence,axiom,(
! [X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( isSolutionSequence(X1,X2,X3,X4,X5,X6,X7,X8,X9)
% <= ( ( X1 = "1" | X2 = "1" | X3 = "1"
% | X4 = "1" | X5 = "1" | X6 = "1"
% | X7 = "1" | X8 = "1" | X9 = "1" )
% & ( X1 = "2" | X2 = "2" | X3 = "2"
% | X4 = "2" | X5 = "2" | X6 = "2"
% | X7 = "2" | X8 = "2" | X9 = "2" )
% & ( X1 = "3" | X2 = "3" | X3 = "3"
% | X4 = "3" | X5 = "3" | X6 = "3"
% | X7 = "3" | X8 = "3" | X9 = "3" )
% & ( X1 = "4" | X2 = "4" | X3 = "4"
% | X4 = "4" | X5 = "4" | X6 = "4"
% | X7 = "4" | X8 = "4" | X9 = "4" )
% & ( X1 = "5" | X2 = "5" | X3 = "5"
% | X4 = "5" | X5 = "5" | X6 = "5"
% | X7 = "5" | X8 = "5" | X9 = "5" )
% & ( X1 = "6" | X2 = "6" | X3 = "6"
% | X4 = "6" | X5 = "6" | X6 = "6"
% | X7 = "6" | X8 = "6" | X9 = "6" )
% & ( X1 = "7" | X2 = "7" | X3 = "7"
% | X4 = "7" | X5 = "7" | X6 = "7"
% | X7 = "7" | X8 = "7" | X9 = "7" )
% & ( X1 = "8" | X2 = "8" | X3 = "8"
% | X4 = "8" | X5 = "8" | X6 = "8"
% | X7 = "8" | X8 = "8" | X9 = "8" )
% & ( X1 = "9" | X2 = "9" | X3 = "9"
% | X4 = "9" | X5 = "9" | X6 = "9"
% | X7 = "9" | X8 = "9" | X9 = "9" ) ) ) )).
<= ( X1 != X9 & X1 != X8 & X1 != X7 & X1 != X6 & X1 != X5 & X1 != X4 & X1 != X3 & X1 != X2
& X2 != X9 & X2 != X8 & X2 != X7 & X2 != X6 & X2 != X5 & X2 != X4 & X2 != X3
& X3 != X9 & X3 != X8 & X3 != X7 & X3 != X6 & X3 != X5 & X3 != X4
& X4 != X9 & X4 != X8 & X4 != X7 & X4 != X6 & X4 != X5
& X5 != X9 & X5 != X8 & X5 != X7 & X5 != X6
& X6 != X9 & X6 != X8 & X6 != X7
& X7 != X9 & X7 != X8
& X8 != X9 ) ) )).
fof(solution,axiom,(
! [X11,X12,X13,X14,X15,X16,X17,X18,X19,
X21,X22,X23,X24,X25,X26,X27,X28,X29,
X31,X32,X33,X34,X35,X36,X37,X38,X39,
X41,X42,X43,X44,X45,X46,X47,X48,X49,
X51,X52,X53,X54,X55,X56,X57,X58,X59,
X61,X62,X63,X64,X65,X66,X67,X68,X69,
X71,X72,X73,X74,X75,X76,X77,X78,X79,
X81,X82,X83,X84,X85,X86,X87,X88,X89,
X91,X92,X93,X94,X95,X96,X97,X98,X99] :
( isSolution(X11,X12,X13,X14,X15,X16,X17,X18,X19,
X21,X22,X23,X24,X25,X26,X27,X28,X29,
X31,X32,X33,X34,X35,X36,X37,X38,X39,
X41,X42,X43,X44,X45,X46,X47,X48,X49,
X51,X52,X53,X54,X55,X56,X57,X58,X59,
X61,X62,X63,X64,X65,X66,X67,X68,X69,
X71,X72,X73,X74,X75,X76,X77,X78,X79,
X81,X82,X83,X84,X85,X86,X87,X88,X89,
X91,X92,X93,X94,X95,X96,X97,X98,X99)
<= ( isSolutionSequence(X11,X12,X13,X14,X15,X16,X17,X18,X19)
& isSolutionSequence(X21,X22,X23,X24,X25,X26,X27,X28,X29)
& isSolutionSequence(X31,X32,X33,X34,X35,X36,X37,X38,X39)
& isSolutionSequence(X41,X42,X43,X44,X45,X46,X47,X48,X49)
& isSolutionSequence(X51,X52,X53,X54,X55,X56,X57,X58,X59)
& isSolutionSequence(X61,X62,X63,X64,X65,X66,X67,X68,X69)
& isSolutionSequence(X71,X72,X73,X74,X75,X76,X77,X78,X79)
& isSolutionSequence(X81,X82,X83,X84,X85,X86,X87,X88,X89)
& isSolutionSequence(X91,X92,X93,X94,X95,X96,X97,X98,X99)
& isSolutionSequence(X11,X21,X31,X41,X51,X61,X71,X81,X91)
& isSolutionSequence(X12,X22,X32,X42,X52,X62,X72,X82,X92)
& isSolutionSequence(X13,X23,X33,X43,X53,X63,X73,X83,X93)
& isSolutionSequence(X14,X24,X34,X44,X54,X64,X74,X84,X94)
& isSolutionSequence(X15,X25,X35,X45,X55,X65,X75,X85,X95)
& isSolutionSequence(X16,X26,X36,X46,X56,X66,X76,X86,X96)
& isSolutionSequence(X17,X27,X37,X47,X57,X67,X77,X87,X97)
& isSolutionSequence(X18,X28,X38,X48,X58,X68,X78,X88,X98)
& isSolutionSequence(X19,X29,X39,X49,X59,X69,X79,X89,X99)
& isSolutionSequence(X11,X12,X13,X21,X22,X23,X31,X32,X33)
& isSolutionSequence(X14,X15,X16,X24,X25,X26,X34,X35,X36)
& isSolutionSequence(X17,X18,X19,X27,X28,X29,X37,X38,X39)
& isSolutionSequence(X41,X42,X43,X51,X52,X53,X61,X62,X63)
& isSolutionSequence(X44,X45,X46,X54,X55,X56,X64,X65,X66)
& isSolutionSequence(X47,X48,X49,X57,X58,X59,X67,X68,X69)
& isSolutionSequence(X71,X72,X73,X81,X82,X83,X91,X92,X93)
& isSolutionSequence(X74,X75,X76,X84,X85,X86,X94,X95,X96)
& isSolutionSequence(X77,X78,X79,X87,X88,X89,X97,X98,X99) ) ) )).
fof(querySolution,question,(
? [ X12,X13,X14, X16,X17, X19,
X23 ,X25,X26,X27,X28,X29,
X31,X32, X35,X36, X38,
X42,X43,X44,X45, X48,
X51, X53,X54,X55,X56,X57, X59,
X62, X65,X66,X67,X68,
X72, X74,X75, X78,X79,
X81,X82,X83,X84,X85, X87,
X91, X93,X94, X96,X97,X98 ] :
isSolution("1",X12,X13,X14,"7",X16,X17,"3",X19,
"8","3",X23,"6",X25,X26,X27,X28,X29,
X31,X32,"2","9",X35,X36,"6",X38,"8",
"6",X42,X43,X44,X45,"4","9",X48,"7",
X51,"9",X53,X54,X55,X56,X57,"5",X59,
"3",X62,"7","5",X65,X66,X67,X68,"4",
"2",X72,"3",X74,X75,"9","1",X78,X79,
X81,X82,X83,X84,X85,"2",X87,"4","3",
X91,"4",X93,X94,"8",X96,X97,X98,"9") )).
%fof(querySolution,question,(
% ? [X11,X12,X13,X14,X15,X16,X17,X18,X19,
% X21,X22,X23,X24,X25,X26,X27,X28,X29,
% X31,X32,X33,X34,X35,X36,X37,X38,X39,
% X41,X42,X43,X44,X45,X46,X47,X48,X49,
% X51,X52,X53,X54,X55,X56,X57,X58,X59,
% X61,X62,X63,X64,X65,X66,X67,X68,X69,
% X71,X72,X73,X74,X75,X76,X77,X78,X79,
% X81,X82,X83,X84,X85,X86,X87,X88,X89,
% X91,X92,X93,X94,X95,X96,X97,X98,X99] :
% ( problem(X11,X12,X13,X14,X15,X16,X17,X18,X19,
% X21,X22,X23,X24,X25,X26,X27,X28,X29,
% X31,X32,X33,X34,X35,X36,X37,X38,X39,
% X41,X42,X43,X44,X45,X46,X47,X48,X49,
% X51,X52,X53,X54,X55,X56,X57,X58,X59,
% X61,X62,X63,X64,X65,X66,X67,X68,X69,
% X71,X72,X73,X74,X75,X76,X77,X78,X79,
% X81,X82,X83,X84,X85,X86,X87,X88,X89,
% X91,X92,X93,X94,X95,X96,X97,X98,X99)
% & isSolution(X11,X12,X13,X14,X15,X16,X17,X18,X19,
% X21,X22,X23,X24,X25,X26,X27,X28,X29,
% X31,X32,X33,X34,X35,X36,X37,X38,X39,
% X41,X42,X43,X44,X45,X46,X47,X48,X49,
% X51,X52,X53,X54,X55,X56,X57,X58,X59,
% X61,X62,X63,X64,X65,X66,X67,X68,X69,
% X71,X72,X73,X74,X75,X76,X77,X78,X79,
% X81,X82,X83,X84,X85,X86,X87,X88,X89,
% X91,X92,X93,X94,X95,X96,X97,X98,X99) ) )).
%