-
Notifications
You must be signed in to change notification settings - Fork 5
/
Copy pathcclusters1132.pl
2406 lines (2406 loc) · 273 KB
/
cclusters1132.pl
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
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
v3_lattice3(A) :- l1_orders_2(A),v13_struct_0(A, 1),v3_orders_2(A).
v1_abcmiz_0(A) :- l1_orders_2(A),v13_struct_0(A, 1).
v1_lattice3(A) :- l1_orders_2(A),v3_orders_2(A),v4_orders_2(A),v5_orders_2(A),v2_abcmiz_0(A).
v2_yellow_0(A) :- l1_orders_2(A),v3_orders_2(A),v4_orders_2(A),v5_orders_2(A),v2_abcmiz_0(A).
v1_abcmiz_0(A) :- l1_orders_2(A),v3_orders_2(A),v4_orders_2(A),v5_orders_2(A),v2_abcmiz_0(A).
v2_abcmiz_0(A) :- l1_orders_2(A),v3_orders_2(A),v4_orders_2(A),v5_orders_2(A),v1_lattice3(A),v1_abcmiz_0(A).
~ (v1_facirc_1(A)) :- ~ (v11_struct_0(B)) ,v1_instalg1(B),l1_msualg_1(B),v1_relat_1(C), ~ (v3_relat_1(C)) ,v4_relat_1(C, u1_struct_0(B)),v1_funct_1(C),v1_partfun1(C, u1_struct_0(B)),m1_subset_1(A, k3_card_3(u3_msualg_1(B, k1_msafree3(B, C)))),true.
v6_trees_3(A) :- ~ (v11_struct_0(B)) ,v1_instalg1(B),l1_msualg_1(B),v1_relat_1(C), ~ (v3_relat_1(C)) ,v4_relat_1(C, u1_struct_0(B)),v1_funct_1(C),v1_partfun1(C, u1_struct_0(B)),m1_finseq_1(A, k3_card_3(u3_msualg_1(B, k1_msafree3(B, C)))),true.
v2_funct_1(A) :- m1_subset_1(A, k4_abcmiz_1),true.
~ (v2_struct_0(A)) :- l1_msualg_1(A),v1_instalg1(A),v1_abcmiz_1(A).
~ (v11_struct_0(A)) :- l1_msualg_1(A),v1_instalg1(A),v1_abcmiz_1(A).
~ (v7_abcmiz_1(A, B)) :- v1_instalg1(B),v1_abcmiz_1(B),v3_abcmiz_1(B),l1_msualg_1(B),m1_abcmiz_1(A, B, k13_abcmiz_1(B)),v6_abcmiz_1(A, B).
v8_abcmiz_1(A, B) :- v1_instalg1(B),v1_abcmiz_1(B),v3_abcmiz_1(B),l1_msualg_1(B),m1_abcmiz_1(A, B, k13_abcmiz_1(B)),v6_abcmiz_1(A, B).
~ (v6_abcmiz_1(A, B)) :- v1_instalg1(B),v1_abcmiz_1(B),v3_abcmiz_1(B),l1_msualg_1(B),m1_abcmiz_1(A, B, k13_abcmiz_1(B)),v7_abcmiz_1(A, B).
v8_abcmiz_1(A, B) :- v1_instalg1(B),v1_abcmiz_1(B),v3_abcmiz_1(B),l1_msualg_1(B),m1_abcmiz_1(A, B, k13_abcmiz_1(B)),v7_abcmiz_1(A, B).
v7_abcmiz_1(A, B) :- v1_instalg1(B),v1_abcmiz_1(B),v3_abcmiz_1(B),l1_msualg_1(B),m1_abcmiz_1(A, B, k13_abcmiz_1(B)), ~ (v6_abcmiz_1(A, B)) ,v8_abcmiz_1(A, B).
v6_abcmiz_1(A, B) :- v1_instalg1(B),v1_abcmiz_1(B),v3_abcmiz_1(B),l1_msualg_1(B),m1_abcmiz_1(A, B, k13_abcmiz_1(B)), ~ (v7_abcmiz_1(A, B)) ,v8_abcmiz_1(A, B).
v1_facirc_1(A) :- v1_instalg1(B),v1_abcmiz_1(B),v3_abcmiz_1(B),l1_msualg_1(B),m3_abcmiz_1(A, B),true.
v13_abcmiz_1(A, B) :- l1_msualg_1(B),v1_relat_1(A),v2_relat_1(A),v4_relat_1(A, u1_struct_0(B)),v1_funct_1(A),v1_partfun1(A, u1_struct_0(B)).
v13_abcmiz_1(A, B) :- v12_abcmiz_1(B),l1_msualg_1(B),v1_relat_1(A),v4_relat_1(A, u1_struct_0(B)),v1_funct_1(A),v1_partfun1(A, u1_struct_0(B)).
v15_abcmiz_1(A, B) :- v1_instalg1(B),v1_abcmiz_1(B),v3_abcmiz_1(B),l1_msualg_1(B),m1_subset_1(A, k1_zfmisc_1(k2_zfmisc_1(k2_abcmiz_1, k34_abcmiz_1(B)))),v1_xboole_0(A),v1_funct_1(A).
v1_abcmiz_a(A) :- v1_instalg1(B),v1_abcmiz_1(B),v1_abcmiz_a(B),l1_msualg_1(B),m1_instalg1(A, B),v1_abcmiz_1(A).
v1_facirc_1(A) :- m1_subset_1(A, k2_abcmiz_1),true.
v5_abcmiz_1(A, B, k28_abcmiz_1(B)) :- v1_instalg1(B),v1_abcmiz_1(B),v3_abcmiz_1(B),l1_msualg_1(B),m1_subset_1(A, k3_card_3(u3_msualg_1(B, k1_msafree3(B, k28_abcmiz_1(B))))),v2_abcmiz_a(A, B).
v2_abcmiz_1(A, B) :- v1_instalg1(B),v1_abcmiz_1(B),l1_msualg_1(B),m1_subset_1(A, u4_struct_0(B)),v4_abcmiz_a(A, B).
v12_abcmiz_1(A) :- l1_msualg_1(A), ~ (v11_struct_0(A)) ,v1_instalg1(A),v3_abcmiz_a(A).
v3_abcmiz_1(A) :- l1_msualg_1(A),v1_instalg1(A),v1_abcmiz_1(A),v3_abcmiz_a(A).
v1_zfmisc_1(A) :- true,v2_setfam_1(A).
~ (v1_xboole_0(A)) :- true,v1_int_1(A), ~ (v1_abian(A)) .
v5_ordinal1(A) :- true,v1_relat_1(A),v1_funct_1(A),v1_xboole_0(A).
v3_valued_0(A) :- true,v1_relat_1(A),v5_relat_1(A, k1_numbers),v5_ordinal1(A),v1_funct_1(A),v1_finset_1(A).
v6_valued_0(A) :- true,v1_relat_1(A),v5_relat_1(A, k5_numbers),v5_ordinal1(A),v1_funct_1(A),v1_finset_1(A).
v1_afinsq_1(A) :- true,v1_relat_1(A),v1_funct_1(A),v1_xboole_0(A).
v1_afinsq_1(A) :- true,v1_relat_1(A),v5_ordinal1(A),v1_funct_1(A),v1_finset_1(A).
v4_relat_1(A, k5_numbers) :- true,v1_relat_1(A),v5_ordinal1(A),v1_funct_1(A),v1_finset_1(A).
v5_ordinal1(A) :- true,v1_relat_1(A),v4_relat_1(A, k5_numbers),v1_funct_1(A),v1_finset_1(A),v1_afinsq_1(A).
v5_ordinal1(A) :- m1_subset_1(A, k8_afinsq_1(B)),true.
v1_finset_1(A) :- m1_subset_1(A, k8_afinsq_1(B)),true.
v6_membered(A) :- true,v7_ordinal1(A).
v4_partfun3(A) :- true,v1_relat_1(A),v6_valued_0(A).
v1_afvect0(A) :- l1_analoaf(A), ~ (v2_struct_0(A)) ,v2_tdgroup(A).
~ (v2_struct_0(A)) :- ~ (v2_struct_0(B)) ,v1_instalg1(B),l1_msualg_1(B),m2_algspec1(A, B),true.
~ (v11_struct_0(A)) :- ~ (v11_struct_0(B)) ,v1_instalg1(B),l1_msualg_1(B),m2_algspec1(A, B),true.
v4_algstr_0(A, B) :- l1_algstr_0(B),m1_subset_1(A, u1_struct_0(B)),v2_algstr_0(A, B),v3_algstr_0(A, B).
v2_algstr_0(A, B) :- l1_algstr_0(B),m1_subset_1(A, u1_struct_0(B)),v4_algstr_0(A, B).
v3_algstr_0(A, B) :- l1_algstr_0(B),m1_subset_1(A, u1_struct_0(B)),v4_algstr_0(A, B).
v7_algstr_0(A) :- l1_algstr_0(A),v5_algstr_0(A),v6_algstr_0(A).
v5_algstr_0(A) :- l1_algstr_0(A),v7_algstr_0(A).
v6_algstr_0(A) :- l1_algstr_0(A),v7_algstr_0(A).
v2_algstr_0(A, B) :- v5_algstr_0(B),l1_algstr_0(B),m1_subset_1(A, u1_struct_0(B)),true.
v3_algstr_0(A, B) :- v6_algstr_0(B),l1_algstr_0(B),m1_subset_1(A, u1_struct_0(B)),true.
v11_algstr_0(A, B) :- l2_algstr_0(B),m1_subset_1(A, u1_struct_0(B)),v9_algstr_0(A, B),v10_algstr_0(A, B).
v9_algstr_0(A, B) :- l2_algstr_0(B),m1_subset_1(A, u1_struct_0(B)),v11_algstr_0(A, B).
v10_algstr_0(A, B) :- l2_algstr_0(B),m1_subset_1(A, u1_struct_0(B)),v11_algstr_0(A, B).
v14_algstr_0(A) :- l2_algstr_0(A),v12_algstr_0(A),v13_algstr_0(A).
v12_algstr_0(A) :- l2_algstr_0(A),v14_algstr_0(A).
v13_algstr_0(A) :- l2_algstr_0(A),v14_algstr_0(A).
v9_algstr_0(A, B) :- v12_algstr_0(B),l2_algstr_0(B),m1_subset_1(A, u1_struct_0(B)),true.
v10_algstr_0(A, B) :- v13_algstr_0(B),l2_algstr_0(B),m1_subset_1(A, u1_struct_0(B)),true.
v18_algstr_0(A, B) :- l3_algstr_0(B),m1_subset_1(A, u1_struct_0(B)),v16_algstr_0(A, B),v17_algstr_0(A, B).
v16_algstr_0(A, B) :- l3_algstr_0(B),m1_subset_1(A, u1_struct_0(B)),v18_algstr_0(A, B).
v17_algstr_0(A, B) :- l3_algstr_0(B),m1_subset_1(A, u1_struct_0(B)),v18_algstr_0(A, B).
v21_algstr_0(A) :- l3_algstr_0(A),v19_algstr_0(A),v20_algstr_0(A).
v19_algstr_0(A) :- l3_algstr_0(A),v21_algstr_0(A).
v20_algstr_0(A) :- l3_algstr_0(A),v21_algstr_0(A).
v16_algstr_0(A, B) :- v19_algstr_0(B),l3_algstr_0(B),m1_subset_1(A, u1_struct_0(B)),true.
v17_algstr_0(A, B) :- v20_algstr_0(B),l3_algstr_0(B),m1_subset_1(A, u1_struct_0(B)),true.
v25_algstr_0(A, B) :- l4_algstr_0(B),m1_subset_1(A, u1_struct_0(B)),v23_algstr_0(A, B),v24_algstr_0(A, B).
v23_algstr_0(A, B) :- l4_algstr_0(B),m1_subset_1(A, u1_struct_0(B)),v25_algstr_0(A, B).
v24_algstr_0(A, B) :- l4_algstr_0(B),m1_subset_1(A, u1_struct_0(B)),v25_algstr_0(A, B).
v28_algstr_0(A) :- l4_algstr_0(A),v26_algstr_0(A),v27_algstr_0(A).
v26_algstr_0(A) :- l4_algstr_0(A),v28_algstr_0(A).
v27_algstr_0(A) :- l4_algstr_0(A),v28_algstr_0(A).
v23_algstr_0(A, B) :- v26_algstr_0(B),l4_algstr_0(B),m1_subset_1(A, u1_struct_0(B)),true.
v24_algstr_0(A, B) :- v27_algstr_0(B),l4_algstr_0(B),m1_subset_1(A, u1_struct_0(B)),true.
v32_algstr_0(A) :- l5_algstr_0(A),v30_algstr_0(A),v31_algstr_0(A).
v30_algstr_0(A) :- l5_algstr_0(A),v32_algstr_0(A).
v31_algstr_0(A) :- l5_algstr_0(A),v32_algstr_0(A).
v35_algstr_0(A) :- l5_algstr_0(A),v33_algstr_0(A),v34_algstr_0(A).
v33_algstr_0(A) :- l5_algstr_0(A),v35_algstr_0(A).
v34_algstr_0(A) :- l5_algstr_0(A),v35_algstr_0(A).
v5_algstr_0(A) :- l2_algstr_0(A), ~ (v2_struct_0(A)) ,v4_algstr_1(A).
v6_algstr_0(A) :- l2_algstr_0(A), ~ (v2_struct_0(A)) ,v4_algstr_1(A).
v2_algstr_1(A) :- l2_algstr_0(A), ~ (v2_struct_0(A)) ,v4_algstr_1(A).
v3_algstr_1(A) :- l2_algstr_0(A), ~ (v2_struct_0(A)) ,v4_algstr_1(A).
v4_algstr_1(A) :- l2_algstr_0(A), ~ (v2_struct_0(A)) ,v5_algstr_0(A),v6_algstr_0(A),v2_algstr_1(A),v3_algstr_1(A).
v2_algstr_1(A) :- l2_algstr_0(A), ~ (v2_struct_0(A)) ,v4_algstr_1(A).
v1_algstr_1(A) :- l2_algstr_0(A), ~ (v2_struct_0(A)) ,v13_algstr_0(A),v3_rlvect_1(A),v4_rlvect_1(A).
v4_algstr_1(A) :- l2_algstr_0(A), ~ (v2_struct_0(A)) ,v13_algstr_0(A),v3_rlvect_1(A),v4_rlvect_1(A).
v23_algstr_0(A, B) :- ~ (v2_struct_0(B)) ,v21_algstr_0(B),v5_algstr_1(B),l4_algstr_0(B),m1_subset_1(A, u1_struct_0(B)),true.
v32_algstr_0(A) :- l5_algstr_0(A), ~ (v2_struct_0(A)) ,v7_algstr_1(A).
v6_algstr_1(A) :- l5_algstr_0(A), ~ (v2_struct_0(A)) ,v7_algstr_1(A).
v13_algstr_0(A) :- l2_algstr_0(A),v13_struct_0(A, 1).
v2_rlvect_1(A) :- l2_algstr_0(A),v13_struct_0(A, 1).
v3_rlvect_1(A) :- l2_algstr_0(A),v13_struct_0(A, 1).
v4_rlvect_1(A) :- l2_algstr_0(A),v13_struct_0(A, 1).
v1_vectsp_1(A) :- l6_algstr_0(A), ~ (v2_struct_0(A)) ,v7_struct_0(A).
v4_vectsp_1(A) :- l6_algstr_0(A), ~ (v2_struct_0(A)) ,v7_struct_0(A).
v2_group_1(A) :- l3_algstr_0(A),v13_struct_0(A, 1).
v3_group_1(A) :- l3_algstr_0(A),v13_struct_0(A, 1).
v5_group_1(A) :- l3_algstr_0(A),v13_struct_0(A, 1).
v10_altcat_1(A) :- l2_altcat_1(A), ~ (v2_struct_0(A)) ,v2_altcat_1(A),v8_altcat_1(A),v9_altcat_1(A).
v8_altcat_1(A) :- l2_altcat_1(A), ~ (v2_struct_0(A)) ,v2_altcat_1(A),v10_altcat_1(A),v12_altcat_1(A).
v9_altcat_1(A) :- l2_altcat_1(A), ~ (v2_struct_0(A)) ,v2_altcat_1(A),v10_altcat_1(A),v12_altcat_1(A).
v13_altcat_1(A) :- l2_altcat_1(A),v13_struct_0(A, 1).
v2_altcat_1(A) :- l2_altcat_1(A),v13_altcat_1(A).
v1_altcat_2(A) :- l2_altcat_1(A), ~ (v2_struct_0(A)) ,v12_altcat_1(A).
v2_altcat_1(A) :- ~ (v2_struct_0(B)) ,v2_altcat_1(B),l2_altcat_1(B),m1_altcat_2(A, B), ~ (v2_struct_0(A)) ,v2_altcat_2(A, B).
v11_altcat_1(A) :- ~ (v2_struct_0(B)) ,v2_altcat_1(B),v11_altcat_1(B),l2_altcat_1(B),m1_altcat_2(A, B), ~ (v2_struct_0(A)) ,v2_altcat_1(A).
v12_altcat_1(A) :- ~ (v2_struct_0(B)) ,v2_altcat_1(B),v12_altcat_1(B),l2_altcat_1(B),m1_altcat_2(A, B), ~ (v2_struct_0(A)) ,v2_altcat_1(A),v3_altcat_2(A, B).
v1_ami_wstd(A, B) :- ~ (v1_xboole_0(B)) ,v1_setfam_1(B),l1_extpro_1(A, B), ~ (v2_struct_0(A)) ,v2_memstr_0(A, B),v2_ami_wstd(A, B).
~ (v2_extpro_1(A, B, C)) :- ~ (v1_xboole_0(B)) ,v1_setfam_1(B), ~ (v2_struct_0(C)) ,v2_memstr_0(C, B),v2_ami_wstd(C, B),l1_extpro_1(C, B),m1_subset_1(A, u1_compos_1(C)),v3_ami_wstd(A, B, C).
~ (v3_ami_wstd(A, B, C)) :- ~ (v1_xboole_0(B)) ,v1_setfam_1(B), ~ (v2_struct_0(C)) ,v2_memstr_0(C, B),v2_ami_wstd(C, B),l1_extpro_1(C, B),m1_subset_1(A, u1_compos_1(C)),v2_extpro_1(A, B, C).
v5_ami_wstd(A, C, B) :- ~ (v1_xboole_0(C)) ,v1_setfam_1(C), ~ (v2_struct_0(B)) ,v2_memstr_0(B, C),l1_extpro_1(B, C),v1_relat_1(A),v4_relat_1(A, k5_numbers),v5_relat_1(A, u1_compos_1(B)),v1_xboole_0(A),v1_funct_1(A),v1_finset_1(A).
v4_ami_wstd(A, C, B) :- ~ (v1_xboole_0(C)) ,v1_setfam_1(C), ~ (v2_struct_0(B)) ,v2_memstr_0(B, C),v2_ami_wstd(B, C),l1_extpro_1(B, C),v1_relat_1(A),v4_relat_1(A, k5_numbers),v5_relat_1(A, u1_compos_1(B)), ~ (v1_xboole_0(A)) ,v1_funct_1(A),v1_finset_1(A),v5_amistd_1(A, C, B),v5_ami_wstd(A, C, B).
v9_compos_1(A, k4_amistd_1(B)) :- ~ (v1_xboole_0(B)) ,v1_setfam_1(B),m1_subset_1(A, u1_compos_1(k4_amistd_1(B))),true.
~ (v2_extpro_1(A, B, C)) :- ~ (v1_xboole_0(B)) ,v1_setfam_1(B), ~ (v2_struct_0(C)) ,v2_memstr_0(C, B),l1_extpro_1(C, B),m1_subset_1(A, u1_compos_1(C)),v4_amistd_1(A, B, C).
~ (v4_amistd_1(A, B, C)) :- ~ (v1_xboole_0(B)) ,v1_setfam_1(B), ~ (v2_struct_0(C)) ,v2_memstr_0(C, B),l1_extpro_1(C, B),m1_subset_1(A, u1_compos_1(C)),v2_extpro_1(A, B, C).
v6_amistd_1(A, C, B) :- ~ (v1_xboole_0(C)) ,v1_setfam_1(C), ~ (v2_struct_0(B)) ,v2_memstr_0(B, C),v3_amistd_1(B, C),l1_extpro_1(B, C),v1_relat_1(A),v4_relat_1(A, k5_numbers),v5_relat_1(A, u1_compos_1(B)), ~ (v1_xboole_0(A)) ,v1_funct_1(A),v1_finset_1(A),v1_afinsq_1(A),v5_amistd_1(A, C, B).
v1_amistd_2(A, B, C) :- ~ (v1_xboole_0(B)) ,v1_setfam_1(B),v3_compos_1(C), ~ (v2_struct_0(C)) ,v2_memstr_0(C, B),v2_amistd_2(C, B),l1_extpro_1(C, B),m1_subset_1(A, u1_compos_1(C)),true.
v9_compos_1(A, B) :- ~ (v1_xboole_0(C)) ,v1_setfam_1(C),v3_compos_1(B), ~ (v2_struct_0(B)) ,v2_memstr_0(B, C),v2_amistd_2(B, C),l1_extpro_1(B, C),m1_subset_1(A, u1_compos_1(B)),v2_extpro_1(A, C, B).
v9_compos_1(A, B) :- ~ (v1_xboole_0(C)) ,v1_setfam_1(C),v3_compos_1(B), ~ (v2_struct_0(B)) ,v2_memstr_0(B, C),v2_amistd_2(B, C),l1_extpro_1(B, C),m1_subset_1(A, u1_compos_1(B)),v4_amistd_1(A, C, B).
v3_amistd_2(A, B, C) :- ~ (v1_xboole_0(B)) ,v1_setfam_1(B),v3_compos_1(C),v6_compos_1(C),v7_compos_1(C),v8_compos_1(C), ~ (v2_struct_0(C)) ,v2_memstr_0(C, B),v3_extpro_1(C, B),v2_amistd_2(C, B),l1_extpro_1(C, B),m1_subset_1(A, u1_compos_1(C)),v4_amistd_1(A, B, C).
v3_amistd_2(A, B, C) :- ~ (v1_xboole_0(B)) ,v1_setfam_1(B),v3_compos_1(C),v6_compos_1(C),v7_compos_1(C),v8_compos_1(C), ~ (v2_struct_0(C)) ,v2_memstr_0(C, B),v3_extpro_1(C, B),v2_amistd_2(C, B),l1_extpro_1(C, B),m1_subset_1(A, u1_compos_1(C)),v2_extpro_1(A, B, C).
v3_amistd_2(A, B, C) :- ~ (v1_xboole_0(B)) ,v1_setfam_1(B),v3_compos_1(C),v6_compos_1(C),v7_compos_1(C),v8_compos_1(C), ~ (v2_struct_0(C)) ,v2_memstr_0(C, B),v3_extpro_1(C, B),v4_amistd_2(C, B),l1_extpro_1(C, B),m1_subset_1(A, u1_compos_1(C)),true.
v3_amistd_2(A, B, C) :- ~ (v1_xboole_0(B)) ,v1_setfam_1(B),v3_compos_1(C),v6_compos_1(C),v7_compos_1(C),v8_compos_1(C), ~ (v2_struct_0(C)) ,v2_memstr_0(C, B),v3_extpro_1(C, B),l1_extpro_1(C, B),m1_subset_1(A, u1_compos_1(C)),v1_amistd_5(A, B, C).
v1_amistd_5(A, B, C) :- ~ (v1_xboole_0(B)) ,v1_setfam_1(B),v3_compos_1(C),v6_compos_1(C),v7_compos_1(C),v8_compos_1(C), ~ (v2_struct_0(C)) ,v2_memstr_0(C, B),v3_extpro_1(C, B),v2_amistd_5(C, B),l1_extpro_1(C, B),m1_subset_1(A, u1_compos_1(C)),true.
v2_analmetr(A) :- l1_analmetr(A), ~ (v2_struct_0(A)) ,v3_analmetr(A).
~ (v7_struct_0(A)) :- l1_rlvect_1(A), ~ (v2_struct_0(A)) ,v13_algstr_0(A),v2_rlvect_1(A),v3_rlvect_1(A),v4_rlvect_1(A),v5_rlvect_1(A),v6_rlvect_1(A),v7_rlvect_1(A),v8_rlvect_1(A),v1_anproj_2(A).
v1_relat_1(A) :- ~ (v1_xboole_0(B)) ,m1_finseq_1(B, k5_numbers), ~ (v1_xboole_0(C)) ,v1_freealg(C),m1_subset_1(A, u1_struct_0(k7_freealg(B, C))),true.
v1_funct_1(A) :- ~ (v1_xboole_0(B)) ,m1_finseq_1(B, k5_numbers), ~ (v1_xboole_0(C)) ,v1_freealg(C),m1_subset_1(A, u1_struct_0(k7_freealg(B, C))),true.
v3_trees_2(A) :- ~ (v1_xboole_0(B)) ,m1_finseq_1(B, k5_numbers), ~ (v1_xboole_0(C)) ,v1_freealg(C),m1_subset_1(A, u1_struct_0(k7_freealg(B, C))),true.
v6_trees_3(A) :- ~ (v1_xboole_0(B)) ,m1_finseq_1(B, k5_numbers), ~ (v1_xboole_0(C)) ,v1_freealg(C),m1_finseq_1(A, u1_struct_0(k7_freealg(B, C))),true.
~ (v10_aofa_000(A)) :- l1_unialg_1(A), ~ (v2_struct_0(A)) ,v2_unialg_1(A),v3_unialg_1(A),v4_unialg_1(A),v3_freealg(A),v3_aofa_000(A),v4_aofa_000(A),v5_aofa_000(A),v6_aofa_000(A).
v11_aofa_000(A) :- l1_unialg_1(A), ~ (v2_struct_0(A)) ,v2_unialg_1(A),v3_unialg_1(A),v4_unialg_1(A),v3_freealg(A),v3_aofa_000(A),v4_aofa_000(A),v5_aofa_000(A),v6_aofa_000(A).
v13_aofa_000(A, B, C) :- ~ (v2_struct_0(B)) ,v2_unialg_1(B),v3_unialg_1(B),v4_unialg_1(B),v3_aofa_000(B),v4_aofa_000(B),v5_aofa_000(B),v6_aofa_000(B),l1_unialg_1(B), ~ (v1_xboole_0(C)) ,m1_subset_1(D, k1_zfmisc_1(C)),m1_aofa_000(A, B, C, D),true.
v14_aofa_000(A, B, C) :- ~ (v2_struct_0(B)) ,v2_unialg_1(B),v3_unialg_1(B),v4_unialg_1(B),v3_aofa_000(B),v4_aofa_000(B),v5_aofa_000(B),v6_aofa_000(B),l1_unialg_1(B), ~ (v1_xboole_0(C)) ,m1_subset_1(D, k1_zfmisc_1(C)),m1_aofa_000(A, B, C, D),true.
v1_aofa_i00(A, k7_freealg(k19_aofa_000, k26_aofa_i00), k5_numbers, k1_aofa_i00(k9_funct_2(k5_numbers, k4_numbers), k6_numbers, k6_numbers)) :- m4_aofa_i00(A),true.
v1_aofa_i00(A, k7_freealg(k19_aofa_000, k26_aofa_i00), B, C) :- ~ (v1_xboole_0(B)) ,v4_card_3(B),m1_subset_1(C, k1_zfmisc_1(k9_funct_2(B, k4_numbers))),v1_funct_1(D),v2_funct_1(D),v1_funct_2(D, B, k1_card_1(B)),v2_funct_2(D, k1_card_1(B)),m1_subset_1(D, k1_zfmisc_1(k2_zfmisc_1(B, k1_card_1(B)))),m6_aofa_i00(A, B, C, D),true.
v1_pre_poly(A) :- ~ (v1_xboole_0(B)) , ~ (v1_xboole_0(D)) ,m1_subset_1(C, k5_numbers),m1_subset_1(A, k1_zfmisc_1(k2_zfmisc_1(B, k4_finseq_2(C, D)))),v1_funct_1(A),v1_funct_2(A, B, k4_finseq_2(C, D)).
v1_finset_1(A) :- v1_finset_1(B),m1_subset_1(A, k1_zfmisc_1(k2_zfmisc_1(k9_setfam_1(B), k9_setfam_1(B)))),true.
v8_relat_2(A) :- m1_subset_1(A, k1_zfmisc_1(k2_zfmisc_1(k9_setfam_1(B), k9_setfam_1(B)))),v6_armstrng(A, B).
v3_armstrng(A, B) :- m1_subset_1(A, k1_zfmisc_1(k2_zfmisc_1(k9_setfam_1(B), k9_setfam_1(B)))),v6_armstrng(A, B).
v4_armstrng(A, B) :- m1_subset_1(A, k1_zfmisc_1(k2_zfmisc_1(k9_setfam_1(B), k9_setfam_1(B)))),v6_armstrng(A, B).
v5_armstrng(A, B) :- m1_subset_1(A, k1_zfmisc_1(k2_zfmisc_1(k9_setfam_1(B), k9_setfam_1(B)))),v6_armstrng(A, B).
v6_armstrng(A, B) :- m1_subset_1(A, k1_zfmisc_1(k2_zfmisc_1(k9_setfam_1(B), k9_setfam_1(B)))),v8_relat_2(A),v3_armstrng(A, B),v4_armstrng(A, B),v5_armstrng(A, B).
v7_armstrng(A, B) :- m1_subset_1(A, k1_zfmisc_1(k2_zfmisc_1(k9_setfam_1(B), k9_setfam_1(B)))),v3_armstrng(A, B),v4_armstrng(A, B).
v3_armstrng(A, B) :- m1_subset_1(A, k1_zfmisc_1(k2_zfmisc_1(k9_setfam_1(B), k9_setfam_1(B)))),v8_relat_2(A),v7_armstrng(A, B).
v4_armstrng(A, B) :- m1_subset_1(A, k1_zfmisc_1(k2_zfmisc_1(k9_setfam_1(B), k9_setfam_1(B)))),v8_relat_2(A),v7_armstrng(A, B).
~ (v1_xboole_0(A)) :- m1_subset_1(A, k1_zfmisc_1(k2_zfmisc_1(k9_setfam_1(B), k9_setfam_1(B)))),v3_armstrng(A, B).
v1_relat_1(A) :- ~ (v1_xboole_0(B)) ,m1_subset_1(A, k2_arrow(B)),true.
v1_relat_1(A) :- ~ (v1_xboole_0(B)) ,m1_subset_1(A, k3_arrow(B)),true.
v7_ordinal1(A) :- m1_subset_1(A, k5_arytm_3),v3_ordinal1(A).
v4_asympt_0(A) :- m1_subset_1(A, k1_zfmisc_1(k2_zfmisc_1(k5_numbers, k1_numbers))),v1_funct_1(A),v1_funct_2(A, k5_numbers, k1_numbers),v3_asympt_0(A).
v2_asympt_0(A) :- m1_subset_1(A, k1_zfmisc_1(k2_zfmisc_1(k5_numbers, k1_numbers))),v1_funct_1(A),v1_funct_2(A, k5_numbers, k1_numbers),v4_asympt_0(A).
v5_asympt_0(A) :- m1_subset_1(A, k1_zfmisc_1(k2_zfmisc_1(k5_numbers, k1_numbers))),v1_funct_1(A),v1_funct_2(A, k5_numbers, k1_numbers),v4_asympt_0(A).
v4_asympt_0(A) :- m1_subset_1(A, k1_zfmisc_1(k2_zfmisc_1(k5_numbers, k1_numbers))),v1_funct_1(A),v1_funct_2(A, k5_numbers, k1_numbers),v2_asympt_0(A),v5_asympt_0(A).
v13_bcialg_1(A) :- l2_bcialg_1(A), ~ (v2_struct_0(A)) ,v3_bcialg_1(A),v4_bcialg_1(A),v5_bcialg_1(A),v7_bcialg_1(A),v20_bcialg_1(A).
v20_bcialg_1(A) :- l2_bcialg_1(A), ~ (v2_struct_0(A)) ,v3_bcialg_1(A),v4_bcialg_1(A),v5_bcialg_1(A),v7_bcialg_1(A),v13_bcialg_1(A).
v17_bcialg_1(A) :- l2_bcialg_1(A), ~ (v2_struct_0(A)) ,v3_bcialg_1(A),v4_bcialg_1(A),v5_bcialg_1(A),v7_bcialg_1(A),v20_bcialg_1(A).
v16_bcialg_1(A) :- l2_bcialg_1(A), ~ (v2_struct_0(A)) ,v3_bcialg_1(A),v4_bcialg_1(A),v5_bcialg_1(A),v7_bcialg_1(A),v13_bcialg_1(A).
v16_bcialg_1(A) :- l2_bcialg_1(A), ~ (v2_struct_0(A)) ,v3_bcialg_1(A),v4_bcialg_1(A),v5_bcialg_1(A),v7_bcialg_1(A),v19_bcialg_1(A).
v16_bcialg_1(A) :- l2_bcialg_1(A), ~ (v2_struct_0(A)) ,v3_bcialg_1(A),v4_bcialg_1(A),v5_bcialg_1(A),v7_bcialg_1(A),v15_bcialg_1(A).
v16_bcialg_1(A) :- l2_bcialg_1(A), ~ (v2_struct_0(A)) ,v3_bcialg_1(A),v4_bcialg_1(A),v5_bcialg_1(A),v7_bcialg_1(A),v20_bcialg_1(A).
v1_partfun1(A, u1_struct_0(B)) :- ~ (v2_struct_0(B)) ,v3_bcialg_1(B),v4_bcialg_1(B),v5_bcialg_1(B),v7_bcialg_1(B),l2_bcialg_1(B),m2_bcialg_1(C, B),m4_bcialg_2(A, B, C),true.
v3_relat_2(A) :- ~ (v2_struct_0(B)) ,v3_bcialg_1(B),v4_bcialg_1(B),v5_bcialg_1(B),v7_bcialg_1(B),l2_bcialg_1(B),m2_bcialg_1(C, B),m4_bcialg_2(A, B, C),true.
v8_relat_2(A) :- ~ (v2_struct_0(B)) ,v3_bcialg_1(B),v4_bcialg_1(B),v5_bcialg_1(B),v7_bcialg_1(B),l2_bcialg_1(B),m2_bcialg_1(C, B),m4_bcialg_2(A, B, C),true.
v1_bcialg_3(A) :- l2_bcialg_1(A), ~ (v2_struct_0(A)) ,v3_bcialg_1(A),v4_bcialg_1(A),v5_bcialg_1(A),v7_bcialg_1(A),v8_bcialg_1(A),v11_bcialg_3(A).
v10_bcialg_3(A) :- l2_bcialg_1(A), ~ (v2_struct_0(A)) ,v3_bcialg_1(A),v4_bcialg_1(A),v5_bcialg_1(A),v7_bcialg_1(A),v8_bcialg_1(A),v11_bcialg_3(A).
v5_algstr_0(A) :- l2_algstr_0(A), ~ (v2_struct_0(A)) ,v6_algstr_0(A),v2_rlvect_1(A).
v6_algstr_0(A) :- l2_algstr_0(A), ~ (v2_struct_0(A)) ,v5_algstr_0(A),v2_rlvect_1(A).
v6_algstr_0(A) :- l2_algstr_0(A), ~ (v2_struct_0(A)) ,v13_algstr_0(A),v3_rlvect_1(A),v4_rlvect_1(A).
v1_xboole_0(A) :- m1_subset_1(A, k1_zfmisc_1(k2_zfmisc_1(k2_zfmisc_1(k1_xboole_0, k1_xboole_0), k1_xboole_0))),v1_funct_1(A),v1_funct_2(A, k2_zfmisc_1(k1_xboole_0, k1_xboole_0), k1_xboole_0).
v1_binop_1(A, k1_xboole_0) :- m1_subset_1(A, k1_zfmisc_1(k2_zfmisc_1(k2_zfmisc_1(k1_xboole_0, k1_xboole_0), k1_xboole_0))),v1_funct_1(A),v1_funct_2(A, k2_zfmisc_1(k1_xboole_0, k1_xboole_0), k1_xboole_0).
v2_binop_1(A, k1_xboole_0) :- m1_subset_1(A, k1_zfmisc_1(k2_zfmisc_1(k2_zfmisc_1(k1_xboole_0, k1_xboole_0), k1_xboole_0))),v1_funct_1(A),v1_funct_2(A, k2_zfmisc_1(k1_xboole_0, k1_xboole_0), k1_xboole_0).
v1_rat_1(A) :- m1_subset_1(A, k3_numbers),true.
v1_trees_2(A) :- true, ~ (v1_xboole_0(A)) ,v1_trees_1(A),v1_bintree1(A).
v2_bintree1(A) :- ~ (v2_struct_0(B)) ,v1_dtconstr(B),v2_dtconstr(B),v3_bintree1(B),l1_lang1(B),m1_subset_1(A, k4_dtconstr(B)),true.
v1_bintree1(A) :- true, ~ (v1_xboole_0(A)) ,v1_trees_1(A),v1_bintree2(A).
v5_pre_topc(A, k5_topmetr, B) :- v1_borsuk_2(B),l1_pre_topc(B),m1_subset_1(C, u1_struct_0(B)),m1_subset_1(D, u1_struct_0(B)),m1_borsuk_2(A, B, C, D),true.
v1_connsp_1(A) :- l1_pre_topc(A), ~ (v2_struct_0(A)) ,v2_pre_topc(A),v1_borsuk_2(A).
v6_pre_topc(A) :- l1_pre_topc(A),v2_struct_0(A).
v1_compts_1(A) :- l1_pre_topc(A),v2_struct_0(A),v2_pre_topc(A).
~ (v1_zfmisc_1(A)) :- m1_subset_1(A, k1_zfmisc_1(u1_struct_0(k15_euclid(2)))),v1_topreal2(A).
v1_xreal_0(A) :- m1_subset_1(A, k3_numbers),true.
~ (v1_xboole_0(A)) :- true,v1_xreal_0(A), ~ (v1_rat_1(A)) .
v1_xreal_0(A) :- v3_topmetr(B),l1_struct_0(B),m1_subset_1(A, u1_struct_0(B)),true.
v3_topmetr(A) :- v3_topmetr(B),l1_pre_topc(B),m1_pre_topc(A, B),true.
v1_ideal_1(A, B) :- ~ (v2_struct_0(B)) ,l6_algstr_0(B),m1_subset_1(A, k1_zfmisc_1(u1_struct_0(B))),v2_c0sp1(A, B).
v1_c0sp1(A, B) :- ~ (v2_struct_0(B)) ,l6_algstr_0(B),m1_subset_1(A, k1_zfmisc_1(u1_struct_0(B))),v2_c0sp1(A, B).
v2_c0sp1(A, B) :- ~ (v2_struct_0(B)) ,l6_algstr_0(B),m1_subset_1(A, k1_zfmisc_1(u1_struct_0(B))),v1_ideal_1(A, B),v1_c0sp1(A, B).
v2_c0sp1(A, B) :- ~ (v2_struct_0(B)) ,v13_algstr_0(B),v2_rlvect_1(B),v3_rlvect_1(B),v4_rlvect_1(B),v5_rlvect_1(B),v6_rlvect_1(B),v7_rlvect_1(B),v2_funcsdom(B),v3_group_1(B),v5_group_1(B),v1_vectsp_1(B),v3_vectsp_1(B),l1_funcsdom(B),m1_subset_1(A, k1_zfmisc_1(u1_struct_0(B))),v4_c0sp1(A, B).
v2_cantor_1(A, B) :- l1_pre_topc(B),m1_subset_1(A, k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(B)))),v1_tops_2(A, B),v1_cantor_1(A, B).
v3_ordinal1(A) :- true,v1_card_1(A).
v1_card_1(A) :- true,v1_xboole_0(A).
v1_card_1(A) :- true,v7_ordinal1(A).
v1_finset_1(A) :- m1_subset_1(A, k4_ordinal1),true.
v1_finset_1(A) :- true,v7_ordinal1(A).
v7_ordinal1(A) :- true,v3_ordinal1(A),v1_finset_1(A).
v1_xboole_0(A) :- true,v3_card_1(A, k1_xboole_0).
v3_card_1(A, k1_xboole_0) :- true,v1_xboole_0(A).
~ (v1_xboole_0(A)) :- true,v3_card_1(A, 1).
v1_zfmisc_1(A) :- true,v3_card_1(A, 1).
v3_card_1(A, 1) :- true, ~ (v1_xboole_0(A)) ,v1_zfmisc_1(A).
v4_ordinal1(A) :- true, ~ (v1_finset_1(A)) ,v1_card_1(A).
v1_card_3(A) :- true,v1_xboole_0(A),v1_relat_1(A),v1_funct_1(A).
v2_relat_1(A) :- v1_setfam_1(C),m1_subset_1(A, k1_zfmisc_1(k2_zfmisc_1(B, C))),v1_funct_1(A),v1_funct_2(A, B, C).
v4_funct_1(A) :- true,v3_card_3(A).
v2_card_3(A) :- true,v3_card_3(A).
~ (v1_finset_1(A)) :- true,v5_card_3(A).
v4_card_3(A) :- true,v5_card_3(A).
v5_card_3(A) :- true, ~ (v1_finset_1(A)) ,v4_card_3(A).
v4_card_3(A) :- true,v1_finset_1(A).
v4_card_3(A) :- v4_card_3(B),m1_subset_1(A, k1_zfmisc_1(B)),true.
v2_card_3(A) :- v2_card_3(B),m1_subset_1(A, k1_zfmisc_1(B)),true.
v5_funct_1(A, B) :- v1_relat_1(B),v2_relat_1(B),v1_funct_1(B),m1_subset_1(A, k4_card_3(B)),true.
v4_relat_1(A, B) :- v1_relat_1(C),v2_relat_1(C),v4_relat_1(C, B),v1_funct_1(C),m1_subset_1(A, k4_card_3(C)),true.
v5_funct_1(A, B) :- v1_relat_1(B),v1_funct_1(B),m1_subset_1(A, k8_card_3(B)),true.
v4_relat_1(A, B) :- v1_relat_1(C),v4_relat_1(C, B),v1_funct_1(C),m1_subset_1(A, k8_card_3(C)),true.
v1_partfun1(A, B) :- v1_relat_1(C),v2_relat_1(C),v4_relat_1(C, B),v1_funct_1(C),v1_partfun1(C, B),m1_subset_1(A, k4_card_3(C)),true.
v1_partfun1(A, B) :- v1_relat_1(C),v2_relat_1(C),v4_relat_1(C, B),v1_funct_1(C),v1_partfun1(C, B),m1_subset_1(A, k4_card_3(C)),true.
~ (v1_xboole_0(A)) :- true, ~ (v1_finset_1(A)) .
~ (v2_card_fil(A, B)) :- ~ (v1_finset_1(B)) ,m1_card_fil(A, B),v1_card_fil(A, B),v3_card_fil(A, B).
v2_card_1(A) :- true, ~ (v1_finset_1(A)) ,v1_card_1(A),v4_card_fil(A).
v1_card_5(A) :- true, ~ (v1_finset_1(A)) ,v1_card_1(A),v4_card_fil(A).
v2_card_1(A) :- true, ~ (v1_finset_1(A)) ,v1_card_1(A),v5_card_fil(A).
v1_card_5(A) :- true, ~ (v1_finset_1(A)) ,v1_card_1(A),v6_card_fil(A).
v5_card_fil(A) :- true, ~ (v1_finset_1(A)) ,v1_card_1(A),v6_card_fil(A).
v4_card_fil(A) :- true, ~ (v1_finset_1(A)) ,v1_card_1(A),v6_card_fil(A).
v1_card_5(A) :- true, ~ (v1_finset_1(A)) ,v1_card_1(A), ~ (v2_card_1(A)) .
v2_finset_1(A) :- true,v1_xboole_0(A),v1_relat_1(A),v1_funct_1(A).
v4_ordinal1(A) :- true,v3_ordinal1(A), ~ (v1_finset_1(A)) ,v1_card_1(A).
~ (v1_finset_1(A)) :- true,v3_ordinal1(A),v4_ordinal1(A), ~ (v1_xboole_0(A)) .
~ (v4_card_3(A)) :- true, ~ (v1_finset_1(A)) ,v1_card_1(A), ~ (v2_card_1(A)) .
v1_cat_5(A) :- l1_cat_1(A), ~ (v2_struct_0(A)) , ~ (v11_struct_0(A)) ,v2_cat_1(A),v3_cat_5(A).
v3_cat_5(A) :- ~ (v2_struct_0(B)) , ~ (v11_struct_0(B)) ,v2_cat_1(B),v3_cat_5(B),l1_cat_1(B),m3_cat_2(A, B),true.
v5_ordinal1(A) :- m1_catalan2(C, B),m1_subset_1(A, C),true.
v5_relat_1(A, B) :- m1_catalan2(C, B),m1_subset_1(A, C),true.
v1_finset_1(A) :- m1_catalan2(C, B),m1_subset_1(A, C),true.
~ (v1_catalg_1(A, B)) :- ~ (v2_struct_0(B)) ,l1_msualg_1(B),l3_msualg_1(A, B),v4_msualg_1(A, B).
~ (v11_struct_0(A)) :- l1_msualg_1(A), ~ (v2_struct_0(A)) ,v1_instalg1(A),v2_catalg_1(A).
v2_catalg_1(A) :- m1_catalg_1(A, B),true.
~ (v2_struct_0(A)) :- ~ (v1_xboole_0(B)) ,m1_catalg_1(A, B),true.
v4_funct_1(A) :- true,v3_matrix_2(A).
v2_relat_1(A) :- m1_subset_1(A, k1_zfmisc_1(k2_zfmisc_1(k5_numbers, k2_numbers))),v1_funct_1(A),v1_funct_2(A, k5_numbers, k2_numbers),v1_cfdiff_1(A).
v1_comseq_2(A) :- m1_subset_1(A, k1_zfmisc_1(k2_zfmisc_1(k5_numbers, k2_numbers))),v1_funct_1(A),v1_funct_2(A, k5_numbers, k2_numbers),v1_cfdiff_1(A).
v2_cgames_1(A) :- v3_ordinal1(B),m1_subset_1(A, k2_cgames_1(B)),true.
v1_cgames_1(A) :- l1_cgames_1(A),v2_cgames_1(A).
v7_ordinal1(A) :- v1_relat_1(B),v1_funct_1(B), ~ (v1_xboole_0(B)) ,v1_finseq_1(B),m1_subset_1(A, k4_finseq_1(B)),true.
~ (v1_xboole_0(A)) :- v1_relat_1(B),v1_funct_1(B), ~ (v1_xboole_0(B)) ,v1_finseq_1(B),m1_subset_1(A, k4_finseq_1(B)),true.
v2_cgames_1(A) :- v2_cgames_1(B),m1_subset_1(A, k10_cgames_1(B)),true.
v5_cgames_1(A) :- true,v2_cgames_1(A),v7_cgames_1(A).
v6_cgames_1(A) :- true,v2_cgames_1(A),v7_cgames_1(A).
v7_cgames_1(A) :- true,v2_cgames_1(A),v5_cgames_1(A),v6_cgames_1(A).
v6_cgames_1(A) :- true,v2_cgames_1(A),v10_cgames_1(A).
~ (v7_cgames_1(A)) :- true,v2_cgames_1(A),v10_cgames_1(A).
v10_cgames_1(A) :- true,v2_cgames_1(A),v6_cgames_1(A), ~ (v7_cgames_1(A)) .
v5_cgames_1(A) :- true,v2_cgames_1(A),v9_cgames_1(A).
~ (v7_cgames_1(A)) :- true,v2_cgames_1(A),v9_cgames_1(A).
v9_cgames_1(A) :- true,v2_cgames_1(A),v5_cgames_1(A), ~ (v7_cgames_1(A)) .
~ (v5_cgames_1(A)) :- true,v2_cgames_1(A),v8_cgames_1(A).
~ (v6_cgames_1(A)) :- true,v2_cgames_1(A),v8_cgames_1(A).
v8_cgames_1(A) :- true,v2_cgames_1(A), ~ (v5_cgames_1(A)) , ~ (v6_cgames_1(A)) .
v2_chord(A) :- true,v1_relat_1(A),v4_relat_1(A, k5_numbers),v1_funct_1(A),v1_finset_1(A),v1_glib_000(A),v4_glib_000(A).
v6_chord(A) :- true,v1_relat_1(A),v4_relat_1(A, k5_numbers),v1_funct_1(A),v1_finset_1(A),v1_glib_000(A),v2_chord(A).
v6_chord(A) :- v1_relat_1(B),v4_relat_1(B, k5_numbers),v1_funct_1(B),v1_finset_1(B),v1_glib_000(B),v6_chord(B),m2_glib_000(A, B, C, k21_glib_000(B, C)),true.
~ (v1_xboole_0(A)) :- v1_relat_1(B),v4_relat_1(B, k5_numbers),v1_funct_1(B),v1_finset_1(B),v1_glib_000(B),v2_glib_000(B),m3_chord(A, B),true.
v2_circcmb3(A, B) :- ~ (v2_struct_0(B)) , ~ (v11_struct_0(B)) ,v2_msafree2(B),l1_msualg_1(B),l3_msualg_1(A, B),v4_msualg_1(A, B),v4_msafree2(A, B),v3_circcmb3(A, B).
~ (v2_struct_0(A)) :- l1_msualg_1(A),v4_circcmb3(A).
v8_struct_0(A) :- l1_msualg_1(A),v4_circcmb3(A).
~ (v11_struct_0(A)) :- l1_msualg_1(A),v4_circcmb3(A).
v1_msualg_1(A) :- l1_msualg_1(A),v4_circcmb3(A).
v1_circcomb(A) :- l1_msualg_1(A),v4_circcmb3(A).
v2_circcomb(A) :- l1_msualg_1(A),v4_circcmb3(A).
v5_circcomb(A) :- l1_msualg_1(A), ~ (v2_struct_0(A)) ,v4_circcmb3(A).
v3_msualg_1(A, B) :- v4_circcmb3(B),l1_msualg_1(B),l3_msualg_1(A, B),v4_msafree2(A, B),v5_circcmb3(A, B).
v4_msualg_1(A, B) :- v4_circcmb3(B),l1_msualg_1(B),l3_msualg_1(A, B),v4_msafree2(A, B),v5_circcmb3(A, B).
v3_circcmb3(A, B) :- ~ (v2_struct_0(B)) , ~ (v11_struct_0(B)) ,v2_msafree2(B),l1_msualg_1(B),l3_msualg_1(A, B),v4_msualg_1(A, B),v4_msafree2(A, B),v5_circcmb3(A, B).
v4_msualg_1(A, B) :- ~ (v1_xboole_0(C)) ,v1_finset_1(C),m1_circcmb3(B, C),m2_circcmb3(A, C, B),true.
v4_circcomb(A, B) :- ~ (v1_xboole_0(C)) ,v1_finset_1(C),m1_circcmb3(B, C),m2_circcmb3(A, C, B),true.
v3_circcmb3(A, B) :- ~ (v1_xboole_0(C)) ,v1_finset_1(C),v8_struct_0(B),m1_circcmb3(B, C),m2_circcmb3(A, C, B),true.
~ (v2_facirc_1(A)) :- ~ (v2_facirc_1(B)) ,m1_subset_1(A, k1_zfmisc_1(B)),true.
v3_facirc_1(A) :- true,v1_relat_1(A),v1_funct_1(A),v6_valued_0(A).
v5_circcomb(A) :- l1_msualg_1(A), ~ (v2_struct_0(A)) ,v3_circcomb(A).
v2_msafree2(A) :- l1_msualg_1(A), ~ (v2_struct_0(A)) ,v1_circcomb(A).
v4_msualg_1(A, B) :- ~ (v2_struct_0(B)) ,l1_msualg_1(B),l3_msualg_1(A, B),v6_circcomb(A, B).
v4_msafree2(A, B) :- ~ (v2_struct_0(B)) ,l1_msualg_1(B),l3_msualg_1(A, B),v6_circcomb(A, B).
v1_relat_1(A) :- ~ (v2_struct_0(B)) , ~ (v11_struct_0(B)) ,l1_msualg_1(B),v1_relat_1(C),v2_relat_1(C),v4_relat_1(C, u1_struct_0(B)),v1_funct_1(C),v1_partfun1(C, u1_struct_0(B)), ~ (v1_xboole_0(D)) ,m1_subset_1(D, k1_zfmisc_1(k1_msaterm(B, C))),m1_subset_1(A, u1_struct_0(k1_circtrm1(B, C, D))),true.
v1_funct_1(A) :- ~ (v2_struct_0(B)) , ~ (v11_struct_0(B)) ,l1_msualg_1(B),v1_relat_1(C),v2_relat_1(C),v4_relat_1(C, u1_struct_0(B)),v1_funct_1(C),v1_partfun1(C, u1_struct_0(B)), ~ (v1_xboole_0(D)) ,m1_subset_1(D, k1_zfmisc_1(k1_msaterm(B, C))),m1_subset_1(A, u1_struct_0(k1_circtrm1(B, C, D))),true.
v1_finset_1(A) :- ~ (v2_struct_0(B)) , ~ (v11_struct_0(B)) ,l1_msualg_1(B),v1_relat_1(C),v2_relat_1(C),v4_relat_1(C, u1_struct_0(B)),v1_funct_1(C),v1_partfun1(C, u1_struct_0(B)), ~ (v1_xboole_0(D)) ,m1_subset_1(D, k1_zfmisc_1(k1_msaterm(B, C))),m1_subset_1(A, u1_struct_0(k1_circtrm1(B, C, D))),true.
v3_trees_2(A) :- ~ (v2_struct_0(B)) , ~ (v11_struct_0(B)) ,l1_msualg_1(B),v1_relat_1(C),v2_relat_1(C),v4_relat_1(C, u1_struct_0(B)),v1_funct_1(C),v1_partfun1(C, u1_struct_0(B)), ~ (v1_xboole_0(D)) ,m1_subset_1(D, k1_zfmisc_1(k1_msaterm(B, C))),m1_subset_1(A, u1_struct_0(k1_circtrm1(B, C, D))),true.
v1_relat_1(A) :- ~ (v2_struct_0(B)) , ~ (v11_struct_0(B)) ,l1_msualg_1(B),v1_relat_1(C),v2_relat_1(C),v4_relat_1(C, u1_struct_0(B)),v1_funct_1(C),v1_partfun1(C, u1_struct_0(B)),m3_msaterm(D, B, C),m1_subset_1(A, u4_struct_0(k1_circtrm1(B, C, D))),true.
v1_funct_1(A) :- ~ (v2_struct_0(B)) , ~ (v11_struct_0(B)) ,l1_msualg_1(B),v1_relat_1(C),v2_relat_1(C),v4_relat_1(C, u1_struct_0(B)),v1_funct_1(C),v1_partfun1(C, u1_struct_0(B)),m3_msaterm(D, B, C),m1_subset_1(A, u4_struct_0(k1_circtrm1(B, C, D))),true.
v1_finset_1(A) :- ~ (v2_struct_0(B)) , ~ (v11_struct_0(B)) ,l1_msualg_1(B),v1_relat_1(C),v2_relat_1(C),v4_relat_1(C, u1_struct_0(B)),v1_funct_1(C),v1_partfun1(C, u1_struct_0(B)),m3_msaterm(D, B, C),m1_subset_1(A, u4_struct_0(k1_circtrm1(B, C, D))),true.
v3_trees_2(A) :- ~ (v2_struct_0(B)) , ~ (v11_struct_0(B)) ,l1_msualg_1(B),v1_relat_1(C),v2_relat_1(C),v4_relat_1(C, u1_struct_0(B)),v1_funct_1(C),v1_partfun1(C, u1_struct_0(B)),m3_msaterm(D, B, C),m1_subset_1(A, u4_struct_0(k1_circtrm1(B, C, D))),true.
v1_relat_1(A) :- ~ (v2_struct_0(B)) , ~ (v11_struct_0(B)) ,v2_msafree2(B),v5_msafree2(B),l1_msualg_1(B),v4_msualg_1(C, B),v4_msafree2(C, B),l3_msualg_1(C, B),m1_subset_1(D, u1_struct_0(B)),m1_subset_1(A, k1_funct_1(u3_msualg_1(B, k5_msafree2(B, C)), D)),true.
v1_funct_1(A) :- ~ (v2_struct_0(B)) , ~ (v11_struct_0(B)) ,v2_msafree2(B),v5_msafree2(B),l1_msualg_1(B),v4_msualg_1(C, B),v4_msafree2(C, B),l3_msualg_1(C, B),m1_subset_1(D, u1_struct_0(B)),m1_subset_1(A, k1_funct_1(u3_msualg_1(B, k5_msafree2(B, C)), D)),true.
~ (v1_xboole_0(A)) :- ~ (v2_struct_0(B)) , ~ (v11_struct_0(B)) ,v2_msafree2(B),v5_msafree2(B),l1_msualg_1(B),v4_msualg_1(C, B),v4_msafree2(C, B),l3_msualg_1(C, B),m1_subset_1(D, u1_struct_0(B)),m1_subset_1(A, k1_funct_1(u3_msualg_1(B, k5_msafree2(B, C)), D)),true.
v1_finset_1(A) :- ~ (v2_struct_0(B)) , ~ (v11_struct_0(B)) ,v2_msafree2(B),v5_msafree2(B),l1_msualg_1(B),v4_msualg_1(C, B),v4_msafree2(C, B),l3_msualg_1(C, B),m1_subset_1(D, u1_struct_0(B)),m1_subset_1(A, k1_funct_1(u3_msualg_1(B, k5_msafree2(B, C)), D)),true.
v3_trees_2(A) :- ~ (v2_struct_0(B)) , ~ (v11_struct_0(B)) ,v2_msafree2(B),v5_msafree2(B),l1_msualg_1(B),v4_msualg_1(C, B),v4_msafree2(C, B),l3_msualg_1(C, B),m1_subset_1(D, u1_struct_0(B)),m1_subset_1(A, k1_funct_1(u3_msualg_1(B, k5_msafree2(B, C)), D)),true.
v1_classes1(A) :- true,v2_classes1(A).
v1_ordinal1(A) :- true,v1_classes2(A).
v2_classes1(A) :- true,v1_classes2(A).
v1_classes2(A) :- true,v1_ordinal1(A),v2_classes1(A).
v1_relat_1(A) :- ~ (v2_struct_0(B)) ,v13_algstr_0(B),v2_rlvect_1(B),v3_rlvect_1(B),v4_rlvect_1(B),v3_normsp_0(B),v4_normsp_0(B),v2_clvect_1(B),v3_clvect_1(B),v4_clvect_1(B),v5_clvect_1(B),v8_clvect_1(B),l2_clvect_1(B), ~ (v2_struct_0(C)) ,v13_algstr_0(C),v2_rlvect_1(C),v3_rlvect_1(C),v4_rlvect_1(C),v3_normsp_0(C),v4_normsp_0(C),v2_clvect_1(C),v3_clvect_1(C),v4_clvect_1(C),v5_clvect_1(C),v8_clvect_1(C),l2_clvect_1(C),m1_subset_1(A, u1_struct_0(k9_clopban1(B, C))),true.
v1_funct_1(A) :- ~ (v2_struct_0(B)) ,v13_algstr_0(B),v2_rlvect_1(B),v3_rlvect_1(B),v4_rlvect_1(B),v3_normsp_0(B),v4_normsp_0(B),v2_clvect_1(B),v3_clvect_1(B),v4_clvect_1(B),v5_clvect_1(B),v8_clvect_1(B),l2_clvect_1(B), ~ (v2_struct_0(C)) ,v13_algstr_0(C),v2_rlvect_1(C),v3_rlvect_1(C),v4_rlvect_1(C),v3_normsp_0(C),v4_normsp_0(C),v2_clvect_1(C),v3_clvect_1(C),v4_clvect_1(C),v5_clvect_1(C),v8_clvect_1(C),l2_clvect_1(C),m1_subset_1(A, u1_struct_0(k9_clopban1(B, C))),true.
v1_relat_1(A) :- ~ (v2_struct_0(B)) ,v13_algstr_0(B),v2_rlvect_1(B),v3_rlvect_1(B),v4_rlvect_1(B),v3_normsp_0(B),v4_normsp_0(B),v2_clvect_1(B),v3_clvect_1(B),v4_clvect_1(B),v5_clvect_1(B),v8_clvect_1(B),l2_clvect_1(B), ~ (v2_struct_0(C)) ,v13_algstr_0(C),v2_rlvect_1(C),v3_rlvect_1(C),v4_rlvect_1(C),v3_normsp_0(C),v4_normsp_0(C),v2_clvect_1(C),v3_clvect_1(C),v4_clvect_1(C),v5_clvect_1(C),v8_clvect_1(C),l2_clvect_1(C),m1_subset_1(A, u1_struct_0(k14_clopban1(B, C))),true.
v1_funct_1(A) :- ~ (v2_struct_0(B)) ,v13_algstr_0(B),v2_rlvect_1(B),v3_rlvect_1(B),v4_rlvect_1(B),v3_normsp_0(B),v4_normsp_0(B),v2_clvect_1(B),v3_clvect_1(B),v4_clvect_1(B),v5_clvect_1(B),v8_clvect_1(B),l2_clvect_1(B), ~ (v2_struct_0(C)) ,v13_algstr_0(C),v2_rlvect_1(C),v3_rlvect_1(C),v4_rlvect_1(C),v3_normsp_0(C),v4_normsp_0(C),v2_clvect_1(C),v3_clvect_1(C),v4_clvect_1(C),v5_clvect_1(C),v8_clvect_1(C),l2_clvect_1(C),m1_subset_1(A, u1_struct_0(k14_clopban1(B, C))),true.
v3_clopban1(A) :- l1_clopban2(A), ~ (v2_struct_0(A)) ,v13_algstr_0(A),v2_rlvect_1(A),v3_rlvect_1(A),v4_rlvect_1(A),v3_normsp_0(A),v4_normsp_0(A),v2_clvect_1(A),v3_clvect_1(A),v4_clvect_1(A),v5_clvect_1(A),v8_clvect_1(A),v2_cfuncdom(A),v3_group_1(A),v1_vectsp_1(A),v3_vectsp_1(A),v5_clopban2(A).
v2_vectsp_1(A) :- l1_clopban2(A), ~ (v2_struct_0(A)) ,v13_algstr_0(A),v2_rlvect_1(A),v3_rlvect_1(A),v4_rlvect_1(A),v3_normsp_0(A),v4_normsp_0(A),v2_clvect_1(A),v3_clvect_1(A),v4_clvect_1(A),v5_clvect_1(A),v8_clvect_1(A),v2_cfuncdom(A),v3_group_1(A),v1_vectsp_1(A),v3_vectsp_1(A),v5_clopban2(A).
v6_vectsp_1(A) :- l1_clopban2(A), ~ (v2_struct_0(A)) ,v13_algstr_0(A),v2_rlvect_1(A),v3_rlvect_1(A),v4_rlvect_1(A),v3_normsp_0(A),v4_normsp_0(A),v2_clvect_1(A),v3_clvect_1(A),v4_clvect_1(A),v5_clvect_1(A),v8_clvect_1(A),v2_cfuncdom(A),v3_group_1(A),v1_vectsp_1(A),v3_vectsp_1(A),v5_clopban2(A).
v2_clopban2(A) :- l1_clopban2(A), ~ (v2_struct_0(A)) ,v13_algstr_0(A),v2_rlvect_1(A),v3_rlvect_1(A),v4_rlvect_1(A),v3_normsp_0(A),v4_normsp_0(A),v2_clvect_1(A),v3_clvect_1(A),v4_clvect_1(A),v5_clvect_1(A),v8_clvect_1(A),v2_cfuncdom(A),v3_group_1(A),v1_vectsp_1(A),v3_vectsp_1(A),v5_clopban2(A).
v3_clopban2(A) :- l1_clopban2(A), ~ (v2_struct_0(A)) ,v13_algstr_0(A),v2_rlvect_1(A),v3_rlvect_1(A),v4_rlvect_1(A),v3_normsp_0(A),v4_normsp_0(A),v2_clvect_1(A),v3_clvect_1(A),v4_clvect_1(A),v5_clvect_1(A),v8_clvect_1(A),v2_cfuncdom(A),v3_group_1(A),v1_vectsp_1(A),v3_vectsp_1(A),v5_clopban2(A).
v4_clopban2(A) :- l1_clopban2(A), ~ (v2_struct_0(A)) ,v13_algstr_0(A),v2_rlvect_1(A),v3_rlvect_1(A),v4_rlvect_1(A),v3_normsp_0(A),v4_normsp_0(A),v2_clvect_1(A),v3_clvect_1(A),v4_clvect_1(A),v5_clvect_1(A),v8_clvect_1(A),v2_cfuncdom(A),v3_group_1(A),v1_vectsp_1(A),v3_vectsp_1(A),v5_clopban2(A).
v5_clopban2(A) :- l1_clopban2(A), ~ (v2_struct_0(A)) ,v13_algstr_0(A),v2_rlvect_1(A),v3_rlvect_1(A),v4_rlvect_1(A),v3_normsp_0(A),v4_normsp_0(A),v2_clvect_1(A),v3_clvect_1(A),v4_clvect_1(A),v5_clvect_1(A),v8_clvect_1(A),v3_clopban1(A),v2_cfuncdom(A),v3_group_1(A),v1_vectsp_1(A),v2_vectsp_1(A),v3_vectsp_1(A),v6_vectsp_1(A),v2_clopban2(A),v3_clopban2(A),v4_clopban2(A).
v9_clvect_1(A, B) :- ~ (v2_struct_0(B)) ,v13_algstr_0(B),v2_rlvect_1(B),v3_rlvect_1(B),v4_rlvect_1(B),v3_normsp_0(B),v4_normsp_0(B),v2_clvect_1(B),v3_clvect_1(B),v4_clvect_1(B),v5_clvect_1(B),v8_clvect_1(B),l2_clvect_1(B),m1_subset_1(A, k1_zfmisc_1(k2_zfmisc_1(k5_numbers, u1_struct_0(B)))),v1_funct_1(A),v1_funct_2(A, k5_numbers, u1_struct_0(B)),v1_clopban3(A, B).
v1_clopban3(A, B) :- ~ (v2_struct_0(B)) ,v13_algstr_0(B),v2_rlvect_1(B),v3_rlvect_1(B),v4_rlvect_1(B),v3_normsp_0(B),v4_normsp_0(B),v2_clvect_1(B),v3_clvect_1(B),v4_clvect_1(B),v5_clvect_1(B),v8_clvect_1(B),v3_clopban1(B),l2_clvect_1(B),m1_subset_1(A, k1_zfmisc_1(k2_zfmisc_1(k5_numbers, u1_struct_0(B)))),v1_funct_1(A),v1_funct_2(A, k5_numbers, u1_struct_0(B)),v2_clopban3(A, B).
v4_vectsp_1(A) :- l1_clopban2(A), ~ (v2_struct_0(A)) ,v13_algstr_0(A),v2_rlvect_1(A),v3_rlvect_1(A),v4_rlvect_1(A),v3_normsp_0(A),v4_normsp_0(A),v3_group_1(A),v1_vectsp_1(A),v3_vectsp_1(A),v2_clvect_1(A),v3_clvect_1(A),v4_clvect_1(A),v5_clvect_1(A),v8_clvect_1(A),v2_cfuncdom(A),v5_clopban2(A).
v2_closure1(A, B, C) :- v1_relat_1(C),v4_relat_1(C, B),v1_funct_1(C),v1_partfun1(C, B),m2_pboole(A, B, k5_mssubfam(B, C), k5_mssubfam(B, C)),v4_closure1(A, B, C).
v6_closure1(A, B) :- l1_struct_0(B),l1_closure1(A, B),v7_closure1(A, B).
v8_closure1(A, B) :- l1_struct_0(B),l1_closure1(A, B),v9_closure1(A, B).
v10_closure1(A, B) :- l1_struct_0(B),l1_closure1(A, B),v9_closure1(A, B).
v11_closure1(A, B) :- l1_struct_0(B),l1_closure1(A, B),v7_closure1(A, B).
v1_closure2(A, B, C) :- v1_relat_1(C),v4_relat_1(C, B),v1_funct_1(C),v1_partfun1(C, B),m1_subset_1(A, k1_zfmisc_1(k1_closure2(B, C))),v2_closure2(A, B, C).
v3_closure2(A, B, C) :- v1_relat_1(C),v4_relat_1(C, B),v1_funct_1(C),v1_partfun1(C, B),m1_subset_1(A, k1_zfmisc_1(k1_closure2(B, C))),v4_closure2(A, B, C).
v5_closure2(A, B, C) :- v1_relat_1(C),v4_relat_1(C, B),v1_funct_1(C),v1_partfun1(C, B),m1_subset_1(A, k1_zfmisc_1(k1_closure2(B, C))),v4_closure2(A, B, C).
~ (v1_xboole_0(A)) :- v1_relat_1(B),v4_relat_1(B, C),v1_funct_1(B),v1_partfun1(B, C),m1_subset_1(A, k1_zfmisc_1(k1_closure2(C, B))),v5_closure2(A, C, B).
v6_closure2(A, B, C) :- v1_relat_1(C),v4_relat_1(C, B),v1_funct_1(C),v1_partfun1(C, B),m1_subset_1(A, k1_zfmisc_1(k1_closure2(B, C))),v2_closure2(A, B, C).
~ (v1_xboole_0(A)) :- v1_relat_1(B),v4_relat_1(B, C),v1_funct_1(B),v1_partfun1(B, C),m1_subset_1(A, k1_zfmisc_1(k1_closure2(C, B))),v6_closure2(A, C, B).
v8_closure2(A, B, C) :- v1_relat_1(C),v4_relat_1(C, B),v1_funct_1(C),v1_partfun1(C, B),m1_subset_1(A, k1_zfmisc_1(k2_zfmisc_1(k6_closure2(B, C), k6_closure2(B, C)))),v1_funct_1(A),v1_funct_2(A, k6_closure2(B, C), k6_closure2(B, C)),v10_closure2(A, B, C).
v12_closure2(A, B) :- l1_struct_0(B),l1_closure2(A, B),v13_closure2(A, B).
v14_closure2(A, B) :- l1_struct_0(B),l1_closure2(A, B),v15_closure2(A, B).
v16_closure2(A, B) :- l1_struct_0(B),l1_closure2(A, B),v15_closure2(A, B).
v17_closure2(A, B) :- l1_struct_0(B),l1_closure2(A, B),v13_closure2(A, B).
~ (v1_xboole_0(A)) :- m1_subset_1(A, k3_coh_sp(B)),true.
v1_classes1(A) :- m1_subset_1(A, k3_coh_sp(B)),true.
v1_coh_sp(A) :- m1_subset_1(A, k3_coh_sp(B)),true.
~ (v1_xboole_0(A)) :- true,v1_cohsp_1(A).
~ (v1_xboole_0(A)) :- true,v2_cohsp_1(A).
v2_finsub_1(A) :- true,v1_classes1(A).
v3_cohsp_1(A) :- true, ~ (v1_xboole_0(A)) ,v1_classes1(A),v1_coh_sp(A).
v6_cohsp_1(A) :- true,v1_relat_1(A),v1_funct_1(A),v5_cohsp_1(A).
v5_cohsp_1(A) :- true,v1_relat_1(A),v1_funct_1(A),v4_cohsp_1(A).
v5_cohsp_1(A) :- true,v1_relat_1(A),v1_funct_1(A),v8_cohsp_1(A).
v7_cohsp_1(A) :- true,v1_relat_1(A),v1_funct_1(A),v9_cohsp_1(A).
v8_cohsp_1(A) :- true,v1_relat_1(A),v1_funct_1(A),v9_cohsp_1(A).
v4_cohsp_1(A) :- true,v1_relat_1(A),v1_funct_1(A),v10_cohsp_1(A).
v9_cohsp_1(A) :- true,v1_relat_1(A),v1_funct_1(A),v10_cohsp_1(A).
v8_cohsp_1(A) :- v3_cohsp_1(B),v1_relat_1(A),v4_relat_1(A, B),v1_funct_1(A),v1_partfun1(A, B),v5_cohsp_1(A).
v9_cohsp_1(A) :- v2_finsub_1(B),v1_relat_1(A),v4_relat_1(A, B),v1_funct_1(A),v1_partfun1(A, B),v7_cohsp_1(A),v8_cohsp_1(A).
v10_cohsp_1(A) :- true,v1_relat_1(A),v1_funct_1(A),v4_cohsp_1(A),v9_cohsp_1(A).
v2_compact1(A, B) :- v2_pre_topc(B),l1_pre_topc(B),m1_subset_1(A, k1_zfmisc_1(u1_struct_0(B))),v1_xboole_0(A).
v5_compact1(A) :- l1_pre_topc(A), ~ (v2_struct_0(A)) ,v2_pre_topc(A),v6_waybel_3(A).
v6_waybel_3(A) :- l1_pre_topc(A), ~ (v2_struct_0(A)) ,v2_pre_topc(A),v9_pre_topc(A),v5_compact1(A).
v4_compact1(A) :- l1_pre_topc(A), ~ (v2_struct_0(A)) ,v2_pre_topc(A),v3_compact1(A).
v3_compact1(A) :- l1_pre_topc(A), ~ (v2_struct_0(A)) ,v2_pre_topc(A),v4_compact1(A).
v5_compact1(A) :- l1_pre_topc(A), ~ (v2_struct_0(A)) ,v2_pre_topc(A),v3_compact1(A).
v3_compact1(A) :- l1_pre_topc(A), ~ (v2_struct_0(A)) ,v2_pre_topc(A),v8_pre_topc(A),v5_compact1(A).
v5_compact1(A) :- l1_pre_topc(A), ~ (v2_struct_0(A)) ,v2_pre_topc(A),v1_compts_1(A).
v5_compact1(A) :- l1_pre_topc(A), ~ (v2_struct_0(A)) ,v2_pre_topc(A),v1_tdlat_3(A).
v6_compact1(A, B, C) :- v2_pre_topc(B),l1_pre_topc(B),v2_pre_topc(C),l1_pre_topc(C),m1_subset_1(A, k1_zfmisc_1(k2_zfmisc_1(u1_struct_0(B), u1_struct_0(C)))),v1_funct_1(A),v1_funct_2(A, u1_struct_0(B), u1_struct_0(C)),v7_compact1(A, B, C).
v2_compl_sp(A, B) :- l1_metric_1(B),m1_subset_1(A, k1_zfmisc_1(u1_struct_0(B))),v1_xboole_0(A).
v3_compl_sp(A, B) :- l1_metric_1(B),m1_subset_1(A, k1_zfmisc_1(u1_struct_0(B))),v1_xboole_0(A).
v1_xcmplx_0(A) :- m1_subset_1(A, u1_struct_0(k1_complfld)),true.
v5_compos_1(A, B) :- l1_compos_1(B), ~ (v1_xboole_0(A)) ,v1_zfmisc_1(A),v1_relat_1(A),v4_relat_1(A, k5_numbers),v5_relat_1(A, u1_compos_1(B)),v1_funct_1(A),v1_finset_1(A).
v2_compos_1(A, B) :- l1_compos_1(B),v1_xboole_0(A),v1_relat_1(A),v4_relat_1(A, k5_numbers),v5_relat_1(A, u1_compos_1(B)),v1_funct_1(A),v1_finset_1(A).
v5_compos_1(A, B) :- l1_compos_1(B), ~ (v1_xboole_0(A)) ,v1_relat_1(A),v4_relat_1(A, k5_numbers),v5_relat_1(A, u1_compos_1(B)),v1_funct_1(A),v1_finset_1(A),v2_compos_1(A, B).
v2_compts_1(A, B) :- l1_pre_topc(B),m1_subset_1(A, k1_zfmisc_1(u1_struct_0(B))),v1_xboole_0(A).
v4_pre_topc(A, B) :- ~ (v2_struct_0(B)) ,v2_pre_topc(B),v8_pre_topc(B),l1_pre_topc(B),m1_subset_1(A, k1_zfmisc_1(u1_struct_0(B))),v2_compts_1(A, B).
v1_compts_1(A) :- l1_pre_topc(A),v8_struct_0(A),v2_pre_topc(A).
v2_compts_1(A, B) :- v2_pre_topc(B),l1_pre_topc(B),m1_subset_1(A, k1_zfmisc_1(u1_struct_0(B))),v1_finset_1(A).
v8_pre_topc(A) :- l1_pre_topc(A),v2_struct_0(A).
v8_pre_topc(A) :- v8_pre_topc(B),l1_pre_topc(B),m1_pre_topc(A, B),true.
v4_funct_1(A) :- m1_rfunct_3(A, B, C), ~ (v1_xboole_0(A)) .
v2_margrel1(A) :- true,v1_xboole_0(A),v1_relat_1(A).
v4_relat_1(A, k3_finseq_2(k5_numbers)) :- m1_subset_1(A, k1_zfmisc_1(k2_zfmisc_1(k3_finseq_2(k5_numbers), k5_numbers))),v1_funct_1(A).
v6_valued_0(A) :- m1_subset_1(A, k1_zfmisc_1(k2_zfmisc_1(k3_finseq_2(k5_numbers), k5_numbers))),v1_funct_1(A).
v2_comput_1(A) :- m1_subset_1(A, k1_zfmisc_1(k2_zfmisc_1(k3_finseq_2(k5_numbers), k5_numbers))),v1_funct_1(A),v3_margrel1(A, k5_numbers).
v3_comput_1(A) :- true,v1_xboole_0(A),v1_relat_1(A).
v2_margrel1(A) :- m1_subset_1(A, k2_comput_1(B)),true.
v2_margrel1(A) :- ~ (v1_xboole_0(B)) , ~ (v1_xboole_0(C)) ,m1_subset_1(C, k1_zfmisc_1(k2_comput_1(B))),m1_subset_1(A, C),true.
v4_relat_1(A, k3_finseq_2(k5_numbers)) :- m1_subset_1(A, k2_comput_1(k5_numbers)),true.
v6_valued_0(A) :- m1_subset_1(A, k2_comput_1(k5_numbers)),true.
v2_margrel1(A) :- m1_subset_1(A, k2_comput_1(k5_numbers)),true.
v2_margrel1(A) :- m1_subset_1(A, k9_comput_1),true.
v1_relat_1(A) :- true,v7_comput_1(A).
v1_funct_1(A) :- true,v7_comput_1(A).
v4_relat_1(A, k3_finseq_2(k5_numbers)) :- true,v1_relat_1(A),v7_comput_1(A).
v6_valued_0(A) :- true,v1_relat_1(A),v7_comput_1(A).
v2_margrel1(A) :- true,v1_relat_1(A),v7_comput_1(A).
v7_comput_1(A) :- m1_subset_1(A, k9_comput_1),true.
v2_margrel1(A) :- m1_subset_1(A, k9_comput_1),true.
v3_margrel1(A, k5_numbers) :- m1_subset_1(A, k9_comput_1),true.
v3_margrel1(A, k5_numbers) :- m1_subset_1(A, k2_comput_1(k5_numbers)),v7_comput_1(A).
v2_comput_1(A) :- true,v1_relat_1(A),v4_relat_1(A, k3_finseq_2(k5_numbers)),v1_funct_1(A),v7_comput_1(A).
~ (v1_xboole_0(A)) :- true,v1_relat_1(A),v1_funct_1(A),v2_margrel1(A),v8_comput_1(A, 1).
~ (v1_xboole_0(A)) :- true,v1_relat_1(A),v1_funct_1(A),v2_margrel1(A),v8_comput_1(A, 2).
~ (v1_xboole_0(A)) :- true,v1_relat_1(A),v1_funct_1(A),v2_margrel1(A),v8_comput_1(A, 3).
v3_seq_2(A) :- m1_subset_1(A, k1_zfmisc_1(k2_zfmisc_1(k5_numbers, k2_numbers))),v1_funct_1(A),v1_funct_2(A, k5_numbers, k2_numbers),v1_comseq_2(A).
~ (v1_comseq_2(A)) :- m1_subset_1(A, k1_zfmisc_1(k2_zfmisc_1(k5_numbers, k2_numbers))),v1_funct_1(A),v1_funct_2(A, k5_numbers, k2_numbers), ~ (v3_seq_2(A)) .
v4_seq_2(A) :- m1_subset_1(A, k1_zfmisc_1(k2_zfmisc_1(k5_numbers, k1_numbers))),v1_funct_1(A),v1_funct_2(A, k5_numbers, k1_numbers),v1_series_1(A).
v1_series_1(A) :- m1_subset_1(A, k1_zfmisc_1(k2_zfmisc_1(k5_numbers, k1_numbers))),v1_funct_1(A),v1_funct_2(A, k5_numbers, k1_numbers),v2_series_1(A).
v1_comseq_2(A) :- m1_subset_1(A, k1_zfmisc_1(k2_zfmisc_1(k5_numbers, k2_numbers))),v1_funct_1(A),v1_funct_2(A, k5_numbers, k2_numbers),v1_comseq_3(A).
v1_comseq_3(A) :- m1_subset_1(A, k1_zfmisc_1(k2_zfmisc_1(k5_numbers, k2_numbers))),v1_funct_1(A),v1_funct_2(A, k5_numbers, k2_numbers),v2_comseq_3(A).
v5_conlat_1(A, B) :- v2_struct_0(B),v11_struct_0(B),l5_struct_0(B),l2_conlat_1(A, B),true.
v6_conlat_1(A, B) :- v1_conlat_1(B),l5_struct_0(B),l2_conlat_1(A, B),true.
v2_connsp_1(A, B) :- l1_pre_topc(B),m1_subset_1(A, k1_zfmisc_1(u1_struct_0(B))),v3_connsp_1(A, B).
~ (v1_xboole_0(A)) :- ~ (v2_struct_0(B)) ,v2_pre_topc(B),l1_pre_topc(B),m1_subset_1(A, k1_zfmisc_1(u1_struct_0(B))),v3_connsp_1(A, B).
v4_pre_topc(A, B) :- v2_pre_topc(B),l1_pre_topc(B),m1_subset_1(A, k1_zfmisc_1(u1_struct_0(B))),v3_connsp_1(A, B).
v2_connsp_1(A, B) :- l1_pre_topc(B),m1_subset_1(A, k1_zfmisc_1(u1_struct_0(B))),v1_xboole_0(A).
v1_convex4(A, B) :- ~ (v2_struct_0(B)) ,l1_clvect_1(B),m1_subset_1(A, k1_zfmisc_1(u1_struct_0(B))),v1_xboole_0(A).
v6_ordinal1(A) :- true,v1_xboole_0(A).
v6_ordinal1(A) :- v6_ordinal1(B),m1_subset_1(A, k1_zfmisc_1(B)),true.
v1_dilworth(A, B) :- l1_orders_2(B),m1_subset_1(A, k1_zfmisc_1(u1_struct_0(B))),v1_zfmisc_1(A).
v6_orders_2(A, B) :- v3_orders_2(B),l1_orders_2(B),m1_subset_1(A, k1_zfmisc_1(u1_struct_0(B))),v1_dilworth(A, B).
v2_dilworth(A, B) :- l1_orders_2(B),m1_subset_1(A, k1_zfmisc_1(u1_struct_0(B))),v1_zfmisc_1(A).
v3_dilworth(A) :- l1_orders_2(A),v8_struct_0(A).
v1_finset_1(A) :- v3_dilworth(B),l1_orders_2(B),m1_subset_1(A, k1_zfmisc_1(u1_struct_0(B))),v1_dilworth(A, B).
v4_dilworth(A) :- l1_orders_2(A),v8_struct_0(A).
v1_finset_1(A) :- v4_dilworth(B),l1_orders_2(B),m1_subset_1(A, k1_zfmisc_1(u1_struct_0(B))),v2_dilworth(A, B).
v8_struct_0(A) :- l1_orders_2(A),v3_dilworth(A),v4_dilworth(A).
v5_dilworth(A, B) :- v2_struct_0(B),l1_orders_2(B),m1_eqrel_1(A, u1_struct_0(B)),v1_xboole_0(A).
v6_dilworth(A, B) :- v2_struct_0(B),l1_orders_2(B),m1_eqrel_1(A, u1_struct_0(B)),true.
v1_dilworth(A, B) :- ~ (v2_struct_0(B)) ,v4_dilworth(B),l1_orders_2(B),m1_subset_1(A, k1_zfmisc_1(u1_struct_0(B))),v7_dilworth(A, B).
v7_dilworth(A, B) :- ~ (v2_struct_0(B)) ,v4_orders_2(B),v5_orders_2(B),v4_dilworth(B),l1_orders_2(B),m1_subset_1(A, k1_zfmisc_1(u1_struct_0(B))),v3_card_1(A, 1).
v6_trees_3(A) :- ~ (v1_xboole_0(B)) ,m1_trees_3(C, B),m1_finseq_1(A, C),true.
~ (v1_xboole_0(A)) :- ~ (v1_xboole_0(B)) ,m1_dynkin(A, B),true.
~ (v1_xboole_0(A)) :- m1_finseq_1(A, k1_numbers),v1_matrprob(A).
v4_partfun3(A) :- m1_finseq_1(A, k1_numbers),v1_matrprob(A).
~ (v3_relat_1(A)) :- m1_finseq_1(A, k3_finseq_2(k1_numbers)),v1_matrix_1(A),v3_matrprob(A).
~ (v3_relat_1(A)) :- m1_finseq_1(A, k3_finseq_2(k1_numbers)),v1_matrix_1(A),v4_matrprob(A).
~ (v1_xboole_0(A)) :- ~ (v1_xboole_0(B)) ,m1_eqrel_1(A, B),true.
v1_setfam_1(A) :- m1_eqrel_1(A, B),true.
v3_card_1(A, B) :- v7_ordinal1(B),m1_subset_1(A, k1_euclid(B)),true.
v1_finseq_1(A) :- v7_ordinal1(B),m1_subset_1(A, u1_struct_0(k15_euclid(B))),true.
v3_valued_0(A) :- v7_ordinal1(B),m1_subset_1(A, u1_struct_0(k15_euclid(B))),true.
v3_card_1(A, B) :- v7_ordinal1(B),m1_subset_1(A, u1_struct_0(k15_euclid(B))),true.
v1_euclid_7(A) :- true,v1_xboole_0(A).
v2_euclid_7(A) :- true,v1_xboole_0(A).
v1_euclid_7(A) :- true,v3_euclid_7(A).
v2_euclid_7(A) :- true,v3_euclid_7(A).
v3_euclid_7(A) :- true,v1_euclid_7(A),v2_euclid_7(A).
v3_euclid_7(A) :- v7_ordinal1(B),m1_subset_1(A, k1_zfmisc_1(k1_euclid(B))),v5_euclid_7(A, B).
v4_euclid_7(A, B) :- v7_ordinal1(B),m1_subset_1(A, k1_zfmisc_1(k1_euclid(B))),v5_euclid_7(A, B).
v5_euclid_7(A, B) :- v7_ordinal1(B),m1_subset_1(A, k1_zfmisc_1(k1_euclid(B))),v3_euclid_7(A),v4_euclid_7(A, B).
~ (v1_xboole_0(A)) :- ~ (v1_xboole_0(B)) ,v7_ordinal1(B),m1_subset_1(A, k1_zfmisc_1(k1_euclid(B))),v5_euclid_7(A, B).
v3_valued_0(A) :- m1_subset_1(B, k5_numbers),m1_subset_1(A, u1_struct_0(k7_real_ns1(B))),true.
v3_valued_0(A) :- m1_subset_1(A, u1_struct_0(k10_funcsdom(B))),true.
v1_rlvect_3(A, k10_funcsdom(k2_finseq_1(B))) :- v7_ordinal1(B),m1_subset_1(A, k1_zfmisc_1(u1_struct_0(k10_funcsdom(k2_finseq_1(B))))),v3_euclid_7(A).
v1_rlvect_3(A, k7_real_ns1(B)) :- m1_subset_1(B, k5_numbers),m1_subset_1(A, k1_zfmisc_1(u1_struct_0(k7_real_ns1(B)))),v3_euclid_7(A).
v5_relat_1(A, k1_numbers) :- v7_ordinal1(B),m1_subset_1(A, u1_struct_0(k14_euclid(B))),true.
v3_card_1(A, B) :- v7_ordinal1(B),m1_subset_1(A, u1_struct_0(k14_euclid(B))),true.
v1_exchsort(A) :- true,v5_ordinal1(A),v1_relat_1(A),v1_funct_1(A).
v1_exchsort(A) :- true,v1_relat_1(A),v1_funct_1(A),v1_finseq_1(A).
v2_exchsort(A, k1_xboole_0) :- true,v5_ordinal1(A),v1_relat_1(A),v1_funct_1(A).
v2_exchsort(A, 1) :- true,v1_relat_1(A),v1_funct_1(A),v1_finseq_1(A).
v5_ordinal1(A) :- true,v1_relat_1(A),v1_funct_1(A),v1_exchsort(A),v2_exchsort(A, k1_xboole_0).
v5_exchsort(A, B) :- l1_orders_2(B),v1_xboole_0(A),v1_relat_1(A),v5_relat_1(A, u1_struct_0(B)),v1_funct_1(A),v1_exchsort(A).
v5_relat_1(A, B) :- m1_subset_1(A, k8_afinsq_1(B)),true.
v3_valued_0(A) :- v1_relat_1(B),v1_funct_1(B),v3_valued_0(B),v1_exchsort(B),m1_exchsort(A, B),true.
v5_ordinal1(A) :- v3_ordinal1(B), ~ (v1_xboole_0(C)) ,m1_subset_1(A, k9_funct_2(B, C)),true.
v3_valued_0(A) :- v3_membered(B), ~ (v1_xboole_0(B)) ,m1_subset_1(A, k9_funct_2(C, B)),true.
v5_relat_1(A, B) :- v1_relat_1(C),v5_relat_1(C, B),v1_funct_1(C),v1_exchsort(C),m1_exchsort(A, C),true.
v5_relat_1(A, B) :- m1_subset_1(C, k1_zfmisc_1(B)),m1_subset_1(A, k1_funct_2(D, C)),true.
~ (v1_xboole_0(A)) :- true,v1_facirc_1(A).
~ (v1_facirc_1(A)) :- true,v7_ordinal1(A).
~ (v2_facirc_1(A)) :- true,v1_xboole_0(A).
v1_xboole_0(A) :- true,v1_relat_1(A), ~ (v2_facirc_1(A)) .
v1_circcomb(A) :- l1_msualg_1(A),v11_struct_0(A).
v2_circcomb(A) :- l1_msualg_1(A),v11_struct_0(A).
v3_circcomb(A) :- l1_msualg_1(A),v11_struct_0(A).
~ (v1_facirc_1(A)) :- true,v1_xboole_0(A).
v3_facirc_1(A) :- true,v1_xboole_0(A),v1_relat_1(A),v1_funct_1(A).
v1_fcont_1(A) :- m1_subset_1(A, k1_zfmisc_1(k2_zfmisc_1(k1_numbers, k1_numbers))),v1_funct_1(A),v3_funct_1(A).
v1_fcont_1(A) :- m1_subset_1(A, k1_zfmisc_1(k2_zfmisc_1(k1_numbers, k1_numbers))),v1_funct_1(A),v1_xboole_0(A).
v2_fcont_1(A) :- m1_subset_1(A, k1_zfmisc_1(k2_zfmisc_1(k1_numbers, k1_numbers))),v1_funct_1(A),v1_xboole_0(A).
v2_fcont_1(A) :- m1_subset_1(A, k1_zfmisc_1(k2_zfmisc_1(k1_numbers, k1_numbers))),v1_funct_1(A),v3_funct_1(A).
v1_fcont_1(A) :- m1_subset_1(A, k1_zfmisc_1(k2_zfmisc_1(k1_numbers, k1_numbers))),v1_funct_1(A),v2_fcont_1(A).
v2_rcomp_1(A) :- m1_subset_1(A, k1_zfmisc_1(k1_numbers)),v1_xboole_0(A).
v3_rcomp_1(A) :- m1_subset_1(A, k1_zfmisc_1(k1_numbers)),v1_xboole_0(A).
v1_setfam_1(A) :- v1_setfam_1(B),m1_subset_1(A, k1_zfmisc_1(B)),true.
v14_lattices(A) :- l3_lattices(A), ~ (v2_struct_0(A)) ,v10_lattices(A),v3_filter_0(A).
v11_lattices(A) :- l3_lattices(A), ~ (v2_struct_0(A)) ,v10_lattices(A),v3_filter_0(A).
v3_filter_0(A) :- l3_lattices(A), ~ (v2_struct_0(A)) ,v10_lattices(A),v17_lattices(A).
v11_lattices(A) :- l3_lattices(A), ~ (v2_struct_0(A)) ,v10_lattices(A),v3_filter_0(A).
v1_finseq_1(A) :- true,v1_relat_1(A),v1_xboole_0(A).
v1_finset_1(A) :- true,v1_relat_1(A),v1_funct_1(A),v1_finseq_1(A).
v5_relat_1(A, B) :- m1_finseq_1(A, B),true.
v1_finseq_1(A) :- true,v1_relat_1(A),v1_xboole_0(A).
v4_relat_1(A, k5_numbers) :- true,v1_relat_1(A),v1_funct_1(A),v1_finseq_1(A).
v2_finseq_1(A) :- true,v1_relat_1(A),v1_funct_1(A),v1_finseq_1(A).
v4_relat_1(A, k5_numbers) :- true,v1_relat_1(A),v1_funct_1(A),v2_finseq_1(A).
v3_finseq_1(A) :- true,v1_xboole_0(A).
v4_funct_1(A) :- true,v3_finseq_1(A).
v1_finseq_1(A) :- v3_finseq_1(B),m1_subset_1(A, B),true.
v3_finseq_1(A) :- v3_finseq_1(B),m1_subset_1(A, k1_zfmisc_1(B)),true.
v2_funct_1(A) :- true,v1_relat_1(A),v1_funct_1(A),v3_valued_0(A),v7_valued_0(A),v1_finseq_1(A).
v3_card_1(A, B) :- ~ (v1_xboole_0(C)) ,v7_ordinal1(B),m1_subset_1(A, k4_finseq_2(B, C)),true.
v4_funct_1(A) :- m1_finseq_2(A, B),true.
v1_finset_1(A) :- v1_finset_1(B),m1_eqrel_1(A, B),true.
v1_finset_1(A) :- true,v1_xboole_0(A).
v1_finset_1(A) :- v1_finset_1(B),m1_subset_1(A, k1_zfmisc_1(B)),true.
v1_finset_1(A) :- v1_finset_1(B),m1_subset_1(A, k1_zfmisc_1(k2_zfmisc_1(B, C))),v1_funct_1(A),v1_funct_2(A, B, C).
v1_finset_1(A) :- true,v1_zfmisc_1(A).
~ (v1_zfmisc_1(A)) :- true, ~ (v1_finset_1(A)) .
v1_finsub_1(A) :- true,v4_finsub_1(A).
v3_finsub_1(A) :- true,v4_finsub_1(A).
v4_finsub_1(A) :- true,v1_finsub_1(A),v3_finsub_1(A).
v1_finset_1(A) :- m1_subset_1(A, k5_finsub_1(B)),true.
v4_fin_topo(A, B) :- ~ (v2_struct_0(B)) ,l1_orders_2(B),m1_subset_1(A, k1_zfmisc_1(u1_struct_0(B))),v1_xboole_0(A).
v3_orders_2(A) :- ~ (v2_struct_0(B)) ,v3_orders_2(B),l1_orders_2(B),m1_fintopo6(A, B), ~ (v2_struct_0(A)) .
v3_fintopo6(A, B) :- ~ (v2_struct_0(B)) ,l1_orders_2(B),m1_subset_1(A, k1_zfmisc_1(u1_struct_0(B))),v1_xboole_0(A).
v2_setfam_1(A) :- true,v1_xboole_0(A).
v2_setfam_1(A) :- v2_setfam_1(B),m1_subset_1(A, k1_zfmisc_1(B)),true.
v3_fomodel0(A, B) :- ~ (v1_xboole_0(B)) ,m1_subset_1(A, k1_zfmisc_1(k4_finseq_2(1, B))),true.
v5_relat_1(A, B) :- m1_subset_1(C, k1_zfmisc_1(B)),v1_relat_1(A),v5_relat_1(A, C).
v1_partfun1(A, B) :- ~ (v1_xboole_0(C)) ,m1_subset_1(A, k1_zfmisc_1(k2_zfmisc_1(B, C))),v1_funct_2(A, B, C).
v5_relat_1(A, B) :- m1_subset_1(A, k3_finseq_2(B)),true.
v3_relat_1(A) :- true,v1_relat_1(A),v5_relat_1(A, k1_tarski(k1_xboole_0)).
v5_relat_1(A, k1_tarski(k1_xboole_0)) :- true,v1_relat_1(A),v3_relat_1(A).
v7_ordinal1(A) :- true,v1_int_1(A), ~ (v3_xxreal_0(A)) .
~ (v1_xboole_0(A)) :- ~ (v1_xboole_0(B)) ,v7_ordinal1(B),v1_relat_1(A),v1_funct_1(A),v3_card_1(A, k2_xcmplx_0(B, k1_xboole_0)),v1_finseq_1(A).
v1_pre_poly(A) :- ~ (v1_xboole_0(B)) ,v3_finseq_1(B),v1_relat_1(A),v5_relat_1(A, B),v1_funct_1(A).
v1_pre_poly(A) :- m1_subset_1(A, k9_funct_2(B, k3_finseq_2(C))),true.
~ (v1_xboole_0(A)) :- v7_ordinal1(B),v1_relat_1(A),v1_funct_1(A),v3_card_1(A, k2_xcmplx_0(B, 1)),v1_finseq_1(A).
v1_lexbfs(A) :- true,v3_finseq_1(A).
~ (v3_relat_1(A)) :- ~ (v1_xboole_0(B)) ,m1_subset_1(A, k2_fomodel0(k3_finseq_2(B), k6_subset_1(k3_finseq_2(B), k1_tarski(k1_xboole_0)))), ~ (v1_xboole_0(A)) .
v1_xboole_0(A) :- v1_xboole_0(B),m1_subset_1(A, k3_finseq_2(B)),true.
~ (v3_relat_1(A)) :- v1_setfam_1(B),v1_relat_1(A),v5_relat_1(A, B), ~ (v1_xboole_0(A)) .
v1_setfam_1(A) :- v1_setfam_1(B),m1_subset_1(A, k1_zfmisc_1(B)),true.
v7_ordinal1(A) :- true,v1_int_1(A),v2_xxreal_0(A).
v10_fomodel1(A, B) :- ~ (v6_struct_0(B)) ,v11_fomodel1(B),l1_fomodel1(B),m1_subset_1(A, k1_fomodel1(B)),v9_fomodel1(A, B).
v5_fomodel1(A, B) :- ~ (v6_struct_0(B)) ,v11_fomodel1(B),l1_fomodel1(B),m1_subset_1(A, k1_fomodel1(B)),v7_fomodel1(A, B).
v8_fomodel1(A, B) :- ~ (v6_struct_0(B)) ,v11_fomodel1(B),l1_fomodel1(B),m1_subset_1(A, k1_fomodel1(B)),v6_fomodel1(A, B).
v8_fomodel1(A, B) :- ~ (v6_struct_0(B)) ,v11_fomodel1(B),l1_fomodel1(B),m1_subset_1(A, k1_fomodel1(B)),v4_fomodel1(A, B).
v9_fomodel1(A, B) :- ~ (v6_struct_0(B)) ,v11_fomodel1(B),l1_fomodel1(B),m1_subset_1(A, k1_fomodel1(B)),v8_fomodel1(A, B).
v5_fomodel1(A, B) :- ~ (v6_struct_0(B)) ,v11_fomodel1(B),l1_fomodel1(B),m1_subset_1(A, k1_fomodel1(B)),v6_fomodel1(A, B).
v10_fomodel1(A, B) :- ~ (v6_struct_0(B)) ,v11_fomodel1(B),l1_fomodel1(B),m1_subset_1(A, k1_fomodel1(B)),v5_fomodel1(A, B).
~ (v7_fomodel1(A, B)) :- ~ (v6_struct_0(B)) ,v11_fomodel1(B),l1_fomodel1(B),m1_subset_1(A, k1_fomodel1(B)),v8_fomodel1(A, B).
~ (v7_fomodel1(A, B)) :- ~ (v6_struct_0(B)) ,v11_fomodel1(B),l1_fomodel1(B),m1_subset_1(A, k1_fomodel1(B)),v4_fomodel1(A, B).
~ (v6_fomodel1(A, B)) :- ~ (v6_struct_0(B)) ,v11_fomodel1(B),l1_fomodel1(B),m1_subset_1(A, k1_fomodel1(B)),v4_fomodel1(A, B).
v6_fomodel1(A, B) :- ~ (v6_struct_0(B)) ,v11_fomodel1(B),l1_fomodel1(B),m1_subset_1(A, k1_fomodel1(B)),v5_fomodel1(A, B),v8_fomodel1(A, B).
v3_fomodel0(A, k15_fomodel1(B)) :- ~ (v6_struct_0(B)) ,v11_fomodel1(B),l1_fomodel1(B),v12_fomodel1(A, B).
v12_fomodel1(A, B) :- ~ (v6_struct_0(B)) ,v11_fomodel1(B),l1_fomodel1(B),v3_fomodel0(A, k15_fomodel1(B)).
~ (v1_xboole_0(A)) :- ~ (v6_struct_0(B)) ,v11_fomodel1(B),l1_fomodel1(B),m1_subset_1(A, k6_subset_1(k3_finseq_2(k15_fomodel1(B)), k1_tarski(k1_xboole_0))),true.
~ (v8_struct_0(A)) :- l1_fomodel1(A), ~ (v6_struct_0(A)) ,v11_fomodel1(A).
v13_fomodel1(A, B) :- v7_ordinal1(C), ~ (v6_struct_0(B)) ,v11_fomodel1(B),l1_fomodel1(B),m1_subset_1(A, k6_subset_1(k3_finseq_2(k15_fomodel1(B)), k1_tarski(k1_xboole_0))),v14_fomodel1(A, C, B).
~ (v1_xboole_0(A)) :- ~ (v6_struct_0(B)) ,v11_fomodel1(B),l1_fomodel1(B),v7_ordinal1(C),m1_subset_1(A, k1_funct_1(k28_fomodel1(B), C)),true.
~ (v1_xboole_0(A)) :- ~ (v6_struct_0(B)) ,v11_fomodel1(B),l1_fomodel1(B),m1_subset_1(A, k29_fomodel1(B)),true.
v3_card_1(A, 1) :- ~ (v6_struct_0(B)) ,v11_fomodel1(B),l1_fomodel1(B),m1_subset_1(A, k6_subset_1(k3_finseq_2(k15_fomodel1(B)), k1_tarski(k1_xboole_0))),v14_fomodel1(A, k6_numbers, B).
v15_fomodel1(A, B) :- ~ (v6_struct_0(B)) ,v11_fomodel1(B),l1_fomodel1(B),m1_subset_1(A, k32_fomodel1(B)),true.
v13_fomodel1(A, B) :- ~ (v6_struct_0(B)) ,v11_fomodel1(B),l1_fomodel1(B),m1_subset_1(A, k35_fomodel1(B)),true.
v8_fomodel1(A, B) :- ~ (v6_struct_0(B)) ,v11_fomodel1(B),l1_fomodel1(B),m1_subset_1(A, k1_fomodel1(B)), ~ (v7_fomodel1(A, B)) ,v10_fomodel1(A, B).
v6_fomodel1(A, B) :- ~ (v6_struct_0(B)) ,v11_fomodel1(B),l1_fomodel1(B),m1_subset_1(A, k1_fomodel1(B)), ~ (v4_fomodel1(A, B)) ,v8_fomodel1(A, B).
v4_fomodel1(A, B) :- ~ (v6_struct_0(B)) ,v11_fomodel1(B),l1_fomodel1(B),m1_subset_1(A, k16_fomodel1(B)),true.
v14_fomodel1(A, k2_xcmplx_0(B, C), D) :- ~ (v6_struct_0(D)) ,v11_fomodel1(D),l1_fomodel1(D),v7_ordinal1(B),v7_ordinal1(C),m1_subset_1(A, k6_subset_1(k3_finseq_2(k15_fomodel1(D)), k1_tarski(k1_xboole_0))),v14_fomodel1(A, k2_xcmplx_0(B, k3_xcmplx_0(k6_numbers, C)), D).
v4_fomodel1(A, B) :- ~ (v6_struct_0(B)) ,v11_fomodel1(B),l1_fomodel1(B),m1_subset_1(A, k1_fomodel1(B)), ~ (v5_fomodel1(A, B)) ,v9_fomodel1(A, B).
v5_relat_1(A, k5_fomodel1(B)) :- ~ (v6_struct_0(B)) ,v11_fomodel1(B),l1_fomodel1(B),m1_subset_1(A, k6_subset_1(k3_finseq_2(k15_fomodel1(B)), k1_tarski(k1_xboole_0))),v13_fomodel1(A, B).
v5_relat_1(A, k17_fomodel1(B)) :- ~ (v6_struct_0(B)) ,v11_fomodel1(B),l1_fomodel1(B),m1_subset_1(A, k6_subset_1(k3_finseq_2(k15_fomodel1(B)), k1_tarski(k1_xboole_0))),v15_fomodel1(A, B).
~ (v6_struct_0(A)) :- ~ (v6_struct_0(B)) ,l1_fomodel1(B),l1_fomodel1(A),v16_fomodel1(A, B).
v11_fomodel1(A) :- v11_fomodel1(B),l1_fomodel1(B),l1_fomodel1(A),v16_fomodel1(A, B).
v5_relat_1(A, B) :- ~ (v6_struct_0(C)) ,v11_fomodel1(C),l1_fomodel1(C), ~ (v1_xboole_0(B)) ,v8_fomodel1(D, C),m1_subset_1(D, k1_fomodel1(C)),m1_fomodel2(A, C, B, D),true.
v9_fomodel1(A, B) :- ~ (v6_struct_0(B)) ,v11_fomodel1(B),l1_fomodel1(B),m1_subset_1(A, k1_fomodel1(B)),v4_fomodel1(A, B).
v1_funcop_1(A) :- ~ (v6_struct_0(B)) ,v11_fomodel1(B),l1_fomodel1(B), ~ (v1_xboole_0(C)) ,v1_relat_1(A),v1_funct_1(A),v1_fomodel2(A, B, C).
~ (v1_xboole_0(A)) :- ~ (v6_struct_0(B)) ,v11_fomodel1(B),l1_fomodel1(B), ~ (v1_xboole_0(C)) ,v9_fomodel1(D, B),m1_subset_1(D, k1_fomodel1(B)),m1_fomodel2(A, B, C, D),true.
v1_funcop_1(A) :- ~ (v1_xboole_0(B)) , ~ (v1_xboole_0(D)) ,m1_subset_1(A, k1_zfmisc_1(k2_zfmisc_1(B, k9_funct_2(C, D)))),v1_funct_1(A),v1_funct_2(A, B, k9_funct_2(C, D)).
v1_funcop_1(A) :- v3_finseq_1(B),v1_relat_1(A),v5_relat_1(A, B),v1_funct_1(A).
v1_funct_1(A) :- ~ (v6_struct_0(B)) ,v11_fomodel1(B),l1_fomodel1(B), ~ (v1_xboole_0(C)) ,v1_relat_1(D),v1_funct_1(D),v1_fomodel2(D, B, C),v2_fomodel2(A, B, C, D).
v1_fomodel2(A, B, C) :- ~ (v6_struct_0(B)) ,v11_fomodel1(B),l1_fomodel1(B), ~ (v1_xboole_0(C)) ,m1_subset_1(A, k16_fomodel2(B, C)),true.
v15_fomodel1(A, B) :- ~ (v6_struct_0(B)) ,v11_fomodel1(B),l1_fomodel1(B),m1_subset_1(A, k6_subset_1(k3_finseq_2(k15_fomodel1(B)), k1_tarski(k1_xboole_0))),v3_fomodel2(A, B, k6_numbers).
v3_fomodel2(A, B, k6_numbers) :- ~ (v6_struct_0(B)) ,v11_fomodel1(B),l1_fomodel1(B),m1_subset_1(A, k6_subset_1(k3_finseq_2(k15_fomodel1(B)), k1_tarski(k1_xboole_0))),v15_fomodel1(A, B).
v4_fomodel2(A, B) :- ~ (v6_struct_0(B)) ,v11_fomodel1(B),l1_fomodel1(B),v7_ordinal1(C),m1_subset_1(A, k6_subset_1(k3_finseq_2(k15_fomodel1(B)), k1_tarski(k1_xboole_0))),v3_fomodel2(A, B, C).
v3_fomodel2(A, B, k2_xcmplx_0(C, D)) :- ~ (v6_struct_0(B)) ,v11_fomodel1(B),l1_fomodel1(B),v7_ordinal1(C),v7_ordinal1(D),m1_subset_1(A, k6_subset_1(k3_finseq_2(k15_fomodel1(B)), k1_tarski(k1_xboole_0))),v3_fomodel2(A, B, k1_nat_1(C, k4_nat_1(k6_numbers, D))).
~ (v15_fomodel1(A, B)) :- ~ (v6_struct_0(B)) ,v11_fomodel1(B),l1_fomodel1(B),m1_subset_1(A, k6_subset_1(k3_finseq_2(k15_fomodel1(B)), k1_tarski(k1_xboole_0))),v5_fomodel2(A, B).
v4_fomodel2(A, B) :- ~ (v6_struct_0(B)) ,v11_fomodel1(B),l1_fomodel1(B),m1_subset_1(A, k33_fomodel2(B)),true.
~ (v5_fomodel2(A, B)) :- ~ (v6_struct_0(B)) ,v11_fomodel1(B),l1_fomodel1(B),v7_ordinal1(C),m1_subset_1(A, k35_fomodel2(B, C)),true.
v5_fomodel2(A, B) :- ~ (v6_struct_0(B)) ,v11_fomodel1(B),l1_fomodel1(B),v7_ordinal1(C),m1_subset_1(A, k36_fomodel2(B, C)),true.
v4_relat_1(A, k37_fomodel1(B)) :- ~ (v6_struct_0(B)) ,v11_fomodel1(B),l1_fomodel1(B), ~ (v1_xboole_0(C)) ,m1_subset_1(A, k16_fomodel2(B, C)),true.
v1_partfun1(A, k37_fomodel1(B)) :- ~ (v6_struct_0(B)) ,v11_fomodel1(B),l1_fomodel1(B), ~ (v1_xboole_0(C)) ,m1_subset_1(A, k16_fomodel2(B, C)),v4_relat_1(A, k37_fomodel1(B)).
v7_fomodel2(A, B, C) :- ~ (v6_struct_0(C)) ,v11_fomodel1(C),l1_fomodel1(C),m1_subset_1(D, k1_zfmisc_1(B)),m1_subset_1(A, k1_fomodel1(C)),v7_fomodel2(A, D, C).
~ (v7_fomodel2(A, k3_xboole_0(B, C), D)) :- ~ (v6_struct_0(D)) ,v11_fomodel1(D),l1_fomodel1(D),m1_subset_1(A, k1_fomodel1(D)), ~ (v7_fomodel2(A, k13_fomodel0(C, B), D)) .
~ (v7_fomodel2(A, k2_xboole_0(D, B), C)) :- v1_finset_1(B), ~ (v6_struct_0(C)) ,v11_fomodel1(C),l1_fomodel1(C),m1_subset_1(A, k1_fomodel1(C)), ~ (v7_fomodel2(A, B, C)) , ~ (v7_fomodel2(A, D, C)) .
v9_fomodel2(A, B) :- ~ (v6_struct_0(B)) ,v11_fomodel1(B),l1_fomodel1(B),v6_fomodel2(A, B).
v4_fomodel2(A, B) :- ~ (v6_struct_0(B)) ,v11_fomodel1(B),l1_fomodel1(B),m1_subset_1(A, k43_fomodel2(B)),true.
v5_fomodel2(A, B) :- ~ (v6_struct_0(B)) ,v11_fomodel1(B),l1_fomodel1(B),m1_subset_1(A, k43_fomodel2(B)),true.
v4_fomodel2(A, B) :- ~ (v6_struct_0(B)) ,v11_fomodel1(B),l1_fomodel1(B),m1_subset_1(A, k43_fomodel2(B)),true.
v5_fomodel2(A, B) :- ~ (v6_struct_0(B)) ,v11_fomodel1(B),l1_fomodel1(B),m1_subset_1(A, k43_fomodel2(B)),true.
v1_fomodel2(A, B, C) :- ~ (v1_xboole_0(C)) , ~ (v6_struct_0(B)) ,v11_fomodel1(B),l1_fomodel1(B), ~ (v6_struct_0(D)) ,v11_fomodel1(D),v16_fomodel1(D, B),l1_fomodel1(D),v1_relat_1(A),v1_funct_1(A),v1_fomodel2(A, D, C).
v10_fomodel2(A, B, C, D) :- ~ (v1_xboole_0(B)) , ~ (v6_struct_0(C)) ,v11_fomodel1(C),l1_fomodel1(C),m1_subset_1(D, k16_fomodel2(C, B)),v10_fomodel2(E, B, C, D),m1_subset_1(A, k1_zfmisc_1(E)),true.
~ (v1_xboole_0(A)) :- ~ (v1_xboole_0(B)) ,v1_partfun1(C, B),v3_relat_2(C),v8_relat_2(C),m1_subset_1(C, k1_zfmisc_1(k2_zfmisc_1(B, B))),m1_subset_1(A, k8_eqrel_1(B, C)),true.
v9_fomodel1(A, B) :- ~ (v6_struct_0(B)) ,v11_fomodel1(B),l1_fomodel1(B),m1_subset_1(A, k37_fomodel1(B)),true.
v10_fomodel1(A, B) :- ~ (v6_struct_0(B)) ,v11_fomodel1(B),l1_fomodel1(B),m1_subset_1(A, k37_fomodel1(B)),true.
v1_fomodel3(A, k9_fomodel3(B, C, k1_int_2(k19_fomodel1(D, E))), C) :- ~ (v6_struct_0(D)) ,v11_fomodel1(D),l1_fomodel1(D), ~ (v1_xboole_0(B)) , ~ (v7_fomodel1(E, D)) ,v10_fomodel1(E, D),m1_subset_1(E, k1_fomodel1(D)),m1_subset_1(C, k1_zfmisc_1(k2_zfmisc_1(B, B))),m1_fomodel2(A, D, B, E),v2_fomodel3(A, D, B, E, C).
v1_fomodel3(A, k9_fomodel3(B, C, k1_int_2(k19_fomodel1(D, E))), k3_fomodel2(k6_margrel1)) :- ~ (v6_struct_0(D)) ,v11_fomodel1(D),l1_fomodel1(D), ~ (v1_xboole_0(B)) ,v7_fomodel1(E, D),m1_subset_1(E, k1_fomodel1(D)),m1_subset_1(C, k1_zfmisc_1(k2_zfmisc_1(B, B))),m1_fomodel2(A, D, B, E),v2_fomodel3(A, D, B, E, C).
v1_pre_poly(A) :- ~ (v6_struct_0(B)) ,v11_fomodel1(B),l1_fomodel1(B),m1_subset_1(A, k9_funct_2(k33_fomodel2(B), k33_fomodel2(B))),true.
v2_fomodel4(A, B) :- ~ (v6_struct_0(B)) ,v11_fomodel1(B),l1_fomodel1(B),m1_subset_1(A, k1_zfmisc_1(k1_fomodel4(B))),true.
v1_fomodel4(A, B) :- ~ (v6_struct_0(B)) ,v11_fomodel1(B),l1_fomodel1(B),m1_subset_1(A, k1_fomodel4(B)),true.
v3_fomodel4(A, B, C, k1_xboole_0) :- ~ (v6_struct_0(B)) ,v11_fomodel1(B),l1_fomodel1(B),m1_subset_1(C, k1_zfmisc_1(k9_funct_2(k9_setfam_1(k1_fomodel4(B)), k9_setfam_1(k1_fomodel4(B))))),v7_fomodel4(A, B, C).
v7_fomodel4(A, B, C) :- ~ (v6_struct_0(B)) ,v11_fomodel1(B),l1_fomodel1(B),m1_subset_1(C, k1_zfmisc_1(k9_funct_2(k9_setfam_1(k1_fomodel4(B)), k9_setfam_1(k1_fomodel4(B))))),v3_fomodel4(A, B, C, k1_xboole_0).
v7_fomodel4(A, B, C) :- ~ (v6_struct_0(B)) ,v11_fomodel1(B),l1_fomodel1(B),m1_subset_1(C, k1_zfmisc_1(k9_funct_2(k9_setfam_1(k1_fomodel4(B)), k9_setfam_1(k1_fomodel4(B))))),v1_xboole_0(D),v3_fomodel4(A, B, C, D).
v11_fomodel4(A, B) :- ~ (v6_struct_0(B)) ,v11_fomodel1(B),l1_fomodel1(B),v1_fomodel4(A, B).
v11_fomodel4(A, B) :- ~ (v6_struct_0(B)) ,v11_fomodel1(B),l1_fomodel1(B),m1_subset_1(A, k1_fomodel4(B)),true.
v1_fomodel4(A, B) :- ~ (v6_struct_0(B)) ,v11_fomodel1(B),l1_fomodel1(B),m1_subset_1(C, k1_zfmisc_1(k9_funct_2(k9_setfam_1(k1_fomodel4(B)), k9_setfam_1(k1_fomodel4(B))))),v7_ordinal1(D),v4_fomodel4(A, D, B, C, E).
v8_fomodel4(A, B, C, D) :- ~ (v6_struct_0(B)) ,v11_fomodel1(B),l1_fomodel1(B),m1_subset_1(C, k1_zfmisc_1(k9_funct_2(k9_setfam_1(k1_fomodel4(B)), k9_setfam_1(k1_fomodel4(B))))),v8_fomodel4(A, B, C, k6_subset_1(D, E)).
v8_fomodel4(A, B, C, k2_xboole_0(D, E)) :- ~ (v6_struct_0(B)) ,v11_fomodel1(B),l1_fomodel1(B),m1_subset_1(C, k1_zfmisc_1(k9_funct_2(k9_setfam_1(k1_fomodel4(B)), k9_setfam_1(k1_fomodel4(B))))),v8_fomodel4(A, B, C, k6_subset_1(D, E)).
v8_fomodel4(A, B, C, D) :- ~ (v6_struct_0(B)) ,v11_fomodel1(B),l1_fomodel1(B),m1_subset_1(C, k1_zfmisc_1(k9_funct_2(k9_setfam_1(k1_fomodel4(B)), k9_setfam_1(k1_fomodel4(B))))),v8_fomodel4(A, B, C, k3_xboole_0(D, E)).
v8_fomodel4(A, B, C, D) :- ~ (v6_struct_0(B)) ,v11_fomodel1(B),l1_fomodel1(B),m1_subset_1(C, k1_zfmisc_1(k9_funct_2(k9_setfam_1(k1_fomodel4(B)), k9_setfam_1(k1_fomodel4(B))))),m1_subset_1(E, k1_zfmisc_1(D)),v8_fomodel4(A, B, C, E).
v12_fomodel4(A, k6_numbers, B) :- ~ (v6_struct_0(B)) ,v11_fomodel1(B),l1_fomodel1(B),m1_subset_1(A, k1_zfmisc_1(k9_funct_2(k9_setfam_1(k1_fomodel4(B)), k9_setfam_1(k1_fomodel4(B))))),v12_fomodel4(A, 1, B).
v12_fomodel4(A, 1, B) :- ~ (v6_struct_0(B)) ,v11_fomodel1(B),l1_fomodel1(B),m1_subset_1(A, k1_zfmisc_1(k9_funct_2(k9_setfam_1(k1_fomodel4(B)), k9_setfam_1(k1_fomodel4(B))))),v12_fomodel4(A, 2, B).
v2_fomodel4(A, B) :- ~ (v6_struct_0(B)) ,v11_fomodel1(B),l1_fomodel1(B),m1_subset_1(C, k1_zfmisc_1(k9_funct_2(k9_setfam_1(k1_fomodel4(B)), k9_setfam_1(k1_fomodel4(B))))),v3_fomodel4(A, B, C, D).
~ (v1_xboole_0(A)) :- ~ (v6_struct_0(B)) ,v11_fomodel1(B),l1_fomodel1(B),m1_subset_1(A, k1_zfmisc_1(k9_funct_2(k9_setfam_1(k1_fomodel4(B)), k9_setfam_1(k1_fomodel4(B))))),v12_fomodel4(A, k6_numbers, B).
v1_finset_1(A) :- ~ (v6_struct_0(B)) ,v11_fomodel1(B),l1_fomodel1(B),v13_fomodel4(A, B).
v13_fomodel4(A, B) :- ~ (v6_struct_0(B)) ,v11_fomodel1(B),l1_fomodel1(B),v13_fomodel4(C, B),m1_subset_1(A, k1_zfmisc_1(C)),true.
v11_fomodel4(A, B) :- ~ (v6_struct_0(B)) ,v11_fomodel1(B),l1_fomodel1(B),v1_fomodel4(A, B).
~ (v1_xboole_0(A)) :- ~ (v2_struct_0(B)) ,v2_pre_topc(B),l1_pre_topc(B),m1_subset_1(C, u1_struct_0(B)),m1_subset_1(A, k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(B)))),v1_tops_2(A, B),v1_yellow_8(A, B, C).
v3_frechet(A) :- l1_pre_topc(A), ~ (v2_struct_0(A)) ,v2_pre_topc(A),v1_frechet(A).
v4_frechet(A) :- l1_pre_topc(A), ~ (v2_struct_0(A)) ,v2_pre_topc(A),v3_frechet(A).
v1_funcop_1(A) :- v4_funct_1(B),v1_relat_1(A),v5_relat_1(A, B),v1_funct_1(A).
v2_funcop_1(A) :- true,v1_relat_1(A),v1_funct_1(A),v1_funcop_1(A).
v1_funcop_1(A) :- true,v1_relat_1(A),v1_funct_1(A),v1_xboole_0(A).
v1_funct_1(A) :- true,v1_xboole_0(A).
v2_funct_1(A) :- true,v1_xboole_0(A),v1_relat_1(A),v1_funct_1(A).
v1_funct_1(A) :- v1_relat_1(B),v1_funct_1(B),m1_subset_1(A, k1_zfmisc_1(B)),true.
v3_funct_1(A) :- true,v1_xboole_0(A),v1_relat_1(A),v1_funct_1(A).
~ (v1_zfmisc_1(A)) :- true,v1_relat_1(A),v1_funct_1(A), ~ (v3_funct_1(A)) .
v3_funct_1(A) :- true,v1_zfmisc_1(A),v1_relat_1(A),v1_funct_1(A).
v4_funct_1(A) :- true,v1_xboole_0(A).
v1_relat_1(A) :- v4_funct_1(B),m1_subset_1(A, B),true.
v1_funct_1(A) :- v4_funct_1(B),m1_subset_1(A, B),true.
v4_funct_1(A) :- v4_funct_1(B),m1_subset_1(A, k1_zfmisc_1(B)),true.
v4_relat_1(A, B) :- v1_relat_1(C),v4_relat_1(C, B),v1_funct_1(C),v1_relat_1(A),v1_funct_1(A),v5_funct_1(A, C).
v1_funct_2(A, B, C) :- m1_subset_1(A, k1_zfmisc_1(k2_zfmisc_1(B, C))),v1_funct_1(A),v1_partfun1(A, B).
v2_funct_1(A) :- m1_subset_1(A, k1_zfmisc_1(k2_zfmisc_1(C, B))),v1_funct_1(A),v3_funct_2(A, C, B).
v2_funct_2(A, B) :- m1_subset_1(A, k1_zfmisc_1(k2_zfmisc_1(C, B))),v1_funct_1(A),v3_funct_2(A, C, B).
v3_funct_2(A, B, C) :- m1_subset_1(A, k1_zfmisc_1(k2_zfmisc_1(B, C))),v1_funct_1(A),v2_funct_1(A),v2_funct_2(A, C).
v3_funct_2(A, B, B) :- m1_subset_1(A, k1_zfmisc_1(k2_zfmisc_1(B, B))),v1_relat_2(A),v1_funct_1(A),v1_partfun1(A, B),v1_funct_2(A, B, B).
v1_partfun1(A, B) :- ~ (v1_xboole_0(C)) ,m1_subset_1(A, k1_zfmisc_1(k2_zfmisc_1(B, C))),v1_funct_1(A),v1_funct_2(A, B, C).
~ (v1_xboole_0(A)) :- ~ (v1_xboole_0(B)) , ~ (v1_xboole_0(C)) ,m1_subset_1(A, k1_zfmisc_1(k2_zfmisc_1(B, C))),v1_funct_1(A),v1_funct_2(A, B, C).
v4_funct_1(A) :- m1_funct_2(A, B, C),true.
v1_funcop_1(A) :- true,v1_xboole_0(A),v1_relat_1(A),v1_funct_1(A).
v1_funcop_1(A) :- true,v1_relat_1(A),v1_funct_1(A),v1_finseq_1(A),v1_funct_7(A).
v1_funct_7(A) :- true,v1_xboole_0(A),v1_relat_1(A),v1_funct_1(A),v1_finseq_1(A).
v2_relat_1(A) :- ~ (v1_xboole_0(B)) ,v1_relat_1(B),v2_relat_1(B),v1_funct_1(B),v1_finseq_1(B),m2_funct_7(A, B),true.
v1_funct_7(A) :- ~ (v1_xboole_0(B)) ,v1_relat_1(B),v2_relat_1(B),v1_funct_1(B),v1_finseq_1(B),m2_funct_7(A, B),true.
v2_funct_8(A) :- true,v1_xboole_0(A),v1_relat_1(A).
v4_funct_8(A, B, C) :- v1_membered(B),v1_membered(C),m1_subset_1(A, k1_zfmisc_1(k2_zfmisc_1(B, C))),v1_funct_1(A),v2_funct_8(A),v3_funct_8(A, B, C).
v2_funct_8(A) :- v1_membered(B),v1_membered(C),m1_subset_1(A, k1_zfmisc_1(k2_zfmisc_1(B, C))),v1_funct_1(A),v4_funct_8(A, B, C).
v3_funct_8(A, B, C) :- v1_membered(B),v1_membered(C),m1_subset_1(A, k1_zfmisc_1(k2_zfmisc_1(B, C))),v1_funct_1(A),v4_funct_8(A, B, C).
v6_funct_8(A, B, C) :- v1_membered(B),v1_membered(C),m1_subset_1(A, k1_zfmisc_1(k2_zfmisc_1(B, C))),v1_funct_1(A),v2_funct_8(A),v5_funct_8(A, B, C).
v2_funct_8(A) :- v1_membered(B),v1_membered(C),m1_subset_1(A, k1_zfmisc_1(k2_zfmisc_1(B, C))),v1_funct_1(A),v6_funct_8(A, B, C).
v5_funct_8(A, B, C) :- v1_membered(B),v1_membered(C),m1_subset_1(A, k1_zfmisc_1(k2_zfmisc_1(B, C))),v1_funct_1(A),v6_funct_8(A, B, C).
v1_funcop_1(A) :- v1_funct_1(B),v1_funct_2(B, C, D),m1_subset_1(B, k1_zfmisc_1(k2_zfmisc_1(C, D))),v1_relat_1(E),v4_relat_1(E, C),v1_funct_1(E),v1_partfun1(E, C),v1_relat_1(F),v4_relat_1(F, D),v1_funct_1(F),v1_partfun1(F, D),m1_functor0(A, C, D, B, E, F),true.
v1_altcat_2(A) :- l2_altcat_1(A), ~ (v2_struct_0(A)) ,v12_altcat_1(A).
v6_functor0(A, B, C) :- l1_struct_0(B), ~ (v2_struct_0(C)) ,l1_struct_0(C),l1_functor0(A, B, C),v10_functor0(A, B, C).
v6_functor0(A, B, C) :- l1_struct_0(B), ~ (v2_struct_0(C)) ,l1_struct_0(C),l1_functor0(A, B, C),v11_functor0(A, B, C).
v6_functor0(A, B, C) :- ~ (v2_struct_0(B)) ,v2_altcat_1(B),v12_altcat_1(B),l2_altcat_1(B), ~ (v2_struct_0(C)) ,v12_altcat_1(C),l2_altcat_1(C),m2_functor0(A, B, C),v15_functor0(A, B, C).
v6_functor0(A, B, C) :- ~ (v2_struct_0(B)) ,v2_altcat_1(B),v12_altcat_1(B),l2_altcat_1(B), ~ (v2_struct_0(C)) ,v12_altcat_1(C),l2_altcat_1(C),m2_functor0(A, B, C),v16_functor0(A, B, C).
v8_functor0(A, B, C) :- ~ (v2_struct_0(B)) ,v2_altcat_1(B),v12_altcat_1(B),l2_altcat_1(B), ~ (v2_struct_0(C)) ,v12_altcat_1(C),l2_altcat_1(C),m2_functor0(A, B, C),true.
v12_functor0(A, B, C) :- ~ (v2_struct_0(B)) ,v2_altcat_1(B),v12_altcat_1(B),l2_altcat_1(B), ~ (v2_struct_0(C)) ,v12_altcat_1(C),l2_altcat_1(C),m2_functor0(A, B, C),true.
v10_functor0(A, B, C) :- ~ (v2_struct_0(B)) ,v2_altcat_1(B),v12_altcat_1(B),l2_altcat_1(B), ~ (v2_struct_0(C)) ,v12_altcat_1(C),l2_altcat_1(C),m2_functor0(A, B, C),v15_functor0(A, B, C).
v13_functor0(A, B, C) :- ~ (v2_struct_0(B)) ,v2_altcat_1(B),v12_altcat_1(B),l2_altcat_1(B), ~ (v2_struct_0(C)) ,v12_altcat_1(C),l2_altcat_1(C),m2_functor0(A, B, C),v15_functor0(A, B, C).
v15_functor0(A, B, C) :- ~ (v2_struct_0(B)) ,v2_altcat_1(B),v12_altcat_1(B),l2_altcat_1(B), ~ (v2_struct_0(C)) ,v12_altcat_1(C),l2_altcat_1(C),m2_functor0(A, B, C),v10_functor0(A, B, C),v13_functor0(A, B, C).
v11_functor0(A, B, C) :- ~ (v2_struct_0(B)) ,v2_altcat_1(B),v12_altcat_1(B),l2_altcat_1(B), ~ (v2_struct_0(C)) ,v12_altcat_1(C),l2_altcat_1(C),m2_functor0(A, B, C),v16_functor0(A, B, C).
v14_functor0(A, B, C) :- ~ (v2_struct_0(B)) ,v2_altcat_1(B),v12_altcat_1(B),l2_altcat_1(B), ~ (v2_struct_0(C)) ,v12_altcat_1(C),l2_altcat_1(C),m2_functor0(A, B, C),v16_functor0(A, B, C).
v16_functor0(A, B, C) :- ~ (v2_struct_0(B)) ,v2_altcat_1(B),v12_altcat_1(B),l2_altcat_1(B), ~ (v2_struct_0(C)) ,v12_altcat_1(C),l2_altcat_1(C),m2_functor0(A, B, C),v11_functor0(A, B, C),v14_functor0(A, B, C).
v3_valued_0(A) :- ~ (v1_xboole_0(B)) ,m1_subset_1(A, k1_zfmisc_1(k2_zfmisc_1(B, k1_numbers))),v5_relat_1(A, k1_rcomp_1(k6_numbers, 1)),v1_funct_1(A),v1_funct_2(A, B, k1_numbers).
v1_xxreal_0(A) :- true,v1_fvaluat1(A).
v1_fvaluat1(A) :- true,v1_int_1(A).
v1_int_1(A) :- true,v1_xreal_0(A),v1_fvaluat1(A).
v1_algstr_1(A) :- l2_algstr_0(A), ~ (v2_struct_0(A)) ,v2_rlvect_1(A),v4_rlvect_1(A).
v6_vectsp_1(A) :- l4_algstr_0(A), ~ (v2_struct_0(A)) ,v5_group_1(A),v3_vectsp_1(A).
v5_vectsp_1(A) :- l6_algstr_0(A), ~ (v2_struct_0(A)) ,v5_group_1(A),v1_vectsp_1(A).
v5_vectsp_1(A) :- l6_algstr_0(A), ~ (v2_struct_0(A)) ,v5_group_1(A),v2_vectsp_1(A).
v3_gcd_1(A) :- l6_algstr_0(A), ~ (v2_struct_0(A)) ,v13_algstr_0(A),v33_algstr_0(A),v5_group_1(A),v1_vectsp_1(A),v2_vectsp_1(A),v4_vectsp_1(A),v6_vectsp_1(A),v3_rlvect_1(A),v4_rlvect_1(A).
v6_glib_000(A) :- true,v1_relat_1(A),v4_relat_1(A, k5_numbers),v1_funct_1(A),v1_finset_1(A),v1_glib_000(A),v5_glib_000(A).
v3_glib_000(A) :- true,v1_relat_1(A),v4_relat_1(A, k5_numbers),v1_funct_1(A),v1_finset_1(A),v1_glib_000(A),v7_glib_000(A).
v5_glib_000(A) :- true,v1_relat_1(A),v4_relat_1(A, k5_numbers),v1_funct_1(A),v1_finset_1(A),v1_glib_000(A),v7_glib_000(A).
v7_glib_000(A) :- true,v1_relat_1(A),v4_relat_1(A, k5_numbers),v1_funct_1(A),v1_finset_1(A),v1_glib_000(A),v3_glib_000(A),v5_glib_000(A).
v8_glib_000(A) :- true,v1_relat_1(A),v4_relat_1(A, k5_numbers),v1_funct_1(A),v1_finset_1(A),v1_glib_000(A),v3_glib_000(A),v6_glib_000(A).
v3_glib_000(A) :- true,v1_relat_1(A),v4_relat_1(A, k5_numbers),v1_funct_1(A),v1_finset_1(A),v1_glib_000(A),v8_glib_000(A).
v6_glib_000(A) :- true,v1_relat_1(A),v4_relat_1(A, k5_numbers),v1_funct_1(A),v1_finset_1(A),v1_glib_000(A),v8_glib_000(A).
v2_glib_000(A) :- true,v1_relat_1(A),v4_relat_1(A, k5_numbers),v1_funct_1(A),v1_finset_1(A),v1_glib_000(A),v3_glib_000(A),v4_glib_000(A).
v2_glib_000(A) :- true,v1_relat_1(A),v4_relat_1(A, k5_numbers),v1_funct_1(A),v1_finset_1(A),v1_glib_000(A),v4_glib_000(A),v6_glib_000(A).
v2_glib_000(A) :- v1_relat_1(B),v4_relat_1(B, k5_numbers),v1_funct_1(B),v1_finset_1(B),v1_glib_000(B),v2_glib_000(B),m1_glib_000(A, B),true.
v3_glib_000(A) :- v1_relat_1(B),v4_relat_1(B, k5_numbers),v1_funct_1(B),v1_finset_1(B),v1_glib_000(B),v3_glib_000(B),m1_glib_000(A, B),true.
v4_glib_000(A) :- v1_relat_1(B),v4_relat_1(B, k5_numbers),v1_funct_1(B),v1_finset_1(B),v1_glib_000(B),v4_glib_000(B),m1_glib_000(A, B),true.
v5_glib_000(A) :- v1_relat_1(B),v4_relat_1(B, k5_numbers),v1_funct_1(B),v1_finset_1(B),v1_glib_000(B),v5_glib_000(B),m1_glib_000(A, B),true.
v2_glib_000(A) :- v1_relat_1(B),v4_relat_1(B, k5_numbers),v1_funct_1(B),v1_finset_1(B),v1_glib_000(B), ~ (v1_xboole_0(C)) ,v1_finset_1(C),m1_subset_1(C, k1_zfmisc_1(k6_glib_000(B))),v1_finset_1(D),m1_subset_1(D, k1_zfmisc_1(k21_glib_000(B, C))),m2_glib_000(A, B, C, D),true.
v4_glib_000(A) :- v1_relat_1(B),v4_relat_1(B, k5_numbers),v1_funct_1(B),v1_finset_1(B),v1_glib_000(B),m1_subset_1(C, k6_glib_000(B)),m1_subset_1(D, k1_zfmisc_1(k21_glib_000(B, k6_domain_1(k6_glib_000(B), C)))),m2_glib_000(A, B, k6_domain_1(k6_glib_000(B), C), D),true.
v2_glib_000(A) :- v1_relat_1(B),v4_relat_1(B, k5_numbers),v1_funct_1(B),v1_finset_1(B),v1_glib_000(B),m1_subset_1(C, k6_glib_000(B)),m2_glib_000(A, B, k6_domain_1(k6_glib_000(B), C), k1_xboole_0),true.
v4_glib_000(A) :- v1_relat_1(B),v4_relat_1(B, k5_numbers),v1_funct_1(B),v1_finset_1(B),v1_glib_000(B),m1_subset_1(C, k6_glib_000(B)),m2_glib_000(A, B, k6_domain_1(k6_glib_000(B), C), k1_xboole_0),true.
v7_glib_000(A) :- v1_relat_1(B),v4_relat_1(B, k5_numbers),v1_funct_1(B),v1_finset_1(B),v1_glib_000(B), ~ (v1_xboole_0(C)) ,m1_subset_1(C, k1_zfmisc_1(k6_glib_000(B))),m2_glib_000(A, B, C, k1_xboole_0),true.
v9_glib_000(A, B) :- v1_relat_1(B),v4_relat_1(B, k5_numbers),v1_funct_1(B),v1_finset_1(B),v1_glib_000(B),m1_subset_1(C, k1_zfmisc_1(k7_glib_000(B))),m2_glib_000(A, B, k6_glib_000(B), C),true.
v9_glib_000(A, B) :- v1_relat_1(B),v4_relat_1(B, k5_numbers),v1_funct_1(B),v1_finset_1(B),v1_glib_000(B),m2_glib_000(A, B, k6_glib_000(B), k1_xboole_0),true.
v9_glib_000(A, B) :- v1_relat_1(B),v4_relat_1(B, k5_numbers),v1_funct_1(B),v1_finset_1(B),v1_glib_000(B),m2_glib_000(A, B, k6_glib_000(B), k6_subset_1(k7_glib_000(B), k1_tarski(C))),true.
v9_glib_000(A, B) :- v1_relat_1(B),v4_relat_1(B, k5_numbers),v1_funct_1(B),v1_finset_1(B),v1_glib_000(B),m2_glib_000(A, B, k6_glib_000(B), k6_subset_1(k7_glib_000(B), C)),true.
v19_glib_000(A) :- true,v1_relat_1(A),v4_relat_1(A, k5_numbers),v1_funct_1(A),v1_partfun1(A, k5_numbers),v12_glib_000(A),v18_glib_000(A).
v15_glib_000(A) :- true,v1_relat_1(A),v4_relat_1(A, k5_numbers),v1_funct_1(A),v1_partfun1(A, k5_numbers),v12_glib_000(A),v20_glib_000(A).
v18_glib_000(A) :- true,v1_relat_1(A),v4_relat_1(A, k5_numbers),v1_funct_1(A),v1_partfun1(A, k5_numbers),v12_glib_000(A),v20_glib_000(A).
v20_glib_000(A) :- true,v1_relat_1(A),v4_relat_1(A, k5_numbers),v1_funct_1(A),v1_partfun1(A, k5_numbers),v12_glib_000(A),v15_glib_000(A),v18_glib_000(A).
v21_glib_000(A) :- true,v1_relat_1(A),v4_relat_1(A, k5_numbers),v1_funct_1(A),v1_partfun1(A, k5_numbers),v12_glib_000(A),v15_glib_000(A),v19_glib_000(A).
v15_glib_000(A) :- true,v1_relat_1(A),v4_relat_1(A, k5_numbers),v1_funct_1(A),v1_partfun1(A, k5_numbers),v12_glib_000(A),v21_glib_000(A).
v19_glib_000(A) :- true,v1_relat_1(A),v4_relat_1(A, k5_numbers),v1_funct_1(A),v1_partfun1(A, k5_numbers),v12_glib_000(A),v21_glib_000(A).
v14_glib_000(A) :- true,v1_relat_1(A),v4_relat_1(A, k5_numbers),v1_funct_1(A),v1_partfun1(A, k5_numbers),v12_glib_000(A),v15_glib_000(A),v16_glib_000(A).
v14_glib_000(A) :- true,v1_relat_1(A),v4_relat_1(A, k5_numbers),v1_funct_1(A),v1_partfun1(A, k5_numbers),v12_glib_000(A),v16_glib_000(A),v19_glib_000(A).
v4_glib_001(A, B) :- v1_relat_1(B),v4_relat_1(B, k5_numbers),v1_funct_1(B),v1_finset_1(B),v1_glib_000(B),m3_glib_001(A, B),v5_glib_001(A, B).
v5_glib_001(A, B) :- v1_relat_1(B),v4_relat_1(B, k5_numbers),v1_funct_1(B),v1_finset_1(B),v1_glib_000(B),m3_glib_001(A, B),v3_glib_001(A, B).
v6_glib_001(A, B) :- v1_relat_1(B),v4_relat_1(B, k5_numbers),v1_funct_1(B),v1_finset_1(B),v1_glib_000(B),m3_glib_001(A, B),v3_glib_001(A, B).
v5_glib_001(A, B) :- v1_relat_1(B),v4_relat_1(B, k5_numbers),v1_funct_1(B),v1_finset_1(B),v1_glib_000(B),m3_glib_001(A, B),v6_glib_001(A, B).
v1_glib_001(A, B) :- v1_relat_1(B),v4_relat_1(B, k5_numbers),v1_funct_1(B),v1_finset_1(B),v1_glib_000(B),m3_glib_001(A, B),v7_glib_001(A, B).
~ (v3_glib_001(A, B)) :- v1_relat_1(B),v4_relat_1(B, k5_numbers),v1_funct_1(B),v1_finset_1(B),v1_glib_000(B),m3_glib_001(A, B),v7_glib_001(A, B).
v4_glib_001(A, B) :- v1_relat_1(B),v4_relat_1(B, k5_numbers),v1_funct_1(B),v1_finset_1(B),v1_glib_000(B),m3_glib_001(A, B),v7_glib_001(A, B).
v1_glib_001(A, B) :- v1_relat_1(B),v4_relat_1(B, k5_numbers),v1_funct_1(B),v1_finset_1(B),v1_glib_000(B),m3_glib_001(A, B),v8_glib_001(A, B).
~ (v3_glib_001(A, B)) :- v1_relat_1(B),v4_relat_1(B, k5_numbers),v1_funct_1(B),v1_finset_1(B),v1_glib_000(B),m3_glib_001(A, B),v8_glib_001(A, B).
v5_glib_001(A, B) :- v1_relat_1(B),v4_relat_1(B, k5_numbers),v1_funct_1(B),v1_finset_1(B),v1_glib_000(B),m3_glib_001(A, B),v8_glib_001(A, B).
v1_glib_002(A) :- true,v1_relat_1(A),v4_relat_1(A, k5_numbers),v1_funct_1(A),v1_finset_1(A),v1_glib_000(A),v4_glib_000(A).
v3_glib_002(A) :- true,v1_relat_1(A),v4_relat_1(A, k5_numbers),v1_funct_1(A),v1_finset_1(A),v1_glib_000(A),v3_glib_000(A),v4_glib_000(A).
v7_glib_000(A) :- true,v1_relat_1(A),v4_relat_1(A, k5_numbers),v1_funct_1(A),v1_finset_1(A),v1_glib_000(A),v2_glib_002(A).
v1_glib_002(A) :- true,v1_relat_1(A),v4_relat_1(A, k5_numbers),v1_funct_1(A),v1_finset_1(A),v1_glib_000(A),v3_glib_002(A).
v2_glib_002(A) :- true,v1_relat_1(A),v4_relat_1(A, k5_numbers),v1_funct_1(A),v1_finset_1(A),v1_glib_000(A),v3_glib_002(A).
v3_glib_002(A) :- true,v1_relat_1(A),v4_relat_1(A, k5_numbers),v1_funct_1(A),v1_finset_1(A),v1_glib_000(A),v1_glib_002(A),v2_glib_002(A).
v3_glib_002(A) :- v1_relat_1(B),v4_relat_1(B, k5_numbers),v1_funct_1(B),v1_finset_1(B),v1_glib_000(B),m1_subset_1(C, k6_glib_000(B)),m2_glib_000(A, B, k6_domain_1(k6_glib_000(B), C), k1_xboole_0),true.
v2_glib_002(A) :- v1_relat_1(B),v4_relat_1(B, k5_numbers),v1_funct_1(B),v1_finset_1(B),v1_glib_000(B),v2_glib_002(B),m1_glib_000(A, B),true.
v1_glib_002(A) :- v1_relat_1(B),v4_relat_1(B, k5_numbers),v1_funct_1(B),v1_finset_1(B),v1_glib_000(B),m1_glib_000(A, B),v4_glib_002(A, B).
v4_glib_002(A, B) :- v1_relat_1(B),v4_relat_1(B, k5_numbers),v1_funct_1(B),v1_finset_1(B),v1_glib_000(B),m1_subset_1(C, k6_glib_000(B)),m2_glib_000(A, B, k1_glib_002(B, C), k21_glib_000(B, k1_glib_002(B, C))),true.
v4_glib_002(A, B) :- v1_relat_1(B),v4_relat_1(B, k5_numbers),v1_funct_1(B),v1_finset_1(B),v1_glib_000(B),m1_subset_1(C, k3_glib_002(B)),m2_glib_000(A, B, C, k21_glib_000(B, C)),true.
v3_glib_002(A) :- v1_relat_1(B),v4_relat_1(B, k5_numbers),v1_funct_1(B),v1_finset_1(B),v1_glib_000(B),v2_glib_000(B), ~ (v4_glib_000(B)) ,v3_glib_002(B),v11_glib_000(C, B),m1_subset_1(C, k6_glib_000(B)),m2_glib_000(A, B, k6_subset_1(k6_glib_000(B), k1_tarski(C)), k21_glib_000(B, k6_subset_1(k6_glib_000(B), k1_tarski(C)))),true.
v6_glib_002(A) :- true,v1_relat_1(A),v4_relat_1(A, k5_numbers),v1_funct_1(A),v1_partfun1(A, k5_numbers),v12_glib_000(A),v16_glib_000(A).
v8_glib_002(A) :- true,v1_relat_1(A),v4_relat_1(A, k5_numbers),v1_funct_1(A),v1_partfun1(A, k5_numbers),v12_glib_000(A),v15_glib_000(A),v16_glib_000(A).
v20_glib_000(A) :- true,v1_relat_1(A),v4_relat_1(A, k5_numbers),v1_funct_1(A),v1_partfun1(A, k5_numbers),v12_glib_000(A),v7_glib_002(A).
v6_glib_002(A) :- true,v1_relat_1(A),v4_relat_1(A, k5_numbers),v1_funct_1(A),v1_partfun1(A, k5_numbers),v12_glib_000(A),v8_glib_002(A).
v7_glib_002(A) :- true,v1_relat_1(A),v4_relat_1(A, k5_numbers),v1_funct_1(A),v1_partfun1(A, k5_numbers),v12_glib_000(A),v8_glib_002(A).
v8_glib_002(A) :- true,v1_relat_1(A),v4_relat_1(A, k5_numbers),v1_funct_1(A),v1_partfun1(A, k5_numbers),v12_glib_000(A),v6_glib_002(A),v7_glib_002(A).
v7_glib_003(A) :- true,v1_relat_1(A),v4_relat_1(A, k5_numbers),v1_funct_1(A),v1_finset_1(A),v1_glib_000(A),v1_glib_003(A),v8_glib_003(A).
v7_glib_003(A) :- true,v1_relat_1(A),v4_relat_1(A, k5_numbers),v1_funct_1(A),v1_finset_1(A),v1_glib_000(A),v1_glib_003(A),v2_glib_003(A),v3_glib_003(A),v11_glib_003(A).
v9_glib_003(A) :- true,v1_relat_1(A),v4_relat_1(A, k5_numbers),v1_funct_1(A),v1_finset_1(A),v1_glib_000(A),v1_glib_003(A),v2_glib_003(A),v3_glib_003(A),v11_glib_003(A).
v10_glib_003(A) :- true,v1_relat_1(A),v4_relat_1(A, k5_numbers),v1_funct_1(A),v1_finset_1(A),v1_glib_000(A),v1_glib_003(A),v2_glib_003(A),v3_glib_003(A),v11_glib_003(A).
v11_glib_003(A) :- true,v1_relat_1(A),v4_relat_1(A, k5_numbers),v1_funct_1(A),v1_finset_1(A),v1_glib_000(A),v1_glib_003(A),v2_glib_003(A),v3_glib_003(A),v7_glib_003(A),v9_glib_003(A),v10_glib_003(A).
v7_glib_003(A) :- v1_relat_1(B),v4_relat_1(B, k5_numbers),v1_funct_1(B),v1_finset_1(B),v1_glib_000(B),v1_glib_003(B),v7_glib_003(B),m1_glib_000(A, B),v1_glib_003(A),v4_glib_003(A, B).
v8_glib_003(A) :- v1_relat_1(B),v4_relat_1(B, k5_numbers),v1_funct_1(B),v1_finset_1(B),v1_glib_000(B),v1_glib_003(B),v8_glib_003(B),m1_glib_000(A, B),v1_glib_003(A),v4_glib_003(A, B).
v9_glib_003(A) :- v1_relat_1(B),v4_relat_1(B, k5_numbers),v1_funct_1(B),v1_finset_1(B),v1_glib_000(B),v2_glib_003(B),v9_glib_003(B),m1_glib_000(A, B),v2_glib_003(A),v5_glib_003(A, B).
v10_glib_003(A) :- v1_relat_1(B),v4_relat_1(B, k5_numbers),v1_funct_1(B),v1_finset_1(B),v1_glib_000(B),v3_glib_003(B),v10_glib_003(B),m1_glib_000(A, B),v3_glib_003(A),v6_glib_003(A, B).
v15_glib_003(A) :- true,v1_relat_1(A),v4_relat_1(A, k5_numbers),v1_funct_1(A),v1_partfun1(A, k5_numbers),v12_glib_000(A),v12_glib_003(A),v13_glib_003(A),v14_glib_003(A),v19_glib_003(A).
v17_glib_003(A) :- true,v1_relat_1(A),v4_relat_1(A, k5_numbers),v1_funct_1(A),v1_partfun1(A, k5_numbers),v12_glib_000(A),v12_glib_003(A),v13_glib_003(A),v14_glib_003(A),v19_glib_003(A).
v18_glib_003(A) :- true,v1_relat_1(A),v4_relat_1(A, k5_numbers),v1_funct_1(A),v1_partfun1(A, k5_numbers),v12_glib_000(A),v12_glib_003(A),v13_glib_003(A),v14_glib_003(A),v19_glib_003(A).
v19_glib_003(A) :- true,v1_relat_1(A),v4_relat_1(A, k5_numbers),v1_funct_1(A),v1_partfun1(A, k5_numbers),v12_glib_000(A),v12_glib_003(A),v13_glib_003(A),v14_glib_003(A),v15_glib_003(A),v17_glib_003(A),v18_glib_003(A).
v1_glib_002(A) :- v1_relat_1(B),v4_relat_1(B, k5_numbers),v1_funct_1(B),v1_finset_1(B),v1_glib_000(B),v2_glib_000(B),v1_glib_003(B),v7_glib_003(B),v7_ordinal1(C),m2_glib_000(A, B, k1_mcart_1(k15_glib_004(B, k16_glib_004(B), C)), k21_glib_000(B, k1_mcart_1(k15_glib_004(B, k16_glib_004(B), C)))),true.
v1_glib_002(A) :- v1_relat_1(B),v4_relat_1(B, k5_numbers),v1_funct_1(B),v1_finset_1(B),v1_glib_000(B),v2_glib_000(B),v1_glib_003(B),v7_glib_003(B),v7_ordinal1(C),m2_glib_000(A, B, k1_mcart_1(k15_glib_004(B, k16_glib_004(B), C)), k2_mcart_1(k15_glib_004(B, k16_glib_004(B), C))),true.
v8_glib_003(A) :- true,v1_relat_1(A),v4_relat_1(A, k5_numbers),v1_funct_1(A),v1_finset_1(A),v1_glib_000(A),v1_glib_003(A),v1_glib_005(A).
v5_group_1(A) :- l3_algstr_0(A), ~ (v2_struct_0(A)) ,v2_group_1(A),v3_group_1(A),v1_gr_cy_1(A).
v7_ordinal1(A) :- ~ (v1_xboole_0(B)) ,v7_ordinal1(B),m1_subset_1(A, u1_struct_0(k4_gr_cy_1(B))),true.
v7_graph_1(A, B) :- ~ (v2_struct_0(B)) ,l1_graph_1(B),m1_graph_1(A, B),v1_xboole_0(A).
v9_graph_1(A, B) :- ~ (v2_struct_0(B)) ,l1_graph_1(B),m1_graph_1(A, B),v2_funct_1(A),v1_xboole_0(A).
v2_finseq_1(A) :- m1_finseq_1(B, C),m1_subset_1(A, k1_zfmisc_1(B)),true.
v2_funct_1(A) :- ~ (v2_struct_0(B)) ,l1_graph_1(B),m1_graph_1(A, B),v1_xboole_0(A).
v7_graph_1(A, B) :- ~ (v2_struct_0(B)) ,l1_graph_1(B),m1_graph_1(A, B),v1_xboole_0(A).
v5_funct_1(A, B) :- v1_relat_1(B),v1_funct_1(B),m1_subset_1(C, k1_zfmisc_1(B)),v1_relat_1(A),v1_funct_1(A),v5_funct_1(A, C).
v5_funct_1(A, B) :- v1_relat_1(B),v1_funct_1(B),v1_relat_1(C),v1_funct_1(C),v5_funct_1(C, B),m1_subset_1(A, k1_zfmisc_1(C)),true.
v1_grnilp_1(A) :- ~ (v2_struct_0(B)) ,v2_group_1(B),v3_group_1(B),v1_grnilp_1(B),l3_algstr_0(B),m1_group_2(A, B),true.
v1_grnilp_1(A) :- l3_algstr_0(A), ~ (v2_struct_0(A)) ,v2_group_1(A),v3_group_1(A),v5_group_1(A).
v1_grnilp_1(A) :- l3_algstr_0(A), ~ (v2_struct_0(A)) ,v2_group_1(A),v3_group_1(A),v1_gr_cy_1(A).
v1_grsolv_1(A) :- l3_algstr_0(A), ~ (v2_struct_0(A)) ,v2_group_1(A),v3_group_1(A),v1_grnilp_1(A).
v1_group_1(A) :- l3_algstr_0(A),v2_group_1(A).
v3_group_1(A) :- ~ (v2_struct_0(B)) ,v2_group_1(B),v3_group_1(B),l3_algstr_0(B),m1_group_2(A, B),true.
v5_group_1(A) :- ~ (v2_struct_0(B)) ,v2_group_1(B),v3_group_1(B),v5_group_1(B),l3_algstr_0(B),m1_group_2(A, B),true.
v8_struct_0(A) :- ~ (v2_struct_0(B)) ,v8_struct_0(B),v2_group_1(B),v3_group_1(B),l3_algstr_0(B),m1_group_2(A, B),true.
v6_group_1(A, B, C) :- ~ (v2_struct_0(B)) ,v2_group_1(B),v3_group_1(B),l3_algstr_0(B), ~ (v2_struct_0(C)) ,v2_group_1(C),v3_group_1(C),l3_algstr_0(C),m1_subset_1(A, k1_zfmisc_1(k2_zfmisc_1(u1_struct_0(B), u1_struct_0(C)))),v1_funct_1(A),v1_funct_2(A, u1_struct_0(B), u1_struct_0(C)),v1_group_6(A, B, C).
v2_pralg_1(A) :- true,v1_relat_1(A),v1_funct_1(A),v1_group_7(A).
v1_finseq_1(A) :- ~ (v2_struct_0(B)) ,l3_algstr_0(B),m1_subset_1(A, k4_card_3(k12_pralg_1(k1_tarski(1), k9_finseq_1(B)))),true.
v1_finseq_1(A) :- ~ (v2_struct_0(B)) ,l3_algstr_0(B),m1_subset_1(A, u1_struct_0(k2_group_7(k1_tarski(1), k9_finseq_1(B)))),true.
v1_finseq_1(A) :- ~ (v2_struct_0(B)) ,l3_algstr_0(B), ~ (v2_struct_0(C)) ,l3_algstr_0(C),m1_subset_1(A, k4_card_3(k12_pralg_1(k2_tarski(1, 2), k10_finseq_1(B, C)))),true.
v1_finseq_1(A) :- ~ (v2_struct_0(B)) ,l3_algstr_0(B), ~ (v2_struct_0(C)) ,l3_algstr_0(C),m1_subset_1(A, u1_struct_0(k2_group_7(k2_tarski(1, 2), k10_finseq_1(B, C)))),true.
v1_finseq_1(A) :- ~ (v2_struct_0(B)) ,l3_algstr_0(B), ~ (v2_struct_0(C)) ,l3_algstr_0(C), ~ (v2_struct_0(D)) ,l3_algstr_0(D),m1_subset_1(A, k4_card_3(k12_pralg_1(k1_enumset1(1, 2, 3), k11_finseq_1(B, C, D)))),true.
v1_finseq_1(A) :- ~ (v2_struct_0(B)) ,l3_algstr_0(B), ~ (v2_struct_0(C)) ,l3_algstr_0(C), ~ (v2_struct_0(D)) ,l3_algstr_0(D),m1_subset_1(A, u1_struct_0(k2_group_7(k1_enumset1(1, 2, 3), k11_finseq_1(B, C, D)))),true.
v1_groupp_1(A, B, C) :- v7_ordinal1(B),v1_int_2(B), ~ (v2_struct_0(C)) ,v8_struct_0(C),v2_group_1(C),v3_group_1(C),v2_group_10(C, B),l3_algstr_0(C),m1_subset_1(A, u1_struct_0(C)),true.
v2_group_10(A, B) :- v7_ordinal1(B),v1_int_2(B), ~ (v2_struct_0(C)) ,v8_struct_0(C),v2_group_1(C),v3_group_1(C),v2_group_10(C, B),l3_algstr_0(C),m1_group_2(A, C),true.
v2_group_10(A, B) :- v7_ordinal1(B),l3_algstr_0(A), ~ (v2_struct_0(A)) ,v2_group_1(A),v3_group_1(A),v3_groupp_1(A, B).
v2_groupp_1(A, B) :- v7_ordinal1(B),l3_algstr_0(A), ~ (v2_struct_0(A)) ,v2_group_1(A),v3_group_1(A),v3_groupp_1(A, B).
v3_groupp_1(A, B) :- v7_ordinal1(B),l3_algstr_0(A), ~ (v2_struct_0(A)) ,v2_group_1(A),v3_group_1(A),v2_group_10(A, B),v2_groupp_1(A, B).
v2_groupp_1(A, B) :- v7_ordinal1(B),v1_int_2(B), ~ (v2_struct_0(C)) ,v8_struct_0(C),v2_group_1(C),v3_group_1(C),v2_groupp_1(C, B),l3_algstr_0(C),m1_group_2(A, C),true.
v3_groupp_1(A, B) :- v7_ordinal1(B),v1_int_2(B),l3_algstr_0(A), ~ (v2_struct_0(A)) ,v8_struct_0(A),v2_group_1(A),v3_group_1(A),v5_group_1(A),v2_group_10(A, B).
v1_hahnban(A, B) :- ~ (v2_struct_0(B)) ,v13_algstr_0(B),v2_rlvect_1(B),v3_rlvect_1(B),v4_rlvect_1(B),v5_rlvect_1(B),v6_rlvect_1(B),v7_rlvect_1(B),v8_rlvect_1(B),l1_rlvect_1(B),m1_subset_1(A, k1_zfmisc_1(k2_zfmisc_1(u1_struct_0(B), k1_numbers))),v1_funct_1(A),v1_funct_2(A, u1_struct_0(B), k1_numbers),v2_hahnban(A, B).
v4_hahnban(A, B) :- ~ (v2_struct_0(B)) ,v13_algstr_0(B),v2_rlvect_1(B),v3_rlvect_1(B),v4_rlvect_1(B),v5_rlvect_1(B),v6_rlvect_1(B),v7_rlvect_1(B),v8_rlvect_1(B),l1_rlvect_1(B),m1_subset_1(A, k1_zfmisc_1(k2_zfmisc_1(u1_struct_0(B), k1_numbers))),v1_funct_1(A),v1_funct_2(A, u1_struct_0(B), k1_numbers),v3_hahnban(A, B).
v4_hahnban(A, B) :- ~ (v2_struct_0(B)) ,v13_algstr_0(B),v2_rlvect_1(B),v3_rlvect_1(B),v4_rlvect_1(B),v5_rlvect_1(B),v6_rlvect_1(B),v7_rlvect_1(B),v8_rlvect_1(B),l1_rlvect_1(B),m1_subset_1(A, k1_zfmisc_1(k2_zfmisc_1(u1_struct_0(B), k1_numbers))),v1_funct_1(A),v1_funct_2(A, u1_struct_0(B), k1_numbers),v5_hahnban(A, B).
v7_hahnban(A, B) :- ~ (v2_struct_0(B)) ,v13_algstr_0(B),v2_rlvect_1(B),v3_rlvect_1(B),v4_rlvect_1(B),v5_rlvect_1(B),v6_rlvect_1(B),v7_rlvect_1(B),v8_rlvect_1(B),l1_rlvect_1(B),m1_subset_1(A, k1_zfmisc_1(k2_zfmisc_1(u1_struct_0(B), k1_numbers))),v1_funct_1(A),v1_funct_2(A, u1_struct_0(B), k1_numbers),v5_hahnban(A, B).
v5_hahnban(A, B) :- ~ (v2_struct_0(B)) ,v13_algstr_0(B),v2_rlvect_1(B),v3_rlvect_1(B),v4_rlvect_1(B),v5_rlvect_1(B),v6_rlvect_1(B),v7_rlvect_1(B),v8_rlvect_1(B),l1_rlvect_1(B),m1_subset_1(A, k1_zfmisc_1(k2_zfmisc_1(u1_struct_0(B), k1_numbers))),v1_funct_1(A),v1_funct_2(A, u1_struct_0(B), k1_numbers),v6_hahnban(A, B).
v5_hahnban(A, B) :- ~ (v2_struct_0(B)) ,v13_algstr_0(B),v2_rlvect_1(B),v3_rlvect_1(B),v4_rlvect_1(B),v5_rlvect_1(B),v6_rlvect_1(B),v7_rlvect_1(B),v8_rlvect_1(B),l1_rlvect_1(B),m1_subset_1(A, k1_zfmisc_1(k2_zfmisc_1(u1_struct_0(B), k1_numbers))),v1_funct_1(A),v1_funct_2(A, u1_struct_0(B), k1_numbers),v4_hahnban(A, B),v7_hahnban(A, B).
v2_hahnban1(A, C, B) :- ~ (v2_struct_0(C)) ,v13_algstr_0(C),v2_rlvect_1(C),v3_rlvect_1(C),v4_rlvect_1(C),v3_group_1(C),v4_vectsp_1(C),v5_vectsp_1(C),l6_algstr_0(C), ~ (v2_struct_0(B)) ,v13_algstr_0(B),v2_rlvect_1(B),v3_rlvect_1(B),v4_rlvect_1(B),v8_vectsp_1(B, C),v9_vectsp_1(B, C),v10_vectsp_1(B, C),v11_vectsp_1(B, C),l1_vectsp_1(B, C),m1_subset_1(A, k1_zfmisc_1(k2_zfmisc_1(u1_struct_0(B), u1_struct_0(C)))),v1_funct_1(A),v1_funct_2(A, u1_struct_0(B), u1_struct_0(C)),v1_hahnban1(A, C, B).
v3_hahnban1(A, C, B) :- l1_struct_0(C), ~ (v2_struct_0(B)) ,l1_vectsp_1(B, C),m1_subset_1(A, k1_zfmisc_1(k2_zfmisc_1(u1_struct_0(B), k1_numbers))),v1_funct_1(A),v1_funct_2(A, u1_struct_0(B), k1_numbers),v4_hahnban1(A, C, B).
v7_hahnban1(A, k1_complfld, B) :- ~ (v2_struct_0(B)) ,v13_algstr_0(B),v2_rlvect_1(B),v3_rlvect_1(B),v4_rlvect_1(B),v8_vectsp_1(B, k1_complfld),v9_vectsp_1(B, k1_complfld),v10_vectsp_1(B, k1_complfld),v11_vectsp_1(B, k1_complfld),l1_vectsp_1(B, k1_complfld),m1_subset_1(A, k1_zfmisc_1(k2_zfmisc_1(u1_struct_0(B), k1_numbers))),v1_funct_1(A),v1_funct_2(A, u1_struct_0(B), k1_numbers),v5_hahnban1(A, B).
v2_relat_1(A) :- v1_finset_1(B),m1_finseq_1(A, k1_zfmisc_1(B)), ~ (v1_xboole_0(A)) ,v1_hallmar1(A, B).
~ (v1_xboole_0(A)) :- ~ (v1_xboole_0(B)) ,v1_finset_1(B), ~ (v1_xboole_0(C)) ,m1_finseq_1(C, k1_zfmisc_1(B)),m1_subset_1(D, k5_numbers),m3_hallmar1(A, B, C, D),true.
~ (v1_xboole_0(A)) :- ~ (v1_xboole_0(B)) ,v1_finset_1(B), ~ (v1_xboole_0(C)) ,m1_finseq_1(C, k1_zfmisc_1(B)),m4_hallmar1(A, B, C),true.
~ (v1_xboole_0(A)) :- v1_relat_1(B),v4_relat_1(B, k5_numbers),v1_funct_1(B),v1_finset_1(B),v1_glib_000(B),m3_glib_001(A, B),true.
v5_glib_001(A, B) :- v1_relat_1(B),v4_relat_1(B, k5_numbers),v1_funct_1(B),v1_finset_1(B),v1_glib_000(B),v3_glib_002(B),m3_glib_001(A, B),v4_glib_001(A, B).
~ (v1_glib_001(A, B)) :- v1_relat_1(B),v4_relat_1(B, k5_numbers),v1_funct_1(B),v1_finset_1(B),v1_glib_000(B),v3_glib_002(B),m3_glib_001(A, B), ~ (v3_glib_001(A, B)) ,v5_glib_001(A, B).
v2_hahnban1(A, k1_complfld, B) :- ~ (v2_struct_0(B)) ,v13_algstr_0(B),v3_rlvect_1(B),v4_rlvect_1(B),v8_vectsp_1(B, k1_complfld),v9_vectsp_1(B, k1_complfld),v10_vectsp_1(B, k1_complfld),v11_vectsp_1(B, k1_complfld),l1_vectsp_1(B, k1_complfld),m1_subset_1(A, k1_zfmisc_1(k2_zfmisc_1(u1_struct_0(B), u1_struct_0(k1_complfld)))),v1_funct_1(A),v1_funct_2(A, u1_struct_0(B), u1_struct_0(k1_complfld)),v1_hermitan(A, B).
v4_hermitan(A, B) :- ~ (v2_struct_0(B)) ,l1_vectsp_1(B, k1_complfld),m1_subset_1(A, k1_zfmisc_1(k2_zfmisc_1(k2_zfmisc_1(u1_struct_0(B), u1_struct_0(B)), u1_struct_0(k1_complfld)))),v1_funct_1(A),v1_funct_2(A, k2_zfmisc_1(u1_struct_0(B), u1_struct_0(B)), u1_struct_0(k1_complfld)),v3_hermitan(A, B).
v2_bilinear(A, k1_complfld, B, B) :- ~ (v2_struct_0(B)) ,l1_vectsp_1(B, k1_complfld),m1_subset_1(A, k1_zfmisc_1(k2_zfmisc_1(k2_zfmisc_1(u1_struct_0(B), u1_struct_0(B)), u1_struct_0(k1_complfld)))),v1_funct_1(A),v1_funct_2(A, k2_zfmisc_1(u1_struct_0(B), u1_struct_0(B)), u1_struct_0(k1_complfld)),v1_bilinear(A, k1_complfld, B, B),v3_hermitan(A, B).
v1_bilinear(A, k1_complfld, B, B) :- ~ (v2_struct_0(B)) ,l1_vectsp_1(B, k1_complfld),m1_subset_1(A, k1_zfmisc_1(k2_zfmisc_1(k2_zfmisc_1(u1_struct_0(B), u1_struct_0(B)), u1_struct_0(k1_complfld)))),v1_funct_1(A),v1_funct_2(A, k2_zfmisc_1(u1_struct_0(B), u1_struct_0(B)), u1_struct_0(k1_complfld)),v2_bilinear(A, k1_complfld, B, B),v3_hermitan(A, B).
v2_hermitan(A, B, B) :- ~ (v2_struct_0(B)) ,l1_vectsp_1(B, k1_complfld),m1_subset_1(A, k1_zfmisc_1(k2_zfmisc_1(k2_zfmisc_1(u1_struct_0(B), u1_struct_0(B)), u1_struct_0(k1_complfld)))),v1_funct_1(A),v1_funct_2(A, k2_zfmisc_1(u1_struct_0(B), u1_struct_0(B)), u1_struct_0(k1_complfld)),v4_bilinear(A, k1_complfld, B, B),v3_hermitan(A, B).
v4_bilinear(A, k1_complfld, B, B) :- ~ (v2_struct_0(B)) ,l1_vectsp_1(B, k1_complfld),m1_subset_1(A, k1_zfmisc_1(k2_zfmisc_1(k2_zfmisc_1(u1_struct_0(B), u1_struct_0(B)), u1_struct_0(k1_complfld)))),v1_funct_1(A),v1_funct_2(A, k2_zfmisc_1(u1_struct_0(B), u1_struct_0(B)), u1_struct_0(k1_complfld)),v2_hermitan(A, B, B),v3_hermitan(A, B).
v5_hermitan(A, B) :- ~ (v2_struct_0(B)) ,v4_rlvect_1(B),l1_vectsp_1(B, k1_complfld),m1_subset_1(A, k1_zfmisc_1(k2_zfmisc_1(k2_zfmisc_1(u1_struct_0(B), u1_struct_0(B)), u1_struct_0(k1_complfld)))),v1_funct_1(A),v1_funct_2(A, k2_zfmisc_1(u1_struct_0(B), u1_struct_0(B)), u1_struct_0(k1_complfld)),v2_bilinear(A, k1_complfld, B, B),v6_hermitan(A, B).
v5_hermitan(A, B) :- ~ (v2_struct_0(B)) ,v4_rlvect_1(B),l1_vectsp_1(B, k1_complfld),m1_subset_1(A, k1_zfmisc_1(k2_zfmisc_1(k2_zfmisc_1(u1_struct_0(B), u1_struct_0(B)), u1_struct_0(k1_complfld)))),v1_funct_1(A),v1_funct_2(A, k2_zfmisc_1(u1_struct_0(B), u1_struct_0(B)), u1_struct_0(k1_complfld)),v1_bilinear(A, k1_complfld, B, B),v6_hermitan(A, B).
v5_anproj_2(A) :- l1_collsp(A), ~ (v2_struct_0(A)) ,v2_collsp(A),v3_collsp(A),v4_collsp(A),v2_anproj_2(A),v3_anproj_2(A),v6_anproj_2(A).
~ (v1_xboole_0(A)) :- true,v5_hilbert1(A).
v1_hilbert1(A) :- true,v5_hilbert1(A).
v2_hilbert1(A) :- true,v5_hilbert1(A).
v3_hilbert1(A) :- true,v5_hilbert1(A).
v4_hilbert1(A) :- true,v5_hilbert1(A).
v5_hilbert1(A) :- m1_subset_1(A, k1_zfmisc_1(k13_finseq_1(k5_numbers))),v1_hilbert1(A),v2_hilbert1(A),v3_hilbert1(A),v4_hilbert1(A).
v1_finseq_1(A) :- m1_subset_1(A, k1_hilbert1),true.
v1_funcop_1(A) :- v1_relat_1(B),v2_relat_1(B),v4_relat_1(B, k5_numbers),v1_funct_1(B),v1_partfun1(B, k5_numbers),m1_subset_1(C, k1_hilbert1),m1_subset_1(D, k1_hilbert1),m1_subset_1(E, k1_hilbert1),m1_subset_1(A, k3_hilbert3(B, k3_hilbert1(C, k3_hilbert1(D, E)))),true.
v2_hilbert3(A) :- m1_subset_1(A, k1_hilbert1),v1_hilbert3(A).
v1_finseq_1(A) :- m1_subset_1(A, k14_idea_1),true.
v3_ideal_1(A, B) :- ~ (v2_struct_0(B)) ,v5_group_1(B),l3_algstr_0(B),m1_subset_1(A, k1_zfmisc_1(u1_struct_0(B))), ~ (v1_xboole_0(A)) ,v2_ideal_1(A, B).
v2_ideal_1(A, B) :- ~ (v2_struct_0(B)) ,v5_group_1(B),l3_algstr_0(B),m1_subset_1(A, k1_zfmisc_1(u1_struct_0(B))), ~ (v1_xboole_0(A)) ,v3_ideal_1(A, B).
v5_incsp_1(A) :- l2_incsp_1(A),v15_incsp_1(A).
v6_incsp_1(A) :- l2_incsp_1(A),v15_incsp_1(A).
v7_incsp_1(A) :- l2_incsp_1(A),v15_incsp_1(A).
v8_incsp_1(A) :- l2_incsp_1(A),v15_incsp_1(A).
v9_incsp_1(A) :- l2_incsp_1(A),v15_incsp_1(A).
v10_incsp_1(A) :- l2_incsp_1(A),v15_incsp_1(A).
v11_incsp_1(A) :- l2_incsp_1(A),v15_incsp_1(A).
v12_incsp_1(A) :- l2_incsp_1(A),v15_incsp_1(A).
v13_incsp_1(A) :- l2_incsp_1(A),v15_incsp_1(A).
v14_incsp_1(A) :- l2_incsp_1(A),v15_incsp_1(A).
~ (v1_xboole_0(A)) :- ~ (v1_xboole_0(B)) ,v1_relat_1(A),v4_relat_1(A, B),v1_funct_1(A),v1_partfun1(A, B).
v6_trees_3(A) :- ~ (v2_struct_0(B)) , ~ (v11_struct_0(B)) ,l1_msualg_1(B),v1_relat_1(C),v2_relat_1(C),v4_relat_1(C, u1_struct_0(B)),v1_funct_1(C),v1_partfun1(C, u1_struct_0(B)),m1_subset_1(D, u4_struct_0(B)),m1_subset_1(A, k3_msualg_1(B, D, k11_msafree(B, C))),true.
v1_instalg1(A) :- l1_msualg_1(A), ~ (v2_struct_0(A)) .
v1_instalg1(A) :- l1_msualg_1(A),v11_struct_0(A).
v11_struct_0(A) :- l1_msualg_1(A),v2_struct_0(A),v1_instalg1(A).
~ (v2_struct_0(A)) :- l1_msualg_1(A), ~ (v11_struct_0(A)) ,v1_instalg1(A).
v1_instalg1(A) :- v1_instalg1(B),l1_msualg_1(B),m1_instalg1(A, B),true.
v1_int_1(A) :- m1_subset_1(A, k4_numbers),true.
v1_int_1(A) :- true,v7_ordinal1(A).
v1_xreal_0(A) :- true,v1_int_1(A).
v3_gcd_1(A) :- l6_algstr_0(A), ~ (v2_struct_0(A)) , ~ (v6_struct_0(A)) ,v13_algstr_0(A),v3_group_1(A),v5_group_1(A),v2_rlvect_1(A),v3_rlvect_1(A),v4_rlvect_1(A),v1_vectsp_1(A),v4_vectsp_1(A),v1_vectsp_2(A),v1_int_3(A).
v1_int_3(A) :- l6_algstr_0(A), ~ (v2_struct_0(A)) ,v33_algstr_0(A),v3_group_1(A),v5_group_1(A),v4_rlvect_1(A),v4_vectsp_1(A).
~ (v1_xboole_0(A)) :- true,v7_ordinal1(A),v1_int_2(A).
v2_relat_1(A) :- true,v1_relat_1(A),v1_funct_1(A), ~ (v1_xboole_0(A)) ,v1_finseq_1(A),v5_valued_0(A),v1_partfun3(A),v1_int_6(A).
~ (v1_xboole_0(A)) :- true,v1_relat_1(A), ~ (v2_relat_1(A)) ,v1_funct_1(A),v1_finseq_1(A),v5_valued_0(A).
v5_valued_0(A) :- v1_relat_1(B),v1_funct_1(B), ~ (v1_xboole_0(B)) ,v1_finseq_1(B),v5_valued_0(B),v1_partfun3(B),v1_int_6(B),m1_int_6(A, B),true.
v1_rcomp_1(A) :- m1_subset_1(A, k1_zfmisc_1(k1_numbers)),v2_measure5(A).
v5_xxreal_2(A) :- m1_subset_1(A, k1_zfmisc_1(k1_numbers)), ~ (v1_xboole_0(A)) ,v2_measure5(A).
v1_relat_1(A) :- ~ (v1_xboole_0(B)) ,v1_rcomp_1(B),m1_subset_1(B, k1_zfmisc_1(k1_numbers)),m1_subset_1(A, k1_integra1(B)),true.
v1_funct_1(A) :- ~ (v1_xboole_0(B)) ,v1_rcomp_1(B),m1_subset_1(B, k1_zfmisc_1(k1_numbers)),m1_subset_1(A, k1_integra1(B)),true.
v1_finseq_1(A) :- ~ (v1_xboole_0(B)) ,v1_rcomp_1(B),m1_subset_1(B, k1_zfmisc_1(k1_numbers)),m1_subset_1(A, k1_integra1(B)),true.
v3_valued_0(A) :- ~ (v1_xboole_0(B)) ,v1_rcomp_1(B),m1_subset_1(B, k1_zfmisc_1(k1_numbers)),m1_subset_1(A, k1_integra1(B)),true.
~ (v1_xboole_0(A)) :- true,v7_intpro_1(A).
v1_intpro_1(A) :- true,v7_intpro_1(A).
v2_intpro_1(A) :- true,v7_intpro_1(A).
v3_intpro_1(A) :- true,v7_intpro_1(A).
v4_intpro_1(A) :- true,v7_intpro_1(A).
v5_intpro_1(A) :- true,v7_intpro_1(A).
v6_intpro_1(A) :- true,v7_intpro_1(A).
v7_intpro_1(A) :- m1_subset_1(A, k1_zfmisc_1(k13_finseq_1(k5_numbers))),v1_intpro_1(A),v2_intpro_1(A),v3_intpro_1(A),v4_intpro_1(A),v5_intpro_1(A),v6_intpro_1(A).
v1_finseq_1(A) :- m1_subset_1(A, k1_intpro_1),true.
v1_isomichi(A, B) :- v2_pre_topc(B),l1_pre_topc(B),m1_subset_1(A, k1_zfmisc_1(u1_struct_0(B))),v4_pre_topc(A, B).
v1_isomichi(A, B) :- v2_pre_topc(B),l1_pre_topc(B),m1_subset_1(A, k1_zfmisc_1(u1_struct_0(B))),v4_tops_1(A, B).
v2_isomichi(A, B) :- v2_pre_topc(B),l1_pre_topc(B),m1_subset_1(A, k1_zfmisc_1(u1_struct_0(B))),v4_tops_1(A, B).
v4_tops_1(A, B) :- v2_pre_topc(B),l1_pre_topc(B),m1_subset_1(A, k1_zfmisc_1(u1_struct_0(B))),v1_isomichi(A, B),v2_isomichi(A, B).
v1_decomp_1(A, B) :- v2_pre_topc(B),l1_pre_topc(B),m1_subset_1(A, k1_zfmisc_1(u1_struct_0(B))),v2_isomichi(A, B).
v2_isomichi(A, B) :- v2_pre_topc(B),l1_pre_topc(B),m1_subset_1(A, k1_zfmisc_1(u1_struct_0(B))),v1_decomp_1(A, B).
v5_tops_1(A, B) :- v2_pre_topc(B),l1_pre_topc(B),m1_subset_1(A, k1_zfmisc_1(u1_struct_0(B))),v1_xboole_0(A).
v6_tops_1(A, B) :- v2_pre_topc(B),l1_pre_topc(B),m1_subset_1(A, k1_zfmisc_1(u1_struct_0(B))),v1_xboole_0(A).
v3_pre_topc(A, B) :- v2_pre_topc(B),l1_pre_topc(B),m1_subset_1(A, k1_zfmisc_1(u1_struct_0(B))),v6_tops_1(A, B).
v4_pre_topc(A, B) :- v2_pre_topc(B),l1_pre_topc(B),m1_subset_1(A, k1_zfmisc_1(u1_struct_0(B))),v5_tops_1(A, B).
v3_pre_topc(A, B) :- v2_pre_topc(B),l1_pre_topc(B),m1_subset_1(A, k1_zfmisc_1(u1_struct_0(B))),v6_tops_1(A, B).
v4_tops_1(A, B) :- v2_pre_topc(B),l1_pre_topc(B),m1_subset_1(A, k1_zfmisc_1(u1_struct_0(B))),v6_tops_1(A, B).
v6_tops_1(A, B) :- v2_pre_topc(B),l1_pre_topc(B),m1_subset_1(A, k1_zfmisc_1(u1_struct_0(B))),v3_pre_topc(A, B),v4_tops_1(A, B).
v4_pre_topc(A, B) :- v2_pre_topc(B),l1_pre_topc(B),m1_subset_1(A, k1_zfmisc_1(u1_struct_0(B))),v5_tops_1(A, B).
v4_tops_1(A, B) :- v2_pre_topc(B),l1_pre_topc(B),m1_subset_1(A, k1_zfmisc_1(u1_struct_0(B))),v5_tops_1(A, B).
v5_tops_1(A, B) :- v2_pre_topc(B),l1_pre_topc(B),m1_subset_1(A, k1_zfmisc_1(u1_struct_0(B))),v4_pre_topc(A, B),v4_tops_1(A, B).
~ (v4_isomichi(A, B)) :- v2_pre_topc(B),l1_pre_topc(B),m1_subset_1(A, k1_zfmisc_1(u1_struct_0(B))),v3_isomichi(A, B).
~ (v5_isomichi(A, B)) :- v2_pre_topc(B),l1_pre_topc(B),m1_subset_1(A, k1_zfmisc_1(u1_struct_0(B))),v3_isomichi(A, B).
~ (v3_isomichi(A, B)) :- v2_pre_topc(B),l1_pre_topc(B),m1_subset_1(A, k1_zfmisc_1(u1_struct_0(B))),v4_isomichi(A, B).
~ (v5_isomichi(A, B)) :- v2_pre_topc(B),l1_pre_topc(B),m1_subset_1(A, k1_zfmisc_1(u1_struct_0(B))),v4_isomichi(A, B).
~ (v3_isomichi(A, B)) :- v2_pre_topc(B),l1_pre_topc(B),m1_subset_1(A, k1_zfmisc_1(u1_struct_0(B))),v5_isomichi(A, B).
~ (v4_isomichi(A, B)) :- v2_pre_topc(B),l1_pre_topc(B),m1_subset_1(A, k1_zfmisc_1(u1_struct_0(B))),v5_isomichi(A, B).
v3_isomichi(A, B) :- v2_pre_topc(B),l1_pre_topc(B),m1_subset_1(A, k1_zfmisc_1(u1_struct_0(B))),v1_isomichi(A, B).
v3_isomichi(A, B) :- v2_pre_topc(B),l1_pre_topc(B),m1_subset_1(A, k1_zfmisc_1(u1_struct_0(B))),v2_isomichi(A, B).
v4_isomichi(A, B) :- ~ (v2_struct_0(B)) ,v2_pre_topc(B),v2_tdlat_3(B),l1_pre_topc(B),m1_subset_1(A, k1_zfmisc_1(u1_struct_0(B))), ~ (v1_xboole_0(A)) ,v1_subset_1(A, u1_struct_0(B)).
v1_jordan21(A) :- m1_subset_1(A, k1_zfmisc_1(u1_struct_0(k15_euclid(2)))), ~ (v1_xboole_0(A)) ,v2_compts_1(A, k15_euclid(2)),v2_sppol_1(A).
v1_jordan2c(A, B) :- m1_subset_1(B, k5_numbers),m1_subset_1(A, k1_zfmisc_1(u1_struct_0(k15_euclid(B)))),v1_xboole_0(A).
~ (v1_xboole_0(A)) :- m1_subset_1(B, k5_numbers),m1_subset_1(A, k1_zfmisc_1(u1_struct_0(k15_euclid(B)))), ~ (v1_jordan2c(A, B)) .
v1_subset_1(A, u1_struct_0(k15_euclid(B))) :- ~ (v1_xboole_0(B)) ,m1_subset_1(B, k5_numbers),m1_subset_1(A, k1_zfmisc_1(u1_struct_0(k15_euclid(B)))),v1_jordan2c(A, B).
v8_pre_topc(A) :- ~ (v2_struct_0(B)) ,v2_pre_topc(B),v8_pre_topc(B),l1_pre_topc(B),m1_pre_topc(A, B), ~ (v2_struct_0(A)) .
v2_connsp_1(A, k15_euclid(B)) :- m1_subset_1(B, k5_numbers),m1_subset_1(A, k1_zfmisc_1(u1_struct_0(k15_euclid(B)))),v1_convex1(A, k15_euclid(B)).
v1_goboard5(A) :- m1_finseq_1(A, u1_struct_0(k15_euclid(2))),v3_topreal1(A).
~ (v1_xboole_0(A)) :- m1_finseq_1(A, k3_finseq_2(u1_struct_0(k15_euclid(2)))), ~ (v3_relat_1(A)) ,v1_matrix_1(A),v2_goboard1(A),v3_goboard1(A),v4_goboard1(A),v5_goboard1(A).
v2_relat_1(A) :- m1_finseq_1(A, k3_finseq_2(u1_struct_0(k15_euclid(2)))), ~ (v3_relat_1(A)) ,v1_matrix_1(A),v2_goboard1(A),v3_goboard1(A),v4_goboard1(A),v5_goboard1(A).
~ (v1_xboole_0(A)) :- m1_subset_1(A, k1_zfmisc_1(u1_struct_0(k15_euclid(2)))),v1_jordan21(A).
v1_jordan21(A) :- m1_subset_1(A, k1_zfmisc_1(u1_struct_0(k15_euclid(2)))),v1_topreal2(A).
v1_jordan23(A) :- true,v1_relat_1(A),v1_funct_1(A),v2_funct_1(A),v1_finseq_1(A).
v3_jordan23(A) :- true,v1_relat_1(A),v1_funct_1(A),v1_finseq_1(A),v1_jordan23(A).
v2_jordan23(A) :- true,v1_relat_1(A),v1_funct_1(A),v1_xboole_0(A),v1_finseq_1(A).
v2_jordan23(A) :- true,v1_relat_1(A),v1_funct_1(A),v2_funct_1(A),v1_finseq_1(A).
v5_pre_topc(A, k3_pcomps_1(B), k3_pcomps_1(B)) :- ~ (v2_struct_0(B)) ,v6_metric_1(B),v7_metric_1(B),v8_metric_1(B),v9_metric_1(B),l1_metric_1(B),m1_subset_1(A, k1_zfmisc_1(k2_zfmisc_1(u1_struct_0(k3_pcomps_1(B)), u1_struct_0(k3_pcomps_1(B))))),v1_funct_1(A),v1_funct_2(A, u1_struct_0(k3_pcomps_1(B)), u1_struct_0(k3_pcomps_1(B))),v1_jordan24(A, B).
v3_tops_2(A, k3_pcomps_1(B), k3_pcomps_1(B)) :- ~ (v2_struct_0(B)) ,v6_metric_1(B),v7_metric_1(B),v8_metric_1(B),v9_metric_1(B),l1_metric_1(B),m1_subset_1(A, k1_zfmisc_1(k2_zfmisc_1(u1_struct_0(k3_pcomps_1(B)), u1_struct_0(k3_pcomps_1(B))))),v1_funct_1(A),v1_funct_2(A, u1_struct_0(k3_pcomps_1(B)), u1_struct_0(k3_pcomps_1(B))),v2_funct_2(A, u1_struct_0(k3_pcomps_1(B))),v1_jordan24(A, B).
v5_relat_1(A, k1_numbers) :- v7_ordinal1(B),m1_subset_1(A, u1_struct_0(k15_euclid(B))),true.
v1_jordan2c(A, B) :- m1_subset_1(B, k5_numbers),m1_subset_1(A, k1_zfmisc_1(u1_struct_0(k15_euclid(B)))),v2_compts_1(A, k15_euclid(B)).
~ (v1_zfmisc_1(A)) :- v1_topreal2(B),m1_subset_1(B, k1_zfmisc_1(u1_struct_0(k15_euclid(2)))),m1_jordan_a(A, B),true.
v15_lattices(A) :- l3_lattices(A), ~ (v2_struct_0(A)) ,v10_lattices(A),v4_lattice3(A).
~ (v1_xboole_0(A)) :- m1_subset_1(A, k1_zfmisc_1(k2_zfmisc_1(k5_numbers, k9_setfam_1(B)))),v1_funct_1(A),v1_funct_2(A, k5_numbers, k9_setfam_1(B)).
v2_prob_1(A) :- m1_subset_1(A, k1_zfmisc_1(k2_zfmisc_1(k5_numbers, k9_setfam_1(B)))),v1_funct_1(A),v3_funct_1(A),v1_funct_2(A, k5_numbers, k9_setfam_1(B)).
v3_prob_1(A) :- m1_subset_1(A, k1_zfmisc_1(k2_zfmisc_1(k5_numbers, k9_setfam_1(B)))),v1_funct_1(A),v3_funct_1(A),v1_funct_2(A, k5_numbers, k9_setfam_1(B)).
v3_kurato_0(A, B) :- m1_subset_1(A, k1_zfmisc_1(k2_zfmisc_1(k5_numbers, k9_setfam_1(B)))),v1_funct_1(A),v3_funct_1(A),v1_funct_2(A, k5_numbers, k9_setfam_1(B)).
v13_lattices(A) :- l3_lattices(A), ~ (v2_struct_0(A)) ,v10_lattices(A),v1_lattice2(A).
v3_filter_0(A) :- l3_lattices(A), ~ (v2_struct_0(A)) ,v10_lattices(A),v1_lattice2(A).
v1_lattice2(A) :- l3_lattices(A), ~ (v2_struct_0(A)) ,v10_lattices(A),v13_lattices(A),v3_filter_0(A).
v13_lattices(A) :- l3_lattices(A), ~ (v2_struct_0(A)) ,v8_struct_0(A),v10_lattices(A).
v14_lattices(A) :- l3_lattices(A), ~ (v2_struct_0(A)) ,v8_struct_0(A),v10_lattices(A).
v15_lattices(A) :- l3_lattices(A), ~ (v2_struct_0(A)) ,v8_struct_0(A),v10_lattices(A).
v1_lattice2(A) :- l3_lattices(A), ~ (v2_struct_0(A)) ,v8_struct_0(A),v10_lattices(A),v11_lattices(A).
~ (v2_struct_0(A)) :- l1_orders_2(A),v1_lattice3(A).
~ (v2_struct_0(A)) :- l1_orders_2(A),v2_lattice3(A).
v4_lattice3(A) :- l3_lattices(A), ~ (v2_struct_0(A)) ,v8_struct_0(A),v10_lattices(A).
v1_lattice6(A) :- l3_lattices(A), ~ (v2_struct_0(A)) ,v8_struct_0(A),v10_lattices(A).
v2_lattice6(A) :- l3_lattices(A), ~ (v2_struct_0(A)) ,v8_struct_0(A),v10_lattices(A).
v4_lattices(A) :- l3_lattices(A), ~ (v2_struct_0(A)) ,v10_lattices(A).
v5_lattices(A) :- l3_lattices(A), ~ (v2_struct_0(A)) ,v10_lattices(A).
v6_lattices(A) :- l3_lattices(A), ~ (v2_struct_0(A)) ,v10_lattices(A).
v7_lattices(A) :- l3_lattices(A), ~ (v2_struct_0(A)) ,v10_lattices(A).
v8_lattices(A) :- l3_lattices(A), ~ (v2_struct_0(A)) ,v10_lattices(A).
v9_lattices(A) :- l3_lattices(A), ~ (v2_struct_0(A)) ,v10_lattices(A).
v10_lattices(A) :- l3_lattices(A), ~ (v2_struct_0(A)) ,v4_lattices(A),v5_lattices(A),v6_lattices(A),v7_lattices(A),v8_lattices(A),v9_lattices(A).
v15_lattices(A) :- l3_lattices(A), ~ (v2_struct_0(A)) ,v13_lattices(A),v14_lattices(A).
v13_lattices(A) :- l3_lattices(A), ~ (v2_struct_0(A)) ,v15_lattices(A).
v14_lattices(A) :- l3_lattices(A), ~ (v2_struct_0(A)) ,v15_lattices(A).
v11_lattices(A) :- l3_lattices(A), ~ (v2_struct_0(A)) ,v17_lattices(A).
v15_lattices(A) :- l3_lattices(A), ~ (v2_struct_0(A)) ,v17_lattices(A).
v16_lattices(A) :- l3_lattices(A), ~ (v2_struct_0(A)) ,v17_lattices(A).
v17_lattices(A) :- l3_lattices(A), ~ (v2_struct_0(A)) ,v11_lattices(A),v15_lattices(A),v16_lattices(A).
v12_lattices(A) :- l3_lattices(A), ~ (v2_struct_0(A)) ,v10_lattices(A),v11_lattices(A).
v18_lattices(A, B) :- ~ (v2_struct_0(B)) ,v10_lattices(B),l3_lattices(B),m1_subset_1(A, k1_zfmisc_1(u1_struct_0(B))),v1_xboole_0(A).
v19_lattices(A, B) :- ~ (v2_struct_0(B)) ,v10_lattices(B),l3_lattices(B),m1_subset_1(A, k1_zfmisc_1(u1_struct_0(B))),v1_xboole_0(A).
v20_lattices(A, B) :- ~ (v2_struct_0(B)) ,v10_lattices(B),l3_lattices(B),m1_subset_1(A, k1_zfmisc_1(u1_struct_0(B))),v18_lattices(A, B).
v21_lattices(A, B) :- ~ (v2_struct_0(B)) ,v10_lattices(B),l3_lattices(B),m1_subset_1(A, k1_zfmisc_1(u1_struct_0(B))),v19_lattices(A, B).
v1_finset_1(A) :- v1_lexbfs(B),m1_subset_1(A, B),true.
v4_lexbfs(A) :- true,v1_relat_1(A),v4_relat_1(A, k5_numbers),v1_funct_1(A),v1_partfun1(A, k5_numbers),v13_glib_000(A),v3_lexbfs(A).
v13_glib_000(A) :- true,v1_relat_1(A),v4_relat_1(A, k5_numbers),v1_funct_1(A),v1_partfun1(A, k5_numbers),v4_lexbfs(A).
v13_glib_000(A) :- v1_relat_1(B),v4_relat_1(B, k5_numbers),v1_funct_1(B),v1_finset_1(B),v1_glib_000(B),v2_glib_000(B),m1_lexbfs(A, B),v5_lexbfs(A, B).
v3_lexbfs(A) :- v1_relat_1(B),v4_relat_1(B, k5_numbers),v1_funct_1(B),v1_finset_1(B),v1_glib_000(B),v2_glib_000(B),m1_lexbfs(A, B),v5_lexbfs(A, B).
~ (v2_struct_0(A)) :- l1_orders_2(A),v2_lfuzzy_0(A).
v1_lfuzzy_0(A) :- l1_orders_2(A),v2_lfuzzy_0(A).
v1_lfuzzy_0(A) :- l1_orders_2(A),v2_struct_0(A).
v1_xreal_0(A) :- ~ (v2_struct_0(B)) ,v1_lfuzzy_0(B),l1_orders_2(B),m1_subset_1(A, u1_struct_0(B)),true.
v3_orders_2(A) :- l1_orders_2(A),v1_lfuzzy_0(A).
v4_orders_2(A) :- l1_orders_2(A),v1_lfuzzy_0(A).
v5_orders_2(A) :- l1_orders_2(A),v1_lfuzzy_0(A).
v16_waybel_0(A) :- l1_orders_2(A), ~ (v2_struct_0(A)) ,v1_lfuzzy_0(A).
v1_lattice3(A) :- l1_orders_2(A), ~ (v2_struct_0(A)) ,v1_lfuzzy_0(A).
v2_lattice3(A) :- l1_orders_2(A), ~ (v2_struct_0(A)) ,v1_lfuzzy_0(A).
v3_yellow_0(A) :- l1_orders_2(A), ~ (v2_struct_0(A)) ,v2_lfuzzy_0(A).
v3_lattice3(A) :- l1_orders_2(A), ~ (v2_struct_0(A)) ,v2_lfuzzy_0(A).
v2_waybel_1(A) :- l1_orders_2(A), ~ (v2_struct_0(A)) ,v3_orders_2(A),v4_orders_2(A),v5_orders_2(A),v16_waybel_0(A).
v9_waybel_1(A) :- l1_orders_2(A), ~ (v2_struct_0(A)) ,v2_lfuzzy_0(A).
v3_valued_0(A) :- ~ (v1_xboole_0(B)) ,m1_subset_1(A, k1_zfmisc_1(k2_zfmisc_1(B, k1_numbers))),v5_relat_1(A, k1_rcomp_1(k6_numbers, 1)),v1_funct_1(A),v1_funct_2(A, B, k1_numbers).
v1_relat_1(A) :- ~ (v2_struct_0(B)) ,v13_algstr_0(B),v2_rlvect_1(B),v3_rlvect_1(B),v4_rlvect_1(B),v5_rlvect_1(B),v6_rlvect_1(B),v7_rlvect_1(B),v8_rlvect_1(B),v3_normsp_0(B),v4_normsp_0(B),v2_normsp_1(B),l1_normsp_1(B), ~ (v2_struct_0(C)) ,v13_algstr_0(C),v2_rlvect_1(C),v3_rlvect_1(C),v4_rlvect_1(C),v5_rlvect_1(C),v6_rlvect_1(C),v7_rlvect_1(C),v8_rlvect_1(C),v3_normsp_0(C),v4_normsp_0(C),v2_normsp_1(C),l1_normsp_1(C),m1_subset_1(A, u1_struct_0(k11_lopban_1(B, C))),true.
v1_funct_1(A) :- ~ (v2_struct_0(B)) ,v13_algstr_0(B),v2_rlvect_1(B),v3_rlvect_1(B),v4_rlvect_1(B),v5_rlvect_1(B),v6_rlvect_1(B),v7_rlvect_1(B),v8_rlvect_1(B),v3_normsp_0(B),v4_normsp_0(B),v2_normsp_1(B),l1_normsp_1(B), ~ (v2_struct_0(C)) ,v13_algstr_0(C),v2_rlvect_1(C),v3_rlvect_1(C),v4_rlvect_1(C),v5_rlvect_1(C),v6_rlvect_1(C),v7_rlvect_1(C),v8_rlvect_1(C),v3_normsp_0(C),v4_normsp_0(C),v2_normsp_1(C),l1_normsp_1(C),m1_subset_1(A, u1_struct_0(k11_lopban_1(B, C))),true.
v1_relat_1(A) :- ~ (v2_struct_0(B)) ,v13_algstr_0(B),v2_rlvect_1(B),v3_rlvect_1(B),v4_rlvect_1(B),v5_rlvect_1(B),v6_rlvect_1(B),v7_rlvect_1(B),v8_rlvect_1(B),v3_normsp_0(B),v4_normsp_0(B),v2_normsp_1(B),l1_normsp_1(B), ~ (v2_struct_0(C)) ,v13_algstr_0(C),v2_rlvect_1(C),v3_rlvect_1(C),v4_rlvect_1(C),v5_rlvect_1(C),v6_rlvect_1(C),v7_rlvect_1(C),v8_rlvect_1(C),v3_normsp_0(C),v4_normsp_0(C),v2_normsp_1(C),l1_normsp_1(C),m1_subset_1(A, u1_struct_0(k16_lopban_1(B, C))),true.
v1_funct_1(A) :- ~ (v2_struct_0(B)) ,v13_algstr_0(B),v2_rlvect_1(B),v3_rlvect_1(B),v4_rlvect_1(B),v5_rlvect_1(B),v6_rlvect_1(B),v7_rlvect_1(B),v8_rlvect_1(B),v3_normsp_0(B),v4_normsp_0(B),v2_normsp_1(B),l1_normsp_1(B), ~ (v2_struct_0(C)) ,v13_algstr_0(C),v2_rlvect_1(C),v3_rlvect_1(C),v4_rlvect_1(C),v5_rlvect_1(C),v6_rlvect_1(C),v7_rlvect_1(C),v8_rlvect_1(C),v3_normsp_0(C),v4_normsp_0(C),v2_normsp_1(C),l1_normsp_1(C),m1_subset_1(A, u1_struct_0(k16_lopban_1(B, C))),true.
v3_lopban_1(A) :- l1_lopban_2(A), ~ (v2_struct_0(A)) ,v13_algstr_0(A),v2_rlvect_1(A),v3_rlvect_1(A),v4_rlvect_1(A),v5_rlvect_1(A),v6_rlvect_1(A),v7_rlvect_1(A),v8_rlvect_1(A),v2_funcsdom(A),v3_normsp_0(A),v4_normsp_0(A),v2_normsp_1(A),v3_group_1(A),v1_vectsp_1(A),v3_vectsp_1(A),v5_lopban_2(A).
v2_vectsp_1(A) :- l1_lopban_2(A), ~ (v2_struct_0(A)) ,v13_algstr_0(A),v2_rlvect_1(A),v3_rlvect_1(A),v4_rlvect_1(A),v5_rlvect_1(A),v6_rlvect_1(A),v7_rlvect_1(A),v8_rlvect_1(A),v2_funcsdom(A),v3_normsp_0(A),v4_normsp_0(A),v2_normsp_1(A),v3_group_1(A),v1_vectsp_1(A),v3_vectsp_1(A),v5_lopban_2(A).
v6_vectsp_1(A) :- l1_lopban_2(A), ~ (v2_struct_0(A)) ,v13_algstr_0(A),v2_rlvect_1(A),v3_rlvect_1(A),v4_rlvect_1(A),v5_rlvect_1(A),v6_rlvect_1(A),v7_rlvect_1(A),v8_rlvect_1(A),v2_funcsdom(A),v3_normsp_0(A),v4_normsp_0(A),v2_normsp_1(A),v3_group_1(A),v1_vectsp_1(A),v3_vectsp_1(A),v5_lopban_2(A).
v2_lopban_2(A) :- l1_lopban_2(A), ~ (v2_struct_0(A)) ,v13_algstr_0(A),v2_rlvect_1(A),v3_rlvect_1(A),v4_rlvect_1(A),v5_rlvect_1(A),v6_rlvect_1(A),v7_rlvect_1(A),v8_rlvect_1(A),v2_funcsdom(A),v3_normsp_0(A),v4_normsp_0(A),v2_normsp_1(A),v3_group_1(A),v1_vectsp_1(A),v3_vectsp_1(A),v5_lopban_2(A).
v3_lopban_2(A) :- l1_lopban_2(A), ~ (v2_struct_0(A)) ,v13_algstr_0(A),v2_rlvect_1(A),v3_rlvect_1(A),v4_rlvect_1(A),v5_rlvect_1(A),v6_rlvect_1(A),v7_rlvect_1(A),v8_rlvect_1(A),v2_funcsdom(A),v3_normsp_0(A),v4_normsp_0(A),v2_normsp_1(A),v3_group_1(A),v1_vectsp_1(A),v3_vectsp_1(A),v5_lopban_2(A).
v4_lopban_2(A) :- l1_lopban_2(A), ~ (v2_struct_0(A)) ,v13_algstr_0(A),v2_rlvect_1(A),v3_rlvect_1(A),v4_rlvect_1(A),v5_rlvect_1(A),v6_rlvect_1(A),v7_rlvect_1(A),v8_rlvect_1(A),v2_funcsdom(A),v3_normsp_0(A),v4_normsp_0(A),v2_normsp_1(A),v3_group_1(A),v1_vectsp_1(A),v3_vectsp_1(A),v5_lopban_2(A).
v5_lopban_2(A) :- l1_lopban_2(A), ~ (v2_struct_0(A)) ,v13_algstr_0(A),v2_rlvect_1(A),v3_rlvect_1(A),v4_rlvect_1(A),v5_rlvect_1(A),v6_rlvect_1(A),v7_rlvect_1(A),v8_rlvect_1(A),v2_funcsdom(A),v3_normsp_0(A),v4_normsp_0(A),v2_normsp_1(A),v3_lopban_1(A),v3_group_1(A),v1_vectsp_1(A),v2_vectsp_1(A),v3_vectsp_1(A),v6_vectsp_1(A),v2_lopban_2(A),v3_lopban_2(A),v4_lopban_2(A).
v3_normsp_1(A, B) :- ~ (v2_struct_0(B)) ,v13_algstr_0(B),v2_rlvect_1(B),v3_rlvect_1(B),v4_rlvect_1(B),v5_rlvect_1(B),v6_rlvect_1(B),v7_rlvect_1(B),v8_rlvect_1(B),v3_normsp_0(B),v4_normsp_0(B),v2_normsp_1(B),l1_normsp_1(B),m1_subset_1(A, k1_zfmisc_1(k2_zfmisc_1(k5_numbers, u1_struct_0(B)))),v1_funct_1(A),v1_funct_2(A, k5_numbers, u1_struct_0(B)),v1_lopban_3(A, B).
v1_lopban_3(A, B) :- ~ (v2_struct_0(B)) ,v13_algstr_0(B),v2_rlvect_1(B),v3_rlvect_1(B),v4_rlvect_1(B),v5_rlvect_1(B),v6_rlvect_1(B),v7_rlvect_1(B),v8_rlvect_1(B),v3_normsp_0(B),v4_normsp_0(B),v2_normsp_1(B),v3_lopban_1(B),l1_normsp_1(B),m1_subset_1(A, k1_zfmisc_1(k2_zfmisc_1(k5_numbers, u1_struct_0(B)))),v1_funct_1(A),v1_funct_2(A, k5_numbers, u1_struct_0(B)),v2_lopban_3(A, B).
v4_vectsp_1(A) :- l1_lopban_2(A), ~ (v2_struct_0(A)) ,v13_algstr_0(A),v2_rlvect_1(A),v3_rlvect_1(A),v4_rlvect_1(A),v5_rlvect_1(A),v6_rlvect_1(A),v7_rlvect_1(A),v8_rlvect_1(A),v3_normsp_0(A),v4_normsp_0(A),v2_normsp_1(A),v2_funcsdom(A),v3_group_1(A),v1_vectsp_1(A),v3_vectsp_1(A),v5_lopban_2(A).
v2_xxreal_0(A) :- true,v1_xreal_0(A),v1_lpspace2(A).
v2_card_3(A) :- true,v1_xboole_0(A).
v1_xboolean(A) :- m1_subset_1(A, k6_margrel1),true.
v1_margrel1(A) :- m1_subset_1(A, k9_funct_2(B, k6_margrel1)),true.
v1_relat_1(A) :- ~ (v2_struct_0(B)) , ~ (v6_struct_0(B)) ,v13_algstr_0(B),v33_algstr_0(B),v3_group_1(B),v5_group_1(B),v2_rlvect_1(B),v3_rlvect_1(B),v4_rlvect_1(B),v4_vectsp_1(B),v5_vectsp_1(B),l6_algstr_0(B),v7_ordinal1(C),m1_subset_1(A, u1_struct_0(k7_prvect_1(B, C))),true.
v1_funct_1(A) :- ~ (v2_struct_0(B)) , ~ (v6_struct_0(B)) ,v13_algstr_0(B),v33_algstr_0(B),v3_group_1(B),v5_group_1(B),v2_rlvect_1(B),v3_rlvect_1(B),v4_rlvect_1(B),v4_vectsp_1(B),v5_vectsp_1(B),l6_algstr_0(B),v7_ordinal1(C),m1_subset_1(A, u1_struct_0(k7_prvect_1(B, C))),true.
v1_matrix_2(A, C, B) :- v7_ordinal1(C), ~ (v2_struct_0(B)) , ~ (v6_struct_0(B)) ,v13_algstr_0(B),v33_algstr_0(B),v3_group_1(B),v5_group_1(B),v2_rlvect_1(B),v3_rlvect_1(B),v4_rlvect_1(B),v4_vectsp_1(B),v5_vectsp_1(B),l6_algstr_0(B),m1_matrix_1(A, u1_struct_0(B), C, C),v2_matrix_1(A, B).
v2_matrix_2(A, C, B) :- v7_ordinal1(C), ~ (v2_struct_0(B)) , ~ (v6_struct_0(B)) ,v13_algstr_0(B),v33_algstr_0(B),v3_group_1(B),v5_group_1(B),v2_rlvect_1(B),v3_rlvect_1(B),v4_rlvect_1(B),v4_vectsp_1(B),v5_vectsp_1(B),l6_algstr_0(B),m1_matrix_1(A, u1_struct_0(B), C, C),v2_matrix_1(A, B).
v1_matrixj1(A, B) :- ~ (v1_xboole_0(B)) ,m1_finseq_1(A, k3_finseq_2(k3_finseq_2(B))),v2_matrixj1(A, B).
v2_matrixj1(A, u1_struct_0(B)) :- ~ (v2_struct_0(B)) , ~ (v6_struct_0(B)) ,v13_algstr_0(B),v33_algstr_0(B),v3_group_1(B),v5_group_1(B),v4_vectsp_1(B),v5_vectsp_1(B),v2_rlvect_1(B),v3_rlvect_1(B),v4_rlvect_1(B),l6_algstr_0(B),m1_finseq_1(A, k3_finseq_2(k3_finseq_2(u1_struct_0(B)))),v1_matrixj2(A, B).
v1_pre_poly(A) :- ~ (v1_xboole_0(B)) ,m1_finseq_1(A, k3_finseq_2(B)),v1_matrix_1(A).
v3_pre_topc(A, B) :- ~ (v3_pencil_1(B)) ,v1_matroid0(B),l1_pre_topc(B),m1_subset_1(A, k1_zfmisc_1(u1_struct_0(B))),v1_xboole_0(A).
v3_matroid0(A) :- l1_pre_topc(A),v4_matroid0(A).
v4_matroid0(A) :- l1_pre_topc(A),v8_struct_0(A).
~ (v3_pencil_1(A)) :- l1_pre_topc(A),v1_tdlat_3(A).
v1_matroid0(A) :- l1_pre_topc(A),v1_tdlat_3(A).
v2_matroid0(A) :- l1_pre_topc(A),v1_tdlat_3(A).
v4_taxonom2(A) :- m1_eqrel_1(A, B),true.
v1_finset_1(A) :- ~ (v3_pencil_1(B)) ,v3_matroid0(B),l1_pre_topc(B),m1_subset_1(A, k1_zfmisc_1(u1_struct_0(B))),v3_pre_topc(A, B).
~ (v1_xboole_0(A)) :- ~ (v2_struct_0(B)) , ~ (v3_pencil_1(B)) ,v1_matroid0(B),v2_matroid0(B),v4_matroid0(B),l1_pre_topc(B),m1_subset_1(A, k1_zfmisc_1(u1_struct_0(B))),v5_matroid0(A, B).
v1_finset_1(A) :- ~ (v2_struct_0(B)) , ~ (v3_pencil_1(B)) ,v1_matroid0(B),v2_matroid0(B),v4_matroid0(B),l1_pre_topc(B),m1_subset_1(A, k1_zfmisc_1(u1_struct_0(B))),v5_matroid0(A, B).
v2_matrprob(A) :- m1_finseq_1(A, k3_finseq_2(k1_numbers)),v1_matrix_1(A),v4_matrprob(A).
v3_matrprob(A) :- m1_finseq_1(A, k3_finseq_2(k1_numbers)),v1_matrix_1(A),v4_matrprob(A).
v4_matrprob(A) :- m1_finseq_1(A, k3_finseq_2(k1_numbers)),v1_matrix_1(A),v2_matrprob(A),v3_matrprob(A).
v2_matrprob(A) :- m1_finseq_1(A, k3_finseq_2(k1_numbers)),v1_matrix_1(A),v6_matrprob(A).
v5_matrprob(A) :- m1_finseq_1(A, k3_finseq_2(k1_numbers)),v1_matrix_1(A),v6_matrprob(A).
v6_matrprob(A) :- m1_finseq_1(A, k3_finseq_2(k1_numbers)),v1_matrix_1(A),v2_matrprob(A),v5_matrprob(A).