% 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:2,clause_count:86,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)la => ((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(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(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(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(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])). fof(34, axiom, (leoLit(leoTi(leoAt(leoTi(leoAt(leoTi(leoAt(leoTi(cf,leoFt(i,leoFt(leoFt(i,o),leoFt(i,o)))),leoTi(csK2_SY25,i)),leoFt(leoFt(i,o),leoFt(i,o))),leoTi(csK1_P,leoFt(i,o))),leoFt(i,o)),leoTi(csK3_SY27,i)),o))) , inference(fof_translation, [status(thm)],[28])). fof(35, axiom, (~(leoLit(leoTi(leoAt(leoTi(csK1_P,leoFt(i,o)),leoTi(csK3_SY27,i)),o)))) , inference(fof_translation, [status(thm)],[31])). fof(36, axiom, (![X2]:![X3]:![X4]:(leoLit(leoTi(leoAt(leoTi(X3,leoFt(i,o)),leoTi(X2,i)),o))|~(leoLit(leoTi(leoAt(leoTi(leoAt(leoTi(leoAt(leoTi(cf,leoFt(i,leoFt(leoFt(i,o),leoFt(i,o)))),leoTi(X4,i)),leoFt(leoFt(i,o),leoFt(i,o))),leoTi(X3,leoFt(i,o))),leoFt(i,o)),leoTi(X2,i)),o))))) , inference(fof_translation, [status(thm)],[32])). fof(37, plain, (~leoLit(leoTi(leoAt(leoTi(csK1_P,leoFt(i,o)),leoTi(csK3_SY27,i)),o))) ,inference(fof_simplification, [status(thm)],[35])). fof(38, plain, (![X2]:![X3]:![X4]:(leoLit(leoTi(leoAt(leoTi(X3,leoFt(i,o)),leoTi(X2,i)),o))|~leoLit(leoTi(leoAt(leoTi(leoAt(leoTi(leoAt(leoTi(cf,leoFt(i,leoFt(leoFt(i,o),leoFt(i,o)))),leoTi(X4,i)),leoFt(leoFt(i,o),leoFt(i,o))),leoTi(X3,leoFt(i,o))),leoFt(i,o)),leoTi(X2,i)),o)))) ,inference(fof_simplification, [status(thm)],[36])). cnf(41,plain,(leoLit(leoTi(leoAt(leoTi(leoAt(leoTi(leoAt(leoTi(cf,leoFt(i,leoFt(leoFt(i,o),leoFt(i,o)))),leoTi(csK2_SY25,i)),leoFt(leoFt(i,o),leoFt(i,o))),leoTi(csK1_P,leoFt(i,o))),leoFt(i,o)),leoTi(csK3_SY27,i)),o))),inference(split_conjunct, [status(thm)],[34])). cnf(42,plain,(~leoLit(leoTi(leoAt(leoTi(csK1_P,leoFt(i,o)),leoTi(csK3_SY27,i)),o))),inference(split_conjunct, [status(thm)],[37])). fof(43, plain, (![X2]:![X3]:(leoLit(leoTi(leoAt(leoTi(X3,leoFt(i,o)),leoTi(X2,i)),o))|![X4]:~leoLit(leoTi(leoAt(leoTi(leoAt(leoTi(leoAt(leoTi(cf,leoFt(i,leoFt(leoFt(i,o),leoFt(i,o)))),leoTi(X4,i)),leoFt(leoFt(i,o),leoFt(i,o))),leoTi(X3,leoFt(i,o))),leoFt(i,o)),leoTi(X2,i)),o)))) ,inference(shift_quantors, [status(thm)],[38])). fof(44, plain, (![X5]:![X6]:(leoLit(leoTi(leoAt(leoTi(X6,leoFt(i,o)),leoTi(X5,i)),o))|![X7]:~leoLit(leoTi(leoAt(leoTi(leoAt(leoTi(leoAt(leoTi(cf,leoFt(i,leoFt(leoFt(i,o),leoFt(i,o)))),leoTi(X7,i)),leoFt(leoFt(i,o),leoFt(i,o))),leoTi(X6,leoFt(i,o))),leoFt(i,o)),leoTi(X5,i)),o)))) ,inference(variable_rename, [status(thm)],[43])). fof(45, plain, (![X5]:![X6]:![X7]:(leoLit(leoTi(leoAt(leoTi(X6,leoFt(i,o)),leoTi(X5,i)),o))|~leoLit(leoTi(leoAt(leoTi(leoAt(leoTi(leoAt(leoTi(cf,leoFt(i,leoFt(leoFt(i,o),leoFt(i,o)))),leoTi(X7,i)),leoFt(leoFt(i,o),leoFt(i,o))),leoTi(X6,leoFt(i,o))),leoFt(i,o)),leoTi(X5,i)),o)))) ,inference(shift_quantors, [status(thm)],[44])). cnf(46,plain,(leoLit(leoTi(leoAt(leoTi(X2,leoFt(i,o)),leoTi(X3,i)),o))|~leoLit(leoTi(leoAt(leoTi(leoAt(leoTi(leoAt(leoTi(cf,leoFt(i,leoFt(leoFt(i,o),leoFt(i,o)))),leoTi(X1,i)),leoFt(leoFt(i,o),leoFt(i,o))),leoTi(X2,leoFt(i,o))),leoFt(i,o)),leoTi(X3,i)),o))),inference(split_conjunct, [status(thm)],[45])). cnf(47,plain,(leoLit(leoTi(leoAt(leoTi(csK1_P,leoFt(i,o)),leoTi(csK3_SY27,i)),o))),inference(spm,[status(thm)],[46,41,theory(equality)])). cnf(48,plain,($false),inference(sr,[status(thm)],[47,42,theory(equality)])). thf(49,plain,((($false)=$true)),inference(fo_atp_e,[status(thm)],[48])). thf(51,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(52,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)],[51,all,all_co,all_va,box,cond,impl,not,or,vld])). thf(54,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)],[52])). thf(55,plain,(((~ (![SX0:($i>$o),SX1:$i,SX2:$i]: ((~ (((f@SX1)@SX0)@SX2)) | (SX0@SX2))))=$false)),inference(extcnf_or_neg,[status(thm)],[54])). thf(56,plain,(((~ (~ ((~ (((f@sK4_SY11)@sK5_SY28)@sK6_SY30)) | (~ (~ (sK5_SY28@sK6_SY30))))))=$false)),inference(extcnf_or_neg,[status(thm)],[54])). thf(57,plain,(((![SX0:($i>$o),SX1:$i,SX2:$i]: ((~ (((f@SX1)@SX0)@SX2)) | (SX0@SX2)))=$true)),inference(extcnf_not_neg,[status(thm)],[55])). thf(58,plain,(((~ ((~ (((f@sK4_SY11)@sK5_SY28)@sK6_SY30)) | (~ (~ (sK5_SY28@sK6_SY30)))))=$true)),inference(extcnf_not_neg,[status(thm)],[56])). thf(59,plain,(![SV6:($i>$o)]: (((![SY34:$i,SY35:$i]: ((~ (((f@SY34)@SV6)@SY35)) | (SV6@SY35)))=$true))),inference(extcnf_forall_pos,[status(thm)],[57])). thf(60,plain,((((~ (((f@sK4_SY11)@sK5_SY28)@sK6_SY30)) | (~ (~ (sK5_SY28@sK6_SY30))))=$false)),inference(extcnf_not_pos,[status(thm)],[58])). thf(61,plain,(![SV6:($i>$o),SV7:$i]: (((![SY36:$i]: ((~ (((f@SV7)@SV6)@SY36)) | (SV6@SY36)))=$true))),inference(extcnf_forall_pos,[status(thm)],[59])). thf(62,plain,(((~ (((f@sK4_SY11)@sK5_SY28)@sK6_SY30))=$false)),inference(extcnf_or_neg,[status(thm)],[60])). thf(63,plain,(((~ (~ (sK5_SY28@sK6_SY30)))=$false)),inference(extcnf_or_neg,[status(thm)],[60])). thf(64,plain,(![SV8:$i,SV6:($i>$o),SV7:$i]: ((((~ (((f@SV7)@SV6)@SV8)) | (SV6@SV8))=$true))),inference(extcnf_forall_pos,[status(thm)],[61])). thf(65,plain,(((((f@sK4_SY11)@sK5_SY28)@sK6_SY30)=$true)),inference(extcnf_not_neg,[status(thm)],[62])). thf(66,plain,(((~ (sK5_SY28@sK6_SY30))=$true)),inference(extcnf_not_neg,[status(thm)],[63])). thf(67,plain,(![SV8:$i,SV6:($i>$o),SV7:$i]: (((~ (((f@SV7)@SV6)@SV8))=$true) | ((SV6@SV8)=$true))),inference(extcnf_or_pos,[status(thm)],[64])). thf(68,plain,(((sK5_SY28@sK6_SY30)=$false)),inference(extcnf_not_pos,[status(thm)],[66])). thf(69,plain,(![SV8:$i,SV6:($i>$o),SV7:$i]: (((((f@SV7)@SV6)@SV8)=$false) | ((SV6@SV8)=$true))),inference(extcnf_not_pos,[status(thm)],[67])). fof(71, axiom, (leoLit(leoTi(leoAt(leoTi(leoAt(leoTi(leoAt(leoTi(cf,leoFt(i,leoFt(leoFt(i,o),leoFt(i,o)))),leoTi(csK4_SY11,i)),leoFt(leoFt(i,o),leoFt(i,o))),leoTi(csK5_SY28,leoFt(i,o))),leoFt(i,o)),leoTi(csK6_SY30,i)),o))) , inference(fof_translation, [status(thm)],[65])). fof(72, axiom, (~(leoLit(leoTi(leoAt(leoTi(csK5_SY28,leoFt(i,o)),leoTi(csK6_SY30,i)),o)))) , inference(fof_translation, [status(thm)],[68])). fof(73, axiom, (![X2]:![X3]:![X4]:(leoLit(leoTi(leoAt(leoTi(X3,leoFt(i,o)),leoTi(X2,i)),o))|~(leoLit(leoTi(leoAt(leoTi(leoAt(leoTi(leoAt(leoTi(cf,leoFt(i,leoFt(leoFt(i,o),leoFt(i,o)))),leoTi(X4,i)),leoFt(leoFt(i,o),leoFt(i,o))),leoTi(X3,leoFt(i,o))),leoFt(i,o)),leoTi(X2,i)),o))))) , inference(fof_translation, [status(thm)],[69])). fof(74, plain, (~leoLit(leoTi(leoAt(leoTi(csK5_SY28,leoFt(i,o)),leoTi(csK6_SY30,i)),o))) ,inference(fof_simplification, [status(thm)],[72])). fof(75, plain, (![X2]:![X3]:![X4]:(leoLit(leoTi(leoAt(leoTi(X3,leoFt(i,o)),leoTi(X2,i)),o))|~leoLit(leoTi(leoAt(leoTi(leoAt(leoTi(leoAt(leoTi(cf,leoFt(i,leoFt(leoFt(i,o),leoFt(i,o)))),leoTi(X4,i)),leoFt(leoFt(i,o),leoFt(i,o))),leoTi(X3,leoFt(i,o))),leoFt(i,o)),leoTi(X2,i)),o)))) ,inference(fof_simplification, [status(thm)],[73])). cnf(78,plain,(leoLit(leoTi(leoAt(leoTi(leoAt(leoTi(leoAt(leoTi(cf,leoFt(i,leoFt(leoFt(i,o),leoFt(i,o)))),leoTi(csK4_SY11,i)),leoFt(leoFt(i,o),leoFt(i,o))),leoTi(csK5_SY28,leoFt(i,o))),leoFt(i,o)),leoTi(csK6_SY30,i)),o))),inference(split_conjunct, [status(thm)],[71])). cnf(79,plain,(~leoLit(leoTi(leoAt(leoTi(csK5_SY28,leoFt(i,o)),leoTi(csK6_SY30,i)),o))),inference(split_conjunct, [status(thm)],[74])). fof(80, plain, (![X2]:![X3]:(leoLit(leoTi(leoAt(leoTi(X3,leoFt(i,o)),leoTi(X2,i)),o))|![X4]:~leoLit(leoTi(leoAt(leoTi(leoAt(leoTi(leoAt(leoTi(cf,leoFt(i,leoFt(leoFt(i,o),leoFt(i,o)))),leoTi(X4,i)),leoFt(leoFt(i,o),leoFt(i,o))),leoTi(X3,leoFt(i,o))),leoFt(i,o)),leoTi(X2,i)),o)))) ,inference(shift_quantors, [status(thm)],[75])). fof(81, plain, (![X5]:![X6]:(leoLit(leoTi(leoAt(leoTi(X6,leoFt(i,o)),leoTi(X5,i)),o))|![X7]:~leoLit(leoTi(leoAt(leoTi(leoAt(leoTi(leoAt(leoTi(cf,leoFt(i,leoFt(leoFt(i,o),leoFt(i,o)))),leoTi(X7,i)),leoFt(leoFt(i,o),leoFt(i,o))),leoTi(X6,leoFt(i,o))),leoFt(i,o)),leoTi(X5,i)),o)))) ,inference(variable_rename, [status(thm)],[80])). fof(82, plain, (![X5]:![X6]:![X7]:(leoLit(leoTi(leoAt(leoTi(X6,leoFt(i,o)),leoTi(X5,i)),o))|~leoLit(leoTi(leoAt(leoTi(leoAt(leoTi(leoAt(leoTi(cf,leoFt(i,leoFt(leoFt(i,o),leoFt(i,o)))),leoTi(X7,i)),leoFt(leoFt(i,o),leoFt(i,o))),leoTi(X6,leoFt(i,o))),leoFt(i,o)),leoTi(X5,i)),o)))) ,inference(shift_quantors, [status(thm)],[81])). cnf(83,plain,(leoLit(leoTi(leoAt(leoTi(X2,leoFt(i,o)),leoTi(X3,i)),o))|~leoLit(leoTi(leoAt(leoTi(leoAt(leoTi(leoAt(leoTi(cf,leoFt(i,leoFt(leoFt(i,o),leoFt(i,o)))),leoTi(X1,i)),leoFt(leoFt(i,o),leoFt(i,o))),leoTi(X2,leoFt(i,o))),leoFt(i,o)),leoTi(X3,i)),o))),inference(split_conjunct, [status(thm)],[82])). cnf(84,plain,(leoLit(leoTi(leoAt(leoTi(csK5_SY28,leoFt(i,o)),leoTi(csK6_SY30,i)),o))),inference(spm,[status(thm)],[83,78,theory(equality)])). cnf(85,plain,($false),inference(sr,[status(thm)],[84,79,theory(equality)])). thf(86,plain,((($false)=$true)),inference(fo_atp_e,[status(thm)],[85])). thf(87,plain,($false),inference(solved_all_splits,[solved_all_splits(join,[])],[86,49])). % SZS output end CNFRefutation %**** End of derivation protocol **** %**** no. of clauses in derivation: 74 **** %**** clause counter: 86 **** % 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:2,clause_count:86,loop_count:0,foatp_calls:1,translation:fof_full)