← Back to branch summary

~ubuntu-branches/ubuntu/saucy/ladr/saucy

« back to all changes in this revision

Viewing changes to apps.src/h1.out

  • Committer: Package Import Robot
  • Author(s): Frank Lichtenheld
  • Date: 2013-05-25 11:43:32 UTC
  • mfrom: (5.1.5 sid)
  • Revision ID: package-import@ubuntu.com-20130525114332-lkzco1dti2hwrf7v
Tags: 0.0.200911a-2
* QA upload.
* Upload to unstable.
* Change maintainer to QA group.

Show diffs side-by-side

added added

removed removed

Lines of Context:
apps.src/h1.out
 
1
============================== Mace4 =================================
 
2
Mace4 (32) version 2009-02A, February 2009.
 
3
Process 20734 was started by mccune on cleo,
 
4
Tue Mar 17 10:49:28 2009
 
5
The command was "mace4 -f h1.in".
 
6
============================== end of head ===========================
 
7
 
 
8
============================== INPUT =================================
 
9
 
 
10
% Reading from file h1.in
 
11
 
 
12
op(500,infix,"+").
 
13
op(490,infix,";").
 
14
op(490,infix,"*").
 
15
op(480,postfix,"^").
 
16
op(490,infix,"||").
 
17
op(490,infix,"/\").
 
18
op(490,infix,"!!").
 
19
if(Prover9).
 
20
% Conditional input omitted.
 
21
end_if.
 
22
if(Mace4).
 
23
% Conditional input included.
 
24
assign(max_seconds,60).
 
25
end_if.
 
26
 
 
27
formulas(assumptions).
 
28
x + y = y + x.
 
29
x + 0 = x.
 
30
x + (y + z) = (x + y) + z.
 
31
x ; 1 = x & 1 ; x = x.
 
32
x ; (y ; z) = (x ; y) ; z.
 
33
x * 1 = x & 1 * x = x.
 
34
x * (y * z) = (x * y) * z.
 
35
(x + y) ; z = x ; z + y ; z.
 
36
(x + y) * z = x * z + y * z.
 
37
z ; (x + y) = z ; x + z ; y.
 
38
z * (x + y) = z * x + z * y.
 
39
0 ; x = 0.
 
40
x ; 0 = 0.
 
41
0 * x = 0.
 
42
x * 0 = 0.
 
43
x + x = x.
 
44
x <= y <-> x + y = y.
 
45
(x * x1) ; (y * y1) <= (x1 ; y) * (x ; y1).
 
46
x /\ y <= x.
 
47
x /\ y <= y.
 
48
z <= x & z <= y -> z <= x /\ y.
 
49
x || y = (x ; y) /\ (y ; x).
 
50
x !! y = (x /\ 1) ; y + x ; (y /\ 1).
 
51
end_of_list.
 
52
 
 
53
formulas(goals).
 
54
x !! y = y !! x.
 
55
end_of_list.
 
56
 
 
57
============================== end of input ==========================
 
58
 
 
59
============================== PROCESS NON-CLAUSAL FORMULAS ==========
 
60
 
 
61
% Formulas that are not ordinary clauses:
 
62
1 x ; 1 = x & 1 ; x = x # label(non_clause).  [assumption].
 
63
2 x * 1 = x & 1 * x = x # label(non_clause).  [assumption].
 
64
3 x <= y <-> x + y = y # label(non_clause).  [assumption].
 
65
4 z <= x & z <= y -> z <= x /\ y # label(non_clause).  [assumption].
 
66
5 x !! y = y !! x # label(non_clause) # label(goal).  [goal].
 
67
 
 
68
============================== end of process non-clausal formulas ===
 
69
 
 
70
============================== CLAUSES FOR SEARCH ====================
 
71
 
 
72
formulas(mace4_clauses).
 
73
x + y = y + x.
 
74
x + 0 = x.
 
75
x + (y + z) = (x + y) + z.
 
76
x ; 1 = x.
 
77
1 ; x = x.
 
78
x ; (y ; z) = (x ; y) ; z.
 
79
x * 1 = x.
 
80
1 * x = x.
 
81
x * (y * z) = (x * y) * z.
 
82
(x + y) ; z = x ; z + y ; z.
 
83
(x + y) * z = x * z + y * z.
 
84
x ; (y + z) = x ; y + x ; z.
 
85
x * (y + z) = x * y + x * z.
 
86
0 ; x = 0.
 
87
x ; 0 = 0.
 
88
0 * x = 0.
 
89
x * 0 = 0.
 
90
x + x = x.
 
91
-(x <= y) | x + y = y.
 
92
x <= y | x + y != y.
 
93
(x * y) ; (z * u) <= (y ; z) * (x ; u).
 
94
x /\ y <= x.
 
95
x /\ y <= y.
 
96
-(x <= y) | -(x <= z) | x <= y /\ z.
 
97
x || y = (x ; y) /\ (y ; x).
 
98
x !! y = (x /\ 1) ; y + x ; (y /\ 1).
 
99
c2 !! c1 != c1 !! c2.
 
100
end_of_list.
 
101
 
 
102
============================== end of clauses for search =============
 
103
 
 
104
% The largest natural number in the input is 1.
 
105
 
 
106
============================== DOMAIN SIZE 2 =========================
 
107
 
 
108
============================== STATISTICS ============================
 
109
 
 
110
For domain size 2.
 
111
 
 
112
Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds).
 
