assign(max_mem, 24000). assign(max_seconds, 1800). clear(print_kept). clear(print_new_demod). clear(print_back_demod). clear(print_given). set(para_pairs). % delete for given algorithm set(basic_paramod). set(functional_subsume). set(prime_paramod). assign(ac_superset_limit, 0). assign(pick_given_ratio, 4). %%%%%%%%%%%%%%%%%%%%%% op(400, xfx, [*,+,^,v,/,\,#]). % infix operators assoc_comm(^). assoc_comm(v). assign(max_weight, 23). end_of_commands. list(sos). x ^ x = x. % x ^ y = y ^ x. % commutativity % (x ^ y) ^ z = x ^ (y ^ z). % associativity x v x = x. % x v y = y v x. % commutativity % (x v y) v z = x v (y v z). % associativity x ^ (x v y) = x. x v (x ^ y) = x. (((x ^ y) v z) ^ y) v (z ^ x) = (((x v y) ^ z) v y) ^ (z v x). A ^ (B v C) != (A ^ B) v (A ^ C). % A v (B ^ C) != (A v B) ^ (A v C). end_of_list.