/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
|