set(lrpo). assign(max_mem, 24000). assign(max_seconds, 1800). clear(print_kept). clear(print_new_demod). clear(print_back_demod). clear(print_given). set(basic_paramod). set(functional_subsume). set(ordered_paramod). set(prime_paramod). assign(pick_given_ratio, 4). set(para_pairs). % delete for given algorithm %%%%%%%%%%%%%%%%%%%%%% op(400, xfx, [*,+,^,v,/,\,#]). % infix operators op(300,yf,@). % postfix operator assign(max_weight, 21). end_of_commands. list(sos). 1 * x = x. x@ * x = 1. % (x * (y * z)) * x = (x * y) * (z * x). % Moufang 1 % ((x * y) * z) * y = x * (y * (z * y)). % Moufang 2 ((x * y) * x) * z = x * (y * (x * z)). % Moufang 3 % (A * (B * C)) * A != (A * B) * (C * A). % Moufang 1 ((A * B) * C) * B != A * (B * (C * B)). % Moufang 2 % ((A * B) * A) * C != A * (B * (A * C)). % Moufang 3 end_of_list.