-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathFormulasInMMLOrder
4564 lines (4564 loc) · 62 KB
/
FormulasInMMLOrder
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
dt_k5_xboole_0
dt_k4_xboole_0
idempotence_k2_xboole_0
d3_xboole_0
commutativity_k5_xboole_0
d5_xboole_0
d6_xboole_0
antisymmetry_r2_hidden
commutativity_k2_xboole_0
dt_k2_xboole_0
t1_xboole_0
t2_tarski
t2_xboole_0
rc1_xboole_0
dt_k3_xboole_0
dt_o_0_0_xboole_0
d1_xboole_0
commutativity_k3_xboole_0
idempotence_k3_xboole_0
fc1_xboole_0
l13_xboole_0
d4_xboole_0
rc2_xboole_0
d2_xboole_0
symmetry_r1_xboole_0
dt_k1_xboole_0
d7_xboole_0
t3_xboole_0
t4_xboole_0
t5_xboole_0
antisymmetry_r2_xboole_0
d8_xboole_0
irreflexivity_r2_xboole_0
d3_tarski
t6_xboole_0
t7_xboole_0
t6_boole
t8_boole
t7_boole
t1_xboole_1
t2_xboole_1
d10_xboole_0
t3_xboole_1
t1_boole
fc5_xboole_0
fc4_xboole_0
t4_xboole_1
t5_xboole_1
t6_xboole_1
t7_xboole_1
t8_xboole_1
t9_xboole_1
t10_xboole_1
t11_xboole_1
t12_xboole_1
t13_xboole_1
t14_xboole_1
t15_xboole_1
t2_boole
t16_xboole_1
t17_xboole_1
t18_xboole_1
t19_xboole_1
t20_xboole_1
t21_xboole_1
t22_xboole_1
t23_xboole_1
t24_xboole_1
t25_xboole_1
t26_xboole_1
t27_xboole_1
t28_xboole_1
t29_xboole_1
t30_xboole_1
t31_xboole_1
t3_boole
t4_boole
t32_xboole_1
t33_xboole_1
t34_xboole_1
t35_xboole_1
t36_xboole_1
l32_xboole_1
t37_xboole_1
t38_xboole_1
t39_xboole_1
t40_xboole_1
t41_xboole_1
t42_xboole_1
t43_xboole_1
t44_xboole_1
t45_xboole_1
t46_xboole_1
t47_xboole_1
t48_xboole_1
t49_xboole_1
l36_xboole_1
t50_xboole_1
t51_xboole_1
t52_xboole_1
t53_xboole_1
t54_xboole_1
t55_xboole_1
l58_xboole_1
t56_xboole_1
t57_xboole_1
t58_xboole_1
t59_xboole_1
t60_xboole_1
t61_xboole_1
t62_xboole_1
t63_xboole_1
t64_xboole_1
t65_xboole_1
t66_xboole_1
t67_xboole_1
t68_xboole_1
t69_xboole_1
t70_xboole_1
t71_xboole_1
t72_xboole_1
t73_xboole_1
t74_xboole_1
t75_xboole_1
t76_xboole_1
t77_xboole_1
t78_xboole_1
t79_xboole_1
t80_xboole_1
t81_xboole_1
t82_xboole_1
t83_xboole_1
t84_xboole_1
t85_xboole_1
t86_xboole_1
t87_xboole_1
t88_xboole_1
t89_xboole_1
t90_xboole_1
t91_xboole_1
t5_boole
t92_xboole_1
t93_xboole_1
l97_xboole_1
t94_xboole_1
l98_xboole_1
t95_xboole_1
t96_xboole_1
t97_xboole_1
t98_xboole_1
t99_xboole_1
t100_xboole_1
t101_xboole_1
t102_xboole_1
t103_xboole_1
reflexivity_r3_xboole_0
symmetry_r3_xboole_0
d9_xboole_0
t104_xboole_1
t105_xboole_1
t106_xboole_1
t107_xboole_1
t108_xboole_1
t109_xboole_1
t110_xboole_1
t111_xboole_1
t112_xboole_1
t113_xboole_1
t114_xboole_1
t115_xboole_1
t116_xboole_1
t117_xboole_1
d2_tarski
dt_k1_tarski
commutativity_k2_tarski
d1_tarski
dt_k2_tarski
t41_enumset1
dt_k1_enumset1
d1_enumset1
t42_enumset1
t43_enumset1
l53_enumset1
dt_k2_enumset1
t44_enumset1
t45_enumset1
t46_enumset1
dt_k3_enumset1
l57_enumset1
t47_enumset1
t48_enumset1
t49_enumset1
t50_enumset1
l62_enumset1
dt_k4_enumset1
t51_enumset1
t52_enumset1
t53_enumset1
t54_enumset1
t55_enumset1
dt_k5_enumset1
l68_enumset1
t56_enumset1
t57_enumset1
t58_enumset1
t59_enumset1
t60_enumset1
t61_enumset1
dt_k6_enumset1
l75_enumset1
t62_enumset1
t63_enumset1
t64_enumset1
t65_enumset1
t66_enumset1
t67_enumset1
t68_enumset1
t69_enumset1
t70_enumset1
t71_enumset1
t72_enumset1
t73_enumset1
t74_enumset1
t75_enumset1
t76_enumset1
t77_enumset1
t78_enumset1
t79_enumset1
t80_enumset1
t81_enumset1
t82_enumset1
t83_enumset1
t84_enumset1
t85_enumset1
t86_enumset1
t87_enumset1
t88_enumset1
t89_enumset1
t90_enumset1
t91_enumset1
t92_enumset1
t93_enumset1
t94_enumset1
t95_enumset1
t96_enumset1
t98_enumset1
t99_enumset1
t100_enumset1
t102_enumset1
t103_enumset1
t104_enumset1
t105_enumset1
t107_enumset1
t108_enumset1
l123_enumset1
t109_enumset1
t110_enumset1
t111_enumset1
t112_enumset1
t113_enumset1
l129_enumset1
t116_enumset1
t117_enumset1
t118_enumset1
t119_enumset1
t123_enumset1
t125_enumset1
l142_enumset1
dt_k7_enumset1
t127_enumset1
t128_enumset1
t129_enumset1
t130_enumset1
t131_enumset1
t132_enumset1
t133_enumset1
t134_enumset1
dt_k8_enumset1
d7_enumset1
d8_enumset1
t135_enumset1
t136_enumset1
t137_enumset1
dt_k1_zfmisc_1
fc2_xboole_0
d1_zfmisc_1
t1_zfmisc_1
dt_k3_tarski
d4_tarski
t2_zfmisc_1
l3_zfmisc_1
t6_zfmisc_1
fc3_xboole_0
t8_zfmisc_1
t9_zfmisc_1
t10_zfmisc_1
t12_zfmisc_1
l20_zfmisc_1
t13_zfmisc_1
l22_zfmisc_1
t14_zfmisc_1
l24_zfmisc_1
t16_zfmisc_1
l27_zfmisc_1
t17_zfmisc_1
l29_zfmisc_1
t18_zfmisc_1
l31_zfmisc_1
t19_zfmisc_1
l33_zfmisc_1
t20_zfmisc_1
l35_zfmisc_1
t21_zfmisc_1
t22_zfmisc_1
l38_zfmisc_1
t23_zfmisc_1
t24_zfmisc_1
t25_zfmisc_1
t26_zfmisc_1
t27_zfmisc_1
l45_zfmisc_1
t28_zfmisc_1
t29_zfmisc_1
t30_zfmisc_1
l49_zfmisc_1
t31_zfmisc_1
l51_zfmisc_1
t32_zfmisc_1
dt_k4_tarski
fc1_zfmisc_1
t33_zfmisc_1
l54_zfmisc_1
dt_k2_zfmisc_1
t34_zfmisc_1
d2_zfmisc_1
t35_zfmisc_1
t36_zfmisc_1
l1_zfmisc_1
t37_zfmisc_1
t38_zfmisc_1
t39_zfmisc_1
l2_zfmisc_1
t40_zfmisc_1
l44_zfmisc_1
t41_zfmisc_1
t42_zfmisc_1
t43_zfmisc_1
t44_zfmisc_1
t45_zfmisc_1
t46_zfmisc_1
t47_zfmisc_1
t48_zfmisc_1
t49_zfmisc_1
t50_zfmisc_1
t51_zfmisc_1
t52_zfmisc_1
t53_zfmisc_1
t54_zfmisc_1
t55_zfmisc_1
t56_zfmisc_1
t57_zfmisc_1
t58_zfmisc_1
t59_zfmisc_1
t60_zfmisc_1
t63_zfmisc_1
t64_zfmisc_1
t65_zfmisc_1
t66_zfmisc_1
t67_zfmisc_1
t68_zfmisc_1
t69_zfmisc_1
t70_zfmisc_1
t72_zfmisc_1
t73_zfmisc_1
t74_zfmisc_1
t75_zfmisc_1
t79_zfmisc_1
t80_zfmisc_1
t81_zfmisc_1
t82_zfmisc_1
t83_zfmisc_1
t84_zfmisc_1
t86_zfmisc_1
t92_zfmisc_1
t93_zfmisc_1
t94_zfmisc_1
t95_zfmisc_1
t96_zfmisc_1
t97_zfmisc_1
t98_zfmisc_1
t99_zfmisc_1
t100_zfmisc_1
t101_zfmisc_1
t103_zfmisc_1
t104_zfmisc_1
t105_zfmisc_1
t106_zfmisc_1
t107_zfmisc_1
t108_zfmisc_1
t113_zfmisc_1
t114_zfmisc_1
t115_zfmisc_1
t7_tarski
l139_zfmisc_1
t116_zfmisc_1
t117_zfmisc_1
t118_zfmisc_1
t119_zfmisc_1
l131_zfmisc_1
t120_zfmisc_1
t121_zfmisc_1
l130_zfmisc_1
t122_zfmisc_1
t123_zfmisc_1
t124_zfmisc_1
t125_zfmisc_1
t126_zfmisc_1
t127_zfmisc_1
t128_zfmisc_1
t129_zfmisc_1
t130_zfmisc_1
t131_zfmisc_1
t132_zfmisc_1
t134_zfmisc_1
s1_xboole_0__e1_138_1__zfmisc_1
t135_zfmisc_1
t9_tarski
t136_zfmisc_1
t137_zfmisc_1
t138_zfmisc_1
t139_zfmisc_1
t140_zfmisc_1
t141_zfmisc_1
t142_zfmisc_1
t143_zfmisc_1
l168_zfmisc_1
t144_zfmisc_1
t145_zfmisc_1
t146_zfmisc_1
t147_zfmisc_1
fc2_zfmisc_1
cc1_zfmisc_1
t148_zfmisc_1
t149_zfmisc_1
t151_zfmisc_1
fc4_zfmisc_1
fc3_zfmisc_1
t152_zfmisc_1
t153_zfmisc_1
t154_zfmisc_1
d3_subset_1
existence_m1_subset_1
fc13_subset_1
fc1_subset_1
rc1_subset_1
dt_k1_subset_1
rc2_subset_1
dt_m1_subset_1
t4_subset_1
d2_subset_1
l3_subset_1
t7_subset_1
t8_subset_1
t10_subset_1
redefinition_k4_subset_1
dt_k4_subset_1
commutativity_k4_subset_1
idempotence_k4_subset_1
t15_subset_1
idempotence_k9_subset_1
commutativity_k9_subset_1
redefinition_k9_subset_1
dt_k9_subset_1
t16_subset_1
redefinition_k7_subset_1
dt_k7_subset_1
t17_subset_1
redefinition_k5_subset_1
commutativity_k5_subset_1
dt_k5_subset_1
t18_subset_1
dt_k2_subset_1
d5_subset_1
involutiveness_k3_subset_1
dt_k3_subset_1
d4_subset_1
t22_subset_1
t25_subset_1
t28_subset_1
redefinition_k6_subset_1
dt_k6_subset_1
t31_subset_1
dt_k8_subset_1
idempotence_k8_subset_1
commutativity_k8_subset_1
redefinition_k8_subset_1
t32_subset_1
t33_subset_1
t34_subset_1
t35_subset_1
t36_subset_1
t38_subset_1
t39_subset_1
t40_subset_1
t41_subset_1
t42_subset_1
t43_subset_1
t44_subset_1
t46_subset_1
t47_subset_1
t48_subset_1
t49_subset_1
t50_subset_1
t51_subset_1
t52_subset_1
t53_subset_1
t55_subset_1
t56_subset_1
fc2_subset_1
t57_subset_1
d2_enumset1
fc3_subset_1
t58_subset_1
d3_enumset1
fc4_subset_1
t59_subset_1
d4_enumset1
fc5_subset_1
t60_subset_1
fc6_subset_1
d5_enumset1
t61_subset_1
d6_enumset1
fc7_subset_1
t62_subset_1
t63_subset_1
t64_subset_1
fc10_subset_1
t65_subset_1
d1_setfam_1
t2_subset
t1_subset
dt_k1_setfam_1
t2_setfam_1
rc3_subset_1
t4_subset
rc4_subset_1
cc2_subset_1
cc4_subset_1
cc3_subset_1
cc1_subset_1
t3_subset
dt_o_1_0_setfam_1
t5_subset
t3_setfam_1
t4_setfam_1
t5_setfam_1
t6_setfam_1
t7_setfam_1
t8_setfam_1
t9_setfam_1
t10_setfam_1
t11_setfam_1
t12_setfam_1
reflexivity_r1_setfam_1
d2_setfam_1
t17_setfam_1
t18_setfam_1
reflexivity_r2_setfam_1
d3_setfam_1
t19_setfam_1
t20_setfam_1
t21_setfam_1
t23_setfam_1
t24_setfam_1
t25_setfam_1
d4_setfam_1
dt_k2_setfam_1
commutativity_k2_setfam_1
t29_setfam_1
commutativity_k3_setfam_1
dt_k3_setfam_1
d5_setfam_1
t30_setfam_1
d6_setfam_1
dt_k4_setfam_1
t31_setfam_1
dt_o_2_0_setfam_1
t34_setfam_1
t35_setfam_1
t36_setfam_1
t37_setfam_1
t38_setfam_1
t39_setfam_1
t40_setfam_1
t41_setfam_1
t44_setfam_1
dt_o_2_1_setfam_1
d8_setfam_1
dt_k7_setfam_1
involutiveness_k7_setfam_1
t46_setfam_1
fc14_subset_1
redefinition_k5_setfam_1
dt_k5_setfam_1
redefinition_k6_setfam_1
dt_k6_setfam_1
t47_setfam_1
t48_setfam_1
t49_setfam_1
t51_setfam_1
t52_setfam_1
t53_setfam_1
t54_setfam_1
t55_setfam_1
t56_setfam_1
t57_setfam_1
d10_setfam_1
dt_k8_setfam_1
t58_setfam_1
t59_setfam_1
d12_setfam_1
dt_m1_setfam_1
existence_m1_setfam_1
t60_setfam_1
cc2_setfam_1
fc2_setfam_1
rc1_setfam_1
cc1_setfam_1
cc3_setfam_1
rc3_setfam_1
rc2_setfam_1
t61_setfam_1
d13_setfam_1
t62_setfam_1
rc4_setfam_1
t63_setfam_1
cc2_relat_1
d4_relat_1
dt_k1_relat_1
fc3_relat_1
cc1_relat_1
t13_relat_1
fc1_relat_1
t14_relat_1
fc2_relat_1
t15_relat_1
d5_relat_1
dt_k2_relat_1
t18_relat_1
t19_relat_1
t20_relat_1
d3_relat_1
fc6_relat_1
t21_relat_1
t22_relat_1
fc5_relat_1
t23_relat_1
fc7_relat_1
t24_relat_1
t25_relat_1
t26_relat_1
t27_relat_1
t28_relat_1
d6_relat_1
dt_k3_relat_1
t30_relat_1
t31_relat_1
t32_relat_1
t33_relat_1
t34_relat_1
involutiveness_k4_relat_1
dt_k4_relat_1
d7_relat_1
t37_relat_1
t38_relat_1
d2_relat_1
t39_relat_1
t40_relat_1
t41_relat_1
d8_relat_1
dt_k5_relat_1
t44_relat_1
t45_relat_1
t46_relat_1
t47_relat_1
t48_relat_1
t49_relat_1
t50_relat_1
t51_relat_1
t52_relat_1
t53_relat_1
t54_relat_1
t55_relat_1
rc1_relat_1
d1_relat_1
dt_o_1_1_relat_1
t56_relat_1
fc8_relat_1
fc9_relat_1
t60_relat_1
t62_relat_1
fc11_relat_1
fc10_relat_1
t63_relat_1
t64_relat_1
t65_relat_1
fc14_relat_1
t66_relat_1
fc13_relat_1
fc12_relat_1
t67_relat_1
d10_relat_1
dt_k6_relat_1
t71_relat_1
t72_relat_1
t73_relat_1
t74_relat_1
t75_relat_1
t76_relat_1
t77_relat_1
t78_relat_1
t79_relat_1
t80_relat_1
t81_relat_1
t82_relat_1
fc16_relat_1
d11_relat_1
dt_k7_relat_1
t86_relat_1
t87_relat_1
t88_relat_1
t89_relat_1
t90_relat_1
t91_relat_1
t92_relat_1
t93_relat_1
t94_relat_1
t95_relat_1
t96_relat_1
t97_relat_1
t98_relat_1
t99_relat_1
t100_relat_1
t101_relat_1
t102_relat_1
t103_relat_1
t104_relat_1
t105_relat_1
t106_relat_1
t107_relat_1
t108_relat_1
t109_relat_1
fc17_relat_1
t110_relat_1
t111_relat_1
t112_relat_1
dt_k8_relat_1
fc18_relat_1
d12_relat_1
t115_relat_1
t116_relat_1
t117_relat_1
t118_relat_1
t119_relat_1
t120_relat_1
t121_relat_1
t122_relat_1
t123_relat_1
t124_relat_1
t125_relat_1
t126_relat_1
t127_relat_1
t128_relat_1
t129_relat_1
t130_relat_1
t131_relat_1
t132_relat_1
t133_relat_1
t134_relat_1
t135_relat_1
t136_relat_1
t137_relat_1
t138_relat_1
t139_relat_1
t140_relat_1
d13_relat_1
dt_k9_relat_1
t143_relat_1
t144_relat_1
t145_relat_1
t146_relat_1
t147_relat_1
t148_relat_1
dt_o_1_2_relat_1
t149_relat_1
dt_o_1_3_relat_1
t150_relat_1
dt_o_2_0_relat_1
t151_relat_1
dt_o_1_4_relat_1
t152_relat_1
t153_relat_1
t154_relat_1
t155_relat_1
t156_relat_1
t157_relat_1
t158_relat_1
t159_relat_1
t160_relat_1
t161_relat_1
t162_relat_1
t163_relat_1
dt_k10_relat_1
d14_relat_1
t166_relat_1
t167_relat_1
t168_relat_1
t169_relat_1
t170_relat_1
dt_o_1_5_relat_1
t171_relat_1
dt_o_1_6_relat_1
t172_relat_1
dt_o_2_1_relat_1
t173_relat_1
t174_relat_1
t175_relat_1
t176_relat_1
t177_relat_1
t178_relat_1
t179_relat_1
t180_relat_1
t181_relat_1
t182_relat_1
t183_relat_1
d15_relat_1
t184_relat_1
t185_relat_1
t186_relat_1
t187_relat_1
t188_relat_1
t189_relat_1
fc19_relat_1
t190_relat_1
t191_relat_1
t192_relat_1
cc3_relat_1
t193_relat_1
t194_relat_1
t195_relat_1
t196_relat_1
t197_relat_1
t198_relat_1
t199_relat_1
fc21_relat_1
fc20_relat_1
t200_relat_1
t201_relat_1
d19_relat_1
t202_relat_1
d16_relat_1
dt_k11_relat_1
t203_relat_1
t204_relat_1
t205_relat_1
rc3_relat_1
l222_relat_1
t206_relat_1
rc2_relat_1
cc4_relat_1
t207_relat_1
t208_relat_1
fc23_relat_1
d18_relat_1
cc5_relat_1
t209_relat_1
t210_relat_1
t211_relat_1
t212_relat_1
t213_relat_1
t214_relat_1
t215_relat_1
t216_relat_1
t217_relat_1
cc6_relat_1
t218_relat_1
t219_relat_1
rc1_funct_1
d4_funct_1
cc1_funct_1
dt_k1_funct_1
t8_funct_1
t9_funct_1
d5_funct_1
t12_funct_1
t14_funct_1
dt_o_1_0_funct_1
s3_funct_1__e2_24__funct_1
t15_funct_1
spc1_boole
s3_funct_1__e7_25__funct_1
s3_funct_1__e2_25__funct_1
t16_funct_1
t17_funct_1
s3_funct_1__e1_27_1__funct_1
t18_funct_1
t19_funct_1
fc15_relat_1
fc2_funct_1
t20_funct_1
t21_funct_1
t22_funct_1
t23_funct_1
t25_funct_1
t27_funct_1
s3_funct_1__e9_44_1__funct_1
s2_funct_1__e5_44_1__funct_1
t33_funct_1
fc3_funct_1
fc24_relat_1
t34_funct_1
t35_funct_1
fc26_relat_1
fc25_relat_1
t37_funct_1
t38_funct_1
t40_funct_1
t43_funct_1
t44_funct_1
d8_funct_1
t46_funct_1
t47_funct_1
t48_funct_1
s3_funct_1__e4_61_2__funct_1
s3_funct_1__e12_61_2__funct_1
t49_funct_1
t50_funct_1
t51_funct_1
fc4_funct_1
t52_funct_1
t53_funct_1
dt_k2_funct_1
rc2_funct_1
cc2_funct_1
fc5_funct_1
d9_funct_1
t54_funct_1
t55_funct_1
t56_funct_1
t57_funct_1
t58_funct_1
t59_funct_1
t60_funct_1
t61_funct_1
t62_funct_1
l72_funct_1
fc7_funct_1
fc6_funct_1
t63_funct_1
t64_funct_1
t65_funct_1
t66_funct_1
t67_funct_1
fc8_funct_1
t68_funct_1
t70_funct_1
t71_funct_1
t72_funct_1
t73_funct_1
t82_funct_1
t84_funct_1
fc9_funct_1
t85_funct_1
t86_funct_1
t87_funct_1
t89_funct_1
t97_funct_1
t99_funct_1
d12_funct_1
t117_funct_1
t118_funct_1
t120_funct_1
t121_funct_1
symmetry_r1_subset_1
redefinition_r1_subset_1
irreflexivity_r1_subset_1
t122_funct_1
t123_funct_1
t124_funct_1
t125_funct_1
t126_funct_1
d13_funct_1
t137_funct_1
t138_funct_1
t139_funct_1
t141_funct_1
fc1_funct_1
t142_funct_1
t143_funct_1