113
Ground clauses: seen=129, kept=58.
 
114
Selections=3, assignments=6, propagations=28, current_models=0.
 
115
Rewrite_terms=121, rewrite_bools=61, indexes=0.
 
116
Rules_from_neg_clauses=6, cross_offs=6.
 
117
 
 
118
============================== end of statistics =====================
 
119
 
 
120
============================== DOMAIN SIZE 3 =========================
 
121
 
 
122
============================== STATISTICS ============================
 
123
 
 
124
For domain size 3.
 
125
 
 
126
Current CPU time: 0.00 seconds (total CPU time: 0.12 seconds).
 
127
Ground clauses: seen=391, kept=251.
 
128
Selections=2425, assignments=7275, propagations=14992, current_models=0.
 
129
Rewrite_terms=458623, rewrite_bools=164648, indexes=14310.
 
130
Rules_from_neg_clauses=4543, cross_offs=12388.
 
131
 
 
132
============================== end of statistics =====================
 
133
 
 
134
============================== DOMAIN SIZE 4 =========================
 
135
 
 
136
============================== MODEL =================================
 
137
 
 
138
interpretation( 4, [number=1, seconds=4], [
 
139
 
 
140
        function(c1, [ 2 ]),
 
141
 
 
142
        function(c2, [ 3 ]),
 
143
 
 
144
        function(!!(_,_), [
 
145
                           0, 0, 0, 0,
 
146
                           0, 1, 2, 3,
 
147
                           0, 2, 0, 0,
 
148
                           0, 3, 2, 3 ]),
 
149
 
 
150
        function(*(_,_), [
 
151
                           0, 0, 0, 0,
 
152
                           0, 1, 2, 3,
 
153
                           0, 2, 0, 2,
 
154
                           0, 3, 2, 3 ]),
 
155
 
 
156
        function(+(_,_), [
 
157
                           0, 1, 2, 3,
 
158
                           1, 1, 1, 1,
 
159
                           2, 1, 2, 3,
 
160
                           3, 1, 3, 3 ]),
 
161
 
 
162
        function(/\(_,_), [
 
163
                           0, 0, 0, 0,
 
164
                           0, 1, 2, 3,
 
165
                           0, 2, 2, 2,
 
166
                           0, 3, 2, 3 ]),
 
167
 
 
168
        function(;(_,_), [
 
169
                           0, 0, 0, 0,
 
170
                           0, 1, 2, 3,
 
171
                           0, 2, 0, 0,
 
172
                           0, 3, 2, 3 ]),
 
173
 
 
174
        function(||(_,_), [
 
175
                           0, 0, 0, 0,
 
176
                           0, 1, 2, 3,
 
177
                           0, 2, 0, 0,
 
178
                           0, 3, 0, 3 ]),
 
179
 
 
180
        relation(<=(_,_), [
 
181
                           1, 1, 1, 1,
 
182
                           0, 1, 0, 0,
 
183
                           0, 1, 1, 1,
 
184
                           0, 1, 0, 1 ])
 
185
]).
 
186
 
 
187
============================== end of model ==========================
 
188
 
 
189
============================== STATISTICS ============================
 
190
 
 
191
For domain size 4.
 
192
 
 
193
Current CPU time: 0.00 seconds (total CPU time: 4.83 seconds).
 
194
Ground clauses: seen=921, kept=696.
 
195
Selections=36759, assignments=147005, propagations=665193, current_models=1.
 
196
Rewrite_terms=18503894, rewrite_bools=6591134, indexes=1533814.
 
197
Rules_from_neg_clauses=132667, cross_offs=660041.
 
198
 
 
199
============================== end of statistics =====================
 
200
 
 
201
User_CPU=4.83, System_CPU=0.01, Wall_clock=5.
 
202
 
 
203
Exiting with 1 model.
 
204
 
 
205
Process 20734 exit (max_models) Tue Mar 17 10:49:33 2009
 
206
The process finished Tue Mar 17 10:49:33 2009