% Input File for Rigorous Proof Checking the deducibility of various % axiom systems of two-valued sentential calculus set(hyper_res). % clear(print_kept). assign(report, 60). assign(max_mem, 8000). assign(max_weight, 80). assign(max_proofs, -1). set(input_sos_first). set(order_history). weight_list(pick_and_purge). weight(P(rew($(0),$(0)),$(1)), 99). end_of_list. list(usable). -P(u,i(x,y)) | -P(v,x) | P(rew(u,v),y). -P(x,i(q,i(p,q))) | -P(y,i(i(p,i(q,r)),i(i(p,q),i(p,r)))) | -P(z,i(i(n(p),n(q)),i(q,p))) | $ANSWER(step_allBEH_Church_FL_18_35_49). -P(x,i(q,i(p,q))) | -P(y,i(i(p,i(q,r)),i(i(p,q),i(p,r)))) | -P(z,i(n(n(p)),p)) | -P(u,i(p,n(n(p)))) | -P(v,i(i(p,q),i(n(q),n(p)))) | -P(w,i(i(p,i(q,r)),i(q,i(p,r)))) | $ANSWER(step_allFrege_18_35_39_40_46_21). % 21 is dependent. -P(x,i(q,i(p,q))) | -P(y,i(i(p,i(q,r)),i(q,i(p,r)))) | -P(z,i(i(q,r),i(i(p,q),i(p,r)))) | -P(u,i(p,i(n(p),q))) | -P(v,i(i(p,q),i(i(n(p),q),q))) | -P(w,i(i(p,i(p,q)),i(p,q))) | $ANSWER(step_allHilbert_18_21_22_3_54_30). % 30 is dependent. -P(x,i(i(i(p,q),r),i(q,r))) | -P(y,i(i(i(p,q),r),i(n(p),r))) | -P(z,i(i(n(p),r),i(i(q,r),i(i(p,q),r)))) | $ANSWER(step_allLuka_x_19_37_59). -P(x,i(i(i(p,q),r),i(q,r))) | -P(y,i(i(i(p,q),r),i(n(p),r))) | -P(z,i(i(s,i(n(p),r)),i(s,i(i(q,r),i(i(p,q),r))))) | $ANSWER(step_allWos_x_19_37_60). end_of_list. list(sos). P(c1,i(i(x,y),i(i(y,z),i(x,z)))). P(c2,i(i(n(x),x),x)). P(c3,i(x,i(n(x),y))). end_of_list. list(passive). % -P(x,i(i(i(i(q,r),i(p,r)),s),i(i(p,q),s))) | $ANS(neg_th_04). % -P(x,i(i(p,i(q,r)),i(i(s,q),i(p,i(s,r))))) | $ANS(neg_th_05). % -P(x,i(i(p,q),i(i(i(p,r),s),i(i(q,r),s)))) | $ANS(neg_th_06). % -P(x,i(i(t,i(i(p,r),s)),i(i(p,q),i(t,i(i(q,r),s))))) | $ANS(neg_th_07). % -P(x,i(i(q,r),i(i(p,q),i(i(r,s),i(p,s))))) | $ANS(neg_th_08). % -P(x,i(i(i(n(p),q),r),i(p,r))) | $ANS(neg_th_09). % -P(x,i(p,i(i(i(n(p),p),p),i(i(q,p),p)))) | $ANS(neg_th_10). % -P(x,i(i(q,i(i(n(p),p),p)),i(i(n(p),p),p))) | $ANS(neg_th_11). % -P(x,i(t,i(i(n(p),p),p))) | $ANS(neg_th_12). % -P(x,i(i(n(p),q),i(t,i(i(q,p),p)))) | $ANS(neg_th_13). % -P(x,i(i(i(t,i(i(q,p),p)),r),i(i(n(p),q),r))) | $ANS(neg_th_14). % -P(x,i(i(n(p),q),i(i(q,p),p))) | $ANS(neg_th_15). % -P(x,i(p,p)) | $ANS(neg_th_16). % -P(x,i(p,i(i(q,p),p))) | $ANS(neg_th_17). % -P(x,i(q,i(p,q))) | $ANS(neg_th_18). % -P(x,i(i(i(p,q),r),i(q,r))) | $ANS(neg_th_19). % -P(x,i(p,i(i(p,q),q))) | $ANS(neg_th_20). % -P(x,i(i(p,i(q,r)),i(q,i(p,r)))) | $ANS(neg_th_21). % -P(x,i(i(q,r),i(i(p,q),i(p,r)))) | $ANS(neg_th_22). % -P(x,i(i(i(q,i(p,r)),s),i(i(p,i(q,r)),s))) | $ANS(neg_th_23). % -P(x,i(i(i(p,q),p),p)) | $ANS(neg_th_24). % -P(x,i(i(i(p,r),s),i(i(p,q),i(i(q,r),s)))) | $ANS(neg_th_25). % -P(x,i(i(i(p,q),r),i(i(r,p),p))) | $ANS(neg_th_26). % -P(x,i(i(i(p,q),q),i(i(q,p),p))) | $ANS(neg_th_27). % -P(x,i(i(i(i(r,p),p),s),i(i(i(p,q),r),s))) | $ANS(neg_th_28). % -P(x,i(i(i(p,q),r),i(i(p,r),r))) | $ANS(neg_th_29). % -P(x,i(i(p,i(p,q)),i(p,q))) | $ANS(neg_th_30). % -P(x,i(i(p,s),i(i(i(p,q),r),i(i(s,r),r)))) | $ANS(neg_th_31). % -P(x,i(i(i(p,q),r),i(i(p,s),i(i(s,r),r)))) | $ANS(neg_th_32). % -P(x,i(i(p,s),i(i(s,i(q,i(p,r))),i(q,i(p,r))))) | $ANS(neg_th_33). % -P(x,i(i(s,i(q,i(p,r))),i(i(p,s),i(q,i(p,r))))) | $ANS(neg_th_34). % -P(x,i(i(p,i(q,r)),i(i(p,q),i(p,r)))) | $ANS(neg_th_35). % -P(x,i(n(p),i(p,q))) | $ANS(neg_th_36). % -P(x,i(i(i(p,q),r),i(n(p),r))) | $ANS(neg_th_37). % -P(x,i(i(p,n(p)),n(p))) | $ANS(neg_th_38). % -P(x,i(n(n(p)),p)) | $ANS(neg_th_39). % -P(x,i(p,n(n(p)))) | $ANS(neg_th_40). % -P(x,i(i(p,q),i(n(n(p)),q))) | $ANS(neg_th_41). % -P(x,i(i(i(n(n(p)),q),r),i(i(p,q),r))) | $ANS(neg_th_42). % -P(x,i(i(p,q),i(i(q,n(p)),n(p)))) | $ANS(neg_th_43). % -P(x,i(i(s,i(q,n(p))),i(i(p,q),i(s,n(p))))) | $ANS(neg_th_44). % -P(x,i(i(s,i(q,p)),i(i(n(p),q),i(s,p)))) | $ANS(neg_th_45). % -P(x,i(i(p,q),i(n(q),n(p)))) | $ANS(neg_th_46). % -P(x,i(i(p,n(q)),i(q,n(p)))) | $ANS(neg_th_47). % -P(x,i(i(n(p),q),i(n(q),p))) | $ANS(neg_th_48). % -P(x,i(i(n(p),n(q)),i(q,p))) | $ANS(neg_th_49). % -P(x,i(i(i(n(q),p),r),i(i(n(p),q),r))) | $ANS(neg_th_50). % -P(x,i(i(p,i(q,r)),i(p,i(n(r),n(q))))) | $ANS(neg_th_51). % -P(x,i(i(p,i(q,n(r))),i(p,i(r,n(q))))) | $ANS(neg_th_52). % -P(x,i(i(n(p),q),i(i(p,q),q))) | $ANS(neg_th_53). % -P(x,i(i(p,q),i(i(n(p),q),q))) | $ANS(neg_th_54). % -P(x,i(i(p,q),i(i(p,n(q)),n(p)))) | $ANS(neg_th_55). % -P(x,i(i(i(i(p,q),q),r),i(i(n(p),q),r))) | $ANS(neg_th_56). % -P(x,i(i(n(p),r),i(i(p,q),i(i(q,r),r)))) | $ANS(neg_th_57). % -P(x,i(i(i(i(p,q),i(i(q,r),r)),s),i(i(n(p),r),s))) | $ANS(neg_th_58). % -P(x,i(i(n(p),r),i(i(q,r),i(i(p,q),r)))) | $ANS(neg_th_59). % -P(x,i(i(s,i(n(p),r)),i(s,i(i(q,r),i(i(p,q),r))))) | $ANS(neg_th_60). % -P(x,i(i(p,r),i(i(q,r),i(i(n(p),q),r)))) | $ANS(neg_th_61). % -P(x,i(i(n(n(p)),q),i(p,q))) | $ANS(neg_th_62). % -P(x,i(q,i(p,p))) | $ANS(neg_th_63). % -P(x,i(n(i(p,p)),q)) | $ANS(neg_th_64). % -P(x,i(i(n(q),n(i(p,p))),q)) | $ANS(neg_th_65). % -P(x,i(n(i(p,q)),p)) | $ANS(neg_th_66). % -P(x,i(n(i(p,q)),n(q))) | $ANS(neg_th_67). % -P(x,i(n(i(p,n(q))),q)) | $ANS(neg_th_68). % -P(x,i(p,i(n(q),n(i(p,q))))) | $ANS(neg_th_69). % -P(x,i(p,i(q,n(i(p,n(q)))))) | $ANS(neg_th_70). % -P(x,n(i(i(p,p),n(i(q,q))))) | $ANS(neg_th_71). end_of_list. list(demodulators). % Following essentially mirrrors the Lukasiewicz proof with history. EQ(rew(c1,c1),c4). EQ(rew(c4,c4),c5). EQ(rew(c4,c1),c6). EQ(rew(c5,c6),c7). EQ(rew(c7,c1),c8). EQ(rew(c1,c3),c9). EQ(rew(c9,c6),c10). EQ(rew(c10,c2),c10a). EQ(rew(c10a,c2),c11). EQ(rew(c9,c11),c12). EQ(rew(c7,c12),c13). EQ(rew(c1,c13),c14). EQ(rew(c14,c2),c15). EQ(rew(c9,c2),c16). EQ(rew(c9,c15),c17). EQ(rew(c5,c17),c17a). EQ(rew(c17a,c3),c18). EQ(rew(c1,c18),c19). EQ(rew(c19,c15),c20). EQ(rew(c5,c20),c21). EQ(rew(c21,c1),c22). EQ(rew(c1,c21),c23). EQ(rew(c23,c15),c24a). EQ(rew(c24a,c3),c24). EQ(rew(c21,c6),c25). EQ(rew(c25,c24),c26). EQ(rew(c1,c26),c28). EQ(rew(c28,c26),c29). EQ(rew(c29,c16),c30). EQ(rew(c7,c29),c31). EQ(rew(c21,c31),c32). EQ(rew(c32,c18),c33). EQ(rew(c21,c33),c34). EQ(rew(c34,c22),c35). EQ(rew(c21,c3),c36). EQ(rew(c1,c36),c37). EQ(rew(c26,c2),c38). EQ(rew(c37,c2),c39). EQ(rew(c9,c38),c40). EQ(rew(c1,c39),c41). EQ(rew(c1,c41),c42). EQ(rew(c42,c15),c43). EQ(rew(c5,c43),c44). EQ(rew(c5,c15),c45). EQ(rew(c44,c36),c46). EQ(rew(c44,c3),c47). EQ(rew(c45,c36),c48). EQ(rew(c45,c3),c49). EQ(rew(c1,c48),c50). EQ(rew(c22,c46),c51). EQ(rew(c22,c47),c52). EQ(rew(c50,c15),c53). EQ(rew(c21,c53),c54). EQ(rew(c44,c47),c55). EQ(rew(c1,c53),c56). EQ(rew(c56,c32),c57). EQ(rew(c1,c57),c58). EQ(rew(c58,c21),c59). EQ(rew(c22,c59),c60). EQ(rew(c60,c41),c61). EQ(rew(c1,c40),c62). EQ(rew(c21,c18),c63). EQ(rew(c48,c63),c64). EQ(rew(c61,c16),c64a). EQ(rew(c64a,c64),c65). EQ(rew(c48,c36),c66). EQ(rew(c46,c18),c67). EQ(rew(c48,c18),c68). EQ(rew(c51,c20),c69). EQ(rew(c52,c20),c70). EQ(rew(c70,c16),c70a). EQ(rew(c70a,c16),c71). end_of_list.