This file is indexed.

/usr/share/doc/prover9-doc/examples/send-money.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
 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
============================== Mace4 =================================
Mace4 (32) version 2009-02A, February 2009.
Process 15896 was started by mccune on cleo,
Wed Feb 25 12:26:30 2009
The command was "/home/mccune/bin/mace4 -f send-money.in".
============================== end of head ===========================

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

% Reading from file send-money.in

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

    % Declaring Mace4 arithmetic parse types.
assign(domain_size,10).
    % assign(domain_size, 10) -> assign(start_size, 10).
    % assign(domain_size, 10) -> assign(end_size, 10).

list(distinct).
[S,E,N,D,M,O,R,Y].
end_of_list.

formulas(assumptions).
D + E = Y + C1 * 10.
N + R + C1 = E + C2 * 10.
E + O + C2 = N + C3 * 10.
S + M + C3 = O + M * 10.
S != 0.
M != 0.
end_of_list.

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

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

% Formulas that are not ordinary clauses:

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

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

formulas(mace4_clauses).
D + E = Y + C1 * 10.
N + R + C1 = E + C2 * 10.
E + O + C2 = N + C3 * 10.
S + M + C3 = O + M * 10.
S != 0.
M != 0.
S != E.
S != N.
S != D.
S != M.
S != O.
S != R.
S != Y.
E != N.
E != D.
E != M.
E != O.
E != R.
E != Y.
N != D.
N != M.
N != O.
N != R.
N != Y.
D != M.
D != O.
D != R.
D != Y.
M != O.
M != R.
M != Y.
O != R.
O != Y.
R != Y.
end_of_list.

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

% The largest natural number in the input is 10.

============================== DOMAIN SIZE 10 ========================

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

interpretation( 10, [number=1, seconds=2], [

        function(C1, [ 1 ]),

        function(C2, [ 1 ]),

        function(C3, [ 0 ]),

        function(D, [ 7 ]),

        function(E, [ 5 ]),

        function(M, [ 1 ]),

        function(N, [ 6 ]),

        function(O, [ 0 ]),

        function(R, [ 8 ]),

        function(S, [ 9 ]),

        function(Y, [ 2 ])
]).

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

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

For domain size 10.

Current CPU time: 0.00 seconds (total CPU time: 2.56 seconds).
Ground clauses: seen=34, kept=34.
Selections=242526, assignments=2425201, propagations=0, current_models=1.
Rewrite_terms=7196584, rewrite_bools=5030322, indexes=0.
Rules_from_neg_clauses=0, cross_offs=89005.

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

User_CPU=2.56, System_CPU=0.04, Wall_clock=2.

Exiting with 1 model.

Process 15896 exit (max_models) Wed Feb 25 12:26:32 2009
The process finished Wed Feb 25 12:26:32 2009