% time paradox3 --model sudoku-paradox.tptp
Paradox, version 3.0, 2008-07-29.
+++ PROBLEM: sudoku-paradox.tptp
Reading 'sudoku-paradox.tptp' ... OK
+++ SOLVING: sudoku-paradox.tptp
domain size 1
domain size 2
domain size 3
domain size 4
domain size 5
domain size 6
domain size 7
domain size 8
domain size 9
+++ BEGIN MODEL
% domain size is 9

1 = !1

2 = !2

3 = !3

4 = !4

5 = !5

6 = !6

7 = !7

8 = !8

9 = !9

a(!1,!1) = !1
a(!1,!2) = !4
a(!1,!3) = !5
a(!1,!4) = !2
a(!1,!5) = !8
a(!1,!6) = !9
a(!1,!7) = !3
a(!1,!8) = !7
a(!1,!9) = !6
a(!2,!1) = !7
a(!2,!2) = !2
a(!2,!3) = !6
a(!2,!4) = !5
a(!2,!5) = !3
a(!2,!6) = !1
a(!2,!7) = !8
a(!2,!8) = !4
a(!2,!9) = !9
a(!3,!1) = !9
a(!3,!2) = !8
a(!3,!3) = !3
a(!3,!4) = !7
a(!3,!5) = !6
a(!3,!6) = !4
a(!3,!7) = !1
a(!3,!8) = !2
a(!3,!9) = !5
a(!4,!1) = !6
a(!4,!2) = !1
a(!4,!3) = !9
a(!4,!4) = !4
a(!4,!5) = !2
a(!4,!6) = !7
a(!4,!7) = !5
a(!4,!8) = !3
a(!4,!9) = !8
a(!5,!1) = !3
a(!5,!2) = !7
a(!5,!3) = !4
a(!5,!4) = !1
a(!5,!5) = !5
a(!5,!6) = !8
a(!5,!7) = !9
a(!5,!8) = !6
a(!5,!9) = !2
a(!6,!1) = !2
a(!6,!2) = !5
a(!6,!3) = !8
a(!6,!4) = !3
a(!6,!5) = !9
a(!6,!6) = !6
a(!6,!7) = !4
a(!6,!8) = !1
a(!6,!9) = !7
a(!7,!1) = !8
a(!7,!2) = !6
a(!7,!3) = !2
a(!7,!4) = !9
a(!7,!5) = !4
a(!7,!6) = !3
a(!7,!7) = !7
a(!7,!8) = !5
a(!7,!9) = !1
a(!8,!1) = !4
a(!8,!2) = !9
a(!8,!3) = !7
a(!8,!4) = !6
a(!8,!5) = !1
a(!8,!6) = !5
a(!8,!7) = !2
a(!8,!8) = !8
a(!8,!9) = !3
a(!9,!1) = !5
a(!9,!2) = !3
a(!9,!3) = !1
a(!9,!4) = !8
a(!9,!5) = !7
a(!9,!6) = !2
a(!9,!7) = !6
a(!9,!8) = !9
a(!9,!9) = !4

r1(!1) <=> $true
r1(!2) <=> $true
r1(!3) <=> $true
r1(!4) <=> $false
r1(!5) <=> $false
r1(!6) <=> $false
r1(!7) <=> $false
r1(!8) <=> $false
r1(!9) <=> $false

r2(!1) <=> $false
r2(!2) <=> $false
r2(!3) <=> $false
r2(!4) <=> $true
r2(!5) <=> $true
r2(!6) <=> $true
r2(!7) <=> $false
r2(!8) <=> $false
r2(!9) <=> $false

r3(!1) <=> $false
r3(!2) <=> $false
r3(!3) <=> $false
r3(!4) <=> $false
r3(!5) <=> $false
r3(!6) <=> $false
r3(!7) <=> $true
r3(!8) <=> $true
r3(!9) <=> $true
+++ END MODEL
+++ RESULT: Satisfiable
paradox3 --model sudoku-paradox.tptp  0.01s user 0.00s system 2% cpu 0.697 total
%