-
Notifications
You must be signed in to change notification settings - Fork 0
/
Status
372 lines (365 loc) · 28.5 KB
/
Status
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
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
Proof summary for theory first_order_substitution
subs_TCC1.............................proved - complete [SHOSTAK](0.00 s)
subs_TCC2.............................proved - complete [SHOSTAK](0.00 s)
subs_TCC3.............................proved - complete [SHOSTAK](0.00 s)
subs_TCC4.............................proved - complete [SHOSTAK](0.00 s)
subs_TCC5.............................proved - complete [SHOSTAK](0.00 s)
subs_TCC6.............................proved - complete [SHOSTAK](0.00 s)
subs_TCC7.............................proved - complete [SHOSTAK](0.00 s)
subs_TCC8.............................proved - complete [SHOSTAK](0.00 s)
supset_dom_TCC1.......................proved - complete [SHOSTAK](0.00 s)
supset_dom_TCC2.......................proved - complete [SHOSTAK](0.00 s)
supset_dom_TCC3.......................proved - complete [SHOSTAK](0.00 s)
supset_dom_correct....................proved - complete [SHOSTAK](0.00 s)
dom_TCC1..............................proved - complete [SHOSTAK](0.00 s)
supset_dom_correct2...................proved - complete [SHOSTAK](0.00 s)
img_TCC1..............................proved - complete [SHOSTAK](0.00 s)
shift_TCC1............................proved - complete [SHOSTAK](0.00 s)
shift_TCC2............................proved - complete [SHOSTAK](0.00 s)
shift_TCC3............................proved - incomplete [SHOSTAK](0.00 s)
subs_const............................proved - complete [SHOSTAK](0.00 s)
subs_unit.............................proved - complete [SHOSTAK](0.00 s)
subs_pair.............................proved - complete [SHOSTAK](0.00 s)
subs_app..............................proved - complete [SHOSTAK](0.00 s)
subs_var..............................proved - complete [SHOSTAK](0.00 s)
subs_const2...........................proved - complete [SHOSTAK](0.00 s)
subs_pair2............................proved - complete [SHOSTAK](0.00 s)
subs_func.............................proved - complete [SHOSTAK](0.00 s)
subs_ord..............................proved - complete [SHOSTAK](0.00 s)
subs_mem..............................proved - complete [SHOSTAK](0.00 s)
subs_len..............................proved - complete [SHOSTAK](0.00 s)
subs_append...........................proved - complete [SHOSTAK](0.00 s)
subs_append2..........................proved - complete [SHOSTAK](0.00 s)
subs_map..............................proved - complete [SHOSTAK](0.00 s)
subs_append_args......................proved - complete [SHOSTAK](0.00 s)
subs_map_append_lst_args..............proved - complete [SHOSTAK](0.00 s)
subs_cons.............................proved - complete [SHOSTAK](0.00 s)
subs_equal?...........................proved - complete [SHOSTAK](0.00 s)
vars_subs_t...........................proved - complete [SHOSTAK](0.00 s)
basic_sub_no_effect...................proved - complete [SHOSTAK](0.00 s)
basic_sub_elim_var....................proved - complete [SHOSTAK](0.00 s)
basic_sub_not_elim_var................proved - complete [SHOSTAK](0.00 s)
dom_basic_sub.........................proved - complete [SHOSTAK](0.00 s)
dom_basic_sub2........................proved - complete [SHOSTAK](0.00 s)
dom_null..............................proved - complete [SHOSTAK](0.00 s)
dom_append............................proved - complete [SHOSTAK](0.00 s)
img_basic_sub.........................proved - complete [SHOSTAK](0.00 s)
img_null..............................proved - complete [SHOSTAK](0.00 s)
subs_no_effect_t......................proved - complete [SHOSTAK](0.00 s)
subs_no_effect_t_var..................proved - complete [SHOSTAK](0.00 s)
dom_append2...........................proved - complete [SHOSTAK](0.00 s)
dom_append3...........................proved - complete [SHOSTAK](0.00 s)
subs_no_effect_args...................proved - complete [SHOSTAK](0.00 s)
apply_sub_elim_var_t..................proved - complete [SHOSTAK](0.00 s)
vars_img_append.......................proved - complete [SHOSTAK](0.00 s)
idempotent_null.......................proved - complete [SHOSTAK](0.00 s)
var_dom_sub_dif_term..................proved - complete [SHOSTAK](0.00 s)
idempotent_disjoint_dom_img...........proved - complete [SHOSTAK](0.00 s)
idempotent_disjoint_dom_img2..........proved - complete [SHOSTAK](0.00 s)
apply_sub_elim_var_t2.................proved - complete [SHOSTAK](0.00 s)
subs_singleton........................proved - complete [SHOSTAK](0.00 s)
img_append_subset.....................proved - complete [SHOSTAK](0.00 s)
img_preservation......................proved - complete [SHOSTAK](0.00 s)
img_preservation_basic_subs...........proved - complete [SHOSTAK](0.00 s)
idempotent_append.....................proved - complete [SHOSTAK](0.00 s)
idempotent_subs_subs_t................proved - complete [SHOSTAK](0.00 s)
subs_divide_not_var...................proved - complete [SHOSTAK](0.00 s)
basic_sub_info........................proved - complete [SHOSTAK](0.00 s)
subterms_subs.........................proved - complete [SHOSTAK](0.00 s)
subs_no_effect_subterm................proved - complete [SHOSTAK](0.00 s)
subterms_img_append...................proved - complete [SHOSTAK](0.00 s)
same_func_subs........................proved - complete [SHOSTAK](0.00 s)
func_subterms_subs....................proved - complete [SHOSTAK](0.00 s)
supset_dom_equiv......................proved - complete [SHOSTAK](0.00 s)
supset_dom_append.....................proved - complete [SHOSTAK](0.00 s)
nice_disjoint_dom_img.................proved - complete [SHOSTAK](0.00 s)
nice_idempotent.......................proved - complete [SHOSTAK](0.00 s)
nice_append...........................proved - complete [SHOSTAK](0.00 s)
nice_append2..........................proved - complete [SHOSTAK](0.00 s)
nice_append_supset_dom................proved - complete [SHOSTAK](0.00 s)
niceness_preservation.................proved - complete [SHOSTAK](0.00 s)
nice_basic_sub_append.................proved - complete [SHOSTAK](0.00 s)
vars_img_sec_proj.....................proved - incomplete [SHOSTAK](0.00 s)
equal_sub_equiv.......................proved - complete [SHOSTAK](0.00 s)
equal_sub_equiv_alt...................proved - complete [SHOSTAK](0.00 s)
equal_sub_change_eq_terms.............proved - complete [SHOSTAK](0.00 s)
equal_sub_ref.........................proved - complete [SHOSTAK](0.00 s)
equal_sub_sym.........................proved - complete [SHOSTAK](0.00 s)
equal_sub_trans.......................proved - complete [SHOSTAK](0.00 s)
equal_sub_append......................proved - complete [SHOSTAK](0.00 s)
equal_sub_subset......................proved - complete [SHOSTAK](0.00 s)
equal_sub_res_trans...................proved - complete [SHOSTAK](0.00 s)
equal_sub_res_append..................proved - complete [SHOSTAK](0.00 s)
equal_syn_t...........................proved - complete [SHOSTAK](0.00 s)
idempotent_append_cond................proved - complete [SHOSTAK](0.00 s)
subs_inst.............................proved - complete [SHOSTAK](0.00 s)
contained_append......................proved - complete [SHOSTAK](0.00 s)
contained_supset......................proved - complete [SHOSTAK](0.00 s)
more_general_equal....................proved - complete [SHOSTAK](0.00 s)
more_general_append...................proved - complete [SHOSTAK](0.00 s)
more_general_supset...................proved - complete [SHOSTAK](0.00 s)
renaming_ord..........................proved - complete [SHOSTAK](0.00 s)
renaming_ord2.........................proved - complete [SHOSTAK](0.00 s)
renaming_var..........................proved - complete [SHOSTAK](0.00 s)
renaming_equal........................proved - complete [SHOSTAK](0.00 s)
renaming_var2_TCC1....................proved - complete [SHOSTAK](0.00 s)
renaming_var2.........................proved - complete [SHOSTAK](0.00 s)
renaming_equal_syn_TCC1...............proved - complete [SHOSTAK](0.00 s)
renaming_equal_syn....................proved - complete [SHOSTAK](0.00 s)
shift_cor.............................proved - complete [SHOSTAK](0.00 s)
shift_append_equal_syn................proved - incomplete [SHOSTAK](0.00 s)
shift_dom.............................proved - incomplete [SHOSTAK](0.00 s)
shift_dom2............................proved - incomplete [SHOSTAK](0.00 s)
shift_img.............................proved - incomplete [SHOSTAK](0.00 s)
shift_img2............................proved - incomplete [SHOSTAK](0.00 s)
shift_renaming........................proved - incomplete [SHOSTAK](0.00 s)
shift_append_renaming.................proved - incomplete [SHOSTAK](0.00 s)
Theory first_order_substitution totals: 115 formulas, 115 attempted, 115 succeeded (0.04 s)
Proof summary for theory first_order_terms_properties
size_TCC1.............................proved - complete [SHOSTAK](0.00 s)
size_TCC2.............................proved - complete [SHOSTAK](0.00 s)
size_TCC3.............................proved - complete [SHOSTAK](0.00 s)
size_TCC4.............................proved - complete [SHOSTAK](0.00 s)
size_TCC5.............................proved - complete [SHOSTAK](0.00 s)
size_TCC6.............................proved - complete [SHOSTAK](0.00 s)
size_TCC7.............................proved - complete [SHOSTAK](0.00 s)
size_TCC8.............................proved - complete [SHOSTAK](0.00 s)
size_TCC9.............................proved - complete [SHOSTAK](0.00 s)
size_TCC10............................proved - complete [SHOSTAK](0.00 s)
size_TCC11............................proved - complete [SHOSTAK](0.00 s)
size_TCC12............................proved - complete [SHOSTAK](0.00 s)
member_TCC1...........................proved - complete [SHOSTAK](0.00 s)
num_arg_TCC1..........................proved - complete [SHOSTAK](0.00 s)
num_arg_TCC2..........................proved - complete [SHOSTAK](0.00 s)
select_TCC1...........................proved - complete [SHOSTAK](0.00 s)
nice_ind?_TCC1........................proved - complete [SHOSTAK](0.00 s)
nice_ind?_TCC2........................proved - complete [SHOSTAK](0.00 s)
get_term_from_args_TCC1...............proved - complete [SHOSTAK](0.00 s)
all_var?_TCC1.........................proved - complete [SHOSTAK](0.00 s)
all_var?_TCC2.........................proved - complete [SHOSTAK](0.00 s)
first_order_term_opt..................proved - complete [SHOSTAK](0.00 s)
member_t_lst_args.....................proved - complete [SHOSTAK](0.00 s)
size_ge1..............................proved - complete [SHOSTAK](0.00 s)
size_args_ge1.........................proved - complete [SHOSTAK](0.00 s)
num_arg_ge1...........................proved - complete [SHOSTAK](0.00 s)
num_arg_ge1_type_t....................proved - complete [SHOSTAK](0.00 s)
num_arg_not_pair......................proved - complete [SHOSTAK](0.00 s)
select_num_arg........................proved - complete [SHOSTAK](0.00 s)
select_not_pair.......................proved - complete [SHOSTAK](0.00 s)
select_le1............................proved - complete [SHOSTAK](0.00 s)
select_ge_num_arg.....................proved - complete [SHOSTAK](0.00 s)
select_size...........................proved - complete [SHOSTAK](0.00 s)
remove_size_args......................proved - incomplete [SHOSTAK](0.00 s)
remove_size_lst_args..................proved - incomplete [SHOSTAK](0.00 s)
get_args_len..........................proved - incomplete [SHOSTAK](0.00 s)
get_args_null.........................proved - incomplete [SHOSTAK](0.00 s)
get_args_pair.........................proved - incomplete [SHOSTAK](0.00 s)
get_args_mem_not_pair.................proved - incomplete [SHOSTAK](0.00 s)
get_args_mem_select1..................proved - incomplete [SHOSTAK](0.00 s)
get_args_mem_selecti..................proved - incomplete [SHOSTAK](0.00 s)
get_args_not_pair.....................proved - incomplete [SHOSTAK](0.00 s)
get_args_nth_TCC1.....................proved - incomplete [SHOSTAK](0.00 s)
get_args_nth..........................proved - incomplete [SHOSTAK](0.00 s)
get_args_get_term_from_args...........proved - incomplete [SHOSTAK](0.00 s)
get_args_get_term_from_args_len.......proved - incomplete [SHOSTAK](0.00 s)
subterms_aux_TCC......................proved - complete [SHOSTAK](0.00 s)
vars_TCC1.............................proved - complete [SHOSTAK](0.00 s)
vars_TCC2.............................proved - complete [SHOSTAK](0.00 s)
vars_TCC3.............................proved - complete [SHOSTAK](0.00 s)
vars_TCC4.............................proved - complete [SHOSTAK](0.00 s)
vars_TCC5.............................proved - complete [SHOSTAK](0.00 s)
vars_TCC6.............................proved - complete [SHOSTAK](0.00 s)
vars_TCC7.............................proved - complete [SHOSTAK](0.00 s)
vars_TCC8.............................proved - incomplete [SHOSTAK](0.00 s)
vars_TCC9.............................proved - complete [SHOSTAK](0.00 s)
prop_subterms_TCC1....................proved - complete [SHOSTAK](0.00 s)
size2_TCC1............................proved - complete [SHOSTAK](0.00 s)
size2_TCC2............................proved - complete [SHOSTAK](0.00 s)
var_lst_TCC1..........................proved - complete [SHOSTAK](0.00 s)
vars_append...........................proved - complete [SHOSTAK](0.00 s)
vars_correct..........................proved - complete [SHOSTAK](0.00 s)
vars_singleton........................proved - complete [SHOSTAK](0.00 s)
vars_finset...........................proved - complete [SHOSTAK](0.00 s)
vars_args.............................proved - complete [SHOSTAK](0.00 s)
vars_lst_args.........................proved - complete [SHOSTAK](0.00 s)
vars_lst_lst_vars.....................proved - incomplete [SHOSTAK](0.00 s)
vars_map..............................proved - incomplete [SHOSTAK](0.00 s)
vars_get_args.........................proved - incomplete [SHOSTAK](0.00 s)
vars_select...........................proved - complete [SHOSTAK](0.00 s)
vars_lst_vars.........................proved - incomplete [SHOSTAK](0.00 s)
var_lst_len...........................proved - complete [SHOSTAK](0.00 s)
var_lst_nth_TCC1......................proved - complete [SHOSTAK](0.00 s)
var_lst_nth...........................proved - complete [SHOSTAK](0.00 s)
var_lst_mem...........................proved - complete [SHOSTAK](0.00 s)
all_var?_append.......................proved - complete [SHOSTAK](0.00 s)
all_var?_get_repeat_lst...............proved - incomplete [SHOSTAK](0.00 s)
all_var?_split........................proved - incomplete [SHOSTAK](0.00 s)
all_var?_split2.......................proved - incomplete [SHOSTAK](0.00 s)
all_var?_get_repeat_lst_null..........proved - incomplete [SHOSTAK](0.00 s)
all_var?_split_lst_args...............proved - incomplete [SHOSTAK](0.00 s)
all_var?_split_lst_args2..............proved - incomplete [SHOSTAK](0.00 s)
all_var?_args.........................proved - complete [SHOSTAK](0.00 s)
all_var?_lst_args.....................proved - complete [SHOSTAK](0.00 s)
not_var_args_append...................proved - complete [SHOSTAK](0.00 s)
not_var_args_nth......................proved - complete [SHOSTAK](0.00 s)
not_var_args_mem......................proved - complete [SHOSTAK](0.00 s)
not_var_args_mem2.....................proved - complete [SHOSTAK](0.00 s)
not_var_args_get_args.................proved - incomplete [SHOSTAK](0.00 s)
not_var_args_get_args2................proved - incomplete [SHOSTAK](0.00 s)
not_var_args_nth2.....................proved - incomplete [SHOSTAK](0.00 s)
subterm_fin_set.......................proved - complete [SHOSTAK](0.00 s)
subterm_args..........................proved - complete [SHOSTAK](0.00 s)
subterm_singleton.....................proved - complete [SHOSTAK](0.00 s)
subterm_reflexive.....................proved - complete [SHOSTAK](0.00 s)
subterm_not_pair......................proved - complete [SHOSTAK](0.00 s)
subterm_reflexive_finset..............proved - complete [SHOSTAK](0.00 s)
select_subterms.......................proved - complete [SHOSTAK](0.00 s)
subterm_fin_set_mem...................proved - complete [SHOSTAK](0.00 s)
vars_subterm..........................proved - complete [SHOSTAK](0.00 s)
vars_subterm2.........................proved - complete [SHOSTAK](0.00 s)
subterm_size..........................proved - complete [SHOSTAK](0.00 s)
subterm_transitive....................proved - complete [SHOSTAK](0.00 s)
get_args_subterms.....................proved - incomplete [SHOSTAK](0.00 s)
get_args_subterms2....................proved - incomplete [SHOSTAK](0.00 s)
prop_subterm_subterm_size.............proved - complete [SHOSTAK](0.00 s)
prop_subterm_subterm..................proved - complete [SHOSTAK](0.00 s)
vars_prop_subterm.....................proved - complete [SHOSTAK](0.00 s)
var_flatten_pair_implies_var..........proved - incomplete [SHOSTAK](0.00 s)
flatten_pair_not_pair.................proved - incomplete [SHOSTAK](0.00 s)
flatten_pair_subterms.................proved - incomplete [SHOSTAK](0.00 s)
flatten_pair_size.....................proved - incomplete [SHOSTAK](0.00 s)
same_func_sym.........................proved - complete [SHOSTAK](0.00 s)
same_func_trans.......................proved - complete [SHOSTAK](0.00 s)
same_func_dif_func....................proved - complete [SHOSTAK](0.00 s)
dif_func_sym..........................proved - complete [SHOSTAK](0.00 s)
cond_dif_func.........................proved - complete [SHOSTAK](0.00 s)
size2_ge0.............................proved - complete [SHOSTAK](0.00 s)
size2_get_args........................proved - incomplete [SHOSTAK](0.00 s)
Theory first_order_terms_properties totals: 119 formulas, 119 attempted, 119 succeeded (0.03 s)
Proof summary for theory first_order_term
Theory first_order_term totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)
Proof summary for theory first_order_term_adt_reduce
Theory first_order_term_adt_reduce totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)
Proof summary for theory first_order_term_adt_map
Theory first_order_term_adt_map totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)
Proof summary for theory first_order_term_adt
Theory first_order_term_adt totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)
Proof summary for theory antiunif
vars_TCC1.............................proved - complete [SHOSTAK](0.00 s)
AUEquation_classification.............proved - complete [SHOSTAK](0.00 s)
vars_TCC2.............................proved - complete [SHOSTAK](0.00 s)
vars_TCC3.............................proved - complete [SHOSTAK](0.00 s)
vars_TCC4.............................proved - complete [SHOSTAK](0.00 s)
vars_TCC5.............................proved - complete [SHOSTAK](0.00 s)
vars_in_append_List_eq................proved - complete [SHOSTAK](0.00 s)
subset_vars_eq_listEqs................proved - complete [SHOSTAK](0.00 s)
eq_member_eq_label_in_labels..........proved - complete [SHOSTAK](0.00 s)
eqs_label_eq_this_label...............proved - complete [SHOSTAK](0.00 s)
card_lbls_in_List_eq..................proved - complete [SHOSTAK](0.00 s)
append_labels_is_union_labels.........proved - complete [SHOSTAK](0.00 s)
disjoint_valid_append_validEqs........proved - complete [SHOSTAK](0.00 s)
non_member_label_validEqs.............proved - complete [SHOSTAK](0.00 s)
validity_cdr_ValidEqs.................proved - complete [SHOSTAK](0.00 s)
validity_Eq_in_ValidEqs...............proved - complete [SHOSTAK](0.00 s)
non_member_var_nth_label..............proved - complete [SHOSTAK](0.00 s)
validity_append_valid_Eqs.............proved - complete [SHOSTAK](0.00 s)
eq_repeated_in?_TCC1..................proved - complete [SHOSTAK](0.00 s)
cdr_first_eq_red......................proved - complete [SHOSTAK](0.00 s)
red_eq_in_TCC1........................proved - complete [SHOSTAK](0.00 s)
red_eq_in_TCC2........................proved - complete [SHOSTAK](0.00 s)
red_eq_in_TCC3........................proved - complete [SHOSTAK](0.00 s)
red_eq_in_lhs_rhs_equality............proved - complete [SHOSTAK](0.00 s)
red_eq_in_cdr.........................proved - complete [SHOSTAK](0.00 s)
nonrepeated?_TCC1.....................proved - complete [SHOSTAK](0.00 s)
nonrepeated?_TCC2.....................proved - complete [SHOSTAK](0.00 s)
disjoint_labels_unsolved_solved.......proved - complete [SHOSTAK](0.00 s)
validity_car_conf_unsolved_TCC1.......proved - complete [SHOSTAK](0.00 s)
validity_car_conf_unsolved............proved - complete [SHOSTAK](0.00 s)
validity_cdr_conf_unsolved............proved - incomplete [SHOSTAK](0.00 s)
invariance_labels_in_validConf........proved - complete [SHOSTAK](0.00 s)
cdr_is_validConf......................proved - complete [SHOSTAK](0.00 s)
labels_allEquations_as_union..........proved - complete [SHOSTAK](0.00 s)
freshness_membship....................proved - incomplete [SHOSTAK](0.00 s)
freshness_epsilon_ext.................proved - incomplete [SHOSTAK](0.00 s)
freshness_epsilon.....................proved - incomplete [SHOSTAK](0.00 s)
freshness_vars........................proved - incomplete [SHOSTAK](0.00 s)
freshness_labels......................proved - incomplete [SHOSTAK](0.00 s)
freshness_nth_label_TCC1..............proved - complete [SHOSTAK](0.00 s)
freshness_nth_label...................proved - incomplete [SHOSTAK](0.00 s)
freshness_car_label...................proved - incomplete [SHOSTAK](0.00 s)
freshness_labels_ext..................proved - incomplete [SHOSTAK](0.00 s)
freshness_subs........................proved - incomplete [SHOSTAK](0.00 s)
freshness_subs_ext....................proved - incomplete [SHOSTAK](0.00 s)
freshness_subs_dom_ext................proved - incomplete [SHOSTAK](0.00 s)
car_lbl_fresh_in_cdr..................proved - complete [SHOSTAK](0.00 s)
car_lbl_fresh_dom.....................proved - complete [SHOSTAK](0.00 s)
emptyness_conf_vars_with_lbls_and_fresh_variables...proved - complete [SHOSTAK](0.00 s)
emptyness_conf_supdom_with_lbls_and_fresh_variables...proved - complete [SHOSTAK](0.00 s)
emptyness_conf_supdom_with_car_lbls_and_fresh_variables...proved - complete [SHOSTAK](0.00 s)
emptyness_conf_var_with_lbls_decomposeFuns...proved - complete [SHOSTAK](0.00 s)
emptyness_conf_var_with_lbls_decomposePairs...proved - incomplete [SHOSTAK](0.00 s)
emptyness_conf_var....................proved - complete [SHOSTAK](0.00 s)
niceness_preserv_conditions...........proved - complete [SHOSTAK](0.00 s)
niceness_preserv_conditions_decomposeFuns_TCC1...proved - complete [SHOSTAK](0.00 s)
niceness_preserv_conditions_decomposeFuns...proved - incomplete [SHOSTAK](0.00 s)
nice_sub_decomposeFuns................proved - incomplete [SHOSTAK](0.00 s)
uns_solv_vars_matchingFuns_conf_TCC1...proved - complete [SHOSTAK](0.00 s)
uns_solv_vars_matchingFuns_conf_TCC2...proved - complete [SHOSTAK](0.00 s)
uns_solv_vars_matchingFuns_conf.......proved - complete [SHOSTAK](0.00 s)
decomposeFuns_TCC1....................proved - incomplete [SHOSTAK](0.00 s)
decomposeFuns_TCC2....................proved - incomplete [SHOSTAK](0.00 s)
niceness_preserv_conditions_decomposePairs_TCC1...proved - complete [SHOSTAK](0.00 s)
niceness_preserv_conditions_decomposePairs...proved - incomplete [SHOSTAK](0.00 s)
nice_sub_decomposePairs...............proved - incomplete [SHOSTAK](0.00 s)
uns_solv_vars_matchingPairs_conf_TCC1...proved - complete [SHOSTAK](0.00 s)
uns_solv_vars_matchingPairs_conf_TCC2...proved - complete [SHOSTAK](0.00 s)
uns_solv_vars_matchingPairs_conf......proved - complete [SHOSTAK](0.00 s)
decomposePairs_TCC1...................proved - incomplete [SHOSTAK](0.00 s)
decomposePairs_TCC2...................proved - incomplete [SHOSTAK](0.01 s)
nice_sub_trivialSyn_Eqs_TCC1..........proved - complete [SHOSTAK](0.00 s)
nice_sub_trivialSyn_Eqs...............proved - complete [SHOSTAK](0.00 s)
trivialSyn_Eqs_TCC1...................proved - complete [SHOSTAK](0.00 s)
trivialSyn_Eqs_TCC2...................proved - incomplete [SHOSTAK](0.00 s)
syntEq_inter_vars_unsolv_labels_solv...proved - incomplete [SHOSTAK](0.00 s)
labels_trivialSyn_Eqs.................proved - incomplete [SHOSTAK](0.00 s)
syntEq_car_lhs_member_img.............proved - incomplete [SHOSTAK](0.00 s)
domain_trivialSyn_Eqs.................proved - incomplete [SHOSTAK](0.00 s)
nice_sub_Solved_Eq_TCC1...............proved - complete [SHOSTAK](0.00 s)
nice_sub_Solved_Eq_TCC2...............proved - complete [SHOSTAK](0.00 s)
nice_sub_Solved_Eq....................proved - complete [SHOSTAK](0.00 s)
solve_TCC1............................proved - complete [SHOSTAK](0.00 s)
solve_TCC2............................proved - incomplete [SHOSTAK](0.00 s)
solve_TCC3............................proved - incomplete [SHOSTAK](0.00 s)
antiunify_TCC1........................proved - complete [SHOSTAK](0.00 s)
build_subs_left_TCC1..................proved - complete [SHOSTAK](0.00 s)
build_subs_left_TCC2..................proved - complete [SHOSTAK](0.00 s)
build_subs_left_TCC3..................proved - complete [SHOSTAK](0.00 s)
build_subs_left_TCC4..................proved - complete [SHOSTAK](0.00 s)
super_domain_subs_left................proved - complete [SHOSTAK](0.00 s)
domain_subs_left......................proved - complete [SHOSTAK](0.00 s)
nice_subs_left........................proved - complete [SHOSTAK](0.00 s)
super_domain_subs_right...............proved - complete [SHOSTAK](0.00 s)
domain_subs_right.....................proved - complete [SHOSTAK](0.00 s)
nice_subs_right.......................proved - complete [SHOSTAK](0.00 s)
images_of_build_subs_left_right.......proved - complete [SHOSTAK](0.00 s)
antiunify_normality...................proved - incomplete [SHOSTAK](0.00 s)
antiunify_derivability................proved - complete [SHOSTAK](0.00 s)
matchingPairs_classification..........proved - complete [SHOSTAK](0.00 s)
syntacticallyEq_classification........proved - complete [SHOSTAK](0.00 s)
SolvedEq_classification...............proved - complete [SHOSTAK](0.00 s)
antiunify_monotony_solved_equations...proved - incomplete [SHOSTAK](0.00 s)
antiunify_domain_disjoint_sol_labels...proved - incomplete [SHOSTAK](0.00 s)
antiunify_sub_decomposition...........proved - incomplete [SHOSTAK](0.00 s)
antiunify_sub_preserves_terms.........proved - incomplete [SHOSTAK](0.00 s)
antiunify_dom_sub_preserves_vars_unsolved...proved - incomplete [SHOSTAK](0.01 s)
antiunify_lbls_preserves_vars_unsolved...proved - incomplete [SHOSTAK](0.00 s)
antiunify_solved_labels_preserve_vars_unsolved...proved - incomplete [SHOSTAK](0.00 s)
antiunify_solved_substitution_TCC1....proved - incomplete [SHOSTAK](0.00 s)
antiunify_solved_substitution.........proved - incomplete [SHOSTAK](0.00 s)
antiunif_is_sound_TCC1................proved - incomplete [SHOSTAK](0.00 s)
antiunif_is_sound_TCC2................proved - incomplete [SHOSTAK](0.00 s)
antiunif_is_sound_TCC3................proved - incomplete [SHOSTAK](0.00 s)
antiunif_is_sound_TCC4................proved - incomplete [SHOSTAK](0.00 s)
antiunif_is_sound.....................proved - incomplete [SHOSTAK](0.01 s)
Theory antiunif totals: 116 formulas, 116 attempted, 116 succeeded (0.07 s)
Grand Totals: 350 proofs, 350 attempted, 350 succeeded (0.13 s)