set(hyper_res). assign(max_weight, 22). % limits the purge_gen weight of retained clauses % With OTTER 3.0.4, the following command must be modified; see Section 8.3.4. assign(reduce_weight_limit, 100016). % With OTTER 3.0.4, the following command must be modified; see Section 8.3.6. assign(max_proofs, 0). clear(print_kept). clear(back_sub). assign(max_mem, 128000). assign(report, 900). assign(max_distinct_vars, 4). assign(pick_given_ratio, 3). set(order_history). set(input_sos_first). % With OTTER 3.0.4, remove the following unneeded command; see Section 8.3.2. set(print_level). % OTTER 3.0.4 does not accept the preceding option; level is always computed. weight_list(pick_given). % Following are four lemmas to be proved. weight(P(i(n(n(x)),x)), 2). weight(P(i(x,n(n(x)))), 2). weight(P(i(i(x,y),i(i(z,x),i(z,y)))), 2). weight(P(i(i(x,y),i(n(y),n(x)))), 2). % Following are the axioms for many-valued. weight(P(i(x,i(y,x))), 2). weight(P(i(i(x,y),i(i(y,z),i(x,z)))), 2). weight(P(i(i(i(x,y),y),i(i(y,x),x))), 2). weight(P(i(i(n(x),n(y)),i(y,x))), 2). % Following is for recursive tail strategy. weight(i($(1),$(2)),1). end_of_list. % Used to complete applications of inference rules. list(usable). -P(i(x,y)) | -P(x) | P(y). end_of_list. % Used to initiate applications of inference rules. list(sos). P(i(x,i(y,x))). P(i(i(x,y),i(i(y,z),i(x,z)))). P(i(i(i(x,y),y),i(i(y,x),x))). P(i(i(n(x),n(y)),i(y,x))). end_of_list. % Used mainly to detect proof completion and to monitor progress. list(passive). -P(i(n(n(a)),a)) | $ANS(lemma_24). -P(i(a,n(n(a)))) | $ANS(lemma_29). -P(i(i(a,b),i(i(c,a),i(c,b)))) | $ANS(lemma_25). -P(i(i(a,b),i(n(b),n(a)))) | $ANS(lemma_36). end_of_list. % Following purges unwanted formulas. list(demodulators). (n(n(n(x))) = junk). (i(i(x,x),y) = junk). (i(y,i(x,x)) = junk). (i(junk,x) = junk). (i(x,junk) = junk). (n(junk) = junk). (P(junk) = $T). end_of_list.