op(400, xfx, /). % infix operators 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, 45). list(usable). x = x. end_of_list. list(sos). x / y != z / u | y / (((z / z) / z) / ((x / x) / x)) = u. end_of_list. list(passive). A / A != B / B. end_of_list.