set(para_into). set(para_from_vars). set(para_into_vars). set(para_from_right). set(para_into_left). clear(para_into_right). clear(para_from_left). set(sos_queue). assign(max_mem, 100000). assign(max_kept, 35000). list(usable). p(x,x,y) = y. p(x,y,y) = x. p(x,y,x) = x. f2(x) = x. f1(x) = x. end_of_list. list(sos). p(x,x,y) = y. p(x,y,y) = x. p(x,y,x) = x. end_of_list. % We wish to discard generated clauses with nonvariable % terms as argument of f1 or f2. Also, discard clasues % with more than 3 occurrences of (f1 or f2). assign(max_weight, 2500). weight_list(pick_and_purge). weight(f1(f1($(0))), 3000). weight(f1(f2($(0))), 3000). weight(f2(f1($(0))), 3000). weight(f2(f2($(0))), 3000). weight(f1(p($(0),$(0),$(0))), 3000). weight(f2(p($(0),$(0),$(0))), 3000). weight(f1($(1)), 1000). weight(f2($(1)), 1000). end_of_list.