op(400,xfx,^). op(400,xfx,v). set(knuth_bendix). clear(print_kept). clear(print_new_demod). clear(print_back_demod). assign(pick_given_ratio, 4). assign(max_weight, 23). assign(max_mem, 16000). set(control_memory). list(usable). x = x. end_of_list. list(sos). x ^ x = x. x ^ y = y ^ x. (x ^ y) ^ z = x ^ (y ^ z). x v x = x. x v y = y v x. (x v y) v z = x v (y v z). (x ^ (y v z)) v (x ^ y) = x ^ (y v z). (x v (y ^ z)) ^ (x v y) = x v (y ^ z). (x ^ y) v (z ^ (x v y)) = (x v y) ^ (z v (x ^ y)). A ^ (B v (A ^ C)) != (A ^ B) v (A ^ C). end_of_list. list(passive). end_of_list.