% SZS status Theorem for ID_corr.p : (rf:0,axioms:1,ps:3,u:6,ude:true,rLeibEQ:true,rAndEQ:true,use_choice:true,use_extuni:true,use_extcnf_combined:true,expand_extuni:false,foatp:e,atp_timeout:25,atp_calls_frequency:10,ordering:none,proof_output:1,clause_count:54,loop_count:0,foatp_calls:1,translation:fof_full) %**** Beginning of derivation protocol **** % SZS output start CNFRefutation thf(tp_mu,type,(mu: $tType)). thf(tp_all,type,(all: ((($i>$o)>($i>$o))>($i>$o)))). thf(tp_all_co,type,(all_co: ((mu>($i>$o))>($i>$o)))). thf(tp_all_va,type,(all_va: ((mu>($i>$o))>($i>$o)))). thf(tp_box,type,(box: (($i>$o)>($i>$o)))). thf(tp_cond,type,(cond: (($i>$o)>(($i>$o)>($i>$o))))). thf(tp_eiw,type,(eiw: ($i>(mu>$o)))). thf(tp_f,type,(f: ($i>(($i>$o)>($i>$o))))). thf(tp_impl,type,(impl: (($i>$o)>(($i>$o)>($i>$o))))). thf(tp_not,type,(not: (($i>$o)>($i>$o)))). thf(tp_or,type,(or: (($i>$o)>(($i>$o)>($i>$o))))). thf(tp_sK1_P,type,(sK1_P: ($i>$o))). thf(tp_sK2_SY25,type,(sK2_SY25: $i)). thf(tp_sK3_SY27,type,(sK3_SY27: $i)). thf(tp_sK4_SY11,type,(sK4_SY11: $i)). thf(tp_sK5_SY28,type,(sK5_SY28: ($i>$o))). thf(tp_sK6_SY30,type,(sK6_SY30: $i)). thf(tp_sK7_X,type,(sK7_X: ($i>mu))). thf(tp_vld,type,(vld: (($i>$o)>$o))). thf(all,definition,(all = (^[A:(($i>$o)>($i>$o)),W:$i]: (![P:($i>$o)]: ((A@P)@W)))),file('ID_corr.p',all)). thf(all_co,definition,(all_co = (^[A:(mu>($i>$o)),W:$i]: (![X:mu]: ((A@X)@W)))),file('ID_corr.p',all_co)). thf(all_va,definition,(all_va = (^[A:(mu>($i>$o)),W:$i]: (![X:mu]: (((eiw@W)@X) => ((A@X)@W))))),file('ID_corr.p',all_va)). thf(box,definition,(box = (^[A:($i>$o)]: ((cond@(not@A))@A))),file('ID_corr.p',box)). thf(cond,definition,(cond = (^[A:($i>$o),B:($i>$o),X:$i]: (![W:$i]: ((((f@X)@A)@W) => (B@W))))),file('ID_corr.p',cond)). thf(impl,definition,(impl = (^[A:($i>$o),B:($i>$o),X:$i]: ((A@X) => (B@X)))),file('ID_corr.p',impl)). thf(not,definition,(not = (^[A:($i>$o),X:$i]: (~ (A@X)))),file('ID_corr.p',not)). thf(or,definition,(or = (^[A:($i>$o),B:($i>$o),X:$i]: ((A@X) | (B@X)))),file('ID_corr.p',or)). thf(vld,definition,(vld = (^[A:($i>$o)]: (![S:$i]: (A@S)))),file('ID_corr.p',vld)). thf(1,axiom,(![V:$i]: (?[X:mu]: ((eiw@V)@X))),file('ID_corr.p',nonempty)). thf(2,conjecture,((vld@(all@(^[P:($i>$o)]: ((cond@P)@P)))) <=> (![P:($i>$o),W:$i,Z:$i]: ((((f@W)@P)@Z) => (P@Z)))),file('ID_corr.p',id_corr)). thf(3,negated_conjecture,((((vld@(all@(^[P:($i>$o)]: ((cond@P)@P)))) <=> (![P:($i>$o),W:$i,Z:$i]: ((((f@W)@P)@Z) => (P@Z))))=$false)),inference(negate_conjecture,[status(cth)],[2])). thf(4,plain,((((![SY11:$i,SY12:($i>$o),SY13:$i]: ((((f@SY11)@SY12)@SY13) => (SY12@SY13))) <=> (![P:($i>$o),W:$i,Z:$i]: ((((f@W)@P)@Z) => (P@Z))))=$false)),inference(unfold_def,[status(thm)],[3,all,all_co,all_va,box,cond,impl,not,or,vld])). thf(5,plain,(((![V:$i]: (?[X:mu]: ((eiw@V)@X)))=$true)),inference(unfold_def,[status(thm)],[1,all,all_co,all_va,box,cond,impl,not,or,vld])). thf(6,plain,((((![SY11:$i,SY12:($i>$o),SY13:$i]: ((((f@SY11)@SY12)@SY13) => (SY12@SY13))) => (![P:($i>$o),W:$i,Z:$i]: ((((f@W)@P)@Z) => (P@Z))))=$false)),inference(split_conjecture,[split_conjecture(split,[])],[4])). thf(7,plain,((((![P:($i>$o),W:$i,Z:$i]: ((((f@W)@P)@Z) => (P@Z))) => (![SY11:$i,SY12:($i>$o),SY13:$i]: ((((f@SY11)@SY12)@SY13) => (SY12@SY13))))=$false)),inference(split_conjecture,[split_conjecture(split,[])],[4])). thf(8,plain,(((~ ((![SY11:$i,SY12:($i>$o),SY13:$i]: ((((f@SY11)@SY12)@SY13) => (SY12@SY13))) => (![P:($i>$o),W:$i,Z:$i]: ((((f@W)@P)@Z) => (P@Z)))))=$true)),inference(polarity_switch,[status(thm)],[6])). thf(9,plain,(((~ ((![P:($i>$o),W:$i,Z:$i]: ((((f@W)@P)@Z) => (P@Z))) => (![SY11:$i,SY12:($i>$o),SY13:$i]: ((((f@SY11)@SY12)@SY13) => (SY12@SY13)))))=$true)),inference(polarity_switch,[status(thm)],[7])). thf(10,plain,((((![SY11:$i,SY12:($i>$o),SY13:$i]: ((~ (((f@SY11)@SY12)@SY13)) | (SY12@SY13))) & ((((f@sK2_SY25)@sK1_P)@sK3_SY27) & (~ (sK1_P@sK3_SY27))))=$true)),inference(extcnf_combined,[status(esa)],[8])). thf(11,plain,((((![P:($i>$o),W:$i,Z:$i]: ((~ (((f@W)@P)@Z)) | (P@Z))) & ((((f@sK4_SY11)@sK5_SY28)@sK6_SY30) & (~ (sK5_SY28@sK6_SY30))))=$true)),inference(extcnf_combined,[status(esa)],[9])). thf(12,plain,(((![V:$i]: ((eiw@V)@(sK7_X@V)))=$true)),inference(extcnf_combined,[status(esa)],[5])). thf(13,plain,(((![V:$i]: ((eiw@V)@(sK7_X@V)))=$true)),inference(copy,[status(thm)],[12])). thf(14,plain,((((![SY11:$i,SY12:($i>$o),SY13:$i]: ((~ (((f@SY11)@SY12)@SY13)) | (SY12@SY13))) & ((((f@sK2_SY25)@sK1_P)@sK3_SY27) & (~ (sK1_P@sK3_SY27))))=$true)),inference(copy,[status(thm)],[10])). thf(15,plain,(((~ ((~ (![SX0:$i,SX1:($i>$o),SX2:$i]: ((~ (((f@SX0)@SX1)@SX2)) | (SX1@SX2)))) | (~ (~ ((~ (((f@sK2_SY25)@sK1_P)@sK3_SY27)) | (~ (~ (sK1_P@sK3_SY27))))))))=$true)),inference(unfold_def,[status(thm)],[14,all,all_co,all_va,box,cond,impl,not,or,vld])). thf(16,plain,(![SV1:$i]: ((((eiw@SV1)@(sK7_X@SV1))=$true))),inference(extcnf_forall_pos,[status(thm)],[13])). thf(17,plain,((((~ (![SX0:$i,SX1:($i>$o),SX2:$i]: ((~ (((f@SX0)@SX1)@SX2)) | (SX1@SX2)))) | (~ (~ ((~ (((f@sK2_SY25)@sK1_P)@sK3_SY27)) | (~ (~ (sK1_P@sK3_SY27)))))))=$false)),inference(extcnf_not_pos,[status(thm)],[15])). thf(18,plain,(((~ (![SX0:$i,SX1:($i>$o),SX2:$i]: ((~ (((f@SX0)@SX1)@SX2)) | (SX1@SX2))))=$false)),inference(extcnf_or_neg,[status(thm)],[17])). thf(19,plain,(((~ (~ ((~ (((f@sK2_SY25)@sK1_P)@sK3_SY27)) | (~ (~ (sK1_P@sK3_SY27))))))=$false)),inference(extcnf_or_neg,[status(thm)],[17])). thf(20,plain,(((![SX0:$i,SX1:($i>$o),SX2:$i]: ((~ (((f@SX0)@SX1)@SX2)) | (SX1@SX2)))=$true)),inference(extcnf_not_neg,[status(thm)],[18])). thf(21,plain,(((~ ((~ (((f@sK2_SY25)@sK1_P)@sK3_SY27)) | (~ (~ (sK1_P@sK3_SY27)))))=$true)),inference(extcnf_not_neg,[status(thm)],[19])). thf(22,plain,(![SV2:$i]: (((![SY31:($i>$o),SY32:$i]: ((~ (((f@SV2)@SY31)@SY32)) | (SY31@SY32)))=$true))),inference(extcnf_forall_pos,[status(thm)],[20])). thf(23,plain,((((~ (((f@sK2_SY25)@sK1_P)@sK3_SY27)) | (~ (~ (sK1_P@sK3_SY27))))=$false)),inference(extcnf_not_pos,[status(thm)],[21])). thf(24,plain,(![SV3:($i>$o),SV2:$i]: (((![SY33:$i]: ((~ (((f@SV2)@SV3)@SY33)) | (SV3@SY33)))=$true))),inference(extcnf_forall_pos,[status(thm)],[22])). thf(25,plain,(((~ (((f@sK2_SY25)@sK1_P)@sK3_SY27))=$false)),inference(extcnf_or_neg,[status(thm)],[23])). thf(26,plain,(((~ (~ (sK1_P@sK3_SY27)))=$false)),inference(extcnf_or_neg,[status(thm)],[23])). thf(27,plain,(![SV4:$i,SV3:($i>$o),SV2:$i]: ((((~ (((f@SV2)@SV3)@SV4)) | (SV3@SV4))=$true))),inference(extcnf_forall_pos,[status(thm)],[24])). thf(28,plain,(((((f@sK2_SY25)@sK1_P)@sK3_SY27)=$true)),inference(extcnf_not_neg,[status(thm)],[25])). thf(29,plain,(((~ (sK1_P@sK3_SY27))=$true)),inference(extcnf_not_neg,[status(thm)],[26])). thf(30,plain,(![SV4:$i,SV3:($i>$o),SV2:$i]: (((~ (((f@SV2)@SV3)@SV4))=$true) | ((SV3@SV4)=$true))),inference(extcnf_or_pos,[status(thm)],[27])). thf(31,plain,(((sK1_P@sK3_SY27)=$false)),inference(extcnf_not_pos,[status(thm)],[29])). thf(32,plain,(![SV4:$i,SV3:($i>$o),SV2:$i]: (((((f@SV2)@SV3)@SV4)=$false) | ((SV3@SV4)=$true))),inference(extcnf_not_pos,[status(thm)],[30])). thf(33,plain,((($false)=$true)),inference(fo_atp_e,[status(thm)],[16,32,31,28])). thf(34,plain,(((![V:$i]: ((eiw@V)@(sK7_X@V)))=$true)),inference(copy,[status(thm)],[12])). thf(35,plain,((((![P:($i>$o),W:$i,Z:$i]: ((~ (((f@W)@P)@Z)) | (P@Z))) & ((((f@sK4_SY11)@sK5_SY28)@sK6_SY30) & (~ (sK5_SY28@sK6_SY30))))=$true)),inference(copy,[status(thm)],[11])). thf(36,plain,(((~ ((~ (![SX0:($i>$o),SX1:$i,SX2:$i]: ((~ (((f@SX1)@SX0)@SX2)) | (SX0@SX2)))) | (~ (~ ((~ (((f@sK4_SY11)@sK5_SY28)@sK6_SY30)) | (~ (~ (sK5_SY28@sK6_SY30))))))))=$true)),inference(unfold_def,[status(thm)],[35,all,all_co,all_va,box,cond,impl,not,or,vld])). thf(37,plain,(![SV5:$i]: ((((eiw@SV5)@(sK7_X@SV5))=$true))),inference(extcnf_forall_pos,[status(thm)],[34])). thf(38,plain,((((~ (![SX0:($i>$o),SX1:$i,SX2:$i]: ((~ (((f@SX1)@SX0)@SX2)) | (SX0@SX2)))) | (~ (~ ((~ (((f@sK4_SY11)@sK5_SY28)@sK6_SY30)) | (~ (~ (sK5_SY28@sK6_SY30)))))))=$false)),inference(extcnf_not_pos,[status(thm)],[36])). thf(39,plain,(((~ (![SX0:($i>$o),SX1:$i,SX2:$i]: ((~ (((f@SX1)@SX0)@SX2)) | (SX0@SX2))))=$false)),inference(extcnf_or_neg,[status(thm)],[38])). thf(40,plain,(((~ (~ ((~ (((f@sK4_SY11)@sK5_SY28)@sK6_SY30)) | (~ (~ (sK5_SY28@sK6_SY30))))))=$false)),inference(extcnf_or_neg,[status(thm)],[38])). thf(41,plain,(((![SX0:($i>$o),SX1:$i,SX2:$i]: ((~ (((f@SX1)@SX0)@SX2)) | (SX0@SX2)))=$true)),inference(extcnf_not_neg,[status(thm)],[39])). thf(42,plain,(((~ ((~ (((f@sK4_SY11)@sK5_SY28)@sK6_SY30)) | (~ (~ (sK5_SY28@sK6_SY30)))))=$true)),inference(extcnf_not_neg,[status(thm)],[40])). thf(43,plain,(![SV6:($i>$o)]: (((![SY34:$i,SY35:$i]: ((~ (((f@SY34)@SV6)@SY35)) | (SV6@SY35)))=$true))),inference(extcnf_forall_pos,[status(thm)],[41])). thf(44,plain,((((~ (((f@sK4_SY11)@sK5_SY28)@sK6_SY30)) | (~ (~ (sK5_SY28@sK6_SY30))))=$false)),inference(extcnf_not_pos,[status(thm)],[42])). thf(45,plain,(![SV6:($i>$o),SV7:$i]: (((![SY36:$i]: ((~ (((f@SV7)@SV6)@SY36)) | (SV6@SY36)))=$true))),inference(extcnf_forall_pos,[status(thm)],[43])). thf(46,plain,(((~ (((f@sK4_SY11)@sK5_SY28)@sK6_SY30))=$false)),inference(extcnf_or_neg,[status(thm)],[44])). thf(47,plain,(((~ (~ (sK5_SY28@sK6_SY30)))=$false)),inference(extcnf_or_neg,[status(thm)],[44])). thf(48,plain,(![SV8:$i,SV6:($i>$o),SV7:$i]: ((((~ (((f@SV7)@SV6)@SV8)) | (SV6@SV8))=$true))),inference(extcnf_forall_pos,[status(thm)],[45])). thf(49,plain,(((((f@sK4_SY11)@sK5_SY28)@sK6_SY30)=$true)),inference(extcnf_not_neg,[status(thm)],[46])). thf(50,plain,(((~ (sK5_SY28@sK6_SY30))=$true)),inference(extcnf_not_neg,[status(thm)],[47])). thf(51,plain,(![SV8:$i,SV6:($i>$o),SV7:$i]: (((~ (((f@SV7)@SV6)@SV8))=$true) | ((SV6@SV8)=$true))),inference(extcnf_or_pos,[status(thm)],[48])). thf(52,plain,(((sK5_SY28@sK6_SY30)=$false)),inference(extcnf_not_pos,[status(thm)],[50])). thf(53,plain,(![SV8:$i,SV6:($i>$o),SV7:$i]: (((((f@SV7)@SV6)@SV8)=$false) | ((SV6@SV8)=$true))),inference(extcnf_not_pos,[status(thm)],[51])). thf(54,plain,((($false)=$true)),inference(fo_atp_e,[status(thm)],[37,53,52,49])). thf(55,plain,($false),inference(solved_all_splits,[solved_all_splits(join,[])],[54,33])). % SZS output end CNFRefutation %**** End of derivation protocol **** %**** no. of clauses in derivation: 55 **** %**** clause counter: 54 **** % SZS status Theorem for ID_corr.p : (rf:0,axioms:1,ps:3,u:6,ude:true,rLeibEQ:true,rAndEQ:true,use_choice:true,use_extuni:true,use_extcnf_combined:true,expand_extuni:false,foatp:e,atp_timeout:25,atp_calls_frequency:10,ordering:none,proof_output:1,clause_count:54,loop_count:0,foatp_calls:1,translation:fof_full)