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, 19). end_of_commands. 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 (x ^ z)) = x ^ (y v z). A ^ (B v C) != (A ^ B) v (A ^ C). end_of_list.