9 additive_identity is 82
10 additive_inverse1 is 84
11 additive_inverse2 is 83
14 commutativity_of_add is 92
15 commutativity_of_multiply is 91
21 multiplicative_id1 is 79
22 multiplicative_id2 is 78
23 multiplicative_identity is 85
24 multiplicative_inverse1 is 81
25 multiplicative_inverse2 is 80
27 prove_associativity is 94
29 Id : 4, {_}: add ?2 ?3 =?= add ?3 ?2 [3, 2] by commutativity_of_add ?2 ?3
31 multiply ?5 ?6 =?= multiply ?6 ?5
32 [6, 5] by commutativity_of_multiply ?5 ?6
34 add (multiply ?8 ?9) ?10 =<= multiply (add ?8 ?10) (add ?9 ?10)
35 [10, 9, 8] by distributivity1 ?8 ?9 ?10
37 add ?12 (multiply ?13 ?14) =<= multiply (add ?12 ?13) (add ?12 ?14)
38 [14, 13, 12] by distributivity2 ?12 ?13 ?14
40 multiply (add ?16 ?17) ?18
42 add (multiply ?16 ?18) (multiply ?17 ?18)
43 [18, 17, 16] by distributivity3 ?16 ?17 ?18
45 multiply ?20 (add ?21 ?22)
47 add (multiply ?20 ?21) (multiply ?20 ?22)
48 [22, 21, 20] by distributivity4 ?20 ?21 ?22
50 add ?24 (inverse ?24) =>= multiplicative_identity
51 [24] by additive_inverse1 ?24
53 add (inverse ?26) ?26 =>= multiplicative_identity
54 [26] by additive_inverse2 ?26
56 multiply ?28 (inverse ?28) =>= additive_identity
57 [28] by multiplicative_inverse1 ?28
59 multiply (inverse ?30) ?30 =>= additive_identity
60 [30] by multiplicative_inverse2 ?30
62 multiply ?32 multiplicative_identity =>= ?32
63 [32] by multiplicative_id1 ?32
65 multiply multiplicative_identity ?34 =>= ?34
66 [34] by multiplicative_id2 ?34
67 Id : 28, {_}: add ?36 additive_identity =>= ?36 [36] by additive_id1 ?36
68 Id : 30, {_}: add additive_identity ?38 =>= ?38 [38] by additive_id2 ?38
71 multiply a (multiply b c) =<= multiply (multiply a b) c
72 [] by prove_associativity
73 Found proof, 6.095314s
81 additive_identity is 88
82 additive_inverse1 is 83
85 commutativity_of_add is 92
86 commutativity_of_multiply is 91
90 multiplicative_id1 is 85
91 multiplicative_identity is 86
92 multiplicative_inverse1 is 82
94 prove_associativity is 94
96 Id : 4, {_}: add ?2 ?3 =?= add ?3 ?2 [3, 2] by commutativity_of_add ?2 ?3
98 multiply ?5 ?6 =?= multiply ?6 ?5
99 [6, 5] by commutativity_of_multiply ?5 ?6
101 add ?8 (multiply ?9 ?10) =<= multiply (add ?8 ?9) (add ?8 ?10)
102 [10, 9, 8] by distributivity1 ?8 ?9 ?10
104 multiply ?12 (add ?13 ?14)
106 add (multiply ?12 ?13) (multiply ?12 ?14)
107 [14, 13, 12] by distributivity2 ?12 ?13 ?14
108 Id : 12, {_}: add ?16 additive_identity =>= ?16 [16] by additive_id1 ?16
110 multiply ?18 multiplicative_identity =>= ?18
111 [18] by multiplicative_id1 ?18
113 add ?20 (inverse ?20) =>= multiplicative_identity
114 [20] by additive_inverse1 ?20
116 multiply ?22 (inverse ?22) =>= additive_identity
117 [22] by multiplicative_inverse1 ?22
120 multiply a (multiply b c) =<= multiply (multiply a b) c
121 [] by prove_associativity
123 FAILURE in 625 iterations
130 additive_inverse is 83
131 associativity_of_add is 80
132 associativity_of_multiply is 79
141 multiplicative_inverse is 81
147 prove_multiply_add_property is 93
150 add (multiply ?2 ?3) (add (multiply ?3 ?4) (multiply ?4 ?2))
152 multiply (add ?2 ?3) (multiply (add ?3 ?4) (add ?4 ?2))
153 [4, 3, 2] by distributivity ?2 ?3 ?4
155 add ?6 (multiply ?7 (multiply ?6 ?8)) =>= ?6
156 [8, 7, 6] by l1 ?6 ?7 ?8
158 add (add (multiply ?10 ?11) (multiply ?11 ?12)) ?11 =>= ?11
159 [12, 11, 10] by l3 ?10 ?11 ?12
161 multiply (add ?14 (inverse ?14)) ?15 =>= ?15
162 [15, 14] by property3 ?14 ?15
164 multiply ?17 (add ?18 (add ?17 ?19)) =>= ?17
165 [19, 18, 17] by l2 ?17 ?18 ?19
167 multiply (multiply (add ?21 ?22) (add ?22 ?23)) ?22 =>= ?22
168 [23, 22, 21] by l4 ?21 ?22 ?23
170 add (multiply ?25 (inverse ?25)) ?26 =>= ?26
171 [26, 25] by property3_dual ?25 ?26
172 Id : 18, {_}: add ?28 (inverse ?28) =>= n1 [28] by additive_inverse ?28
174 multiply ?30 (inverse ?30) =>= n0
175 [30] by multiplicative_inverse ?30
177 add (add ?32 ?33) ?34 =?= add ?32 (add ?33 ?34)
178 [34, 33, 32] by associativity_of_add ?32 ?33 ?34
180 multiply (multiply ?36 ?37) ?38 =?= multiply ?36 (multiply ?37 ?38)
181 [38, 37, 36] by associativity_of_multiply ?36 ?37 ?38
184 multiply a (add b c) =<= add (multiply b a) (multiply c a)
185 [] by prove_multiply_add_property
187 FAILURE in 413 iterations
203 prove_single_axiom is 89
205 ternary_multiply_1 is 87
206 ternary_multiply_2 is 86
209 multiply (multiply ?2 ?3 ?4) ?5 (multiply ?2 ?3 ?6)
211 multiply ?2 ?3 (multiply ?4 ?5 ?6)
212 [6, 5, 4, 3, 2] by associativity ?2 ?3 ?4 ?5 ?6
213 Id : 6, {_}: multiply ?8 ?9 ?9 =>= ?9 [9, 8] by ternary_multiply_1 ?8 ?9
215 multiply ?11 ?11 ?12 =>= ?11
216 [12, 11] by ternary_multiply_2 ?11 ?12
218 multiply (inverse ?14) ?14 ?15 =>= ?15
219 [15, 14] by left_inverse ?14 ?15
221 multiply ?17 ?18 (inverse ?18) =>= ?17
222 [18, 17] by right_inverse ?17 ?18
225 multiply (multiply a (inverse a) b)
226 (inverse (multiply (multiply c d e) f (multiply c d g)))
227 (multiply d (multiply g f e) c)
230 [] by prove_single_axiom
232 FAILURE in 424 iterations
246 (add (inverse (add (inverse (add ?2 ?3)) ?4))
248 (add ?2 (inverse (add (inverse ?4) (inverse (add ?4 ?5)))))))
251 [5, 4, 3, 2] by dn1 ?2 ?3 ?4 ?5
253 Id : 2, {_}: add b a =>= add a b [] by huntinton_1
254 Found proof, 0.440809s
269 (add (inverse (add (inverse (add ?2 ?3)) ?4))
271 (add ?2 (inverse (add (inverse ?4) (inverse (add ?4 ?5)))))))
274 [5, 4, 3, 2] by dn1 ?2 ?3 ?4 ?5
276 Id : 2, {_}: add (add a b) c =>= add a (add b c) [] by huntinton_2
277 Found proof, 95.580028s
286 prove_meredith_2_basis_2 is 94
290 nand (nand ?2 (nand (nand ?3 ?2) ?2)) (nand ?3 (nand ?4 ?2)) =>= ?3
291 [4, 3, 2] by sh_1 ?2 ?3 ?4
294 nand a (nand b (nand a c)) =<= nand (nand (nand c b) b) a
295 [] by prove_meredith_2_basis_2
297 FAILURE in 277 iterations
306 prove_strong_fixed_point is 96
311 apply (apply (apply b ?3) ?4) ?5 =>= apply ?3 (apply ?4 ?5)
312 [5, 4, 3] by b_definition ?3 ?4 ?5
314 apply (apply w ?7) ?8 =?= apply (apply ?7 ?8) ?8
315 [8, 7] by w_definition ?7 ?8
318 apply ?1 (f ?1) =<= apply (f ?1) (apply ?1 (f ?1))
319 [1] by prove_strong_fixed_point ?1
321 FAILURE in 1120 iterations
330 prove_strong_fixed_point is 95
331 strong_fixed_point is 98
336 apply (apply (apply b ?2) ?3) ?4 =>= apply ?2 (apply ?3 ?4)
337 [4, 3, 2] by b_definition ?2 ?3 ?4
339 apply (apply w ?6) ?7 =?= apply (apply ?6 ?7) ?7
340 [7, 6] by w_definition ?6 ?7
344 apply (apply b (apply w w))
345 (apply (apply b w) (apply (apply b b) b))
346 [] by strong_fixed_point
349 apply strong_fixed_point fixed_pt
351 apply fixed_pt (apply strong_fixed_point fixed_pt)
352 [] by prove_strong_fixed_point
354 FAILURE in 1252 iterations
363 prove_strong_fixed_point is 95
364 strong_fixed_point is 98
369 apply (apply (apply b ?2) ?3) ?4 =>= apply ?2 (apply ?3 ?4)
370 [4, 3, 2] by b_definition ?2 ?3 ?4
372 apply (apply w ?6) ?7 =?= apply (apply ?6 ?7) ?7
373 [7, 6] by w_definition ?6 ?7
377 apply (apply b (apply w w))
378 (apply (apply b (apply b w)) (apply (apply b b) b))
379 [] by strong_fixed_point
382 apply strong_fixed_point fixed_pt
384 apply fixed_pt (apply strong_fixed_point fixed_pt)
385 [] by prove_strong_fixed_point
387 FAILURE in 1223 iterations
396 prove_strong_fixed_point is 95
399 strong_fixed_point is 98
402 apply (apply (apply s ?2) ?3) ?4
404 apply (apply ?2 ?4) (apply ?3 ?4)
405 [4, 3, 2] by s_definition ?2 ?3 ?4
406 Id : 6, {_}: apply (apply k ?6) ?7 =>= ?6 [7, 6] by k_definition ?6 ?7
413 (apply (apply s (apply (apply s k) k)) (apply (apply s k) k))))
414 (apply (apply s (apply (apply s (apply k s)) k))
416 (apply (apply s (apply (apply s k) k)) (apply (apply s k) k))))
417 [] by strong_fixed_point
420 apply strong_fixed_point fixed_pt
422 apply fixed_pt (apply strong_fixed_point fixed_pt)
423 [] by prove_strong_fixed_point
425 FAILURE in 1708 iterations
434 prove_fixed_point is 96
439 apply (apply o ?3) ?4 =?= apply ?4 (apply ?3 ?4)
440 [4, 3] by o_definition ?3 ?4
442 apply (apply (apply q1 ?6) ?7) ?8 =>= apply ?6 (apply ?8 ?7)
443 [8, 7, 6] by q1_definition ?6 ?7 ?8
445 Id : 2, {_}: ?1 =<= apply combinator ?1 [1] by prove_fixed_point ?1
447 FAILURE in 1839 iterations
458 prove_fixed_point is 96
463 apply (apply (apply s ?3) ?4) ?5
465 apply (apply ?3 ?5) (apply ?4 ?5)
466 [5, 4, 3] by s_definition ?3 ?4 ?5
468 apply (apply (apply b ?7) ?8) ?9 =>= apply ?7 (apply ?8 ?9)
469 [9, 8, 7] by b_definition ?7 ?8 ?9
471 apply (apply (apply c ?11) ?12) ?13 =>= apply (apply ?11 ?13) ?12
472 [13, 12, 11] by c_definition ?11 ?12 ?13
475 apply ?1 (f ?1) =<= apply (f ?1) (apply ?1 (f ?1))
476 [1] by prove_fixed_point ?1
478 FAILURE in 944 iterations
489 prove_fixed_point is 96
494 apply (apply (apply b ?3) ?4) ?5 =>= apply ?3 (apply ?4 ?5)
495 [5, 4, 3] by b_definition ?3 ?4 ?5
496 Id : 6, {_}: apply m ?7 =?= apply ?7 ?7 [7] by m_definition ?7
498 apply (apply (apply v ?9) ?10) ?11 =>= apply (apply ?11 ?9) ?10
499 [11, 10, 9] by v_definition ?9 ?10 ?11
502 apply ?1 (f ?1) =<= apply (f ?1) (apply ?1 (f ?1))
503 [1] by prove_fixed_point ?1
505 FAILURE in 1682 iterations
516 prove_strong_fixed_point is 95
517 strong_fixed_point is 98
520 apply (apply (apply b ?2) ?3) ?4 =>= apply ?2 (apply ?3 ?4)
521 [4, 3, 2] by b_definition ?2 ?3 ?4
523 apply (apply (apply h ?6) ?7) ?8
525 apply (apply (apply ?6 ?7) ?8) ?7
526 [8, 7, 6] by h_definition ?6 ?7 ?8
536 (apply (apply b (apply (apply b h) (apply b b)))
537 (apply h (apply (apply b h) (apply b b))))) h)) b)) b
538 [] by strong_fixed_point
541 apply strong_fixed_point fixed_pt
543 apply fixed_pt (apply strong_fixed_point fixed_pt)
544 [] by prove_strong_fixed_point
546 FAILURE in 1406 iterations
557 prove_strong_fixed_point is 95
558 strong_fixed_point is 98
561 apply (apply (apply b ?2) ?3) ?4 =>= apply ?2 (apply ?3 ?4)
562 [4, 3, 2] by b_definition ?2 ?3 ?4
564 apply (apply (apply n ?6) ?7) ?8
566 apply (apply (apply ?6 ?8) ?7) ?8
567 [8, 7, 6] by n_definition ?6 ?7 ?8
578 (apply (apply b (apply b b))
579 (apply n (apply (apply b b) n))))) n)) b)) b
580 [] by strong_fixed_point
583 apply strong_fixed_point fixed_pt
585 apply fixed_pt (apply strong_fixed_point fixed_pt)
586 [] by prove_strong_fixed_point
588 FAILURE in 1249 iterations
599 prove_fixed_point is 96
604 apply (apply (apply s ?3) ?4) ?5
606 apply (apply ?3 ?5) (apply ?4 ?5)
607 [5, 4, 3] by s_definition ?3 ?4 ?5
609 apply (apply (apply b ?7) ?8) ?9 =>= apply ?7 (apply ?8 ?9)
610 [9, 8, 7] by b_definition ?7 ?8 ?9
611 Id : 8, {_}: apply m ?11 =?= apply ?11 ?11 [11] by m_definition ?11
614 apply ?1 (f ?1) =<= apply (f ?1) (apply ?1 (f ?1))
615 [1] by prove_fixed_point ?1
617 FAILURE in 1258 iterations
628 prove_strong_fixed_point is 96
633 apply (apply (apply b ?3) ?4) ?5 =>= apply ?3 (apply ?4 ?5)
634 [5, 4, 3] by b_definition ?3 ?4 ?5
636 apply (apply w ?7) ?8 =?= apply (apply ?7 ?8) ?8
637 [8, 7] by w_definition ?7 ?8
638 Id : 8, {_}: apply m ?10 =?= apply ?10 ?10 [10] by m_definition ?10
641 apply ?1 (f ?1) =<= apply (f ?1) (apply ?1 (f ?1))
642 [1] by prove_strong_fixed_point ?1
644 FAILURE in 1565 iterations
657 prove_strong_fixed_point is 96
662 apply (apply (apply s ?3) ?4) ?5
664 apply (apply ?3 ?5) (apply ?4 ?5)
665 [5, 4, 3] by s_definition ?3 ?4 ?5
667 apply (apply (apply b ?7) ?8) ?9 =>= apply ?7 (apply ?8 ?9)
668 [9, 8, 7] by b_definition ?7 ?8 ?9
670 apply (apply (apply c ?11) ?12) ?13 =>= apply (apply ?11 ?13) ?12
671 [13, 12, 11] by c_definition ?11 ?12 ?13
672 Id : 10, {_}: apply i ?15 =>= ?15 [15] by i_definition ?15
675 apply ?1 (f ?1) =<= apply (f ?1) (apply ?1 (f ?1))
676 [1] by prove_strong_fixed_point ?1
678 FAILURE in 1505 iterations
689 prove_q_combinator is 94
694 apply (apply (apply b ?3) ?4) ?5 =>= apply ?3 (apply ?4 ?5)
695 [5, 4, 3] by b_definition ?3 ?4 ?5
697 apply (apply t ?7) ?8 =>= apply ?8 ?7
698 [8, 7] by t_definition ?7 ?8
701 apply (apply (apply ?1 (f ?1)) (g ?1)) (h ?1)
703 apply (g ?1) (apply (f ?1) (h ?1))
704 [1] by prove_q_combinator ?1
705 Found proof, 0.103279s
716 prove_q1_combinator is 94
721 apply (apply (apply b ?3) ?4) ?5 =>= apply ?3 (apply ?4 ?5)
722 [5, 4, 3] by b_definition ?3 ?4 ?5
724 apply (apply t ?7) ?8 =>= apply ?8 ?7
725 [8, 7] by t_definition ?7 ?8
728 apply (apply (apply ?1 (f ?1)) (g ?1)) (h ?1)
730 apply (f ?1) (apply (h ?1) (g ?1))
731 [1] by prove_q1_combinator ?1
732 Found proof, 0.116546s
743 prove_f_combinator is 94
748 apply (apply (apply b ?3) ?4) ?5 =>= apply ?3 (apply ?4 ?5)
749 [5, 4, 3] by b_definition ?3 ?4 ?5
751 apply (apply t ?7) ?8 =>= apply ?8 ?7
752 [8, 7] by t_definition ?7 ?8
755 apply (apply (apply ?1 (f ?1)) (g ?1)) (h ?1)
757 apply (apply (h ?1) (g ?1)) (f ?1)
758 [1] by prove_f_combinator ?1
759 Found proof, 1.828433s
770 prove_v_combinator is 94
775 apply (apply (apply b ?3) ?4) ?5 =>= apply ?3 (apply ?4 ?5)
776 [5, 4, 3] by b_definition ?3 ?4 ?5
778 apply (apply t ?7) ?8 =>= apply ?8 ?7
779 [8, 7] by t_definition ?7 ?8
782 apply (apply (apply ?1 (f ?1)) (g ?1)) (h ?1)
784 apply (apply (h ?1) (f ?1)) (g ?1)
785 [1] by prove_v_combinator ?1
786 Found proof, 13.759082s
798 prove_g_combinator is 93
803 apply (apply (apply b ?3) ?4) ?5 =>= apply ?3 (apply ?4 ?5)
804 [5, 4, 3] by b_definition ?3 ?4 ?5
806 apply (apply t ?7) ?8 =>= apply ?8 ?7
807 [8, 7] by t_definition ?7 ?8
810 apply (apply (apply (apply ?1 (f ?1)) (g ?1)) (h ?1)) (i ?1)
812 apply (apply (f ?1) (i ?1)) (apply (g ?1) (h ?1))
813 [1] by prove_g_combinator ?1
814 Found proof, 68.133820s
825 prove_associativity is 94
833 (multiply (inverse ?3) (multiply (inverse ?2) ?4))) ?5)
834 (inverse (multiply ?3 ?5))))
837 [5, 4, 3, 2] by group_axiom ?2 ?3 ?4 ?5
840 multiply a (multiply b c) =<= multiply (multiply a b) c
841 [] by prove_associativity
842 Found proof, 3.453474s
849 associativity_of_commutator is 86
861 Id : 4, {_}: multiply identity ?2 =>= ?2 [2] by left_identity ?2
862 Id : 6, {_}: multiply (inverse ?4) ?4 =>= identity [4] by left_inverse ?4
864 multiply (multiply ?6 ?7) ?8 =?= multiply ?6 (multiply ?7 ?8)
865 [8, 7, 6] by associativity ?6 ?7 ?8
869 multiply (inverse ?10) (multiply (inverse ?11) (multiply ?10 ?11))
870 [11, 10] by name ?10 ?11
872 commutator (commutator ?13 ?14) ?15
874 commutator ?13 (commutator ?14 ?15)
875 [15, 14, 13] by associativity_of_commutator ?13 ?14 ?15
878 multiply a (commutator b c) =<= multiply (commutator b c) a
881 FAILURE in 602 iterations
890 intersection_associative is 79
891 intersection_commutative is 81
892 intersection_idempotent is 84
893 intersection_union_absorbtion is 76
895 inverse_involution is 87
896 inverse_of_identity is 88
897 inverse_product_lemma is 86
901 multiply_intersection1 is 74
902 multiply_intersection2 is 72
903 multiply_union1 is 75
904 multiply_union2 is 73
909 union_associative is 78
910 union_commutative is 80
911 union_idempotent is 82
912 union_intersection_absorbtion is 77
914 Id : 4, {_}: multiply identity ?2 =>= ?2 [2] by left_identity ?2
915 Id : 6, {_}: multiply (inverse ?4) ?4 =>= identity [4] by left_inverse ?4
917 multiply (multiply ?6 ?7) ?8 =?= multiply ?6 (multiply ?7 ?8)
918 [8, 7, 6] by associativity ?6 ?7 ?8
919 Id : 10, {_}: inverse identity =>= identity [] by inverse_of_identity
920 Id : 12, {_}: inverse (inverse ?11) =>= ?11 [11] by inverse_involution ?11
922 inverse (multiply ?13 ?14) =<= multiply (inverse ?14) (inverse ?13)
923 [14, 13] by inverse_product_lemma ?13 ?14
925 intersection ?16 ?16 =>= ?16
926 [16] by intersection_idempotent ?16
927 Id : 18, {_}: union ?18 ?18 =>= ?18 [18] by union_idempotent ?18
929 intersection ?20 ?21 =?= intersection ?21 ?20
930 [21, 20] by intersection_commutative ?20 ?21
932 union ?23 ?24 =?= union ?24 ?23
933 [24, 23] by union_commutative ?23 ?24
935 intersection ?26 (intersection ?27 ?28)
937 intersection (intersection ?26 ?27) ?28
938 [28, 27, 26] by intersection_associative ?26 ?27 ?28
940 union ?30 (union ?31 ?32) =?= union (union ?30 ?31) ?32
941 [32, 31, 30] by union_associative ?30 ?31 ?32
943 union (intersection ?34 ?35) ?35 =>= ?35
944 [35, 34] by union_intersection_absorbtion ?34 ?35
946 intersection (union ?37 ?38) ?38 =>= ?38
947 [38, 37] by intersection_union_absorbtion ?37 ?38
949 multiply ?40 (union ?41 ?42)
951 union (multiply ?40 ?41) (multiply ?40 ?42)
952 [42, 41, 40] by multiply_union1 ?40 ?41 ?42
954 multiply ?44 (intersection ?45 ?46)
956 intersection (multiply ?44 ?45) (multiply ?44 ?46)
957 [46, 45, 44] by multiply_intersection1 ?44 ?45 ?46
959 multiply (union ?48 ?49) ?50
961 union (multiply ?48 ?50) (multiply ?49 ?50)
962 [50, 49, 48] by multiply_union2 ?48 ?49 ?50
964 multiply (intersection ?52 ?53) ?54
966 intersection (multiply ?52 ?54) (multiply ?53 ?54)
967 [54, 53, 52] by multiply_intersection2 ?52 ?53 ?54
969 positive_part ?56 =<= union ?56 identity
970 [56] by positive_part ?56
972 negative_part ?58 =<= intersection ?58 identity
973 [58] by negative_part ?58
976 multiply (positive_part a) (negative_part a) =>= a
979 FAILURE in 1190 iterations
986 associativity_of_glb is 84
987 associativity_of_lub is 83
991 greatest_lower_bound is 94
992 idempotence_of_gld is 81
993 idempotence_of_lub is 82
996 least_upper_bound is 95
1006 symmetry_of_glb is 86
1007 symmetry_of_lub is 85
1009 Id : 4, {_}: multiply identity ?2 =>= ?2 [2] by left_identity ?2
1010 Id : 6, {_}: multiply (inverse ?4) ?4 =>= identity [4] by left_inverse ?4
1012 multiply (multiply ?6 ?7) ?8 =?= multiply ?6 (multiply ?7 ?8)
1013 [8, 7, 6] by associativity ?6 ?7 ?8
1015 greatest_lower_bound ?10 ?11 =?= greatest_lower_bound ?11 ?10
1016 [11, 10] by symmetry_of_glb ?10 ?11
1018 least_upper_bound ?13 ?14 =?= least_upper_bound ?14 ?13
1019 [14, 13] by symmetry_of_lub ?13 ?14
1021 greatest_lower_bound ?16 (greatest_lower_bound ?17 ?18)
1023 greatest_lower_bound (greatest_lower_bound ?16 ?17) ?18
1024 [18, 17, 16] by associativity_of_glb ?16 ?17 ?18
1026 least_upper_bound ?20 (least_upper_bound ?21 ?22)
1028 least_upper_bound (least_upper_bound ?20 ?21) ?22
1029 [22, 21, 20] by associativity_of_lub ?20 ?21 ?22
1031 least_upper_bound ?24 ?24 =>= ?24
1032 [24] by idempotence_of_lub ?24
1034 greatest_lower_bound ?26 ?26 =>= ?26
1035 [26] by idempotence_of_gld ?26
1037 least_upper_bound ?28 (greatest_lower_bound ?28 ?29) =>= ?28
1038 [29, 28] by lub_absorbtion ?28 ?29
1040 greatest_lower_bound ?31 (least_upper_bound ?31 ?32) =>= ?31
1041 [32, 31] by glb_absorbtion ?31 ?32
1043 multiply ?34 (least_upper_bound ?35 ?36)
1045 least_upper_bound (multiply ?34 ?35) (multiply ?34 ?36)
1046 [36, 35, 34] by monotony_lub1 ?34 ?35 ?36
1048 multiply ?38 (greatest_lower_bound ?39 ?40)
1050 greatest_lower_bound (multiply ?38 ?39) (multiply ?38 ?40)
1051 [40, 39, 38] by monotony_glb1 ?38 ?39 ?40
1053 multiply (least_upper_bound ?42 ?43) ?44
1055 least_upper_bound (multiply ?42 ?44) (multiply ?43 ?44)
1056 [44, 43, 42] by monotony_lub2 ?42 ?43 ?44
1058 multiply (greatest_lower_bound ?46 ?47) ?48
1060 greatest_lower_bound (multiply ?46 ?48) (multiply ?47 ?48)
1061 [48, 47, 46] by monotony_glb2 ?46 ?47 ?48
1064 greatest_lower_bound a (least_upper_bound b c)
1066 least_upper_bound (greatest_lower_bound a b)
1067 (greatest_lower_bound a c)
1070 FAILURE in 1400 iterations
1077 associativity_of_glb is 84
1078 associativity_of_lub is 83
1079 glb_absorbtion is 79
1080 greatest_lower_bound is 88
1081 idempotence_of_gld is 81
1082 idempotence_of_lub is 82
1089 least_upper_bound is 86
1092 lub_absorbtion is 80
1101 symmetry_of_glb is 87
1102 symmetry_of_lub is 85
1104 Id : 4, {_}: multiply identity ?2 =>= ?2 [2] by left_identity ?2
1105 Id : 6, {_}: multiply (inverse ?4) ?4 =>= identity [4] by left_inverse ?4
1107 multiply (multiply ?6 ?7) ?8 =?= multiply ?6 (multiply ?7 ?8)
1108 [8, 7, 6] by associativity ?6 ?7 ?8
1110 greatest_lower_bound ?10 ?11 =?= greatest_lower_bound ?11 ?10
1111 [11, 10] by symmetry_of_glb ?10 ?11
1113 least_upper_bound ?13 ?14 =?= least_upper_bound ?14 ?13
1114 [14, 13] by symmetry_of_lub ?13 ?14
1116 greatest_lower_bound ?16 (greatest_lower_bound ?17 ?18)
1118 greatest_lower_bound (greatest_lower_bound ?16 ?17) ?18
1119 [18, 17, 16] by associativity_of_glb ?16 ?17 ?18
1121 least_upper_bound ?20 (least_upper_bound ?21 ?22)
1123 least_upper_bound (least_upper_bound ?20 ?21) ?22
1124 [22, 21, 20] by associativity_of_lub ?20 ?21 ?22
1126 least_upper_bound ?24 ?24 =>= ?24
1127 [24] by idempotence_of_lub ?24
1129 greatest_lower_bound ?26 ?26 =>= ?26
1130 [26] by idempotence_of_gld ?26
1132 least_upper_bound ?28 (greatest_lower_bound ?28 ?29) =>= ?28
1133 [29, 28] by lub_absorbtion ?28 ?29
1135 greatest_lower_bound ?31 (least_upper_bound ?31 ?32) =>= ?31
1136 [32, 31] by glb_absorbtion ?31 ?32
1138 multiply ?34 (least_upper_bound ?35 ?36)
1140 least_upper_bound (multiply ?34 ?35) (multiply ?34 ?36)
1141 [36, 35, 34] by monotony_lub1 ?34 ?35 ?36
1143 multiply ?38 (greatest_lower_bound ?39 ?40)
1145 greatest_lower_bound (multiply ?38 ?39) (multiply ?38 ?40)
1146 [40, 39, 38] by monotony_glb1 ?38 ?39 ?40
1148 multiply (least_upper_bound ?42 ?43) ?44
1150 least_upper_bound (multiply ?42 ?44) (multiply ?43 ?44)
1151 [44, 43, 42] by monotony_lub2 ?42 ?43 ?44
1153 multiply (greatest_lower_bound ?46 ?47) ?48
1155 greatest_lower_bound (multiply ?46 ?48) (multiply ?47 ?48)
1156 [48, 47, 46] by monotony_glb2 ?46 ?47 ?48
1158 positive_part ?50 =<= least_upper_bound ?50 identity
1161 negative_part ?52 =<= greatest_lower_bound ?52 identity
1164 least_upper_bound ?54 (greatest_lower_bound ?55 ?56)
1166 greatest_lower_bound (least_upper_bound ?54 ?55)
1167 (least_upper_bound ?54 ?56)
1168 [56, 55, 54] by lat4_3 ?54 ?55 ?56
1170 greatest_lower_bound ?58 (least_upper_bound ?59 ?60)
1172 least_upper_bound (greatest_lower_bound ?58 ?59)
1173 (greatest_lower_bound ?58 ?60)
1174 [60, 59, 58] by lat4_4 ?58 ?59 ?60
1177 a =<= multiply (positive_part a) (negative_part a)
1180 FAILURE in 1375 iterations
1187 associativity_of_glb is 84
1188 associativity_of_lub is 83
1191 glb_absorbtion is 79
1192 greatest_lower_bound is 94
1193 idempotence_of_gld is 81
1194 idempotence_of_lub is 82
1197 least_upper_bound is 86
1200 lub_absorbtion is 80
1211 symmetry_of_glb is 87
1212 symmetry_of_lub is 85
1214 Id : 4, {_}: multiply identity ?2 =>= ?2 [2] by left_identity ?2
1215 Id : 6, {_}: multiply (inverse ?4) ?4 =>= identity [4] by left_inverse ?4
1217 multiply (multiply ?6 ?7) ?8 =?= multiply ?6 (multiply ?7 ?8)
1218 [8, 7, 6] by associativity ?6 ?7 ?8
1220 greatest_lower_bound ?10 ?11 =?= greatest_lower_bound ?11 ?10
1221 [11, 10] by symmetry_of_glb ?10 ?11
1223 least_upper_bound ?13 ?14 =?= least_upper_bound ?14 ?13
1224 [14, 13] by symmetry_of_lub ?13 ?14
1226 greatest_lower_bound ?16 (greatest_lower_bound ?17 ?18)
1228 greatest_lower_bound (greatest_lower_bound ?16 ?17) ?18
1229 [18, 17, 16] by associativity_of_glb ?16 ?17 ?18
1231 least_upper_bound ?20 (least_upper_bound ?21 ?22)
1233 least_upper_bound (least_upper_bound ?20 ?21) ?22
1234 [22, 21, 20] by associativity_of_lub ?20 ?21 ?22
1236 least_upper_bound ?24 ?24 =>= ?24
1237 [24] by idempotence_of_lub ?24
1239 greatest_lower_bound ?26 ?26 =>= ?26
1240 [26] by idempotence_of_gld ?26
1242 least_upper_bound ?28 (greatest_lower_bound ?28 ?29) =>= ?28
1243 [29, 28] by lub_absorbtion ?28 ?29
1245 greatest_lower_bound ?31 (least_upper_bound ?31 ?32) =>= ?31
1246 [32, 31] by glb_absorbtion ?31 ?32
1248 multiply ?34 (least_upper_bound ?35 ?36)
1250 least_upper_bound (multiply ?34 ?35) (multiply ?34 ?36)
1251 [36, 35, 34] by monotony_lub1 ?34 ?35 ?36
1253 multiply ?38 (greatest_lower_bound ?39 ?40)
1255 greatest_lower_bound (multiply ?38 ?39) (multiply ?38 ?40)
1256 [40, 39, 38] by monotony_glb1 ?38 ?39 ?40
1258 multiply (least_upper_bound ?42 ?43) ?44
1260 least_upper_bound (multiply ?42 ?44) (multiply ?43 ?44)
1261 [44, 43, 42] by monotony_lub2 ?42 ?43 ?44
1263 multiply (greatest_lower_bound ?46 ?47) ?48
1265 greatest_lower_bound (multiply ?46 ?48) (multiply ?47 ?48)
1266 [48, 47, 46] by monotony_glb2 ?46 ?47 ?48
1267 Id : 34, {_}: greatest_lower_bound identity a =>= identity [] by p09b_1
1268 Id : 36, {_}: greatest_lower_bound identity b =>= identity [] by p09b_2
1269 Id : 38, {_}: greatest_lower_bound identity c =>= identity [] by p09b_3
1270 Id : 40, {_}: greatest_lower_bound a b =>= identity [] by p09b_4
1273 greatest_lower_bound a (multiply b c) =>= greatest_lower_bound a c
1276 FAILURE in 2472 iterations
1283 associativity_of_glb is 85
1284 associativity_of_lub is 84
1287 glb_absorbtion is 80
1288 greatest_lower_bound is 89
1289 idempotence_of_gld is 82
1290 idempotence_of_lub is 83
1293 least_upper_bound is 87
1296 lub_absorbtion is 81
1310 symmetry_of_glb is 88
1311 symmetry_of_lub is 86
1313 Id : 4, {_}: multiply identity ?2 =>= ?2 [2] by left_identity ?2
1314 Id : 6, {_}: multiply (inverse ?4) ?4 =>= identity [4] by left_inverse ?4
1316 multiply (multiply ?6 ?7) ?8 =?= multiply ?6 (multiply ?7 ?8)
1317 [8, 7, 6] by associativity ?6 ?7 ?8
1319 greatest_lower_bound ?10 ?11 =?= greatest_lower_bound ?11 ?10
1320 [11, 10] by symmetry_of_glb ?10 ?11
1322 least_upper_bound ?13 ?14 =?= least_upper_bound ?14 ?13
1323 [14, 13] by symmetry_of_lub ?13 ?14
1325 greatest_lower_bound ?16 (greatest_lower_bound ?17 ?18)
1327 greatest_lower_bound (greatest_lower_bound ?16 ?17) ?18
1328 [18, 17, 16] by associativity_of_glb ?16 ?17 ?18
1330 least_upper_bound ?20 (least_upper_bound ?21 ?22)
1332 least_upper_bound (least_upper_bound ?20 ?21) ?22
1333 [22, 21, 20] by associativity_of_lub ?20 ?21 ?22
1335 least_upper_bound ?24 ?24 =>= ?24
1336 [24] by idempotence_of_lub ?24
1338 greatest_lower_bound ?26 ?26 =>= ?26
1339 [26] by idempotence_of_gld ?26
1341 least_upper_bound ?28 (greatest_lower_bound ?28 ?29) =>= ?28
1342 [29, 28] by lub_absorbtion ?28 ?29
1344 greatest_lower_bound ?31 (least_upper_bound ?31 ?32) =>= ?31
1345 [32, 31] by glb_absorbtion ?31 ?32
1347 multiply ?34 (least_upper_bound ?35 ?36)
1349 least_upper_bound (multiply ?34 ?35) (multiply ?34 ?36)
1350 [36, 35, 34] by monotony_lub1 ?34 ?35 ?36
1352 multiply ?38 (greatest_lower_bound ?39 ?40)
1354 greatest_lower_bound (multiply ?38 ?39) (multiply ?38 ?40)
1355 [40, 39, 38] by monotony_glb1 ?38 ?39 ?40
1357 multiply (least_upper_bound ?42 ?43) ?44
1359 least_upper_bound (multiply ?42 ?44) (multiply ?43 ?44)
1360 [44, 43, 42] by monotony_lub2 ?42 ?43 ?44
1362 multiply (greatest_lower_bound ?46 ?47) ?48
1364 greatest_lower_bound (multiply ?46 ?48) (multiply ?47 ?48)
1365 [48, 47, 46] by monotony_glb2 ?46 ?47 ?48
1366 Id : 34, {_}: inverse identity =>= identity [] by p12x_1
1367 Id : 36, {_}: inverse (inverse ?51) =>= ?51 [51] by p12x_2 ?51
1369 inverse (multiply ?53 ?54) =<= multiply (inverse ?54) (inverse ?53)
1370 [54, 53] by p12x_3 ?53 ?54
1372 greatest_lower_bound a c =>= greatest_lower_bound b c
1374 Id : 42, {_}: least_upper_bound a c =>= least_upper_bound b c [] by p12x_5
1376 inverse (greatest_lower_bound ?58 ?59)
1378 least_upper_bound (inverse ?58) (inverse ?59)
1379 [59, 58] by p12x_6 ?58 ?59
1381 inverse (least_upper_bound ?61 ?62)
1383 greatest_lower_bound (inverse ?61) (inverse ?62)
1384 [62, 61] by p12x_7 ?61 ?62
1386 Id : 2, {_}: a =>= b [] by prove_p12x
1388 FAILURE in 1207 iterations
1395 associativity_of_glb is 86
1396 associativity_of_lub is 85
1397 glb_absorbtion is 81
1398 greatest_lower_bound is 94
1399 idempotence_of_gld is 83
1400 idempotence_of_lub is 84
1403 least_upper_bound is 96
1406 lub_absorbtion is 82
1415 symmetry_of_glb is 88
1416 symmetry_of_lub is 87
1418 Id : 4, {_}: multiply identity ?2 =>= ?2 [2] by left_identity ?2
1419 Id : 6, {_}: multiply (inverse ?4) ?4 =>= identity [4] by left_inverse ?4
1421 multiply (multiply ?6 ?7) ?8 =?= multiply ?6 (multiply ?7 ?8)
1422 [8, 7, 6] by associativity ?6 ?7 ?8
1424 greatest_lower_bound ?10 ?11 =?= greatest_lower_bound ?11 ?10
1425 [11, 10] by symmetry_of_glb ?10 ?11
1427 least_upper_bound ?13 ?14 =?= least_upper_bound ?14 ?13
1428 [14, 13] by symmetry_of_lub ?13 ?14
1430 greatest_lower_bound ?16 (greatest_lower_bound ?17 ?18)
1432 greatest_lower_bound (greatest_lower_bound ?16 ?17) ?18
1433 [18, 17, 16] by associativity_of_glb ?16 ?17 ?18
1435 least_upper_bound ?20 (least_upper_bound ?21 ?22)
1437 least_upper_bound (least_upper_bound ?20 ?21) ?22
1438 [22, 21, 20] by associativity_of_lub ?20 ?21 ?22
1440 least_upper_bound ?24 ?24 =>= ?24
1441 [24] by idempotence_of_lub ?24
1443 greatest_lower_bound ?26 ?26 =>= ?26
1444 [26] by idempotence_of_gld ?26
1446 least_upper_bound ?28 (greatest_lower_bound ?28 ?29) =>= ?28
1447 [29, 28] by lub_absorbtion ?28 ?29
1449 greatest_lower_bound ?31 (least_upper_bound ?31 ?32) =>= ?31
1450 [32, 31] by glb_absorbtion ?31 ?32
1452 multiply ?34 (least_upper_bound ?35 ?36)
1454 least_upper_bound (multiply ?34 ?35) (multiply ?34 ?36)
1455 [36, 35, 34] by monotony_lub1 ?34 ?35 ?36
1457 multiply ?38 (greatest_lower_bound ?39 ?40)
1459 greatest_lower_bound (multiply ?38 ?39) (multiply ?38 ?40)
1460 [40, 39, 38] by monotony_glb1 ?38 ?39 ?40
1462 multiply (least_upper_bound ?42 ?43) ?44
1464 least_upper_bound (multiply ?42 ?44) (multiply ?43 ?44)
1465 [44, 43, 42] by monotony_lub2 ?42 ?43 ?44
1467 multiply (greatest_lower_bound ?46 ?47) ?48
1469 greatest_lower_bound (multiply ?46 ?48) (multiply ?47 ?48)
1470 [48, 47, 46] by monotony_glb2 ?46 ?47 ?48
1471 Id : 34, {_}: inverse identity =>= identity [] by p20x_1
1472 Id : 36, {_}: inverse (inverse ?51) =>= ?51 [51] by p20x_1 ?51
1474 inverse (multiply ?53 ?54) =<= multiply (inverse ?54) (inverse ?53)
1475 [54, 53] by p20x_3 ?53 ?54
1478 greatest_lower_bound (least_upper_bound a identity)
1479 (least_upper_bound (inverse a) identity)
1484 FAILURE in 933 iterations
1491 associativity_of_glb is 86
1492 associativity_of_lub is 85
1493 glb_absorbtion is 81
1494 greatest_lower_bound is 95
1495 idempotence_of_gld is 83
1496 idempotence_of_lub is 84
1499 least_upper_bound is 96
1502 lub_absorbtion is 82
1509 symmetry_of_glb is 88
1510 symmetry_of_lub is 87
1512 Id : 4, {_}: multiply identity ?2 =>= ?2 [2] by left_identity ?2
1513 Id : 6, {_}: multiply (inverse ?4) ?4 =>= identity [4] by left_inverse ?4
1515 multiply (multiply ?6 ?7) ?8 =?= multiply ?6 (multiply ?7 ?8)
1516 [8, 7, 6] by associativity ?6 ?7 ?8
1518 greatest_lower_bound ?10 ?11 =?= greatest_lower_bound ?11 ?10
1519 [11, 10] by symmetry_of_glb ?10 ?11
1521 least_upper_bound ?13 ?14 =?= least_upper_bound ?14 ?13
1522 [14, 13] by symmetry_of_lub ?13 ?14
1524 greatest_lower_bound ?16 (greatest_lower_bound ?17 ?18)
1526 greatest_lower_bound (greatest_lower_bound ?16 ?17) ?18
1527 [18, 17, 16] by associativity_of_glb ?16 ?17 ?18
1529 least_upper_bound ?20 (least_upper_bound ?21 ?22)
1531 least_upper_bound (least_upper_bound ?20 ?21) ?22
1532 [22, 21, 20] by associativity_of_lub ?20 ?21 ?22
1534 least_upper_bound ?24 ?24 =>= ?24
1535 [24] by idempotence_of_lub ?24
1537 greatest_lower_bound ?26 ?26 =>= ?26
1538 [26] by idempotence_of_gld ?26
1540 least_upper_bound ?28 (greatest_lower_bound ?28 ?29) =>= ?28
1541 [29, 28] by lub_absorbtion ?28 ?29
1543 greatest_lower_bound ?31 (least_upper_bound ?31 ?32) =>= ?31
1544 [32, 31] by glb_absorbtion ?31 ?32
1546 multiply ?34 (least_upper_bound ?35 ?36)
1548 least_upper_bound (multiply ?34 ?35) (multiply ?34 ?36)
1549 [36, 35, 34] by monotony_lub1 ?34 ?35 ?36
1551 multiply ?38 (greatest_lower_bound ?39 ?40)
1553 greatest_lower_bound (multiply ?38 ?39) (multiply ?38 ?40)
1554 [40, 39, 38] by monotony_glb1 ?38 ?39 ?40
1556 multiply (least_upper_bound ?42 ?43) ?44
1558 least_upper_bound (multiply ?42 ?44) (multiply ?43 ?44)
1559 [44, 43, 42] by monotony_lub2 ?42 ?43 ?44
1561 multiply (greatest_lower_bound ?46 ?47) ?48
1563 greatest_lower_bound (multiply ?46 ?48) (multiply ?47 ?48)
1564 [48, 47, 46] by monotony_glb2 ?46 ?47 ?48
1567 multiply (least_upper_bound a identity)
1568 (inverse (greatest_lower_bound a identity))
1570 multiply (inverse (greatest_lower_bound a identity))
1571 (least_upper_bound a identity)
1574 FAILURE in 1398 iterations
1581 associativity_of_glb is 86
1582 associativity_of_lub is 85
1583 glb_absorbtion is 81
1584 greatest_lower_bound is 95
1585 idempotence_of_gld is 83
1586 idempotence_of_lub is 84
1589 least_upper_bound is 96
1592 lub_absorbtion is 82
1599 symmetry_of_glb is 88
1600 symmetry_of_lub is 87
1602 Id : 4, {_}: multiply identity ?2 =>= ?2 [2] by left_identity ?2
1603 Id : 6, {_}: multiply (inverse ?4) ?4 =>= identity [4] by left_inverse ?4
1605 multiply (multiply ?6 ?7) ?8 =?= multiply ?6 (multiply ?7 ?8)
1606 [8, 7, 6] by associativity ?6 ?7 ?8
1608 greatest_lower_bound ?10 ?11 =?= greatest_lower_bound ?11 ?10
1609 [11, 10] by symmetry_of_glb ?10 ?11
1611 least_upper_bound ?13 ?14 =?= least_upper_bound ?14 ?13
1612 [14, 13] by symmetry_of_lub ?13 ?14
1614 greatest_lower_bound ?16 (greatest_lower_bound ?17 ?18)
1616 greatest_lower_bound (greatest_lower_bound ?16 ?17) ?18
1617 [18, 17, 16] by associativity_of_glb ?16 ?17 ?18
1619 least_upper_bound ?20 (least_upper_bound ?21 ?22)
1621 least_upper_bound (least_upper_bound ?20 ?21) ?22
1622 [22, 21, 20] by associativity_of_lub ?20 ?21 ?22
1624 least_upper_bound ?24 ?24 =>= ?24
1625 [24] by idempotence_of_lub ?24
1627 greatest_lower_bound ?26 ?26 =>= ?26
1628 [26] by idempotence_of_gld ?26
1630 least_upper_bound ?28 (greatest_lower_bound ?28 ?29) =>= ?28
1631 [29, 28] by lub_absorbtion ?28 ?29
1633 greatest_lower_bound ?31 (least_upper_bound ?31 ?32) =>= ?31
1634 [32, 31] by glb_absorbtion ?31 ?32
1636 multiply ?34 (least_upper_bound ?35 ?36)
1638 least_upper_bound (multiply ?34 ?35) (multiply ?34 ?36)
1639 [36, 35, 34] by monotony_lub1 ?34 ?35 ?36
1641 multiply ?38 (greatest_lower_bound ?39 ?40)
1643 greatest_lower_bound (multiply ?38 ?39) (multiply ?38 ?40)
1644 [40, 39, 38] by monotony_glb1 ?38 ?39 ?40
1646 multiply (least_upper_bound ?42 ?43) ?44
1648 least_upper_bound (multiply ?42 ?44) (multiply ?43 ?44)
1649 [44, 43, 42] by monotony_lub2 ?42 ?43 ?44
1651 multiply (greatest_lower_bound ?46 ?47) ?48
1653 greatest_lower_bound (multiply ?46 ?48) (multiply ?47 ?48)
1654 [48, 47, 46] by monotony_glb2 ?46 ?47 ?48
1657 multiply (least_upper_bound a identity)
1658 (inverse (greatest_lower_bound a identity))
1660 multiply (inverse (greatest_lower_bound a identity))
1661 (least_upper_bound a identity)
1664 FAILURE in 1398 iterations
1671 associativity_of_glb is 85
1672 associativity_of_lub is 84
1674 glb_absorbtion is 80
1675 greatest_lower_bound is 88
1676 idempotence_of_gld is 82
1677 idempotence_of_lub is 83
1680 least_upper_bound is 94
1683 lub_absorbtion is 81
1693 symmetry_of_glb is 87
1694 symmetry_of_lub is 86
1696 Id : 4, {_}: multiply identity ?2 =>= ?2 [2] by left_identity ?2
1697 Id : 6, {_}: multiply (inverse ?4) ?4 =>= identity [4] by left_inverse ?4
1699 multiply (multiply ?6 ?7) ?8 =?= multiply ?6 (multiply ?7 ?8)
1700 [8, 7, 6] by associativity ?6 ?7 ?8
1702 greatest_lower_bound ?10 ?11 =?= greatest_lower_bound ?11 ?10
1703 [11, 10] by symmetry_of_glb ?10 ?11
1705 least_upper_bound ?13 ?14 =?= least_upper_bound ?14 ?13
1706 [14, 13] by symmetry_of_lub ?13 ?14
1708 greatest_lower_bound ?16 (greatest_lower_bound ?17 ?18)
1710 greatest_lower_bound (greatest_lower_bound ?16 ?17) ?18
1711 [18, 17, 16] by associativity_of_glb ?16 ?17 ?18
1713 least_upper_bound ?20 (least_upper_bound ?21 ?22)
1715 least_upper_bound (least_upper_bound ?20 ?21) ?22
1716 [22, 21, 20] by associativity_of_lub ?20 ?21 ?22
1718 least_upper_bound ?24 ?24 =>= ?24
1719 [24] by idempotence_of_lub ?24
1721 greatest_lower_bound ?26 ?26 =>= ?26
1722 [26] by idempotence_of_gld ?26
1724 least_upper_bound ?28 (greatest_lower_bound ?28 ?29) =>= ?28
1725 [29, 28] by lub_absorbtion ?28 ?29
1727 greatest_lower_bound ?31 (least_upper_bound ?31 ?32) =>= ?31
1728 [32, 31] by glb_absorbtion ?31 ?32
1730 multiply ?34 (least_upper_bound ?35 ?36)
1732 least_upper_bound (multiply ?34 ?35) (multiply ?34 ?36)
1733 [36, 35, 34] by monotony_lub1 ?34 ?35 ?36
1735 multiply ?38 (greatest_lower_bound ?39 ?40)
1737 greatest_lower_bound (multiply ?38 ?39) (multiply ?38 ?40)
1738 [40, 39, 38] by monotony_glb1 ?38 ?39 ?40
1740 multiply (least_upper_bound ?42 ?43) ?44
1742 least_upper_bound (multiply ?42 ?44) (multiply ?43 ?44)
1743 [44, 43, 42] by monotony_lub2 ?42 ?43 ?44
1745 multiply (greatest_lower_bound ?46 ?47) ?48
1747 greatest_lower_bound (multiply ?46 ?48) (multiply ?47 ?48)
1748 [48, 47, 46] by monotony_glb2 ?46 ?47 ?48
1749 Id : 34, {_}: inverse identity =>= identity [] by p22a_1
1750 Id : 36, {_}: inverse (inverse ?51) =>= ?51 [51] by p22a_2 ?51
1752 inverse (multiply ?53 ?54) =<= multiply (inverse ?54) (inverse ?53)
1753 [54, 53] by p22a_3 ?53 ?54
1756 least_upper_bound (least_upper_bound (multiply a b) identity)
1757 (multiply (least_upper_bound a identity)
1758 (least_upper_bound b identity))
1760 multiply (least_upper_bound a identity)
1761 (least_upper_bound b identity)
1764 FAILURE in 944 iterations
1771 associativity_of_glb is 85
1772 associativity_of_lub is 84
1774 glb_absorbtion is 80
1775 greatest_lower_bound is 93
1776 idempotence_of_gld is 82
1777 idempotence_of_lub is 83
1780 least_upper_bound is 94
1783 lub_absorbtion is 81
1790 symmetry_of_glb is 87
1791 symmetry_of_lub is 86
1793 Id : 4, {_}: multiply identity ?2 =>= ?2 [2] by left_identity ?2
1794 Id : 6, {_}: multiply (inverse ?4) ?4 =>= identity [4] by left_inverse ?4
1796 multiply (multiply ?6 ?7) ?8 =?= multiply ?6 (multiply ?7 ?8)
1797 [8, 7, 6] by associativity ?6 ?7 ?8
1799 greatest_lower_bound ?10 ?11 =?= greatest_lower_bound ?11 ?10
1800 [11, 10] by symmetry_of_glb ?10 ?11
1802 least_upper_bound ?13 ?14 =?= least_upper_bound ?14 ?13
1803 [14, 13] by symmetry_of_lub ?13 ?14
1805 greatest_lower_bound ?16 (greatest_lower_bound ?17 ?18)
1807 greatest_lower_bound (greatest_lower_bound ?16 ?17) ?18
1808 [18, 17, 16] by associativity_of_glb ?16 ?17 ?18
1810 least_upper_bound ?20 (least_upper_bound ?21 ?22)
1812 least_upper_bound (least_upper_bound ?20 ?21) ?22
1813 [22, 21, 20] by associativity_of_lub ?20 ?21 ?22
1815 least_upper_bound ?24 ?24 =>= ?24
1816 [24] by idempotence_of_lub ?24
1818 greatest_lower_bound ?26 ?26 =>= ?26
1819 [26] by idempotence_of_gld ?26
1821 least_upper_bound ?28 (greatest_lower_bound ?28 ?29) =>= ?28
1822 [29, 28] by lub_absorbtion ?28 ?29
1824 greatest_lower_bound ?31 (least_upper_bound ?31 ?32) =>= ?31
1825 [32, 31] by glb_absorbtion ?31 ?32
1827 multiply ?34 (least_upper_bound ?35 ?36)
1829 least_upper_bound (multiply ?34 ?35) (multiply ?34 ?36)
1830 [36, 35, 34] by monotony_lub1 ?34 ?35 ?36
1832 multiply ?38 (greatest_lower_bound ?39 ?40)
1834 greatest_lower_bound (multiply ?38 ?39) (multiply ?38 ?40)
1835 [40, 39, 38] by monotony_glb1 ?38 ?39 ?40
1837 multiply (least_upper_bound ?42 ?43) ?44
1839 least_upper_bound (multiply ?42 ?44) (multiply ?43 ?44)
1840 [44, 43, 42] by monotony_lub2 ?42 ?43 ?44
1842 multiply (greatest_lower_bound ?46 ?47) ?48
1844 greatest_lower_bound (multiply ?46 ?48) (multiply ?47 ?48)
1845 [48, 47, 46] by monotony_glb2 ?46 ?47 ?48
1848 greatest_lower_bound (least_upper_bound (multiply a b) identity)
1849 (multiply (least_upper_bound a identity)
1850 (least_upper_bound b identity))
1852 least_upper_bound (multiply a b) identity
1855 FAILURE in 1232 iterations
1862 associativity_of_glb is 85
1863 associativity_of_lub is 84
1865 glb_absorbtion is 80
1866 greatest_lower_bound is 92
1867 idempotence_of_gld is 82
1868 idempotence_of_lub is 83
1871 least_upper_bound is 94
1874 lub_absorbtion is 81
1881 symmetry_of_glb is 87
1882 symmetry_of_lub is 86
1884 Id : 4, {_}: multiply identity ?2 =>= ?2 [2] by left_identity ?2
1885 Id : 6, {_}: multiply (inverse ?4) ?4 =>= identity [4] by left_inverse ?4
1887 multiply (multiply ?6 ?7) ?8 =?= multiply ?6 (multiply ?7 ?8)
1888 [8, 7, 6] by associativity ?6 ?7 ?8
1890 greatest_lower_bound ?10 ?11 =?= greatest_lower_bound ?11 ?10
1891 [11, 10] by symmetry_of_glb ?10 ?11
1893 least_upper_bound ?13 ?14 =?= least_upper_bound ?14 ?13
1894 [14, 13] by symmetry_of_lub ?13 ?14
1896 greatest_lower_bound ?16 (greatest_lower_bound ?17 ?18)
1898 greatest_lower_bound (greatest_lower_bound ?16 ?17) ?18
1899 [18, 17, 16] by associativity_of_glb ?16 ?17 ?18
1901 least_upper_bound ?20 (least_upper_bound ?21 ?22)
1903 least_upper_bound (least_upper_bound ?20 ?21) ?22
1904 [22, 21, 20] by associativity_of_lub ?20 ?21 ?22
1906 least_upper_bound ?24 ?24 =>= ?24
1907 [24] by idempotence_of_lub ?24
1909 greatest_lower_bound ?26 ?26 =>= ?26
1910 [26] by idempotence_of_gld ?26
1912 least_upper_bound ?28 (greatest_lower_bound ?28 ?29) =>= ?28
1913 [29, 28] by lub_absorbtion ?28 ?29
1915 greatest_lower_bound ?31 (least_upper_bound ?31 ?32) =>= ?31
1916 [32, 31] by glb_absorbtion ?31 ?32
1918 multiply ?34 (least_upper_bound ?35 ?36)
1920 least_upper_bound (multiply ?34 ?35) (multiply ?34 ?36)
1921 [36, 35, 34] by monotony_lub1 ?34 ?35 ?36
1923 multiply ?38 (greatest_lower_bound ?39 ?40)
1925 greatest_lower_bound (multiply ?38 ?39) (multiply ?38 ?40)
1926 [40, 39, 38] by monotony_glb1 ?38 ?39 ?40
1928 multiply (least_upper_bound ?42 ?43) ?44
1930 least_upper_bound (multiply ?42 ?44) (multiply ?43 ?44)
1931 [44, 43, 42] by monotony_lub2 ?42 ?43 ?44
1933 multiply (greatest_lower_bound ?46 ?47) ?48
1935 greatest_lower_bound (multiply ?46 ?48) (multiply ?47 ?48)
1936 [48, 47, 46] by monotony_glb2 ?46 ?47 ?48
1939 least_upper_bound (multiply a b) identity
1941 multiply a (inverse (greatest_lower_bound a (inverse b)))
1944 FAILURE in 1205 iterations
1951 associativity_of_glb is 85
1952 associativity_of_lub is 84
1954 glb_absorbtion is 80
1955 greatest_lower_bound is 92
1956 idempotence_of_gld is 82
1957 idempotence_of_lub is 83
1960 least_upper_bound is 94
1963 lub_absorbtion is 81
1973 symmetry_of_glb is 87
1974 symmetry_of_lub is 86
1976 Id : 4, {_}: multiply identity ?2 =>= ?2 [2] by left_identity ?2
1977 Id : 6, {_}: multiply (inverse ?4) ?4 =>= identity [4] by left_inverse ?4
1979 multiply (multiply ?6 ?7) ?8 =?= multiply ?6 (multiply ?7 ?8)
1980 [8, 7, 6] by associativity ?6 ?7 ?8
1982 greatest_lower_bound ?10 ?11 =?= greatest_lower_bound ?11 ?10
1983 [11, 10] by symmetry_of_glb ?10 ?11
1985 least_upper_bound ?13 ?14 =?= least_upper_bound ?14 ?13
1986 [14, 13] by symmetry_of_lub ?13 ?14
1988 greatest_lower_bound ?16 (greatest_lower_bound ?17 ?18)
1990 greatest_lower_bound (greatest_lower_bound ?16 ?17) ?18
1991 [18, 17, 16] by associativity_of_glb ?16 ?17 ?18
1993 least_upper_bound ?20 (least_upper_bound ?21 ?22)
1995 least_upper_bound (least_upper_bound ?20 ?21) ?22
1996 [22, 21, 20] by associativity_of_lub ?20 ?21 ?22
1998 least_upper_bound ?24 ?24 =>= ?24
1999 [24] by idempotence_of_lub ?24
2001 greatest_lower_bound ?26 ?26 =>= ?26
2002 [26] by idempotence_of_gld ?26
2004 least_upper_bound ?28 (greatest_lower_bound ?28 ?29) =>= ?28
2005 [29, 28] by lub_absorbtion ?28 ?29
2007 greatest_lower_bound ?31 (least_upper_bound ?31 ?32) =>= ?31
2008 [32, 31] by glb_absorbtion ?31 ?32
2010 multiply ?34 (least_upper_bound ?35 ?36)
2012 least_upper_bound (multiply ?34 ?35) (multiply ?34 ?36)
2013 [36, 35, 34] by monotony_lub1 ?34 ?35 ?36
2015 multiply ?38 (greatest_lower_bound ?39 ?40)
2017 greatest_lower_bound (multiply ?38 ?39) (multiply ?38 ?40)
2018 [40, 39, 38] by monotony_glb1 ?38 ?39 ?40
2020 multiply (least_upper_bound ?42 ?43) ?44
2022 least_upper_bound (multiply ?42 ?44) (multiply ?43 ?44)
2023 [44, 43, 42] by monotony_lub2 ?42 ?43 ?44
2025 multiply (greatest_lower_bound ?46 ?47) ?48
2027 greatest_lower_bound (multiply ?46 ?48) (multiply ?47 ?48)
2028 [48, 47, 46] by monotony_glb2 ?46 ?47 ?48
2029 Id : 34, {_}: inverse identity =>= identity [] by p23_1
2030 Id : 36, {_}: inverse (inverse ?51) =>= ?51 [51] by p23_2 ?51
2032 inverse (multiply ?53 ?54) =<= multiply (inverse ?54) (inverse ?53)
2033 [54, 53] by p23_3 ?53 ?54
2036 least_upper_bound (multiply a b) identity
2038 multiply a (inverse (greatest_lower_bound a (inverse b)))
2041 FAILURE in 964 iterations
2048 associativity_of_glb is 85
2049 associativity_of_lub is 84
2051 glb_absorbtion is 80
2052 greatest_lower_bound is 89
2053 idempotence_of_gld is 82
2054 idempotence_of_lub is 83
2057 least_upper_bound is 87
2060 lub_absorbtion is 81
2068 symmetry_of_glb is 88
2069 symmetry_of_lub is 86
2071 Id : 4, {_}: multiply identity ?2 =>= ?2 [2] by left_identity ?2
2072 Id : 6, {_}: multiply (inverse ?4) ?4 =>= identity [4] by left_inverse ?4
2074 multiply (multiply ?6 ?7) ?8 =?= multiply ?6 (multiply ?7 ?8)
2075 [8, 7, 6] by associativity ?6 ?7 ?8
2077 greatest_lower_bound ?10 ?11 =?= greatest_lower_bound ?11 ?10
2078 [11, 10] by symmetry_of_glb ?10 ?11
2080 least_upper_bound ?13 ?14 =?= least_upper_bound ?14 ?13
2081 [14, 13] by symmetry_of_lub ?13 ?14
2083 greatest_lower_bound ?16 (greatest_lower_bound ?17 ?18)
2085 greatest_lower_bound (greatest_lower_bound ?16 ?17) ?18
2086 [18, 17, 16] by associativity_of_glb ?16 ?17 ?18
2088 least_upper_bound ?20 (least_upper_bound ?21 ?22)
2090 least_upper_bound (least_upper_bound ?20 ?21) ?22
2091 [22, 21, 20] by associativity_of_lub ?20 ?21 ?22
2093 least_upper_bound ?24 ?24 =>= ?24
2094 [24] by idempotence_of_lub ?24
2096 greatest_lower_bound ?26 ?26 =>= ?26
2097 [26] by idempotence_of_gld ?26
2099 least_upper_bound ?28 (greatest_lower_bound ?28 ?29) =>= ?28
2100 [29, 28] by lub_absorbtion ?28 ?29
2102 greatest_lower_bound ?31 (least_upper_bound ?31 ?32) =>= ?31
2103 [32, 31] by glb_absorbtion ?31 ?32
2105 multiply ?34 (least_upper_bound ?35 ?36)
2107 least_upper_bound (multiply ?34 ?35) (multiply ?34 ?36)
2108 [36, 35, 34] by monotony_lub1 ?34 ?35 ?36
2110 multiply ?38 (greatest_lower_bound ?39 ?40)
2112 greatest_lower_bound (multiply ?38 ?39) (multiply ?38 ?40)
2113 [40, 39, 38] by monotony_glb1 ?38 ?39 ?40
2115 multiply (least_upper_bound ?42 ?43) ?44
2117 least_upper_bound (multiply ?42 ?44) (multiply ?43 ?44)
2118 [44, 43, 42] by monotony_lub2 ?42 ?43 ?44
2120 multiply (greatest_lower_bound ?46 ?47) ?48
2122 greatest_lower_bound (multiply ?46 ?48) (multiply ?47 ?48)
2123 [48, 47, 46] by monotony_glb2 ?46 ?47 ?48
2125 greatest_lower_bound (least_upper_bound a (inverse a))
2126 (least_upper_bound b (inverse b))
2131 Id : 2, {_}: multiply a b =>= multiply b a [] by prove_p33
2133 FAILURE in 1541 iterations
2143 left_division_multiply is 88
2148 multiply_left_division is 89
2149 multiply_right_division is 86
2150 prove_moufang2 is 94
2151 right_division is 87
2152 right_division_multiply is 85
2153 right_identity is 91
2156 Id : 4, {_}: multiply identity ?2 =>= ?2 [2] by left_identity ?2
2157 Id : 6, {_}: multiply ?4 identity =>= ?4 [4] by right_identity ?4
2159 multiply ?6 (left_division ?6 ?7) =>= ?7
2160 [7, 6] by multiply_left_division ?6 ?7
2162 left_division ?9 (multiply ?9 ?10) =>= ?10
2163 [10, 9] by left_division_multiply ?9 ?10
2165 multiply (right_division ?12 ?13) ?13 =>= ?12
2166 [13, 12] by multiply_right_division ?12 ?13
2168 right_division (multiply ?15 ?16) ?16 =>= ?15
2169 [16, 15] by right_division_multiply ?15 ?16
2171 multiply ?18 (right_inverse ?18) =>= identity
2172 [18] by right_inverse ?18
2174 multiply (left_inverse ?20) ?20 =>= identity
2175 [20] by left_inverse ?20
2177 multiply (multiply ?22 (multiply ?23 ?24)) ?22
2179 multiply (multiply ?22 ?23) (multiply ?24 ?22)
2180 [24, 23, 22] by moufang1 ?22 ?23 ?24
2183 multiply (multiply (multiply a b) c) b
2185 multiply a (multiply b (multiply c b))
2186 [] by prove_moufang2
2188 FAILURE in 712 iterations
2198 left_division_multiply is 88
2203 multiply_left_division is 89
2204 multiply_right_division is 86
2205 prove_moufang1 is 94
2206 right_division is 87
2207 right_division_multiply is 85
2208 right_identity is 91
2211 Id : 4, {_}: multiply identity ?2 =>= ?2 [2] by left_identity ?2
2212 Id : 6, {_}: multiply ?4 identity =>= ?4 [4] by right_identity ?4
2214 multiply ?6 (left_division ?6 ?7) =>= ?7
2215 [7, 6] by multiply_left_division ?6 ?7
2217 left_division ?9 (multiply ?9 ?10) =>= ?10
2218 [10, 9] by left_division_multiply ?9 ?10
2220 multiply (right_division ?12 ?13) ?13 =>= ?12
2221 [13, 12] by multiply_right_division ?12 ?13
2223 right_division (multiply ?15 ?16) ?16 =>= ?15
2224 [16, 15] by right_division_multiply ?15 ?16
2226 multiply ?18 (right_inverse ?18) =>= identity
2227 [18] by right_inverse ?18
2229 multiply (left_inverse ?20) ?20 =>= identity
2230 [20] by left_inverse ?20
2232 multiply (multiply (multiply ?22 ?23) ?22) ?24
2234 multiply ?22 (multiply ?23 (multiply ?22 ?24))
2235 [24, 23, 22] by moufang3 ?22 ?23 ?24
2238 multiply (multiply a (multiply b c)) a
2240 multiply (multiply a b) (multiply c a)
2241 [] by prove_moufang1
2243 FAILURE in 674 iterations
2252 prove_these_axioms_2 is 94
2258 (multiply (inverse (multiply (inverse (multiply ?2 ?3)) ?4))
2259 (inverse (multiply ?3 (multiply (inverse ?3) ?3)))))
2262 [4, 3, 2] by single_axiom ?2 ?3 ?4
2265 multiply (multiply (inverse b2) b2) a2 =>= a2
2266 [] by prove_these_axioms_2
2268 FAILURE in 342 iterations
2278 prove_these_axioms_3 is 94
2284 (multiply (inverse (multiply (inverse (multiply ?2 ?3)) ?4))
2285 (inverse (multiply ?3 (multiply (inverse ?3) ?3)))))
2288 [4, 3, 2] by single_axiom ?2 ?3 ?4
2291 multiply (multiply a3 b3) c3 =>= multiply a3 (multiply b3 c3)
2292 [] by prove_these_axioms_3
2293 Found proof, 234.971871s
2302 prove_these_axioms_2 is 94
2311 (multiply (inverse ?3)
2312 (multiply (inverse ?4)
2313 (inverse (multiply (inverse ?4) ?4)))))))
2317 [4, 3, 2] by single_axiom ?2 ?3 ?4
2320 multiply (multiply (inverse b2) b2) a2 =>= a2
2321 [] by prove_these_axioms_2
2322 Found proof, 14.541466s
2332 prove_these_axioms_3 is 94
2341 (multiply (inverse ?3)
2342 (multiply (inverse ?4)
2343 (inverse (multiply (inverse ?4) ?4)))))))
2347 [4, 3, 2] by single_axiom ?2 ?3 ?4
2350 multiply (multiply a3 b3) c3 =>= multiply a3 (multiply b3 c3)
2351 [] by prove_these_axioms_3
2352 Found proof, 12.056212s
2362 prove_these_axioms_3 is 94
2369 (multiply (multiply ?4 (inverse ?4))
2370 (inverse (multiply ?5 (multiply ?2 ?3))))))
2373 [5, 4, 3, 2] by single_axiom ?2 ?3 ?4 ?5
2376 multiply (multiply a3 b3) c3 =>= multiply a3 (multiply b3 c3)
2377 [] by prove_these_axioms_3
2378 Found proof, 21.164993s
2388 prove_these_axioms_2 is 94
2393 (divide (divide ?2 ?2)
2394 (divide ?2 (divide ?3 (divide (divide (divide ?2 ?2) ?2) ?4))))
2398 [4, 3, 2] by single_axiom ?2 ?3 ?4
2400 multiply ?6 ?7 =<= divide ?6 (divide (divide ?8 ?8) ?7)
2401 [8, 7, 6] by multiply ?6 ?7 ?8
2403 inverse ?10 =<= divide (divide ?11 ?11) ?10
2404 [11, 10] by inverse ?10 ?11
2407 multiply (multiply (inverse b2) b2) a2 =>= a2
2408 [] by prove_these_axioms_2
2409 Found proof, 0.549585s
2420 prove_these_axioms_3 is 94
2425 (divide (divide ?2 ?2)
2426 (divide ?2 (divide ?3 (divide (divide (divide ?2 ?2) ?2) ?4))))
2430 [4, 3, 2] by single_axiom ?2 ?3 ?4
2432 multiply ?6 ?7 =<= divide ?6 (divide (divide ?8 ?8) ?7)
2433 [8, 7, 6] by multiply ?6 ?7 ?8
2435 inverse ?10 =<= divide (divide ?11 ?11) ?10
2436 [11, 10] by inverse ?10 ?11
2439 multiply (multiply a3 b3) c3 =>= multiply a3 (multiply b3 c3)
2440 [] by prove_these_axioms_3
2441 Found proof, 0.716819s
2452 prove_these_axioms_3 is 94
2456 divide (inverse (divide ?2 (divide ?3 (divide ?4 ?5))))
2457 (divide (divide ?5 ?4) ?2)
2460 [5, 4, 3, 2] by single_axiom ?2 ?3 ?4 ?5
2462 multiply ?7 ?8 =<= divide ?7 (inverse ?8)
2463 [8, 7] by multiply ?7 ?8
2466 multiply (multiply a3 b3) c3 =>= multiply a3 (multiply b3 c3)
2467 [] by prove_these_axioms_3
2468 Found proof, 115.504740s
2479 prove_these_axioms_3 is 94
2483 divide (inverse (divide (divide (divide ?2 ?3) ?4) (divide ?5 ?4)))
2487 [5, 4, 3, 2] by single_axiom ?2 ?3 ?4 ?5
2489 multiply ?7 ?8 =<= divide ?7 (inverse ?8)
2490 [8, 7] by multiply ?7 ?8
2493 multiply (multiply a3 b3) c3 =>= multiply a3 (multiply b3 c3)
2494 [] by prove_these_axioms_3
2495 Found proof, 11.020022s
2504 prove_these_axioms_2 is 94
2512 (multiply (inverse (multiply ?2 ?3)) (multiply ?3 ?2)))
2513 (multiply (inverse (multiply ?4 ?5))
2516 (multiply (multiply ?6 (inverse ?7)) (inverse ?5)))))))
2520 [7, 6, 5, 4, 3, 2] by single_axiom ?2 ?3 ?4 ?5 ?6 ?7
2523 multiply (multiply (inverse b2) b2) a2 =>= a2
2524 [] by prove_these_axioms_2
2526 FAILURE in 184 iterations
2535 prove_these_axioms_4 is 95
2543 (multiply (inverse (multiply ?2 ?3)) (multiply ?3 ?2)))
2544 (multiply (inverse (multiply ?4 ?5))
2547 (multiply (multiply ?6 (inverse ?7)) (inverse ?5)))))))
2551 [7, 6, 5, 4, 3, 2] by single_axiom ?2 ?3 ?4 ?5 ?6 ?7
2553 Id : 2, {_}: multiply a b =>= multiply b a [] by prove_these_axioms_4
2555 FAILURE in 183 iterations
2563 prove_normal_axioms_1 is 96
2567 join (meet (join (meet ?2 ?3) (meet ?3 (join ?2 ?3))) ?4)
2569 (join (meet ?2 (join (join (meet ?5 ?3) (meet ?3 ?6)) ?3))
2573 (meet (meet (join ?5 (join ?3 ?6)) (join ?7 ?3)) ?3))
2576 (meet (meet (join ?5 (join ?3 ?6)) (join ?7 ?3)) ?3))))
2577 (join ?2 (join (join (meet ?5 ?3) (meet ?3 ?6)) ?3))))
2578 (join (join (meet ?2 ?3) (meet ?3 (join ?2 ?3))) ?4))
2581 [8, 7, 6, 5, 4, 3, 2] by single_axiom ?2 ?3 ?4 ?5 ?6 ?7 ?8
2583 Id : 2, {_}: meet a a =>= a [] by prove_normal_axioms_1
2584 Found proof, 13.776911s
2593 prove_normal_axioms_8 is 94
2597 join (meet (join (meet ?2 ?3) (meet ?3 (join ?2 ?3))) ?4)
2599 (join (meet ?2 (join (join (meet ?5 ?3) (meet ?3 ?6)) ?3))
2603 (meet (meet (join ?5 (join ?3 ?6)) (join ?7 ?3)) ?3))
2606 (meet (meet (join ?5 (join ?3 ?6)) (join ?7 ?3)) ?3))))
2607 (join ?2 (join (join (meet ?5 ?3) (meet ?3 ?6)) ?3))))
2608 (join (join (meet ?2 ?3) (meet ?3 (join ?2 ?3))) ?4))
2611 [8, 7, 6, 5, 4, 3, 2] by single_axiom ?2 ?3 ?4 ?5 ?6 ?7 ?8
2613 Id : 2, {_}: join a (meet a b) =>= a [] by prove_normal_axioms_8
2614 Found proof, 13.866156s
2623 prove_wal_axioms_2 is 95
2627 join (meet (join (meet ?2 ?3) (meet ?3 (join ?2 ?3))) ?4)
2629 (join (meet ?2 (join (join (meet ?3 ?5) (meet ?6 ?3)) ?3))
2631 (join (meet ?3 (meet (meet (join ?3 ?5) (join ?6 ?3)) ?3))
2633 (join ?3 (meet (meet (join ?3 ?5) (join ?6 ?3)) ?3))))
2634 (join ?2 (join (join (meet ?3 ?5) (meet ?6 ?3)) ?3))))
2635 (join (join (meet ?2 ?3) (meet ?3 (join ?2 ?3))) ?4))
2638 [7, 6, 5, 4, 3, 2] by single_axiom ?2 ?3 ?4 ?5 ?6 ?7
2640 Id : 2, {_}: meet b a =>= meet a b [] by prove_wal_axioms_2
2641 Found proof, 13.533964s
2649 associativity_of_join is 85
2650 associativity_of_meet is 86
2653 commutativity_of_join is 87
2654 commutativity_of_meet is 88
2656 idempotence_of_join is 91
2657 idempotence_of_meet is 92
2662 Id : 4, {_}: meet ?2 ?2 =>= ?2 [2] by idempotence_of_meet ?2
2663 Id : 6, {_}: join ?4 ?4 =>= ?4 [4] by idempotence_of_join ?4
2664 Id : 8, {_}: meet ?6 (join ?6 ?7) =>= ?6 [7, 6] by absorption1 ?6 ?7
2665 Id : 10, {_}: join ?9 (meet ?9 ?10) =>= ?9 [10, 9] by absorption2 ?9 ?10
2667 meet ?12 ?13 =?= meet ?13 ?12
2668 [13, 12] by commutativity_of_meet ?12 ?13
2670 join ?15 ?16 =?= join ?16 ?15
2671 [16, 15] by commutativity_of_join ?15 ?16
2673 meet (meet ?18 ?19) ?20 =?= meet ?18 (meet ?19 ?20)
2674 [20, 19, 18] by associativity_of_meet ?18 ?19 ?20
2676 join (join ?22 ?23) ?24 =?= join ?22 (join ?23 ?24)
2677 [24, 23, 22] by associativity_of_join ?22 ?23 ?24
2679 meet ?26 (join ?27 (meet ?26 ?28))
2683 (meet ?26 (join (meet ?26 ?27) (meet ?28 (join ?26 ?27)))))
2684 [28, 27, 26] by equation_H7 ?26 ?27 ?28
2687 meet a (join b (meet a c))
2689 meet a (join (meet a (join b (meet a c))) (meet c (join a b)))
2692 FAILURE in 250 iterations
2700 associativity_of_join is 85
2701 associativity_of_meet is 86
2704 commutativity_of_join is 87
2705 commutativity_of_meet is 88
2707 idempotence_of_join is 91
2708 idempotence_of_meet is 92
2713 Id : 4, {_}: meet ?2 ?2 =>= ?2 [2] by idempotence_of_meet ?2
2714 Id : 6, {_}: join ?4 ?4 =>= ?4 [4] by idempotence_of_join ?4
2715 Id : 8, {_}: meet ?6 (join ?6 ?7) =>= ?6 [7, 6] by absorption1 ?6 ?7
2716 Id : 10, {_}: join ?9 (meet ?9 ?10) =>= ?9 [10, 9] by absorption2 ?9 ?10
2718 meet ?12 ?13 =?= meet ?13 ?12
2719 [13, 12] by commutativity_of_meet ?12 ?13
2721 join ?15 ?16 =?= join ?16 ?15
2722 [16, 15] by commutativity_of_join ?15 ?16
2724 meet (meet ?18 ?19) ?20 =?= meet ?18 (meet ?19 ?20)
2725 [20, 19, 18] by associativity_of_meet ?18 ?19 ?20
2727 join (join ?22 ?23) ?24 =?= join ?22 (join ?23 ?24)
2728 [24, 23, 22] by associativity_of_join ?22 ?23 ?24
2730 join (meet ?26 ?27) (meet ?26 ?28)
2733 (join (meet ?27 (join ?26 (meet ?27 ?28)))
2734 (meet ?28 (join ?26 ?27)))
2735 [28, 27, 26] by equation_H21 ?26 ?27 ?28
2738 meet a (join b (meet a c))
2740 meet a (join b (meet c (join (meet a (join b c)) (meet b c))))
2743 FAILURE in 250 iterations
2751 associativity_of_join is 84
2752 associativity_of_meet is 85
2755 commutativity_of_join is 86
2756 commutativity_of_meet is 87
2759 idempotence_of_join is 90
2760 idempotence_of_meet is 91
2765 Id : 4, {_}: meet ?2 ?2 =>= ?2 [2] by idempotence_of_meet ?2
2766 Id : 6, {_}: join ?4 ?4 =>= ?4 [4] by idempotence_of_join ?4
2767 Id : 8, {_}: meet ?6 (join ?6 ?7) =>= ?6 [7, 6] by absorption1 ?6 ?7
2768 Id : 10, {_}: join ?9 (meet ?9 ?10) =>= ?9 [10, 9] by absorption2 ?9 ?10
2770 meet ?12 ?13 =?= meet ?13 ?12
2771 [13, 12] by commutativity_of_meet ?12 ?13
2773 join ?15 ?16 =?= join ?16 ?15
2774 [16, 15] by commutativity_of_join ?15 ?16
2776 meet (meet ?18 ?19) ?20 =?= meet ?18 (meet ?19 ?20)
2777 [20, 19, 18] by associativity_of_meet ?18 ?19 ?20
2779 join (join ?22 ?23) ?24 =?= join ?22 (join ?23 ?24)
2780 [24, 23, 22] by associativity_of_join ?22 ?23 ?24
2782 meet ?26 (join ?27 (meet ?28 ?29))
2784 meet ?26 (join ?27 (meet ?28 (join ?27 (meet ?29 (join ?27 ?28)))))
2785 [29, 28, 27, 26] by equation_H34 ?26 ?27 ?28 ?29
2788 meet a (join b (meet a (meet c d)))
2790 meet a (join b (meet c (meet d (join a (meet b d)))))
2793 FAILURE in 250 iterations
2801 associativity_of_join is 85
2802 associativity_of_meet is 86
2805 commutativity_of_join is 87
2806 commutativity_of_meet is 88
2808 idempotence_of_join is 91
2809 idempotence_of_meet is 92
2814 Id : 4, {_}: meet ?2 ?2 =>= ?2 [2] by idempotence_of_meet ?2
2815 Id : 6, {_}: join ?4 ?4 =>= ?4 [4] by idempotence_of_join ?4
2816 Id : 8, {_}: meet ?6 (join ?6 ?7) =>= ?6 [7, 6] by absorption1 ?6 ?7
2817 Id : 10, {_}: join ?9 (meet ?9 ?10) =>= ?9 [10, 9] by absorption2 ?9 ?10
2819 meet ?12 ?13 =?= meet ?13 ?12
2820 [13, 12] by commutativity_of_meet ?12 ?13
2822 join ?15 ?16 =?= join ?16 ?15
2823 [16, 15] by commutativity_of_join ?15 ?16
2825 meet (meet ?18 ?19) ?20 =?= meet ?18 (meet ?19 ?20)
2826 [20, 19, 18] by associativity_of_meet ?18 ?19 ?20
2828 join (join ?22 ?23) ?24 =?= join ?22 (join ?23 ?24)
2829 [24, 23, 22] by associativity_of_join ?22 ?23 ?24
2831 meet ?26 (join ?27 (meet ?28 ?29))
2833 meet ?26 (join ?27 (meet ?28 (join ?27 (meet ?29 (join ?27 ?28)))))
2834 [29, 28, 27, 26] by equation_H34 ?26 ?27 ?28 ?29
2837 meet a (join b (meet a c))
2839 meet a (join b (meet a (join (meet a b) (meet c (join a b)))))
2842 FAILURE in 250 iterations
2850 associativity_of_join is 85
2851 associativity_of_meet is 86
2854 commutativity_of_join is 87
2855 commutativity_of_meet is 88
2857 idempotence_of_join is 91
2858 idempotence_of_meet is 92
2863 Id : 4, {_}: meet ?2 ?2 =>= ?2 [2] by idempotence_of_meet ?2
2864 Id : 6, {_}: join ?4 ?4 =>= ?4 [4] by idempotence_of_join ?4
2865 Id : 8, {_}: meet ?6 (join ?6 ?7) =>= ?6 [7, 6] by absorption1 ?6 ?7
2866 Id : 10, {_}: join ?9 (meet ?9 ?10) =>= ?9 [10, 9] by absorption2 ?9 ?10
2868 meet ?12 ?13 =?= meet ?13 ?12
2869 [13, 12] by commutativity_of_meet ?12 ?13
2871 join ?15 ?16 =?= join ?16 ?15
2872 [16, 15] by commutativity_of_join ?15 ?16
2874 meet (meet ?18 ?19) ?20 =?= meet ?18 (meet ?19 ?20)
2875 [20, 19, 18] by associativity_of_meet ?18 ?19 ?20
2877 join (join ?22 ?23) ?24 =?= join ?22 (join ?23 ?24)
2878 [24, 23, 22] by associativity_of_join ?22 ?23 ?24
2880 meet ?26 (join ?27 (meet ?28 (join ?26 ?29)))
2882 meet ?26 (join ?27 (meet ?28 (join ?29 (meet ?28 (join ?26 ?27)))))
2883 [29, 28, 27, 26] by equation_H40 ?26 ?27 ?28 ?29
2886 meet a (join b (meet a c))
2888 meet a (join (meet a (join b (meet a c))) (meet c (join a b)))
2891 FAILURE in 249 iterations
2899 associativity_of_join is 85
2900 associativity_of_meet is 86
2903 commutativity_of_join is 87
2904 commutativity_of_meet is 88
2906 idempotence_of_join is 91
2907 idempotence_of_meet is 92
2912 Id : 4, {_}: meet ?2 ?2 =>= ?2 [2] by idempotence_of_meet ?2
2913 Id : 6, {_}: join ?4 ?4 =>= ?4 [4] by idempotence_of_join ?4
2914 Id : 8, {_}: meet ?6 (join ?6 ?7) =>= ?6 [7, 6] by absorption1 ?6 ?7
2915 Id : 10, {_}: join ?9 (meet ?9 ?10) =>= ?9 [10, 9] by absorption2 ?9 ?10
2917 meet ?12 ?13 =?= meet ?13 ?12
2918 [13, 12] by commutativity_of_meet ?12 ?13
2920 join ?15 ?16 =?= join ?16 ?15
2921 [16, 15] by commutativity_of_join ?15 ?16
2923 meet (meet ?18 ?19) ?20 =?= meet ?18 (meet ?19 ?20)
2924 [20, 19, 18] by associativity_of_meet ?18 ?19 ?20
2926 join (join ?22 ?23) ?24 =?= join ?22 (join ?23 ?24)
2927 [24, 23, 22] by associativity_of_join ?22 ?23 ?24
2929 meet ?26 (join ?27 (meet ?28 (join ?26 ?29)))
2931 meet ?26 (join ?27 (join (meet ?26 ?28) (meet ?28 (join ?27 ?29))))
2932 [29, 28, 27, 26] by equation_H49 ?26 ?27 ?28 ?29
2935 meet a (join b (meet a c))
2937 meet a (join (meet a (join b (meet a c))) (meet c (join a b)))
2940 FAILURE in 249 iterations
2948 associativity_of_join is 85
2949 associativity_of_meet is 86
2952 commutativity_of_join is 87
2953 commutativity_of_meet is 88
2955 idempotence_of_join is 91
2956 idempotence_of_meet is 92
2961 Id : 4, {_}: meet ?2 ?2 =>= ?2 [2] by idempotence_of_meet ?2
2962 Id : 6, {_}: join ?4 ?4 =>= ?4 [4] by idempotence_of_join ?4
2963 Id : 8, {_}: meet ?6 (join ?6 ?7) =>= ?6 [7, 6] by absorption1 ?6 ?7
2964 Id : 10, {_}: join ?9 (meet ?9 ?10) =>= ?9 [10, 9] by absorption2 ?9 ?10
2966 meet ?12 ?13 =?= meet ?13 ?12
2967 [13, 12] by commutativity_of_meet ?12 ?13
2969 join ?15 ?16 =?= join ?16 ?15
2970 [16, 15] by commutativity_of_join ?15 ?16
2972 meet (meet ?18 ?19) ?20 =?= meet ?18 (meet ?19 ?20)
2973 [20, 19, 18] by associativity_of_meet ?18 ?19 ?20
2975 join (join ?22 ?23) ?24 =?= join ?22 (join ?23 ?24)
2976 [24, 23, 22] by associativity_of_join ?22 ?23 ?24
2978 meet ?26 (join ?27 (meet ?28 (join ?26 ?29)))
2980 meet ?26 (join ?27 (meet ?28 (join ?26 (meet ?28 (join ?27 ?29)))))
2981 [29, 28, 27, 26] by equation_H50 ?26 ?27 ?28 ?29
2984 meet a (join b (meet a c))
2986 meet a (join b (meet a (join (meet a b) (meet c (join a b)))))
2989 FAILURE in 250 iterations
2997 associativity_of_join is 85
2998 associativity_of_meet is 86
3001 commutativity_of_join is 87
3002 commutativity_of_meet is 88
3004 idempotence_of_join is 91
3005 idempotence_of_meet is 92
3010 Id : 4, {_}: meet ?2 ?2 =>= ?2 [2] by idempotence_of_meet ?2
3011 Id : 6, {_}: join ?4 ?4 =>= ?4 [4] by idempotence_of_join ?4
3012 Id : 8, {_}: meet ?6 (join ?6 ?7) =>= ?6 [7, 6] by absorption1 ?6 ?7
3013 Id : 10, {_}: join ?9 (meet ?9 ?10) =>= ?9 [10, 9] by absorption2 ?9 ?10
3015 meet ?12 ?13 =?= meet ?13 ?12
3016 [13, 12] by commutativity_of_meet ?12 ?13
3018 join ?15 ?16 =?= join ?16 ?15
3019 [16, 15] by commutativity_of_join ?15 ?16
3021 meet (meet ?18 ?19) ?20 =?= meet ?18 (meet ?19 ?20)
3022 [20, 19, 18] by associativity_of_meet ?18 ?19 ?20
3024 join (join ?22 ?23) ?24 =?= join ?22 (join ?23 ?24)
3025 [24, 23, 22] by associativity_of_join ?22 ?23 ?24
3027 meet ?26 (join ?27 (meet ?28 (join ?27 ?29)))
3029 meet ?26 (join ?27 (meet ?28 (join ?29 (meet ?26 ?27))))
3030 [29, 28, 27, 26] by equation_H76 ?26 ?27 ?28 ?29
3033 meet a (join b (meet a c))
3035 meet a (join (meet a (join b (meet a c))) (meet c (join a b)))
3038 FAILURE in 250 iterations
3046 associativity_of_join is 84
3047 associativity_of_meet is 85
3050 commutativity_of_join is 86
3051 commutativity_of_meet is 87
3054 idempotence_of_join is 90
3055 idempotence_of_meet is 91
3060 Id : 4, {_}: meet ?2 ?2 =>= ?2 [2] by idempotence_of_meet ?2
3061 Id : 6, {_}: join ?4 ?4 =>= ?4 [4] by idempotence_of_join ?4
3062 Id : 8, {_}: meet ?6 (join ?6 ?7) =>= ?6 [7, 6] by absorption1 ?6 ?7
3063 Id : 10, {_}: join ?9 (meet ?9 ?10) =>= ?9 [10, 9] by absorption2 ?9 ?10
3065 meet ?12 ?13 =?= meet ?13 ?12
3066 [13, 12] by commutativity_of_meet ?12 ?13
3068 join ?15 ?16 =?= join ?16 ?15
3069 [16, 15] by commutativity_of_join ?15 ?16
3071 meet (meet ?18 ?19) ?20 =?= meet ?18 (meet ?19 ?20)
3072 [20, 19, 18] by associativity_of_meet ?18 ?19 ?20
3074 join (join ?22 ?23) ?24 =?= join ?22 (join ?23 ?24)
3075 [24, 23, 22] by associativity_of_join ?22 ?23 ?24
3077 meet ?26 (join ?27 (meet ?28 (join ?27 ?29)))
3079 meet ?26 (join ?27 (meet ?28 (join ?29 (meet ?26 ?27))))
3080 [29, 28, 27, 26] by equation_H76 ?26 ?27 ?28 ?29
3083 meet a (join b (meet c (join b d)))
3085 meet a (join b (meet c (join d (meet a (meet b c)))))
3088 FAILURE in 269 iterations
3096 associativity_of_join is 84
3097 associativity_of_meet is 85
3100 commutativity_of_join is 86
3101 commutativity_of_meet is 87
3104 idempotence_of_join is 90
3105 idempotence_of_meet is 91
3110 Id : 4, {_}: meet ?2 ?2 =>= ?2 [2] by idempotence_of_meet ?2
3111 Id : 6, {_}: join ?4 ?4 =>= ?4 [4] by idempotence_of_join ?4
3112 Id : 8, {_}: meet ?6 (join ?6 ?7) =>= ?6 [7, 6] by absorption1 ?6 ?7
3113 Id : 10, {_}: join ?9 (meet ?9 ?10) =>= ?9 [10, 9] by absorption2 ?9 ?10
3115 meet ?12 ?13 =?= meet ?13 ?12
3116 [13, 12] by commutativity_of_meet ?12 ?13
3118 join ?15 ?16 =?= join ?16 ?15
3119 [16, 15] by commutativity_of_join ?15 ?16
3121 meet (meet ?18 ?19) ?20 =?= meet ?18 (meet ?19 ?20)
3122 [20, 19, 18] by associativity_of_meet ?18 ?19 ?20
3124 join (join ?22 ?23) ?24 =?= join ?22 (join ?23 ?24)
3125 [24, 23, 22] by associativity_of_join ?22 ?23 ?24
3127 meet ?26 (join ?27 (meet ?28 (join ?27 ?29)))
3129 meet ?26 (join ?27 (meet ?28 (join ?29 (meet ?26 (meet ?27 ?28)))))
3130 [29, 28, 27, 26] by equation_H77 ?26 ?27 ?28 ?29
3133 meet a (join b (meet c (join b d)))
3135 meet a (join b (meet c (join d (meet b (join a d)))))
3138 FAILURE in 269 iterations
3146 associativity_of_join is 85
3147 associativity_of_meet is 86
3150 commutativity_of_join is 87
3151 commutativity_of_meet is 88
3152 equation_H21_dual is 84
3153 idempotence_of_join is 91
3154 idempotence_of_meet is 92
3159 Id : 4, {_}: meet ?2 ?2 =>= ?2 [2] by idempotence_of_meet ?2
3160 Id : 6, {_}: join ?4 ?4 =>= ?4 [4] by idempotence_of_join ?4
3161 Id : 8, {_}: meet ?6 (join ?6 ?7) =>= ?6 [7, 6] by absorption1 ?6 ?7
3162 Id : 10, {_}: join ?9 (meet ?9 ?10) =>= ?9 [10, 9] by absorption2 ?9 ?10
3164 meet ?12 ?13 =?= meet ?13 ?12
3165 [13, 12] by commutativity_of_meet ?12 ?13
3167 join ?15 ?16 =?= join ?16 ?15
3168 [16, 15] by commutativity_of_join ?15 ?16
3170 meet (meet ?18 ?19) ?20 =?= meet ?18 (meet ?19 ?20)
3171 [20, 19, 18] by associativity_of_meet ?18 ?19 ?20
3173 join (join ?22 ?23) ?24 =?= join ?22 (join ?23 ?24)
3174 [24, 23, 22] by associativity_of_join ?22 ?23 ?24
3176 meet (join ?26 ?27) (join ?26 ?28)
3179 (meet (join ?27 (meet ?26 (join ?27 ?28)))
3180 (join ?28 (meet ?26 ?27)))
3181 [28, 27, 26] by equation_H21_dual ?26 ?27 ?28
3186 meet a (join b (meet (join a b) (join c (meet a b))))
3189 FAILURE in 268 iterations
3197 associativity_of_join is 85
3198 associativity_of_meet is 86
3201 commutativity_of_join is 87
3202 commutativity_of_meet is 88
3203 equation_H49_dual is 84
3204 idempotence_of_join is 91
3205 idempotence_of_meet is 92
3210 Id : 4, {_}: meet ?2 ?2 =>= ?2 [2] by idempotence_of_meet ?2
3211 Id : 6, {_}: join ?4 ?4 =>= ?4 [4] by idempotence_of_join ?4
3212 Id : 8, {_}: meet ?6 (join ?6 ?7) =>= ?6 [7, 6] by absorption1 ?6 ?7
3213 Id : 10, {_}: join ?9 (meet ?9 ?10) =>= ?9 [10, 9] by absorption2 ?9 ?10
3215 meet ?12 ?13 =?= meet ?13 ?12
3216 [13, 12] by commutativity_of_meet ?12 ?13
3218 join ?15 ?16 =?= join ?16 ?15
3219 [16, 15] by commutativity_of_join ?15 ?16
3221 meet (meet ?18 ?19) ?20 =?= meet ?18 (meet ?19 ?20)
3222 [20, 19, 18] by associativity_of_meet ?18 ?19 ?20
3224 join (join ?22 ?23) ?24 =?= join ?22 (join ?23 ?24)
3225 [24, 23, 22] by associativity_of_join ?22 ?23 ?24
3227 join ?26 (meet ?27 (join ?28 (meet ?26 ?29)))
3229 join ?26 (meet ?27 (meet (join ?26 ?28) (join ?28 (meet ?27 ?29))))
3230 [29, 28, 27, 26] by equation_H49_dual ?26 ?27 ?28 ?29
3235 meet a (join b (meet (join a b) (join c (meet a b))))
3238 FAILURE in 269 iterations
3246 associativity_of_join is 84
3247 associativity_of_meet is 85
3250 commutativity_of_join is 86
3251 commutativity_of_meet is 87
3253 equation_H76_dual is 83
3254 idempotence_of_join is 90
3255 idempotence_of_meet is 91
3260 Id : 4, {_}: meet ?2 ?2 =>= ?2 [2] by idempotence_of_meet ?2
3261 Id : 6, {_}: join ?4 ?4 =>= ?4 [4] by idempotence_of_join ?4
3262 Id : 8, {_}: meet ?6 (join ?6 ?7) =>= ?6 [7, 6] by absorption1 ?6 ?7
3263 Id : 10, {_}: join ?9 (meet ?9 ?10) =>= ?9 [10, 9] by absorption2 ?9 ?10
3265 meet ?12 ?13 =?= meet ?13 ?12
3266 [13, 12] by commutativity_of_meet ?12 ?13
3268 join ?15 ?16 =?= join ?16 ?15
3269 [16, 15] by commutativity_of_join ?15 ?16
3271 meet (meet ?18 ?19) ?20 =?= meet ?18 (meet ?19 ?20)
3272 [20, 19, 18] by associativity_of_meet ?18 ?19 ?20
3274 join (join ?22 ?23) ?24 =?= join ?22 (join ?23 ?24)
3275 [24, 23, 22] by associativity_of_join ?22 ?23 ?24
3277 join ?26 (meet ?27 (join ?28 (meet ?27 ?29)))
3279 join ?26 (meet ?27 (join ?28 (meet ?29 (join ?26 ?27))))
3280 [29, 28, 27, 26] by equation_H76_dual ?26 ?27 ?28 ?29
3283 meet a (join b (meet c (join a d)))
3285 meet a (join b (meet c (join d (meet c (join a b)))))
3288 FAILURE in 269 iterations
3296 associativity_of_join is 84
3297 associativity_of_meet is 85
3300 commutativity_of_join is 86
3301 commutativity_of_meet is 87
3303 equation_H79_dual is 83
3304 idempotence_of_join is 90
3305 idempotence_of_meet is 91
3310 Id : 4, {_}: meet ?2 ?2 =>= ?2 [2] by idempotence_of_meet ?2
3311 Id : 6, {_}: join ?4 ?4 =>= ?4 [4] by idempotence_of_join ?4
3312 Id : 8, {_}: meet ?6 (join ?6 ?7) =>= ?6 [7, 6] by absorption1 ?6 ?7
3313 Id : 10, {_}: join ?9 (meet ?9 ?10) =>= ?9 [10, 9] by absorption2 ?9 ?10
3315 meet ?12 ?13 =?= meet ?13 ?12
3316 [13, 12] by commutativity_of_meet ?12 ?13
3318 join ?15 ?16 =?= join ?16 ?15
3319 [16, 15] by commutativity_of_join ?15 ?16
3321 meet (meet ?18 ?19) ?20 =?= meet ?18 (meet ?19 ?20)
3322 [20, 19, 18] by associativity_of_meet ?18 ?19 ?20
3324 join (join ?22 ?23) ?24 =?= join ?22 (join ?23 ?24)
3325 [24, 23, 22] by associativity_of_join ?22 ?23 ?24
3327 join ?26 (meet ?27 (join ?28 (meet ?26 ?29)))
3329 join ?26 (meet (join ?26 (meet ?27 (join ?26 ?28))) (join ?28 ?29))
3330 [29, 28, 27, 26] by equation_H79_dual ?26 ?27 ?28 ?29
3333 meet a (join b (meet a (meet c d)))
3335 meet a (join b (meet c (join (meet a d) (meet b d))))
3338 FAILURE in 250 iterations
3340 Fatal error: exception Assert_failure("tptp_cnf.ml", 4, 25)
3346 additive_identity is 91
3347 additive_inverse is 85
3348 additive_inverse_additive_inverse is 82
3349 associativity_for_addition is 78
3351 commutativity_for_addition is 79
3355 left_additive_identity is 90
3356 left_additive_inverse is 84
3357 left_alternative is 76
3358 left_multiplicative_zero is 87
3360 prove_linearised_form1 is 92
3361 right_additive_identity is 89
3362 right_additive_inverse is 83
3363 right_alternative is 77
3364 right_multiplicative_zero is 86
3371 add additive_identity ?2 =>= ?2
3372 [2] by left_additive_identity ?2
3374 add ?4 additive_identity =>= ?4
3375 [4] by right_additive_identity ?4
3377 multiply additive_identity ?6 =>= additive_identity
3378 [6] by left_multiplicative_zero ?6
3380 multiply ?8 additive_identity =>= additive_identity
3381 [8] by right_multiplicative_zero ?8
3383 add (additive_inverse ?10) ?10 =>= additive_identity
3384 [10] by left_additive_inverse ?10
3386 add ?12 (additive_inverse ?12) =>= additive_identity
3387 [12] by right_additive_inverse ?12
3389 additive_inverse (additive_inverse ?14) =>= ?14
3390 [14] by additive_inverse_additive_inverse ?14
3392 multiply ?16 (add ?17 ?18)
3394 add (multiply ?16 ?17) (multiply ?16 ?18)
3395 [18, 17, 16] by distribute1 ?16 ?17 ?18
3397 multiply (add ?20 ?21) ?22
3399 add (multiply ?20 ?22) (multiply ?21 ?22)
3400 [22, 21, 20] by distribute2 ?20 ?21 ?22
3402 add ?24 ?25 =?= add ?25 ?24
3403 [25, 24] by commutativity_for_addition ?24 ?25
3405 add ?27 (add ?28 ?29) =?= add (add ?27 ?28) ?29
3406 [29, 28, 27] by associativity_for_addition ?27 ?28 ?29
3408 multiply (multiply ?31 ?32) ?32 =?= multiply ?31 (multiply ?32 ?32)
3409 [32, 31] by right_alternative ?31 ?32
3411 multiply (multiply ?34 ?34) ?35 =?= multiply ?34 (multiply ?34 ?35)
3412 [35, 34] by left_alternative ?34 ?35
3414 associator ?37 ?38 ?39
3416 add (multiply (multiply ?37 ?38) ?39)
3417 (additive_inverse (multiply ?37 (multiply ?38 ?39)))
3418 [39, 38, 37] by associator ?37 ?38 ?39
3422 add (multiply ?42 ?41) (additive_inverse (multiply ?41 ?42))
3423 [42, 41] by commutator ?41 ?42
3426 associator x y (add u v)
3428 add (associator x y u) (associator x y v)
3429 [] by prove_linearised_form1
3431 FAILURE in 393 iterations
3437 additive_identity is 91
3438 additive_inverse is 85
3439 additive_inverse_additive_inverse is 82
3440 associativity_for_addition is 78
3442 commutativity_for_addition is 79
3446 distributivity_of_difference1 is 71
3447 distributivity_of_difference2 is 70
3448 distributivity_of_difference3 is 69
3449 distributivity_of_difference4 is 68
3450 inverse_product1 is 73
3451 inverse_product2 is 72
3452 left_additive_identity is 90
3453 left_additive_inverse is 84
3454 left_alternative is 76
3455 left_multiplicative_zero is 87
3457 product_of_inverses is 74
3458 prove_linearised_form1 is 92
3459 right_additive_identity is 89
3460 right_additive_inverse is 83
3461 right_alternative is 77
3462 right_multiplicative_zero is 86
3469 add additive_identity ?2 =>= ?2
3470 [2] by left_additive_identity ?2
3472 add ?4 additive_identity =>= ?4
3473 [4] by right_additive_identity ?4
3475 multiply additive_identity ?6 =>= additive_identity
3476 [6] by left_multiplicative_zero ?6
3478 multiply ?8 additive_identity =>= additive_identity
3479 [8] by right_multiplicative_zero ?8
3481 add (additive_inverse ?10) ?10 =>= additive_identity
3482 [10] by left_additive_inverse ?10
3484 add ?12 (additive_inverse ?12) =>= additive_identity
3485 [12] by right_additive_inverse ?12
3487 additive_inverse (additive_inverse ?14) =>= ?14
3488 [14] by additive_inverse_additive_inverse ?14
3490 multiply ?16 (add ?17 ?18)
3492 add (multiply ?16 ?17) (multiply ?16 ?18)
3493 [18, 17, 16] by distribute1 ?16 ?17 ?18
3495 multiply (add ?20 ?21) ?22
3497 add (multiply ?20 ?22) (multiply ?21 ?22)
3498 [22, 21, 20] by distribute2 ?20 ?21 ?22
3500 add ?24 ?25 =?= add ?25 ?24
3501 [25, 24] by commutativity_for_addition ?24 ?25
3503 add ?27 (add ?28 ?29) =?= add (add ?27 ?28) ?29
3504 [29, 28, 27] by associativity_for_addition ?27 ?28 ?29
3506 multiply (multiply ?31 ?32) ?32 =?= multiply ?31 (multiply ?32 ?32)
3507 [32, 31] by right_alternative ?31 ?32
3509 multiply (multiply ?34 ?34) ?35 =?= multiply ?34 (multiply ?34 ?35)
3510 [35, 34] by left_alternative ?34 ?35
3512 associator ?37 ?38 ?39
3514 add (multiply (multiply ?37 ?38) ?39)
3515 (additive_inverse (multiply ?37 (multiply ?38 ?39)))
3516 [39, 38, 37] by associator ?37 ?38 ?39
3520 add (multiply ?42 ?41) (additive_inverse (multiply ?41 ?42))
3521 [42, 41] by commutator ?41 ?42
3523 multiply (additive_inverse ?44) (additive_inverse ?45)
3526 [45, 44] by product_of_inverses ?44 ?45
3528 multiply (additive_inverse ?47) ?48
3530 additive_inverse (multiply ?47 ?48)
3531 [48, 47] by inverse_product1 ?47 ?48
3533 multiply ?50 (additive_inverse ?51)
3535 additive_inverse (multiply ?50 ?51)
3536 [51, 50] by inverse_product2 ?50 ?51
3538 multiply ?53 (add ?54 (additive_inverse ?55))
3540 add (multiply ?53 ?54) (additive_inverse (multiply ?53 ?55))
3541 [55, 54, 53] by distributivity_of_difference1 ?53 ?54 ?55
3543 multiply (add ?57 (additive_inverse ?58)) ?59
3545 add (multiply ?57 ?59) (additive_inverse (multiply ?58 ?59))
3546 [59, 58, 57] by distributivity_of_difference2 ?57 ?58 ?59
3548 multiply (additive_inverse ?61) (add ?62 ?63)
3550 add (additive_inverse (multiply ?61 ?62))
3551 (additive_inverse (multiply ?61 ?63))
3552 [63, 62, 61] by distributivity_of_difference3 ?61 ?62 ?63
3554 multiply (add ?65 ?66) (additive_inverse ?67)
3556 add (additive_inverse (multiply ?65 ?67))
3557 (additive_inverse (multiply ?66 ?67))
3558 [67, 66, 65] by distributivity_of_difference4 ?65 ?66 ?67
3561 associator x y (add u v)
3563 add (associator x y u) (associator x y v)
3564 [] by prove_linearised_form1
3566 FAILURE in 546 iterations
3572 additive_identity is 91
3573 additive_inverse is 85
3574 additive_inverse_additive_inverse is 82
3575 associativity_for_addition is 78
3577 commutativity_for_addition is 79
3581 left_additive_identity is 90
3582 left_additive_inverse is 84
3583 left_alternative is 76
3584 left_multiplicative_zero is 87
3586 prove_linearised_form2 is 92
3587 right_additive_identity is 89
3588 right_additive_inverse is 83
3589 right_alternative is 77
3590 right_multiplicative_zero is 86
3597 add additive_identity ?2 =>= ?2
3598 [2] by left_additive_identity ?2
3600 add ?4 additive_identity =>= ?4
3601 [4] by right_additive_identity ?4
3603 multiply additive_identity ?6 =>= additive_identity
3604 [6] by left_multiplicative_zero ?6
3606 multiply ?8 additive_identity =>= additive_identity
3607 [8] by right_multiplicative_zero ?8
3609 add (additive_inverse ?10) ?10 =>= additive_identity
3610 [10] by left_additive_inverse ?10
3612 add ?12 (additive_inverse ?12) =>= additive_identity
3613 [12] by right_additive_inverse ?12
3615 additive_inverse (additive_inverse ?14) =>= ?14
3616 [14] by additive_inverse_additive_inverse ?14
3618 multiply ?16 (add ?17 ?18)
3620 add (multiply ?16 ?17) (multiply ?16 ?18)
3621 [18, 17, 16] by distribute1 ?16 ?17 ?18
3623 multiply (add ?20 ?21) ?22
3625 add (multiply ?20 ?22) (multiply ?21 ?22)
3626 [22, 21, 20] by distribute2 ?20 ?21 ?22
3628 add ?24 ?25 =?= add ?25 ?24
3629 [25, 24] by commutativity_for_addition ?24 ?25
3631 add ?27 (add ?28 ?29) =?= add (add ?27 ?28) ?29
3632 [29, 28, 27] by associativity_for_addition ?27 ?28 ?29
3634 multiply (multiply ?31 ?32) ?32 =?= multiply ?31 (multiply ?32 ?32)
3635 [32, 31] by right_alternative ?31 ?32
3637 multiply (multiply ?34 ?34) ?35 =?= multiply ?34 (multiply ?34 ?35)
3638 [35, 34] by left_alternative ?34 ?35
3640 associator ?37 ?38 ?39
3642 add (multiply (multiply ?37 ?38) ?39)
3643 (additive_inverse (multiply ?37 (multiply ?38 ?39)))
3644 [39, 38, 37] by associator ?37 ?38 ?39
3648 add (multiply ?42 ?41) (additive_inverse (multiply ?41 ?42))
3649 [42, 41] by commutator ?41 ?42
3652 associator x (add u v) y
3654 add (associator x u y) (associator x v y)
3655 [] by prove_linearised_form2
3657 FAILURE in 398 iterations
3664 additive_identity is 90
3665 additive_inverse is 91
3666 additive_inverse_additive_inverse is 82
3667 associativity_for_addition is 78
3671 commutativity_for_addition is 79
3676 left_additive_identity is 88
3677 left_additive_inverse is 84
3678 left_alternative is 76
3679 left_multiplicative_zero is 86
3681 prove_teichmuller_identity is 89
3682 right_additive_identity is 87
3683 right_additive_inverse is 83
3684 right_alternative is 77
3685 right_multiplicative_zero is 85
3688 add additive_identity ?2 =>= ?2
3689 [2] by left_additive_identity ?2
3691 add ?4 additive_identity =>= ?4
3692 [4] by right_additive_identity ?4
3694 multiply additive_identity ?6 =>= additive_identity
3695 [6] by left_multiplicative_zero ?6
3697 multiply ?8 additive_identity =>= additive_identity
3698 [8] by right_multiplicative_zero ?8
3700 add (additive_inverse ?10) ?10 =>= additive_identity
3701 [10] by left_additive_inverse ?10
3703 add ?12 (additive_inverse ?12) =>= additive_identity
3704 [12] by right_additive_inverse ?12
3706 additive_inverse (additive_inverse ?14) =>= ?14
3707 [14] by additive_inverse_additive_inverse ?14
3709 multiply ?16 (add ?17 ?18)
3711 add (multiply ?16 ?17) (multiply ?16 ?18)
3712 [18, 17, 16] by distribute1 ?16 ?17 ?18
3714 multiply (add ?20 ?21) ?22
3716 add (multiply ?20 ?22) (multiply ?21 ?22)
3717 [22, 21, 20] by distribute2 ?20 ?21 ?22
3719 add ?24 ?25 =?= add ?25 ?24
3720 [25, 24] by commutativity_for_addition ?24 ?25
3722 add ?27 (add ?28 ?29) =?= add (add ?27 ?28) ?29
3723 [29, 28, 27] by associativity_for_addition ?27 ?28 ?29
3725 multiply (multiply ?31 ?32) ?32 =?= multiply ?31 (multiply ?32 ?32)
3726 [32, 31] by right_alternative ?31 ?32
3728 multiply (multiply ?34 ?34) ?35 =?= multiply ?34 (multiply ?34 ?35)
3729 [35, 34] by left_alternative ?34 ?35
3731 associator ?37 ?38 ?39
3733 add (multiply (multiply ?37 ?38) ?39)
3734 (additive_inverse (multiply ?37 (multiply ?38 ?39)))
3735 [39, 38, 37] by associator ?37 ?38 ?39
3739 add (multiply ?42 ?41) (additive_inverse (multiply ?41 ?42))
3740 [42, 41] by commutator ?41 ?42
3744 (add (associator (multiply a b) c d)
3745 (associator a b (multiply c d)))
3748 (add (associator a (multiply b c) d)
3749 (multiply a (associator b c d)))
3750 (multiply (associator a b c) d)))
3753 [] by prove_teichmuller_identity
3755 FAILURE in 406 iterations
3761 additive_identity is 93
3762 additive_inverse is 87
3763 additive_inverse_additive_inverse is 84
3764 associativity_for_addition is 80
3766 commutativity_for_addition is 81
3773 distributivity_of_difference1 is 72
3774 distributivity_of_difference2 is 71
3775 distributivity_of_difference3 is 70
3776 distributivity_of_difference4 is 69
3777 inverse_product1 is 74
3778 inverse_product2 is 73
3779 left_additive_identity is 91
3780 left_additive_inverse is 86
3781 left_alternative is 78
3782 left_multiplicative_zero is 89
3784 product_of_inverses is 75
3785 prove_right_moufang is 94
3786 right_additive_identity is 90
3787 right_additive_inverse is 85
3788 right_alternative is 79
3789 right_multiplicative_zero is 88
3792 add additive_identity ?2 =>= ?2
3793 [2] by left_additive_identity ?2
3795 add ?4 additive_identity =>= ?4
3796 [4] by right_additive_identity ?4
3798 multiply additive_identity ?6 =>= additive_identity
3799 [6] by left_multiplicative_zero ?6
3801 multiply ?8 additive_identity =>= additive_identity
3802 [8] by right_multiplicative_zero ?8
3804 add (additive_inverse ?10) ?10 =>= additive_identity
3805 [10] by left_additive_inverse ?10
3807 add ?12 (additive_inverse ?12) =>= additive_identity
3808 [12] by right_additive_inverse ?12
3810 additive_inverse (additive_inverse ?14) =>= ?14
3811 [14] by additive_inverse_additive_inverse ?14
3813 multiply ?16 (add ?17 ?18)
3815 add (multiply ?16 ?17) (multiply ?16 ?18)
3816 [18, 17, 16] by distribute1 ?16 ?17 ?18
3818 multiply (add ?20 ?21) ?22
3820 add (multiply ?20 ?22) (multiply ?21 ?22)
3821 [22, 21, 20] by distribute2 ?20 ?21 ?22
3823 add ?24 ?25 =?= add ?25 ?24
3824 [25, 24] by commutativity_for_addition ?24 ?25
3826 add ?27 (add ?28 ?29) =?= add (add ?27 ?28) ?29
3827 [29, 28, 27] by associativity_for_addition ?27 ?28 ?29
3829 multiply (multiply ?31 ?32) ?32 =?= multiply ?31 (multiply ?32 ?32)
3830 [32, 31] by right_alternative ?31 ?32
3832 multiply (multiply ?34 ?34) ?35 =?= multiply ?34 (multiply ?34 ?35)
3833 [35, 34] by left_alternative ?34 ?35
3835 associator ?37 ?38 ?39
3837 add (multiply (multiply ?37 ?38) ?39)
3838 (additive_inverse (multiply ?37 (multiply ?38 ?39)))
3839 [39, 38, 37] by associator ?37 ?38 ?39
3843 add (multiply ?42 ?41) (additive_inverse (multiply ?41 ?42))
3844 [42, 41] by commutator ?41 ?42
3846 multiply (additive_inverse ?44) (additive_inverse ?45)
3849 [45, 44] by product_of_inverses ?44 ?45
3851 multiply (additive_inverse ?47) ?48
3853 additive_inverse (multiply ?47 ?48)
3854 [48, 47] by inverse_product1 ?47 ?48
3856 multiply ?50 (additive_inverse ?51)
3858 additive_inverse (multiply ?50 ?51)
3859 [51, 50] by inverse_product2 ?50 ?51
3861 multiply ?53 (add ?54 (additive_inverse ?55))
3863 add (multiply ?53 ?54) (additive_inverse (multiply ?53 ?55))
3864 [55, 54, 53] by distributivity_of_difference1 ?53 ?54 ?55
3866 multiply (add ?57 (additive_inverse ?58)) ?59
3868 add (multiply ?57 ?59) (additive_inverse (multiply ?58 ?59))
3869 [59, 58, 57] by distributivity_of_difference2 ?57 ?58 ?59
3871 multiply (additive_inverse ?61) (add ?62 ?63)
3873 add (additive_inverse (multiply ?61 ?62))
3874 (additive_inverse (multiply ?61 ?63))
3875 [63, 62, 61] by distributivity_of_difference3 ?61 ?62 ?63
3877 multiply (add ?65 ?66) (additive_inverse ?67)
3879 add (additive_inverse (multiply ?65 ?67))
3880 (additive_inverse (multiply ?66 ?67))
3881 [67, 66, 65] by distributivity_of_difference4 ?65 ?66 ?67
3884 multiply cz (multiply cx (multiply cy cx))
3886 multiply (multiply (multiply cz cx) cy) cx
3887 [] by prove_right_moufang
3889 FAILURE in 538 iterations
3895 additive_identity is 92
3896 additive_inverse is 86
3897 additive_inverse_additive_inverse is 83
3898 associativity_for_addition is 79
3900 commutativity_for_addition is 80
3904 distributivity_of_difference1 is 72
3905 distributivity_of_difference2 is 71
3906 distributivity_of_difference3 is 70
3907 distributivity_of_difference4 is 69
3908 inverse_product1 is 74
3909 inverse_product2 is 73
3910 left_additive_identity is 90
3911 left_additive_inverse is 85
3912 left_alternative is 77
3913 left_multiplicative_zero is 88
3915 product_of_inverses is 75
3916 prove_left_moufang is 93
3917 right_additive_identity is 89
3918 right_additive_inverse is 84
3919 right_alternative is 78
3920 right_multiplicative_zero is 87
3926 add additive_identity ?2 =>= ?2
3927 [2] by left_additive_identity ?2
3929 add ?4 additive_identity =>= ?4
3930 [4] by right_additive_identity ?4
3932 multiply additive_identity ?6 =>= additive_identity
3933 [6] by left_multiplicative_zero ?6
3935 multiply ?8 additive_identity =>= additive_identity
3936 [8] by right_multiplicative_zero ?8
3938 add (additive_inverse ?10) ?10 =>= additive_identity
3939 [10] by left_additive_inverse ?10
3941 add ?12 (additive_inverse ?12) =>= additive_identity
3942 [12] by right_additive_inverse ?12
3944 additive_inverse (additive_inverse ?14) =>= ?14
3945 [14] by additive_inverse_additive_inverse ?14
3947 multiply ?16 (add ?17 ?18)
3949 add (multiply ?16 ?17) (multiply ?16 ?18)
3950 [18, 17, 16] by distribute1 ?16 ?17 ?18
3952 multiply (add ?20 ?21) ?22
3954 add (multiply ?20 ?22) (multiply ?21 ?22)
3955 [22, 21, 20] by distribute2 ?20 ?21 ?22
3957 add ?24 ?25 =?= add ?25 ?24
3958 [25, 24] by commutativity_for_addition ?24 ?25
3960 add ?27 (add ?28 ?29) =?= add (add ?27 ?28) ?29
3961 [29, 28, 27] by associativity_for_addition ?27 ?28 ?29
3963 multiply (multiply ?31 ?32) ?32 =?= multiply ?31 (multiply ?32 ?32)
3964 [32, 31] by right_alternative ?31 ?32
3966 multiply (multiply ?34 ?34) ?35 =?= multiply ?34 (multiply ?34 ?35)
3967 [35, 34] by left_alternative ?34 ?35
3969 associator ?37 ?38 ?39
3971 add (multiply (multiply ?37 ?38) ?39)
3972 (additive_inverse (multiply ?37 (multiply ?38 ?39)))
3973 [39, 38, 37] by associator ?37 ?38 ?39
3977 add (multiply ?42 ?41) (additive_inverse (multiply ?41 ?42))
3978 [42, 41] by commutator ?41 ?42
3980 multiply (additive_inverse ?44) (additive_inverse ?45)
3983 [45, 44] by product_of_inverses ?44 ?45
3985 multiply (additive_inverse ?47) ?48
3987 additive_inverse (multiply ?47 ?48)
3988 [48, 47] by inverse_product1 ?47 ?48
3990 multiply ?50 (additive_inverse ?51)
3992 additive_inverse (multiply ?50 ?51)
3993 [51, 50] by inverse_product2 ?50 ?51
3995 multiply ?53 (add ?54 (additive_inverse ?55))
3997 add (multiply ?53 ?54) (additive_inverse (multiply ?53 ?55))
3998 [55, 54, 53] by distributivity_of_difference1 ?53 ?54 ?55
4000 multiply (add ?57 (additive_inverse ?58)) ?59
4002 add (multiply ?57 ?59) (additive_inverse (multiply ?58 ?59))
4003 [59, 58, 57] by distributivity_of_difference2 ?57 ?58 ?59
4005 multiply (additive_inverse ?61) (add ?62 ?63)
4007 add (additive_inverse (multiply ?61 ?62))
4008 (additive_inverse (multiply ?61 ?63))
4009 [63, 62, 61] by distributivity_of_difference3 ?61 ?62 ?63
4011 multiply (add ?65 ?66) (additive_inverse ?67)
4013 add (additive_inverse (multiply ?65 ?67))
4014 (additive_inverse (multiply ?66 ?67))
4015 [67, 66, 65] by distributivity_of_difference4 ?65 ?66 ?67
4018 associator x (multiply y x) z =<= multiply x (associator x y z)
4019 [] by prove_left_moufang
4021 FAILURE in 537 iterations
4027 additive_identity is 93
4028 additive_inverse is 87
4029 additive_inverse_additive_inverse is 84
4030 associativity_for_addition is 80
4032 commutativity_for_addition is 81
4036 distributivity_of_difference1 is 72
4037 distributivity_of_difference2 is 71
4038 distributivity_of_difference3 is 70
4039 distributivity_of_difference4 is 69
4040 inverse_product1 is 74
4041 inverse_product2 is 73
4042 left_additive_identity is 91
4043 left_additive_inverse is 86
4044 left_alternative is 78
4045 left_multiplicative_zero is 89
4047 product_of_inverses is 75
4048 prove_middle_moufang is 94
4049 right_additive_identity is 90
4050 right_additive_inverse is 85
4051 right_alternative is 79
4052 right_multiplicative_zero is 88
4058 add additive_identity ?2 =>= ?2
4059 [2] by left_additive_identity ?2
4061 add ?4 additive_identity =>= ?4
4062 [4] by right_additive_identity ?4
4064 multiply additive_identity ?6 =>= additive_identity
4065 [6] by left_multiplicative_zero ?6
4067 multiply ?8 additive_identity =>= additive_identity
4068 [8] by right_multiplicative_zero ?8
4070 add (additive_inverse ?10) ?10 =>= additive_identity
4071 [10] by left_additive_inverse ?10
4073 add ?12 (additive_inverse ?12) =>= additive_identity
4074 [12] by right_additive_inverse ?12
4076 additive_inverse (additive_inverse ?14) =>= ?14
4077 [14] by additive_inverse_additive_inverse ?14
4079 multiply ?16 (add ?17 ?18)
4081 add (multiply ?16 ?17) (multiply ?16 ?18)
4082 [18, 17, 16] by distribute1 ?16 ?17 ?18
4084 multiply (add ?20 ?21) ?22
4086 add (multiply ?20 ?22) (multiply ?21 ?22)
4087 [22, 21, 20] by distribute2 ?20 ?21 ?22
4089 add ?24 ?25 =?= add ?25 ?24
4090 [25, 24] by commutativity_for_addition ?24 ?25
4092 add ?27 (add ?28 ?29) =?= add (add ?27 ?28) ?29
4093 [29, 28, 27] by associativity_for_addition ?27 ?28 ?29
4095 multiply (multiply ?31 ?32) ?32 =?= multiply ?31 (multiply ?32 ?32)
4096 [32, 31] by right_alternative ?31 ?32
4098 multiply (multiply ?34 ?34) ?35 =?= multiply ?34 (multiply ?34 ?35)
4099 [35, 34] by left_alternative ?34 ?35
4101 associator ?37 ?38 ?39
4103 add (multiply (multiply ?37 ?38) ?39)
4104 (additive_inverse (multiply ?37 (multiply ?38 ?39)))
4105 [39, 38, 37] by associator ?37 ?38 ?39
4109 add (multiply ?42 ?41) (additive_inverse (multiply ?41 ?42))
4110 [42, 41] by commutator ?41 ?42
4112 multiply (additive_inverse ?44) (additive_inverse ?45)
4115 [45, 44] by product_of_inverses ?44 ?45
4117 multiply (additive_inverse ?47) ?48
4119 additive_inverse (multiply ?47 ?48)
4120 [48, 47] by inverse_product1 ?47 ?48
4122 multiply ?50 (additive_inverse ?51)
4124 additive_inverse (multiply ?50 ?51)
4125 [51, 50] by inverse_product2 ?50 ?51
4127 multiply ?53 (add ?54 (additive_inverse ?55))
4129 add (multiply ?53 ?54) (additive_inverse (multiply ?53 ?55))
4130 [55, 54, 53] by distributivity_of_difference1 ?53 ?54 ?55
4132 multiply (add ?57 (additive_inverse ?58)) ?59
4134 add (multiply ?57 ?59) (additive_inverse (multiply ?58 ?59))
4135 [59, 58, 57] by distributivity_of_difference2 ?57 ?58 ?59
4137 multiply (additive_inverse ?61) (add ?62 ?63)
4139 add (additive_inverse (multiply ?61 ?62))
4140 (additive_inverse (multiply ?61 ?63))
4141 [63, 62, 61] by distributivity_of_difference3 ?61 ?62 ?63
4143 multiply (add ?65 ?66) (additive_inverse ?67)
4145 add (additive_inverse (multiply ?65 ?67))
4146 (additive_inverse (multiply ?66 ?67))
4147 [67, 66, 65] by distributivity_of_difference4 ?65 ?66 ?67
4150 multiply (multiply x y) (multiply z x)
4152 multiply (multiply x (multiply y z)) x
4153 [] by prove_middle_moufang
4155 FAILURE in 537 iterations
4157 Fatal error: exception Assert_failure("tptp_cnf.ml", 4, 25)
4165 associativity_of_add is 92
4168 commutativity_of_add is 93
4171 prove_huntingtons_axiom is 94
4174 Id : 4, {_}: add ?2 ?3 =?= add ?3 ?2 [3, 2] by commutativity_of_add ?2 ?3
4176 add (add ?5 ?6) ?7 =?= add ?5 (add ?6 ?7)
4177 [7, 6, 5] by associativity_of_add ?5 ?6 ?7
4179 negate (add (negate (add ?9 ?10)) (negate (add ?9 (negate ?10))))
4182 [10, 9] by robbins_axiom ?9 ?10
4183 Id : 10, {_}: add c d =>= d [] by absorbtion
4186 add (negate (add a (negate b)))
4187 (negate (add (negate a) (negate b)))
4190 [] by prove_huntingtons_axiom
4192 FAILURE in 163 iterations
4199 associativity_of_add is 95
4201 commutativity_of_add is 96
4204 prove_idempotence is 97
4207 Id : 4, {_}: add ?3 ?4 =?= add ?4 ?3 [4, 3] by commutativity_of_add ?3 ?4
4209 add (add ?6 ?7) ?8 =?= add ?6 (add ?7 ?8)
4210 [8, 7, 6] by associativity_of_add ?6 ?7 ?8
4212 negate (add (negate (add ?10 ?11)) (negate (add ?10 (negate ?11))))
4215 [11, 10] by robbins_axiom ?10 ?11
4216 Id : 10, {_}: add c d =>= d [] by absorbtion
4218 Id : 2, {_}: add ?1 ?1 =>= ?1 [1] by prove_idempotence ?1
4220 FAILURE in 253 iterations