-
Notifications
You must be signed in to change notification settings - Fork 10
/
Copy pathl10_goboard1
25 lines (25 loc) · 6.31 KB
/
l10_goboard1
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
C * ! / b0 * * c=> * c~ * cv1_xboole_0 b0 * ! / b1 * * c=> * * c& * cv1_matrix_1 b1 * * cm2_finseq_1 b1 * ck3_finseq_2 b0 * * c<=> * c~ * cv3_relat_1 b1 * * c& * c~ * * cr1_xxreal_0 * ck3_finseq_1 b1 ck6_numbers * c~ * * cr1_xxreal_0 * ck1_matrix_1 b1 ck6_numbers
+ * ! / b0 * * c=> * * cm1_subset_1 b0 ck4_ordinal1 * cv7_ordinal1 b0
+ * ! / b0 * * c=> * c~ * cv1_xboole_0 b0 * ! / b1 * * c=> * * c& * cv1_matrix_1 b1 * * cm2_finseq_1 b1 * ck3_finseq_2 b0 * * c<=> * cv3_relat_1 b1 * * c| * * c= ck6_numbers * ck3_finseq_1 b1 * * c= ck6_numbers * ck1_matrix_1 b1
+ * ! / b0 * * c=> * * c& * cv1_relat_1 b0 * * c& * cv1_funct_1 b0 * * c& * cv1_finseq_1 b0 * cv1_matrix_1 b0 * * cm1_subset_1 * ck1_matrix_1 b0 ck5_numbers
+ * ! / b0 * ! / b1 * * c=> * * c& * c~ * cv1_xboole_0 b0 * * c& * cv1_matrix_1 b1 * * cm1_finseq_1 b1 * ck3_finseq_2 b0 * * c& * cv1_matrix_1 * * ck4_matrix_1 b0 b1 * * cm2_finseq_1 * * ck4_matrix_1 b0 b1 * ck3_finseq_2 b0
+ * ! / b0 * ! / b1 * * c=> * * cm1_finseq_1 b1 b0 * * c& * cv1_relat_1 b1 * * c& * cv1_funct_1 b1 * cv1_finseq_1 b1
+ * ! / b0 * ! / b1 * * c=> * * cm2_finseq_1 b1 b0 * * c& * cv1_funct_1 b1 * * c& * cv1_finseq_1 b1 * * cm1_subset_1 b1 * ck1_zfmisc_1 * * ck2_zfmisc_1 ck5_numbers b0
+ * * c= ck5_numbers ck4_ordinal1
+ * * c= ck6_numbers ck1_xboole_0
+ * ! / b0 * ! / b1 * * c<=> * * cm2_finseq_1 b1 b0 * * cm1_finseq_1 b1 b0
+ * ! / b0 * * c=> * c~ * cv1_xboole_0 b0 * ! / b1 * * c=> * * c& * cv1_matrix_1 b1 * * cm2_finseq_1 b1 * ck3_finseq_2 b0 * * c=> * c~ * * cr1_xxreal_0 * ck1_matrix_1 b1 ck6_numbers * * c& * * c= * ck3_finseq_1 * * ck4_matrix_1 b0 b1 * ck1_matrix_1 b1 * * c= * ck1_matrix_1 * * ck4_matrix_1 b0 b1 * ck3_finseq_1 b1
+ * ! / b0 * * c=> * cv7_ordinal1 b0 * * cr1_xxreal_0 ck6_numbers b0
+ * ! / b0 * * c=> * cv7_ordinal1 b0 * c~ * * c& * c~ * * c= ck6_numbers b0 * * cr1_xxreal_0 b0 ck6_numbers
- * ! / b0 * * c=> * c~ * cv1_xboole_0 b0 * ! / b1 * * c=> * * c& * cv1_matrix_1 b1 * * cm2_finseq_1 b1 * ck3_finseq_2 b0 * ! / b2 * * c=> * * c& * cv1_matrix_1 b2 * * cm2_finseq_1 b2 * ck3_finseq_2 b0 * * c=> * * c= * * ck4_matrix_1 b0 b1 * * ck4_matrix_1 b0 b2 * * c| * * cr1_xxreal_0 * ck1_matrix_1 b1 ck6_numbers * * c| * * cr1_xxreal_0 * ck1_matrix_1 b2 ck6_numbers * * c= b1 b2
- * ! / b0 * * c=> * c~ * cv1_xboole_0 b0 * ! / b1 * * c=> * * c& * cv1_matrix_1 b1 * * cm2_finseq_1 b1 * ck3_finseq_2 b0 * * c=> * c~ * * cr1_xxreal_0 * ck1_matrix_1 b1 ck1_xboole_0 * * c& * * c= * ck3_finseq_1 * * ck4_matrix_1 b0 b1 * ck1_matrix_1 b1 * * c= * ck1_matrix_1 * * ck4_matrix_1 b0 b1 * ck3_finseq_1 b1
- * ! / b0 * * c=> * c~ * cv1_xboole_0 b0 * ! / b1 * * c=> * * c& * cv1_matrix_1 b1 * * cm2_finseq_1 b1 * ck3_finseq_2 b0 * ! / b2 * * c=> * * c& * cv1_matrix_1 b2 * * cm2_finseq_1 b2 * ck3_finseq_2 b0 * * c=> * * c& * * c= * * ck4_matrix_1 b0 b1 * * ck4_matrix_1 b0 b2 * * c= * ck3_finseq_1 b1 * ck3_finseq_1 b2 * * c= b1 b2
- * ! / b0 * * c=> * c~ * cv1_xboole_0 b0 * ! / b1 * * c=> * * c& * cv1_matrix_1 b1 * * cm2_finseq_1 b1 * ck3_finseq_2 b0 * ! / b2 * * c=> * * c& * cv1_matrix_1 b2 * * cm2_finseq_1 b2 * ck3_finseq_2 b0 * * c<=> * * c= b2 * * ck4_matrix_1 b0 b1 * * c& * * c= * ck3_finseq_1 b2 * ck1_matrix_1 b1 * * c& * ! / b3 * * c=> * cv7_ordinal1 b3 * ! / b4 * * c=> * cv7_ordinal1 b4 * * c<=> * * cr2_hidden * * ck4_tarski b3 b4 * ck2_matrix_1 b2 * * cr2_hidden * * ck4_tarski b4 b3 * ck2_matrix_1 b1 * ! / b3 * * c=> * cv7_ordinal1 b3 * ! / b4 * * c=> * cv7_ordinal1 b4 * * c=> * * cr2_hidden * * ck4_tarski b4 b3 * ck2_matrix_1 b1 * * c= * * * * ck3_matrix_1 b0 b2 b3 b4 * * * * ck3_matrix_1 b0 b1 b4 b3
- * ! / b0 * * c=> * c~ * cv1_xboole_0 b0 * ! / b1 * * c=> * * c& * cv1_matrix_1 b1 * * cm2_finseq_1 b1 * ck3_finseq_2 b0 * c~ * * c& * c~ * * cr1_xxreal_0 * ck3_finseq_1 b1 ck6_numbers * * c& * c~ * * cr1_xxreal_0 * ck1_matrix_1 b1 ck6_numbers * c~ * * c= * * ck4_matrix_1 b0 * * ck4_matrix_1 b0 b1 b1
- * ! / b0 * * c=> * c~ * cv1_xboole_0 b0 * ! / b1 * * c=> * * c& * cv1_matrix_1 b1 * * cm2_finseq_1 b1 * ck3_finseq_2 b0 * ! / b2 * * c=> * * c& * cv1_matrix_1 b2 * * cm2_finseq_1 b2 * ck3_finseq_2 b0 * c~ * * c& * c~ * * cr1_xxreal_0 * ck1_matrix_1 b1 ck6_numbers * * c& * c~ * * cr1_xxreal_0 * ck1_matrix_1 b2 ck6_numbers * c~ * * c<=> * * c= b1 b2 * * c& * * c= * * ck4_matrix_1 b0 b1 * * ck4_matrix_1 b0 b2 * * c= * ck1_matrix_1 b1 * ck1_matrix_1 b2
- * ! / b0 * ! / b1 * * c=> * cv7_ordinal1 b1 * ! / b2 * * c=> * cv7_ordinal1 b2 * ! / b3 * * c=> * * c& * cv1_matrix_1 b3 * * cm2_finseq_1 b3 * ck3_finseq_2 b0 * * c=> * * c& * * cr1_xxreal_0 c1 b1 * * c& * * cr1_xxreal_0 b1 * ck3_finseq_1 b3 * * c& * * cr1_xxreal_0 c1 b2 * * cr1_xxreal_0 b2 * ck1_matrix_1 b3 * * cr2_hidden * * ck4_tarski b1 b2 * ck2_matrix_1 b3
- * ! / b0 * * c=> * c~ * cv1_xboole_0 b0 * ! / b1 * * c=> * * cm1_subset_1 b1 ck5_numbers * ! / b2 * * c=> * * cm1_subset_1 b2 ck5_numbers * ! / b3 * * c=> * * c& * cv1_matrix_1 b3 * * cm2_finseq_1 b3 * ck3_finseq_2 b0 * * c=> * * c& * * cr1_xxreal_0 c1 b1 * * c& * * cr1_xxreal_0 b1 * ck3_finseq_1 b3 * * c& * * cr1_xxreal_0 c1 b2 * * cr1_xxreal_0 b2 * ck1_matrix_1 b3 * * cr2_hidden * * * * ck3_matrix_1 b0 b3 b1 b2 * ck16_matrix_1 b3
- * ! / b0 * * c=> * * c& * cv1_relat_1 b0 * * c& * cv1_funct_1 b0 * * c& * cv1_finseq_1 b0 * cv1_matrix_1 b0 * ! / b1 * * c=> * cv7_ordinal1 b1 * ! / b2 * * c=> * cv7_ordinal1 b2 * * c=> * * cr2_hidden * * ck4_tarski b1 b2 * ck2_matrix_1 b0 * * c& * * cr1_xxreal_0 c1 b1 * * c& * * cr1_xxreal_0 b1 * ck3_finseq_1 b0 * * c& * * cr1_xxreal_0 c1 b2 * * cr1_xxreal_0 b2 * ck1_matrix_1 b0
- * ! / b0 * * c=> * cv7_ordinal1 b0 * ! / b1 * * c=> * c~ * cv1_xboole_0 b1 * ! / b2 * * c=> * * cm2_finseq_1 b2 b1 * ! / b3 * * c=> * * c& * cv1_matrix_1 b3 * * cm2_finseq_1 b3 * ck3_finseq_2 b1 * * c=> * * c& * * cr2_hidden b0 * ck4_finseq_1 b3 * * c= * * ck1_funct_1 b3 b0 b2 * * c= * ck3_finseq_1 b2 * ck1_matrix_1 b3
- * ! / b0 * * c=> * c~ * cv1_xboole_0 b0 * ! / b1 * * c=> * * c& * cv1_matrix_1 b1 * * cm2_finseq_1 b1 * ck3_finseq_2 b0 * * c=> * c~ * * cr1_xxreal_0 * ck3_finseq_1 b1 ck1_xboole_0 * ! / b2 * * c=> * cv7_ordinal1 b2 * * c<=> * * * * cm1_matrix_1 b1 b0 * ck3_finseq_1 b1 b2 * * c= b2 * ck1_matrix_1 b1
- * ! / b0 * * c=> * c~ * cv1_xboole_0 b0 * ! / b1 * * c=> * * c& * cv1_matrix_1 b1 * * cm2_finseq_1 b1 * ck3_finseq_2 b0 * * cr1_xxreal_0 * ck5_card_1 * ck16_matrix_1 b1 * * ck4_nat_1 * ck3_finseq_1 b1 * ck1_matrix_1 b1