op(400, xfx, -). % infix operator clear(print_kept). clear(print_new_demod). clear(print_back_demod). assign(pick_given_ratio, 4). assign(max_mem, 20000). set(knuth_bendix). set(hyper_res). set(order_history). set(unit_deletion). set(para_from_units_only). set(para_into_units_only). assign(max_weight, 11). list(usable). x = x. end_of_list. list(sos). x - y != z - u | u - (z - x) = y. end_of_list. list(passive). A - (B - (C - (A - B))) != C. end_of_list.