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