This file is indexed.

/usr/share/doc/prover9-doc/examples/queens2.out is in prover9-doc 0.0.200902a-2.

This file is owned by root:root, with mode 0o644.

The actual contents of the file can be viewed below.

 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
============================== Mace4 =================================
Mace4 (32) version 2009-02A, February 2009.
Process 15894 was started by mccune on cleo,
Wed Feb 25 12:26:29 2009
The command was "/home/mccune/bin/mace4 -n8 -f queens2.in".
============================== end of head ===========================

============================== INPUT =================================

% Reading from file queens2.in

set(arithmetic).
    % set(arithmetic) -> clear(lnh).
    % set(arithmetic) -> assign(selection_order, 0).

    % Declaring Mace4 arithmetic parse types.

formulas(assumptions).
(all x exists y Q(x,y)).
Q(x,y1) & Q(x,y2) -> y1 = y2.
Q(x1,y) & Q(x2,y) -> x1 = x2.
Q(x1,y1) & Q(x2,y2) & x2 + -x1 = y2 + -y1 -> x1 = x2 & y1 = y2.
Q(x1,y1) & Q(x2,y2) & x1 + -x2 = y2 + -y1 -> x1 = x2 & y1 = y2.
end_of_list.
    % assign(domain_size, 8) -> assign(start_size, 8).
    % assign(domain_size, 8) -> assign(end_size, 8).

% From the command line: assign(domain_size, 8).

============================== end of input ==========================

============================== PROCESS NON-CLAUSAL FORMULAS ==========

% Formulas that are not ordinary clauses:
1 (all x exists y Q(x,y)) # label(non_clause).  [assumption].
2 Q(x,y1) & Q(x,y2) -> y1 = y2 # label(non_clause).  [assumption].
3 Q(x1,y) & Q(x2,y) -> x1 = x2 # label(non_clause).  [assumption].
4 Q(x1,y1) & Q(x2,y2) & x2 + -x1 = y2 + -y1 -> x1 = x2 & y1 = y2 # label(non_clause).  [assumption].
5 Q(x1,y1) & Q(x2,y2) & x1 + -x2 = y2 + -y1 -> x1 = x2 & y1 = y2 # label(non_clause).  [assumption].

============================== end of process non-clausal formulas ===

============================== CLAUSES FOR SEARCH ====================

formulas(mace4_clauses).
Q(x,f1(x)).
-Q(x,y) | -Q(x,z) | z = y.
-Q(x,y) | -Q(z,y) | z = x.
-Q(x,y) | -Q(z,u) | z + -x != u + -y | z = x.
-Q(x,y) | -Q(z,u) | z + -x != u + -y | u = y.
-Q(x,y) | -Q(z,u) | x + -z != u + -y | z = x.
-Q(x,y) | -Q(z,u) | x + -z != u + -y | u = y.
end_of_list.

============================== end of clauses for search =============

% There are no natural numbers in the input.

============================== DOMAIN SIZE 8 =========================

============================== MODEL =================================

interpretation( 8, [number=1, seconds=0], [

        function(f1(_), [ 0, 4, 7, 5, 2, 6, 1, 3 ]),

        relation(Q(_,_), [
			   1, 0, 0, 0, 0, 0, 0, 0,
			   0, 0, 0, 0, 1, 0, 0, 0,
			   0, 0, 0, 0, 0, 0, 0, 1,
			   0, 0, 0, 0, 0, 1, 0, 0,
			   0, 0, 1, 0, 0, 0, 0, 0,
			   0, 0, 0, 0, 0, 0, 1, 0,
			   0, 1, 0, 0, 0, 0, 0, 0,
			   0, 0, 0, 1, 0, 0, 0, 0 ])
]).

============================== end of model ==========================

============================== STATISTICS ============================

For domain size 8.

Current CPU time: 0.00 seconds (total CPU time: 0.07 seconds).
Ground clauses: seen=17416, kept=2024.
Selections=18, assignments=132, propagations=531, current_models=1.
Rewrite_terms=193, rewrite_bools=9165, indexes=79.
Rules_from_neg_clauses=61, cross_offs=258.

============================== end of statistics =====================

User_CPU=0.07, System_CPU=0.00, Wall_clock=0.

Exiting with 1 model.

Process 15894 exit (max_models) Wed Feb 25 12:26:29 2009
The process finished Wed Feb 25 12:26:29 2009