% Input File for Studying Many-Valued Sentential Calculus with OTTER 3.0 set(hyper_res). assign(max_weight, 22). assign(change_limit_after, 1000). assign(new_max_weight, 16). % The following is set to 4 rather than 5, for MV5 is very difficult to prove. assign(max_proofs, 4). clear(print_kept). clear(back_sub). assign(max_mem, 24000). assign(report, 900). assign(max_distinct_vars, 4). assign(pick_given_ratio, 3). set(order_history). set(input_sos_first). weight_list(pick_given). % Following are four lemmas to prove. 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). % The following is a difficult theorem to prove. weight(P(i(i(i(x,y),i(y,x)),i(y,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. list(usable). -P(i(x,y)) | -P(x) | P(y). end_of_list. 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. list(passive). % The following four clauses are negations of four lemmas to prove. -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). % The following clause is the negation of a difficult theorem to prove. -P(i(i(i(a,b),i(b,a)),i(b,a))) | $ANS(thm_MV5). end_of_list. list(demodulators). (n(n(n(x))) = junk). (i(i(x,x),y) = junk). (i(y,i(x,x)) = junk). (i(n(i(x,x)),y) = junk). (i(y,n(i(x,x))) = junk). (i(junk,x) = junk). (i(x,junk) = junk). (n(junk) = junk). (P(junk) = $T). end_of_list.