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
134
135
136
137
138
139
140
141
142
143
|
============================== Mace4 =================================
Mace4 (64) version 2009-11A, November 2009.
Process 3232 was started by koen on vdheijden-arch,
Sun Jan 15 16:43:42 2017
The command was "mace4 -f logic_b.m4.in".
============================== end of head ===========================
============================== INPUT =================================
% Reading from file logic_b.m4.in
formulas(sos).
x * (y * z) = (x * y) * z.
x * I = x.
x * inv(x) = I.
end_of_list.
formulas(goals).
(all x all y x * y = y * x).
end_of_list.
============================== end of input ==========================
============================== PROCESS NON-CLAUSAL FORMULAS ==========
% Formulas that are not ordinary clauses:
1 (all x all y x * y = y * x) # label(non_clause) # label(goal). [goal].
============================== end of process non-clausal formulas ===
============================== CLAUSES FOR SEARCH ====================
formulas(mace4_clauses).
x * (y * z) = (x * y) * z.
x * I = x.
x * inv(x) = I.
c2 * c1 != c1 * c2.
end_of_list.
============================== end of clauses for search =============
% There are no natural numbers in the input.
============================== DOMAIN SIZE 2 =========================
============================== STATISTICS ============================
For domain size 2.
Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds).
Ground clauses: seen=13, kept=13.
Selections=4, assignments=7, propagations=6, current_models=0.
Rewrite_terms=62, rewrite_bools=16, indexes=8.
Rules_from_neg_clauses=2, cross_offs=2.
============================== end of statistics =====================
============================== DOMAIN SIZE 3 =========================
============================== STATISTICS ============================
For domain size 3.
Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds).
Ground clauses: seen=34, kept=34.
Selections=7, assignments=17, propagations=30, current_models=0.
Rewrite_terms=298, rewrite_bools=71, indexes=52.
Rules_from_neg_clauses=8, cross_offs=24.
============================== end of statistics =====================
============================== DOMAIN SIZE 4 =========================
============================== STATISTICS ============================
For domain size 4.
Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds).
Ground clauses: seen=73, kept=73.
Selections=14, assignments=45, propagations=110, current_models=0.
Rewrite_terms=1132, rewrite_bools=232, indexes=206.
Rules_from_neg_clauses=18, cross_offs=98.
============================== end of statistics =====================
============================== DOMAIN SIZE 5 =========================
============================== STATISTICS ============================
For domain size 5.
Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds).
Ground clauses: seen=136, kept=136.
Selections=24, assignments=91, propagations=201, current_models=0.
Rewrite_terms=2416, rewrite_bools=472, indexes=582.
Rules_from_neg_clauses=31, cross_offs=228.
============================== end of statistics =====================
============================== DOMAIN SIZE 6 =========================
============================== MODEL =================================
interpretation( 6, [number=1, seconds=0], [
function(I, [ 0 ]),
function(c1, [ 1 ]),
function(c2, [ 2 ]),
function(inv(_), [ 0, 1, 2, 4, 3, 5 ]),
function(*(_,_), [
0, 1, 2, 3, 4, 5,
1, 0, 3, 2, 5, 4,
2, 4, 0, 5, 1, 3,
3, 5, 1, 4, 0, 2,
4, 2, 5, 0, 3, 1,
5, 3, 4, 1, 2, 0 ])
]).
============================== end of model ==========================
============================== STATISTICS ============================
For domain size 6.
Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds).
Ground clauses: seen=229, kept=229.
Selections=14, assignments=44, propagations=94, current_models=1.
Rewrite_terms=1566, rewrite_bools=339, indexes=370.
Rules_from_neg_clauses=8, cross_offs=138.
============================== end of statistics =====================
User_CPU=0.01, System_CPU=0.00, Wall_clock=0.
Exiting with 1 model.
Process 3232 exit (max_models) Sun Jan 15 16:43:42 2017
The process finished Sun Jan 15 16:43:42 2017
|
