-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathsudoku.tptp
732 lines (722 loc) · 32.9 KB
/
sudoku.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
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
fof(placement,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,
Y11,Y12,Y13,Y14,Y15,Y16,Y17,Y18,Y19,
Y21,Y22,Y23,Y24,Y25,Y26,Y27,Y28,Y29,
Y31,Y32,Y33,Y34,Y35,Y36,Y37,Y38,Y39,
Y41,Y42,Y43,Y44,Y45,Y46,Y47,Y48,Y49,
Y51,Y52,Y53,Y54,Y55,Y56,Y57,Y58,Y59,
Y61,Y62,Y63,Y64,Y65,Y66,Y67,Y68,Y69,
Y71,Y72,Y73,Y74,Y75,Y76,Y77,Y78,Y79,
Y81,Y82,Y83,Y84,Y85,Y86,Y87,Y88,Y89,
Y91,Y92,Y93,Y94,Y95,Y96,Y97,Y98,Y99] :
( isPlacementFor(placement(Y11,Y12,Y13,Y14,Y15,Y16,Y17,Y18,Y19,
Y21,Y22,Y23,Y24,Y25,Y26,Y27,Y28,Y29,
Y31,Y32,Y33,Y34,Y35,Y36,Y37,Y38,Y39,
Y41,Y42,Y43,Y44,Y45,Y46,Y47,Y48,Y49,
Y51,Y52,Y53,Y54,Y55,Y56,Y57,Y58,Y59,
Y61,Y62,Y63,Y64,Y65,Y66,Y67,Y68,Y69,
Y71,Y72,Y73,Y74,Y75,Y76,Y77,Y78,Y79,
Y81,Y82,Y83,Y84,Y85,Y86,Y87,Y88,Y89,
Y91,Y92,Y93,Y94,Y95,Y96,Y97,Y98,Y99),
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))
<=> ( Y11 != "_" & ( X11 = "_" | Y11 = X11 )
& Y12 != "_" & ( X12 = "_" | Y12 = X12 )
& Y13 != "_" & ( X13 = "_" | Y13 = X13 )
& Y14 != "_" & ( X14 = "_" | Y14 = X14 )
& Y15 != "_" & ( X15 = "_" | Y15 = X15 )
& Y16 != "_" & ( X16 = "_" | Y16 = X16 )
& Y17 != "_" & ( X17 = "_" | Y17 = X17 )
& Y18 != "_" & ( X18 = "_" | Y18 = X18 )
& Y19 != "_" & ( X19 = "_" | Y19 = X19 )
& Y21 != "_" & ( X21 = "_" | Y21 = X21 )
& Y22 != "_" & ( X22 = "_" | Y22 = X22 )
& Y23 != "_" & ( X23 = "_" | Y23 = X23 )
& Y24 != "_" & ( X24 = "_" | Y24 = X24 )
& Y25 != "_" & ( X25 = "_" | Y25 = X25 )
& Y26 != "_" & ( X26 = "_" | Y26 = X26 )
& Y27 != "_" & ( X27 = "_" | Y27 = X27 )
& Y28 != "_" & ( X28 = "_" | Y28 = X28 )
& Y29 != "_" & ( X29 = "_" | Y29 = X29 )
& Y31 != "_" & ( X31 = "_" | Y31 = X31 )
& Y32 != "_" & ( X32 = "_" | Y32 = X32 )
& Y33 != "_" & ( X33 = "_" | Y33 = X33 )
& Y34 != "_" & ( X34 = "_" | Y34 = X34 )
& Y35 != "_" & ( X35 = "_" | Y35 = X35 )
& Y36 != "_" & ( X36 = "_" | Y36 = X36 )
& Y37 != "_" & ( X37 = "_" | Y37 = X37 )
& Y38 != "_" & ( X38 = "_" | Y38 = X38 )
& Y39 != "_" & ( X39 = "_" | Y39 = X39 )
& Y41 != "_" & ( X41 = "_" | Y41 = X41 )
& Y42 != "_" & ( X42 = "_" | Y42 = X42 )
& Y43 != "_" & ( X43 = "_" | Y43 = X43 )
& Y44 != "_" & ( X44 = "_" | Y44 = X44 )
& Y45 != "_" & ( X45 = "_" | Y45 = X45 )
& Y46 != "_" & ( X46 = "_" | Y46 = X46 )
& Y47 != "_" & ( X47 = "_" | Y47 = X47 )
& Y48 != "_" & ( X48 = "_" | Y48 = X48 )
& Y49 != "_" & ( X49 = "_" | Y49 = X49 )
& Y51 != "_" & ( X51 = "_" | Y51 = X51 )
& Y52 != "_" & ( X52 = "_" | Y52 = X52 )
& Y53 != "_" & ( X53 = "_" | Y53 = X53 )
& Y54 != "_" & ( X54 = "_" | Y54 = X54 )
& Y55 != "_" & ( X55 = "_" | Y55 = X55 )
& Y56 != "_" & ( X56 = "_" | Y56 = X56 )
& Y57 != "_" & ( X57 = "_" | Y57 = X57 )
& Y58 != "_" & ( X58 = "_" | Y58 = X58 )
& Y59 != "_" & ( X59 = "_" | Y59 = X59 )
& Y61 != "_" & ( X61 = "_" | Y61 = X61 )
& Y62 != "_" & ( X62 = "_" | Y62 = X62 )
& Y63 != "_" & ( X63 = "_" | Y63 = X63 )
& Y64 != "_" & ( X64 = "_" | Y64 = X64 )
& Y65 != "_" & ( X65 = "_" | Y65 = X65 )
& Y66 != "_" & ( X66 = "_" | Y66 = X66 )
& Y67 != "_" & ( X67 = "_" | Y67 = X67 )
& Y68 != "_" & ( X68 = "_" | Y68 = X68 )
& Y69 != "_" & ( X69 = "_" | Y69 = X69 )
& Y71 != "_" & ( X71 = "_" | Y71 = X71 )
& Y72 != "_" & ( X72 = "_" | Y72 = X72 )
& Y73 != "_" & ( X73 = "_" | Y73 = X73 )
& Y74 != "_" & ( X74 = "_" | Y74 = X74 )
& Y75 != "_" & ( X75 = "_" | Y75 = X75 )
& Y76 != "_" & ( X76 = "_" | Y76 = X76 )
& Y77 != "_" & ( X77 = "_" | Y77 = X77 )
& Y78 != "_" & ( X78 = "_" | Y78 = X78 )
& Y79 != "_" & ( X79 = "_" | Y79 = X79 )
& Y81 != "_" & ( X81 = "_" | Y81 = X81 )
& Y82 != "_" & ( X82 = "_" | Y82 = X82 )
& Y83 != "_" & ( X83 = "_" | Y83 = X83 )
& Y84 != "_" & ( X84 = "_" | Y84 = X84 )
& Y85 != "_" & ( X85 = "_" | Y85 = X85 )
& Y86 != "_" & ( X86 = "_" | Y86 = X86 )
& Y87 != "_" & ( X87 = "_" | Y87 = X87 )
& Y88 != "_" & ( X88 = "_" | Y88 = X88 )
& Y89 != "_" & ( X89 = "_" | Y89 = X89 )
& Y91 != "_" & ( X91 = "_" | Y91 = X91 )
& Y92 != "_" & ( X92 = "_" | Y92 = X92 )
& Y93 != "_" & ( X93 = "_" | Y93 = X93 )
& Y94 != "_" & ( X94 = "_" | Y94 = X94 )
& Y95 != "_" & ( X95 = "_" | Y95 = X95 )
& Y96 != "_" & ( X96 = "_" | Y96 = X96 )
& Y97 != "_" & ( X97 = "_" | Y97 = X97 )
& Y98 != "_" & ( X98 = "_" | Y98 = X98 )
& Y99 != "_" & ( X99 = "_" | Y99 = X99 ) ) ) )).
%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" ) ) ) )).
% another way
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" )
& ( X1 != "2" | X2 != "2" )
& ( X1 != "3" | X2 != "3" )
& ( X1 != "4" | X2 != "4" )
& ( X1 != "5" | X2 != "5" )
& ( X1 != "6" | X2 != "6" )
& ( X1 != "7" | X2 != "7" )
& ( X1 != "8" | X2 != "8" )
& ( X1 != "9" | X2 != "9" )
& ( X1 != "1" | X3 != "1" )
& ( X1 != "2" | X3 != "2" )
& ( X1 != "3" | X3 != "3" )
& ( X1 != "4" | X3 != "4" )
& ( X1 != "5" | X3 != "5" )
& ( X1 != "6" | X3 != "6" )
& ( X1 != "7" | X3 != "7" )
& ( X1 != "8" | X3 != "8" )
& ( X1 != "9" | X3 != "9" )
& ( X1 != "1" | X4 != "1" )
& ( X1 != "2" | X4 != "2" )
& ( X1 != "3" | X4 != "3" )
& ( X1 != "4" | X4 != "4" )
& ( X1 != "5" | X4 != "5" )
& ( X1 != "6" | X4 != "6" )
& ( X1 != "7" | X4 != "7" )
& ( X1 != "8" | X4 != "8" )
& ( X1 != "9" | X4 != "9" )
& ( X1 != "1" | X5 != "1" )
& ( X1 != "2" | X5 != "2" )
& ( X1 != "3" | X5 != "3" )
& ( X1 != "4" | X5 != "4" )
& ( X1 != "5" | X5 != "5" )
& ( X1 != "6" | X5 != "6" )
& ( X1 != "7" | X5 != "7" )
& ( X1 != "8" | X5 != "8" )
& ( X1 != "9" | X5 != "9" )
& ( X1 != "1" | X6 != "1" )
& ( X1 != "2" | X6 != "2" )
& ( X1 != "3" | X6 != "3" )
& ( X1 != "4" | X6 != "4" )
& ( X1 != "5" | X6 != "5" )
& ( X1 != "6" | X6 != "6" )
& ( X1 != "7" | X6 != "7" )
& ( X1 != "8" | X6 != "8" )
& ( X1 != "9" | X6 != "9" )
& ( X1 != "1" | X7 != "1" )
& ( X1 != "2" | X7 != "2" )
& ( X1 != "3" | X7 != "3" )
& ( X1 != "4" | X7 != "4" )
& ( X1 != "5" | X7 != "5" )
& ( X1 != "6" | X7 != "6" )
& ( X1 != "7" | X7 != "7" )
& ( X1 != "8" | X7 != "8" )
& ( X1 != "9" | X7 != "9" )
& ( X1 != "1" | X8 != "1" )
& ( X1 != "2" | X8 != "2" )
& ( X1 != "3" | X8 != "3" )
& ( X1 != "4" | X8 != "4" )
& ( X1 != "5" | X8 != "5" )
& ( X1 != "6" | X8 != "6" )
& ( X1 != "7" | X8 != "7" )
& ( X1 != "8" | X8 != "8" )
& ( X1 != "9" | X8 != "9" )
& ( X1 != "1" | X9 != "1" )
& ( X1 != "2" | X9 != "2" )
& ( X1 != "3" | X9 != "3" )
& ( X1 != "4" | X9 != "4" )
& ( X1 != "5" | X9 != "5" )
& ( X1 != "6" | X9 != "6" )
& ( X1 != "7" | X9 != "7" )
& ( X1 != "8" | X9 != "8" )
& ( X1 != "9" | X9 != "9" )
& ( X2 != "1" | X3 != "1" )
& ( X2 != "2" | X3 != "2" )
& ( X2 != "3" | X3 != "3" )
& ( X2 != "4" | X3 != "4" )
& ( X2 != "5" | X3 != "5" )
& ( X2 != "6" | X3 != "6" )
& ( X2 != "7" | X3 != "7" )
& ( X2 != "8" | X3 != "8" )
& ( X2 != "9" | X3 != "9" )
& ( X2 != "1" | X4 != "1" )
& ( X2 != "2" | X4 != "2" )
& ( X2 != "3" | X4 != "3" )
& ( X2 != "4" | X4 != "4" )
& ( X2 != "5" | X4 != "5" )
& ( X2 != "6" | X4 != "6" )
& ( X2 != "7" | X4 != "7" )
& ( X2 != "8" | X4 != "8" )
& ( X2 != "9" | X4 != "9" )
& ( X2 != "1" | X5 != "1" )
& ( X2 != "2" | X5 != "2" )
& ( X2 != "3" | X5 != "3" )
& ( X2 != "4" | X5 != "4" )
& ( X2 != "5" | X5 != "5" )
& ( X2 != "6" | X5 != "6" )
& ( X2 != "7" | X5 != "7" )
& ( X2 != "8" | X5 != "8" )
& ( X2 != "9" | X5 != "9" )
& ( X2 != "1" | X6 != "1" )
& ( X2 != "2" | X6 != "2" )
& ( X2 != "3" | X6 != "3" )
& ( X2 != "4" | X6 != "4" )
& ( X2 != "5" | X6 != "5" )
& ( X2 != "6" | X6 != "6" )
& ( X2 != "7" | X6 != "7" )
& ( X2 != "8" | X6 != "8" )
& ( X2 != "9" | X6 != "9" )
& ( X2 != "1" | X7 != "1" )
& ( X2 != "2" | X7 != "2" )
& ( X2 != "3" | X7 != "3" )
& ( X2 != "4" | X7 != "4" )
& ( X2 != "5" | X7 != "5" )
& ( X2 != "6" | X7 != "6" )
& ( X2 != "7" | X7 != "7" )
& ( X2 != "8" | X7 != "8" )
& ( X2 != "9" | X7 != "9" )
& ( X2 != "1" | X8 != "1" )
& ( X2 != "2" | X8 != "2" )
& ( X2 != "3" | X8 != "3" )
& ( X2 != "4" | X8 != "4" )
& ( X2 != "5" | X8 != "5" )
& ( X2 != "6" | X8 != "6" )
& ( X2 != "7" | X8 != "7" )
& ( X2 != "8" | X8 != "8" )
& ( X2 != "9" | X8 != "9" )
& ( X2 != "1" | X9 != "1" )
& ( X2 != "2" | X9 != "2" )
& ( X2 != "3" | X9 != "3" )
& ( X2 != "4" | X9 != "4" )
& ( X2 != "5" | X9 != "5" )
& ( X2 != "6" | X9 != "6" )
& ( X2 != "7" | X9 != "7" )
& ( X2 != "8" | X9 != "8" )
& ( X2 != "9" | X9 != "9" )
& ( X3 != "1" | X4 != "1" )
& ( X3 != "2" | X4 != "2" )
& ( X3 != "3" | X4 != "3" )
& ( X3 != "4" | X4 != "4" )
& ( X3 != "5" | X4 != "5" )
& ( X3 != "6" | X4 != "6" )
& ( X3 != "7" | X4 != "7" )
& ( X3 != "8" | X4 != "8" )
& ( X3 != "9" | X4 != "9" )
& ( X3 != "1" | X5 != "1" )
& ( X3 != "2" | X5 != "2" )
& ( X3 != "3" | X5 != "3" )
& ( X3 != "4" | X5 != "4" )
& ( X3 != "5" | X5 != "5" )
& ( X3 != "6" | X5 != "6" )
& ( X3 != "7" | X5 != "7" )
& ( X3 != "8" | X5 != "8" )
& ( X3 != "9" | X5 != "9" )
& ( X3 != "1" | X6 != "1" )
& ( X3 != "2" | X6 != "2" )
& ( X3 != "3" | X6 != "3" )
& ( X3 != "4" | X6 != "4" )
& ( X3 != "5" | X6 != "5" )
& ( X3 != "6" | X6 != "6" )
& ( X3 != "7" | X6 != "7" )
& ( X3 != "8" | X6 != "8" )
& ( X3 != "9" | X6 != "9" )
& ( X3 != "1" | X7 != "1" )
& ( X3 != "2" | X7 != "2" )
& ( X3 != "3" | X7 != "3" )
& ( X3 != "4" | X7 != "4" )
& ( X3 != "5" | X7 != "5" )
& ( X3 != "6" | X7 != "6" )
& ( X3 != "7" | X7 != "7" )
& ( X3 != "8" | X7 != "8" )
& ( X3 != "9" | X7 != "9" )
& ( X3 != "1" | X8 != "1" )
& ( X3 != "2" | X8 != "2" )
& ( X3 != "3" | X8 != "3" )
& ( X3 != "4" | X8 != "4" )
& ( X3 != "5" | X8 != "5" )
& ( X3 != "6" | X8 != "6" )
& ( X3 != "7" | X8 != "7" )
& ( X3 != "8" | X8 != "8" )
& ( X3 != "9" | X8 != "9" )
& ( X3 != "1" | X9 != "1" )
& ( X3 != "2" | X9 != "2" )
& ( X3 != "3" | X9 != "3" )
& ( X3 != "4" | X9 != "4" )
& ( X3 != "5" | X9 != "5" )
& ( X3 != "6" | X9 != "6" )
& ( X3 != "7" | X9 != "7" )
& ( X3 != "8" | X9 != "8" )
& ( X3 != "9" | X9 != "9" )
& ( X4 != "1" | X5 != "1" )
& ( X4 != "2" | X5 != "2" )
& ( X4 != "3" | X5 != "3" )
& ( X4 != "4" | X5 != "4" )
& ( X4 != "5" | X5 != "5" )
& ( X4 != "6" | X5 != "6" )
& ( X4 != "7" | X5 != "7" )
& ( X4 != "8" | X5 != "8" )
& ( X4 != "9" | X5 != "9" )
& ( X4 != "1" | X6 != "1" )
& ( X4 != "2" | X6 != "2" )
& ( X4 != "3" | X6 != "3" )
& ( X4 != "4" | X6 != "4" )
& ( X4 != "5" | X6 != "5" )
& ( X4 != "6" | X6 != "6" )
& ( X4 != "7" | X6 != "7" )
& ( X4 != "8" | X6 != "8" )
& ( X4 != "9" | X6 != "9" )
& ( X4 != "1" | X7 != "1" )
& ( X4 != "2" | X7 != "2" )
& ( X4 != "3" | X7 != "3" )
& ( X4 != "4" | X7 != "4" )
& ( X4 != "5" | X7 != "5" )
& ( X4 != "6" | X7 != "6" )
& ( X4 != "7" | X7 != "7" )
& ( X4 != "8" | X7 != "8" )
& ( X4 != "9" | X7 != "9" )
& ( X4 != "1" | X8 != "1" )
& ( X4 != "2" | X8 != "2" )
& ( X4 != "3" | X8 != "3" )
& ( X4 != "4" | X8 != "4" )
& ( X4 != "5" | X8 != "5" )
& ( X4 != "6" | X8 != "6" )
& ( X4 != "7" | X8 != "7" )
& ( X4 != "8" | X8 != "8" )
& ( X4 != "9" | X8 != "9" )
& ( X4 != "1" | X9 != "1" )
& ( X4 != "2" | X9 != "2" )
& ( X4 != "3" | X9 != "3" )
& ( X4 != "4" | X9 != "4" )
& ( X4 != "5" | X9 != "5" )
& ( X4 != "6" | X9 != "6" )
& ( X4 != "7" | X9 != "7" )
& ( X4 != "8" | X9 != "8" )
& ( X4 != "9" | X9 != "9" )
& ( X5 != "1" | X6 != "1" )
& ( X5 != "2" | X6 != "2" )
& ( X5 != "3" | X6 != "3" )
& ( X5 != "4" | X6 != "4" )
& ( X5 != "5" | X6 != "5" )
& ( X5 != "6" | X6 != "6" )
& ( X5 != "7" | X6 != "7" )
& ( X5 != "8" | X6 != "8" )
& ( X5 != "9" | X6 != "9" )
& ( X5 != "1" | X7 != "1" )
& ( X5 != "2" | X7 != "2" )
& ( X5 != "3" | X7 != "3" )
& ( X5 != "4" | X7 != "4" )
& ( X5 != "5" | X7 != "5" )
& ( X5 != "6" | X7 != "6" )
& ( X5 != "7" | X7 != "7" )
& ( X5 != "8" | X7 != "8" )
& ( X5 != "9" | X7 != "9" )
& ( X5 != "1" | X8 != "1" )
& ( X5 != "2" | X8 != "2" )
& ( X5 != "3" | X8 != "3" )
& ( X5 != "4" | X8 != "4" )
& ( X5 != "5" | X8 != "5" )
& ( X5 != "6" | X8 != "6" )
& ( X5 != "7" | X8 != "7" )
& ( X5 != "8" | X8 != "8" )
& ( X5 != "9" | X8 != "9" )
& ( X5 != "1" | X9 != "1" )
& ( X5 != "2" | X9 != "2" )
& ( X5 != "3" | X9 != "3" )
& ( X5 != "4" | X9 != "4" )
& ( X5 != "5" | X9 != "5" )
& ( X5 != "6" | X9 != "6" )
& ( X5 != "7" | X9 != "7" )
& ( X5 != "8" | X9 != "8" )
& ( X5 != "9" | X9 != "9" )
& ( X6 != "1" | X7 != "1" )
& ( X6 != "2" | X7 != "2" )
& ( X6 != "3" | X7 != "3" )
& ( X6 != "4" | X7 != "4" )
& ( X6 != "5" | X7 != "5" )
& ( X6 != "6" | X7 != "6" )
& ( X6 != "7" | X7 != "7" )
& ( X6 != "8" | X7 != "8" )
& ( X6 != "9" | X7 != "9" )
& ( X6 != "1" | X8 != "1" )
& ( X6 != "2" | X8 != "2" )
& ( X6 != "3" | X8 != "3" )
& ( X6 != "4" | X8 != "4" )
& ( X6 != "5" | X8 != "5" )
& ( X6 != "6" | X8 != "6" )
& ( X6 != "7" | X8 != "7" )
& ( X6 != "8" | X8 != "8" )
& ( X6 != "9" | X8 != "9" )
& ( X6 != "1" | X9 != "1" )
& ( X6 != "2" | X9 != "2" )
& ( X6 != "3" | X9 != "3" )
& ( X6 != "4" | X9 != "4" )
& ( X6 != "5" | X9 != "5" )
& ( X6 != "6" | X9 != "6" )
& ( X6 != "7" | X9 != "7" )
& ( X6 != "8" | X9 != "8" )
& ( X6 != "9" | X9 != "9" )
& ( X7 != "1" | X8 != "1" )
& ( X7 != "2" | X8 != "2" )
& ( X7 != "3" | X8 != "3" )
& ( X7 != "4" | X8 != "4" )
& ( X7 != "5" | X8 != "5" )
& ( X7 != "6" | X8 != "6" )
& ( X7 != "7" | X8 != "7" )
& ( X7 != "8" | X8 != "8" )
& ( X7 != "9" | X8 != "9" )
& ( X7 != "1" | X9 != "1" )
& ( X7 != "2" | X9 != "2" )
& ( X7 != "3" | X9 != "3" )
& ( X7 != "4" | X9 != "4" )
& ( X7 != "5" | X9 != "5" )
& ( X7 != "6" | X9 != "6" )
& ( X7 != "7" | X9 != "7" )
& ( X7 != "8" | X9 != "8" )
& ( X7 != "9" | X9 != "9" )
& ( X8 != "1" | X9 != "1" )
& ( X8 != "2" | X9 != "2" )
& ( X8 != "3" | X9 != "3" )
& ( X8 != "4" | X9 != "4" )
& ( X8 != "5" | X9 != "5" )
& ( X8 != "6" | X9 != "6" )
& ( X8 != "7" | X9 != "7" )
& ( X8 != "8" | X9 != "8" )
& ( X8 != "9" | X9 != "9" ) ) ) )).
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(placement(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(solutionTo,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,
Y11,Y12,Y13,Y14,Y15,Y16,Y17,Y18,Y19,
Y21,Y22,Y23,Y24,Y25,Y26,Y27,Y28,Y29,
Y31,Y32,Y33,Y34,Y35,Y36,Y37,Y38,Y39,
Y41,Y42,Y43,Y44,Y45,Y46,Y47,Y48,Y49,
Y51,Y52,Y53,Y54,Y55,Y56,Y57,Y58,Y59,
Y61,Y62,Y63,Y64,Y65,Y66,Y67,Y68,Y69,
Y71,Y72,Y73,Y74,Y75,Y76,Y77,Y78,Y79,
Y81,Y82,Y83,Y84,Y85,Y86,Y87,Y88,Y89,
Y91,Y92,Y93,Y94,Y95,Y96,Y97,Y98,Y99] :
( isSolutionTo(placement(Y11,Y12,Y13,Y14,Y15,Y16,Y17,Y18,Y19,
Y21,Y22,Y23,Y24,Y25,Y26,Y27,Y28,Y29,
Y31,Y32,Y33,Y34,Y35,Y36,Y37,Y38,Y39,
Y41,Y42,Y43,Y44,Y45,Y46,Y47,Y48,Y49,
Y51,Y52,Y53,Y54,Y55,Y56,Y57,Y58,Y59,
Y61,Y62,Y63,Y64,Y65,Y66,Y67,Y68,Y69,
Y71,Y72,Y73,Y74,Y75,Y76,Y77,Y78,Y79,
Y81,Y82,Y83,Y84,Y85,Y86,Y87,Y88,Y89,
Y91,Y92,Y93,Y94,Y95,Y96,Y97,Y98,Y99),
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))
<=> ( isPlacementFor(placement(Y11,Y12,Y13,Y14,Y15,Y16,Y17,Y18,Y19,
Y21,Y22,Y23,Y24,Y25,Y26,Y27,Y28,Y29,
Y31,Y32,Y33,Y34,Y35,Y36,Y37,Y38,Y39,
Y41,Y42,Y43,Y44,Y45,Y46,Y47,Y48,Y49,
Y51,Y52,Y53,Y54,Y55,Y56,Y57,Y58,Y59,
Y61,Y62,Y63,Y64,Y65,Y66,Y67,Y68,Y69,
Y71,Y72,Y73,Y74,Y75,Y76,Y77,Y78,Y79,
Y81,Y82,Y83,Y84,Y85,Y86,Y87,Y88,Y89,
Y91,Y92,Y93,Y94,Y95,Y96,Y97,Y98,Y99),
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(placement(Y11,Y12,Y13,Y14,Y15,Y16,Y17,Y18,Y19,
Y21,Y22,Y23,Y24,Y25,Y26,Y27,Y28,Y29,
Y31,Y32,Y33,Y34,Y35,Y36,Y37,Y38,Y39,
Y41,Y42,Y43,Y44,Y45,Y46,Y47,Y48,Y49,
Y51,Y52,Y53,Y54,Y55,Y56,Y57,Y58,Y59,
Y61,Y62,Y63,Y64,Y65,Y66,Y67,Y68,Y69,
Y71,Y72,Y73,Y74,Y75,Y76,Y77,Y78,Y79,
Y81,Y82,Y83,Y84,Y85,Y86,Y87,Y88,Y89,
Y91,Y92,Y93,Y94,Y95,Y96,Y97,Y98,Y99)) ) ) )).
% also can be used as the problem
%fof(unfinishedSolution,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] :
% unfinishedSolution("1",X12,"9",X14,"7","5",X17,"3","2",
% "8","3",X23,"6","2",X26,"7","9",X29,
% X31,"7","2","9",X35,"3","6",X38,"8",
% "6",X42,"5",X44,X45,"4","9",X48,"7",
% X51,"9",X53,"2","6",X56,X57,"5",X59,
% "3",X62,"7","5",X65,"8","2",X68,"4",
% "2",X72,"3","4",X75,"9","1","7",X79,
% X81,"5","6",X84,"1","2",X87,"4","3",
% "7","4",X93,"3","8",X96,"5",X98,"9") )).
% example of solving the problem
%fof(solveUnfinishedSolution,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] :
% ( unfinishedSolution(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(placement(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)) ) )).
% test predicates
%fof(checkSolution,conjecture,(
% isSolution(placement("1","6","9","8","7","5","4","3","2",
% "8","3","4","6","2","1","7","9","5",
% "5","7","2","9","4","3","6","1","8",
% "6","2","5","1","3","4","9","8","7",
% "4","9","8","2","6","7","3","5","1",
% "3","1","7","5","9","8","2","6","4",
% "2","8","3","4","5","9","1","7","6",
% "9","5","6","7","1","2","8","4","3",
% "7","4","1","3","8","6","5","2","9")) )).
%fof(checkSolutionTo,conjecture,(
% isSolutionTo(placement("1","6","9","8","7","5","4","3","2",
% "8","3","4","6","2","1","7","9","5",
% "5","7","2","9","4","3","6","1","8",
% "6","2","5","1","3","4","9","8","7",
% "4","9","8","2","6","7","3","5","1",
% "3","1","7","5","9","8","2","6","4",
% "2","8","3","4","5","9","1","7","6",
% "9","5","6","7","1","2","8","4","3",
% "7","4","1","3","8","6","5","2","9"),
% problem("1","_","_","_","7","_","_","3","_",
% "8","3","_","6","_","_","_","_","_",
% "_","_","2","9","_","_","6","_","8",
% "6","_","_","_","_","4","9","_","7",
% "_","9","_","_","_","_","_","5","_",
% "3","_","7","5","_","_","_","_","4",
% "2","_","3","_","_","9","1","_","_",
% "_","_","_","_","_","2","_","4","3",
% "_","4","_","_","8","_","_","_","9")) )).
% example of solving a problem
%fof(sovleProblem,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] :
% isSolutionTo(placement(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("1","_","9","_","7","5","_","3","2",
% "8","3","_","6","2","_","7","9","_",
% "_","7","2","9","_","3","6","_","8",
% "6","_","5","_","_","4","9","_","7",
% "_","9","_","2","6","_","_","5","_",
% "3","_","7","5","_","8","2","_","4",
% "2","_","3","4","_","9","1","7","_",
% "_","5","6","_","1","2","_","4","3",
% "7","4","_","3","8","_","5","_","9")) )).
fof(sovleProblem,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] :
isSolutionTo(placement(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("1","_","_","_","7","_","_","3","_",
"8","3","_","6","_","_","_","_","_",
"_","_","2","9","_","_","6","_","8",
"6","_","_","_","_","4","9","_","7",
"_","9","_","_","_","_","_","5","_",
"3","_","7","5","_","_","_","_","4",
"2","_","3","_","_","9","1","_","_",
"_","_","_","_","_","2","_","4","3",
"_","4","_","_","8","_","_","_","9")) )).