op(400, xfx, ^). op(400, xfx, v). set(knuth_bendix). clear(print_kept). clear(print_new_demod). clear(print_back_demod). assign(max_weight, 17). assign(pick_given_ratio, 5). assign(max_mem, 16000). % assign(max_proofs, 100). set(hyper_res). set(order_history). set(para_from_units_only). set(para_into_units_only). list(sos). (x^y) v (x^ (x v y))=x. (x^x) v (y^ (x v x))=x. (x^y) v (y^ (x v y))=y. ((x ^ y) v (y ^ z)) v y = y. % 3 ((x v (y v z)) ^ (u v y)) ^ y = y. % 26 end_of_list. % list(passive). % % The four absorption laws of Ralph McKenzie: % % b v (a ^ (b ^ c)) != b | $Ans(McKenzie_L1). % L1 % b ^ (a v (b v c)) != b | $Ans(McKenzie_L2). % L2 % ((a ^ b) v (b ^ c)) v b != b | $Ans(McKenzie_L3). % L3 % ((a v b) ^ (b v c)) ^ b != b | $Ans(McKenzie_L4). % L4 % % ((b ^ a) v (b ^ c)) v b != b | $Ans(McKenzie_L3m). % L3m % ((b v a) ^ (b v c)) ^ b != b | $Ans(McKenzie_L4m). % L4m % end_of_list. list(usable). x = x. b ^ (a v (b v c)) != b | ((b v a) ^ (b v c)) ^ b != b. end_of_list.