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