WATCH: 0.00 CPU 0.01 WC No.of.Axioms: 0 .. [E:600s] ******************************** * All subproblems solved!!! * ******************************** % SZS status Theorem for /CW/home-0/sutcliff/CASC/23/Problems/FNE/FNE045.p (rf:0,ps:3,sos:true,u:8,ude:true,foatp:e) %**** Beginning of derivation protocol **** % SZS output start CNFRefutation thf(tp_a_truth,type,(a_truth: ($i>$o))). thf(tp_implies,type,(implies: ($i>($i>$i)))). thf(tp_not,type,(not: ($i>$i))). thf(tp_sK1,type,(sK1: $i)). thf(1,conjecture,(~ (((((![P:$i,Q:$i]: (((~ (a_truth@P)) | (a_truth@Q)) | (~ (a_truth@((implies@P)@Q))))) & (![P:$i,Q:$i]: (a_truth@((implies@P)@((implies@Q)@P))))) & (?[A:$i]: (~ (a_truth@((implies@A)@A))))) & (![P:$i,Q:$i]: (a_truth@((implies@((implies@(not@P))@(not@Q)))@((implies@Q)@P))))) & (![P:$i,Q:$i,R:$i]: (a_truth@((implies@((implies@P)@((implies@Q)@R)))@((implies@((implies@P)@Q))@((implies@P)@R))))))),file('/CW/home-0/sutcliff/CASC/23/Problems/FNE/FNE045.p',thm147)). thf(2,negated_conjecture,(((~ (((((![P:$i,Q:$i]: (((~ (a_truth@P)) | (a_truth@Q)) | (~ (a_truth@((implies@P)@Q))))) & (![P:$i,Q:$i]: (a_truth@((implies@P)@((implies@Q)@P))))) & (?[A:$i]: (~ (a_truth@((implies@A)@A))))) & (![P:$i,Q:$i]: (a_truth@((implies@((implies@(not@P))@(not@Q)))@((implies@Q)@P))))) & (![P:$i,Q:$i,R:$i]: (a_truth@((implies@((implies@P)@((implies@Q)@R)))@((implies@((implies@P)@Q))@((implies@P)@R)))))))=$false)),inference(negate_conjecture,[status(cth)],[1])). thf(3,plain,(((~ (((((![P:$i,Q:$i]: (((~ (a_truth@P)) | (a_truth@Q)) | (~ (a_truth@((implies@P)@Q))))) & (![P:$i,Q:$i]: (a_truth@((implies@P)@((implies@Q)@P))))) & (?[A:$i]: (~ (a_truth@((implies@A)@A))))) & (![P:$i,Q:$i]: (a_truth@((implies@((implies@(not@P))@(not@Q)))@((implies@Q)@P))))) & (![P:$i,Q:$i,R:$i]: (a_truth@((implies@((implies@P)@((implies@Q)@R)))@((implies@((implies@P)@Q))@((implies@P)@R)))))))=$false)),inference(unfold_def,[status(thm)],[2])). thf(4,plain,(((((((![P:$i,Q:$i]: (((~ (a_truth@P)) | (a_truth@Q)) | (~ (a_truth@((implies@P)@Q))))) & (![P:$i,Q:$i]: (a_truth@((implies@P)@((implies@Q)@P))))) & (?[A:$i]: (~ (a_truth@((implies@A)@A))))) & (![P:$i,Q:$i]: (a_truth@((implies@((implies@(not@P))@(not@Q)))@((implies@Q)@P))))) & (![P:$i,Q:$i,R:$i]: (a_truth@((implies@((implies@P)@((implies@Q)@R)))@((implies@((implies@P)@Q))@((implies@P)@R))))))=$true)),inference(polarity_switch,[status(thm)],[3])). thf(5,plain,((((![P:$i,Q:$i,R:$i]: (a_truth@((implies@((implies@P)@((implies@Q)@R)))@((implies@((implies@P)@Q))@((implies@P)@R))))) & ((![P:$i,Q:$i]: (a_truth@((implies@((implies@(not@P))@(not@Q)))@((implies@Q)@P)))) & (((![P:$i,Q:$i]: (((~ (a_truth@P)) | (a_truth@Q)) | (~ (a_truth@((implies@P)@Q))))) & (![P:$i,Q:$i]: (a_truth@((implies@P)@((implies@Q)@P))))) & (~ (a_truth@((implies@sK1)@sK1))))))=$true)),inference(extcnf_combined,[status(esa)],[4])). thf(6,plain,((((![P:$i,Q:$i,R:$i]: (a_truth@((implies@((implies@P)@((implies@Q)@R)))@((implies@((implies@P)@Q))@((implies@P)@R))))) & ((![P:$i,Q:$i]: (a_truth@((implies@((implies@(not@P))@(not@Q)))@((implies@Q)@P)))) & (((![P:$i,Q:$i]: (((~ (a_truth@P)) | (a_truth@Q)) | (~ (a_truth@((implies@P)@Q))))) & (![P:$i,Q:$i]: (a_truth@((implies@P)@((implies@Q)@P))))) & (~ (a_truth@((implies@sK1)@sK1))))))=$true)),inference(copy,[status(thm)],[5])). thf(7,plain,(((~ ((~ (![SX0:$i,SX1:$i,SX2:$i]: (a_truth@((implies@((implies@SX0)@((implies@SX1)@SX2)))@((implies@((implies@SX0)@SX1))@((implies@SX0)@SX2)))))) | (~ (~ ((~ (![SX0:$i,SX1:$i]: (a_truth@((implies@((implies@(not@SX0))@(not@SX1)))@((implies@SX1)@SX0))))) | (~ (~ ((~ (~ ((~ (![SX0:$i,SX1:$i]: (((~ (a_truth@SX0)) | (a_truth@SX1)) | (~ (a_truth@((implies@SX0)@SX1)))))) | (~ (![SX0:$i,SX1:$i]: (a_truth@((implies@SX0)@((implies@SX1)@SX0)))))))) | (~ (~ (a_truth@((implies@sK1)@sK1))))))))))))=$true)),inference(unfold_def,[status(thm)],[6])). thf(8,plain,((((~ (![SX0:$i,SX1:$i,SX2:$i]: (a_truth@((implies@((implies@SX0)@((implies@SX1)@SX2)))@((implies@((implies@SX0)@SX1))@((implies@SX0)@SX2)))))) | (~ (~ ((~ (![SX0:$i,SX1:$i]: (a_truth@((implies@((implies@(not@SX0))@(not@SX1)))@((implies@SX1)@SX0))))) | (~ (~ ((~ (~ ((~ (![SX0:$i,SX1:$i]: (((~ (a_truth@SX0)) | (a_truth@SX1)) | (~ (a_truth@((implies@SX0)@SX1)))))) | (~ (![SX0:$i,SX1:$i]: (a_truth@((implies@SX0)@((implies@SX1)@SX0)))))))) | (~ (~ (a_truth@((implies@sK1)@sK1)))))))))))=$false)),inference(extcnf_not_pos,[status(thm)],[7])). thf(9,plain,(((~ (![SX0:$i,SX1:$i,SX2:$i]: (a_truth@((implies@((implies@SX0)@((implies@SX1)@SX2)))@((implies@((implies@SX0)@SX1))@((implies@SX0)@SX2))))))=$false)),inference(extcnf_or_neg,[status(thm)],[8])). thf(10,plain,(((~ (~ ((~ (![SX0:$i,SX1:$i]: (a_truth@((implies@((implies@(not@SX0))@(not@SX1)))@((implies@SX1)@SX0))))) | (~ (~ ((~ (~ ((~ (![SX0:$i,SX1:$i]: (((~ (a_truth@SX0)) | (a_truth@SX1)) | (~ (a_truth@((implies@SX0)@SX1)))))) | (~ (![SX0:$i,SX1:$i]: (a_truth@((implies@SX0)@((implies@SX1)@SX0)))))))) | (~ (~ (a_truth@((implies@sK1)@sK1))))))))))=$false)),inference(extcnf_or_neg,[status(thm)],[8])). thf(11,plain,(((![SX0:$i,SX1:$i,SX2:$i]: (a_truth@((implies@((implies@SX0)@((implies@SX1)@SX2)))@((implies@((implies@SX0)@SX1))@((implies@SX0)@SX2)))))=$true)),inference(extcnf_not_neg,[status(thm)],[9])). thf(12,plain,(((~ ((~ (![SX0:$i,SX1:$i]: (a_truth@((implies@((implies@(not@SX0))@(not@SX1)))@((implies@SX1)@SX0))))) | (~ (~ ((~ (~ ((~ (![SX0:$i,SX1:$i]: (((~ (a_truth@SX0)) | (a_truth@SX1)) | (~ (a_truth@((implies@SX0)@SX1)))))) | (~ (![SX0:$i,SX1:$i]: (a_truth@((implies@SX0)@((implies@SX1)@SX0)))))))) | (~ (~ (a_truth@((implies@sK1)@sK1)))))))))=$true)),inference(extcnf_not_neg,[status(thm)],[10])). thf(13,plain,(![SV1:$i]: (((![SY10:$i,SY11:$i]: (a_truth@((implies@((implies@SV1)@((implies@SY10)@SY11)))@((implies@((implies@SV1)@SY10))@((implies@SV1)@SY11)))))=$true))),inference(extcnf_forall_pos,[status(thm)],[11])). thf(14,plain,((((~ (![SX0:$i,SX1:$i]: (a_truth@((implies@((implies@(not@SX0))@(not@SX1)))@((implies@SX1)@SX0))))) | (~ (~ ((~ (~ ((~ (![SX0:$i,SX1:$i]: (((~ (a_truth@SX0)) | (a_truth@SX1)) | (~ (a_truth@((implies@SX0)@SX1)))))) | (~ (![SX0:$i,SX1:$i]: (a_truth@((implies@SX0)@((implies@SX1)@SX0)))))))) | (~ (~ (a_truth@((implies@sK1)@sK1))))))))=$false)),inference(extcnf_not_pos,[status(thm)],[12])). thf(15,plain,(![SV2:$i,SV1:$i]: (((![SY12:$i]: (a_truth@((implies@((implies@SV1)@((implies@SV2)@SY12)))@((implies@((implies@SV1)@SV2))@((implies@SV1)@SY12)))))=$true))),inference(extcnf_forall_pos,[status(thm)],[13])). thf(17,plain,(((~ (~ ((~ (~ ((~ (![SX0:$i,SX1:$i]: (((~ (a_truth@SX0)) | (a_truth@SX1)) | (~ (a_truth@((implies@SX0)@SX1)))))) | (~ (![SX0:$i,SX1:$i]: (a_truth@((implies@SX0)@((implies@SX1)@SX0)))))))) | (~ (~ (a_truth@((implies@sK1)@sK1)))))))=$false)),inference(extcnf_or_neg,[status(thm)],[14])). thf(18,plain,(![SV3:$i,SV2:$i,SV1:$i]: (((a_truth@((implies@((implies@SV1)@((implies@SV2)@SV3)))@((implies@((implies@SV1)@SV2))@((implies@SV1)@SV3))))=$true))),inference(extcnf_forall_pos,[status(thm)],[15])). thf(20,plain,(((~ ((~ (~ ((~ (![SX0:$i,SX1:$i]: (((~ (a_truth@SX0)) | (a_truth@SX1)) | (~ (a_truth@((implies@SX0)@SX1)))))) | (~ (![SX0:$i,SX1:$i]: (a_truth@((implies@SX0)@((implies@SX1)@SX0)))))))) | (~ (~ (a_truth@((implies@sK1)@sK1))))))=$true)),inference(extcnf_not_neg,[status(thm)],[17])). thf(22,plain,((((~ (~ ((~ (![SX0:$i,SX1:$i]: (((~ (a_truth@SX0)) | (a_truth@SX1)) | (~ (a_truth@((implies@SX0)@SX1)))))) | (~ (![SX0:$i,SX1:$i]: (a_truth@((implies@SX0)@((implies@SX1)@SX0)))))))) | (~ (~ (a_truth@((implies@sK1)@sK1)))))=$false)),inference(extcnf_not_pos,[status(thm)],[20])). thf(24,plain,(((~ (~ ((~ (![SX0:$i,SX1:$i]: (((~ (a_truth@SX0)) | (a_truth@SX1)) | (~ (a_truth@((implies@SX0)@SX1)))))) | (~ (![SX0:$i,SX1:$i]: (a_truth@((implies@SX0)@((implies@SX1)@SX0))))))))=$false)),inference(extcnf_or_neg,[status(thm)],[22])). thf(25,plain,(((~ (~ (a_truth@((implies@sK1)@sK1))))=$false)),inference(extcnf_or_neg,[status(thm)],[22])). thf(26,plain,(((~ ((~ (![SX0:$i,SX1:$i]: (((~ (a_truth@SX0)) | (a_truth@SX1)) | (~ (a_truth@((implies@SX0)@SX1)))))) | (~ (![SX0:$i,SX1:$i]: (a_truth@((implies@SX0)@((implies@SX1)@SX0)))))))=$true)),inference(extcnf_not_neg,[status(thm)],[24])). thf(27,plain,(((~ (a_truth@((implies@sK1)@sK1)))=$true)),inference(extcnf_not_neg,[status(thm)],[25])). thf(28,plain,((((~ (![SX0:$i,SX1:$i]: (((~ (a_truth@SX0)) | (a_truth@SX1)) | (~ (a_truth@((implies@SX0)@SX1)))))) | (~ (![SX0:$i,SX1:$i]: (a_truth@((implies@SX0)@((implies@SX1)@SX0))))))=$false)),inference(extcnf_not_pos,[status(thm)],[26])). thf(29,plain,(((a_truth@((implies@sK1)@sK1))=$false)),inference(extcnf_not_pos,[status(thm)],[27])). thf(30,plain,(((~ (![SX0:$i,SX1:$i]: (((~ (a_truth@SX0)) | (a_truth@SX1)) | (~ (a_truth@((implies@SX0)@SX1))))))=$false)),inference(extcnf_or_neg,[status(thm)],[28])). thf(31,plain,(((~ (![SX0:$i,SX1:$i]: (a_truth@((implies@SX0)@((implies@SX1)@SX0)))))=$false)),inference(extcnf_or_neg,[status(thm)],[28])). thf(32,plain,(((![SX0:$i,SX1:$i]: (((~ (a_truth@SX0)) | (a_truth@SX1)) | (~ (a_truth@((implies@SX0)@SX1)))))=$true)),inference(extcnf_not_neg,[status(thm)],[30])). thf(33,plain,(((![SX0:$i,SX1:$i]: (a_truth@((implies@SX0)@((implies@SX1)@SX0))))=$true)),inference(extcnf_not_neg,[status(thm)],[31])). thf(34,plain,(![SV6:$i]: (((![SY14:$i]: (((~ (a_truth@SV6)) | (a_truth@SY14)) | (~ (a_truth@((implies@SV6)@SY14)))))=$true))),inference(extcnf_forall_pos,[status(thm)],[32])). thf(35,plain,(![SV7:$i]: (((![SY15:$i]: (a_truth@((implies@SV7)@((implies@SY15)@SV7))))=$true))),inference(extcnf_forall_pos,[status(thm)],[33])). thf(36,plain,(![SV8:$i,SV6:$i]: (((((~ (a_truth@SV6)) | (a_truth@SV8)) | (~ (a_truth@((implies@SV6)@SV8))))=$true))),inference(extcnf_forall_pos,[status(thm)],[34])). thf(37,plain,(![SV9:$i,SV7:$i]: (((a_truth@((implies@SV7)@((implies@SV9)@SV7)))=$true))),inference(extcnf_forall_pos,[status(thm)],[35])). thf(38,plain,(![SV8:$i,SV6:$i]: ((((~ (a_truth@SV6)) | (a_truth@SV8))=$true) | ((~ (a_truth@((implies@SV6)@SV8)))=$true))),inference(extcnf_or_pos,[status(thm)],[36])). thf(39,plain,(![SV8:$i,SV6:$i]: (((a_truth@((implies@SV6)@SV8))=$false) | (((~ (a_truth@SV6)) | (a_truth@SV8))=$true))),inference(extcnf_not_pos,[status(thm)],[38])). thf(40,plain,(![SV8:$i,SV6:$i]: (((~ (a_truth@SV6))=$true) | ((a_truth@SV8)=$true) | ((a_truth@((implies@SV6)@SV8))=$false))),inference(extcnf_or_pos,[status(thm)],[39])). thf(41,plain,(![SV8:$i,SV6:$i]: (((a_truth@SV6)=$false) | ((a_truth@((implies@SV6)@SV8))=$false) | ((a_truth@SV8)=$true))),inference(extcnf_not_pos,[status(thm)],[40])). thf(42,plain,((($false)=$true)),inference(fo_atp_e_( 1 : :![X1]:![X2]:(~(lit(ti(at(ti(a_truth,ft(i,o)),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(X2,i)),ft(i,i)),ti(X1,i)),i)),o)))|(lit(ti(at(ti(a_truth,ft(i,o)),ti(X1,i)),o))|~(lit(ti(at(ti(a_truth,ft(i,o)),ti(X2,i)),o))))) : initial("/tmp/FNE045.p.atp_in", leo_II_clause_41) 2 : :~(lit(ti(at(ti(a_truth,ft(i,o)),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(sK1,i)),ft(i,i)),ti(sK1,i)),i)),o))) : initial("/tmp/FNE045.p.atp_in", leo_II_clause_29) 3 : :![X3]:![X4]:![X5]:lit(ti(at(ti(a_truth,ft(i,o)),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(X5,i)),ft(i,i)),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(X4,i)),ft(i,i)),ti(X3,i)),i)),i)),ft(i,i)),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(X5,i)),ft(i,i)),ti(X4,i)),i)),ft(i,i)),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(X5,i)),ft(i,i)),ti(X3,i)),i)),i)),i)),o)) : initial("/tmp/FNE045.p.atp_in", leo_II_clause_18) 4 : :![X6]:![X7]:lit(ti(at(ti(a_truth,ft(i,o)),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(at(ti(not,ft(i,i)),ti(X7,i)),i)),ft(i,i)),ti(at(ti(not,ft(i,i)),ti(X6,i)),i)),i)),ft(i,i)),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(X6,i)),ft(i,i)),ti(X7,i)),i)),i)),o)) : initial("/tmp/FNE045.p.atp_in", leo_II_clause_23) 5 : :![X8]:![X9]:lit(ti(at(ti(a_truth,ft(i,o)),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(X9,i)),ft(i,i)),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(X8,i)),ft(i,i)),ti(X9,i)),i)),i)),o)) : initial("/tmp/FNE045.p.atp_in", leo_II_clause_37) 6 : :![X1]:![X2]:(~lit(ti(at(ti(a_truth,ft(i,o)),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(X2,i)),ft(i,i)),ti(X1,i)),i)),o))|(lit(ti(at(ti(a_truth,ft(i,o)),ti(X1,i)),o))|~lit(ti(at(ti(a_truth,ft(i,o)),ti(X2,i)),o)))) : fof_simplification(1) 7 : :~lit(ti(at(ti(a_truth,ft(i,o)),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(sK1,i)),ft(i,i)),ti(sK1,i)),i)),o)) : fof_simplification(2) # Garbage collection reclaimed 10 unused term cells. 8 : :![X3]:![X4]:(~lit(ti(at(ti(a_truth,ft(i,o)),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(X4,i)),ft(i,i)),ti(X3,i)),i)),o))|(lit(ti(at(ti(a_truth,ft(i,o)),ti(X3,i)),o))|~lit(ti(at(ti(a_truth,ft(i,o)),ti(X4,i)),o)))) : variable_rename(6) 9 : :[++lit(ti(at(ti(a_truth,ft(i,o)),ti(X2,i)),o)),--lit(ti(at(ti(a_truth,ft(i,o)),ti(X1,i)),o)),--lit(ti(at(ti(a_truth,ft(i,o)),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(X1,i)),ft(i,i)),ti(X2,i)),i)),o))] : split_conjunct(8) 10 : :[--lit(ti(at(ti(a_truth,ft(i,o)),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(sK1,i)),ft(i,i)),ti(sK1,i)),i)),o))] : split_conjunct(7) 11 : :![X6]:![X7]:![X8]:lit(ti(at(ti(a_truth,ft(i,o)),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(X8,i)),ft(i,i)),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(X7,i)),ft(i,i)),ti(X6,i)),i)),i)),ft(i,i)),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(X8,i)),ft(i,i)),ti(X7,i)),i)),ft(i,i)),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(X8,i)),ft(i,i)),ti(X6,i)),i)),i)),i)),o)) : variable_rename(3) 12 : :[++lit(ti(at(ti(a_truth,ft(i,o)),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(X1,i)),ft(i,i)),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(X2,i)),ft(i,i)),ti(X3,i)),i)),i)),ft(i,i)),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(X1,i)),ft(i,i)),ti(X2,i)),i)),ft(i,i)),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(X1,i)),ft(i,i)),ti(X3,i)),i)),i)),i)),o))] : split_conjunct(11) # Garbage collection reclaimed 83 unused term cells. 13 : :![X8]:![X9]:lit(ti(at(ti(a_truth,ft(i,o)),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(at(ti(not,ft(i,i)),ti(X9,i)),i)),ft(i,i)),ti(at(ti(not,ft(i,i)),ti(X8,i)),i)),i)),ft(i,i)),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(X8,i)),ft(i,i)),ti(X9,i)),i)),i)),o)) : variable_rename(4) 14 : :[++lit(ti(at(ti(a_truth,ft(i,o)),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(at(ti(not,ft(i,i)),ti(X1,i)),i)),ft(i,i)),ti(at(ti(not,ft(i,i)),ti(X2,i)),i)),i)),ft(i,i)),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(X2,i)),ft(i,i)),ti(X1,i)),i)),i)),o))] : split_conjunct(13) 15 : :![X10]:![X11]:lit(ti(at(ti(a_truth,ft(i,o)),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(X11,i)),ft(i,i)),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(X10,i)),ft(i,i)),ti(X11,i)),i)),i)),o)) : variable_rename(5) 16 : :[++lit(ti(at(ti(a_truth,ft(i,o)),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(X1,i)),ft(i,i)),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(X2,i)),ft(i,i)),ti(X1,i)),i)),i)),o))] : split_conjunct(15) # Garbage collection reclaimed 74 unused term cells. # Auto-Ordering is analysing problem. # Problem is type HUNSGFFMF22MD # Auto-mode selected ordering type KBO6 # Auto-mode selected ordering precedence scheme # Auto-mode selected weight ordering scheme # # Auto-Heuristic is analysing problem. # Problem is type HUNSGFFMF22MD # Auto-Mode selected heuristic G_E___107_C41_F1_PI_AE_Q4_CS_SP_PS_S0Y # and selection function SelectMaxLComplexAvoidPosPred. # # No equality, disabling AC handling. # # Initializing proof state # Preprocessing time : 0.007 s # Presaturation interreduction done 17 : :[++lit(ti(at(ti(a_truth,ft(i,o)),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(X1,i)),ft(i,i)),ti(X2,i)),i)),o)),--lit(ti(at(ti(a_truth,ft(i,o)),ti(X2,i)),o))] : spm(9,16) 18 : :[++lit(ti(at(ti(a_truth,ft(i,o)),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(X1,i)),ft(i,i)),ti(X2,i)),i)),o)),--lit(ti(at(ti(a_truth,ft(i,o)),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(at(ti(not,ft(i,i)),ti(X2,i)),i)),ft(i,i)),ti(at(ti(not,ft(i,i)),ti(X1,i)),i)),i)),o))] : spm(9,14) 19 : :[++lit(ti(at(ti(a_truth,ft(i,o)),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(X1,i)),ft(i,i)),ti(X2,i)),i)),ft(i,i)),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(X1,i)),ft(i,i)),ti(X3,i)),i)),i)),o)),--lit(ti(at(ti(a_truth,ft(i,o)),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(X1,i)),ft(i,i)),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(X2,i)),ft(i,i)),ti(X3,i)),i)),i)),o))] : spm(9,12) 20 : :[--lit(ti(at(ti(a_truth,ft(i,o)),ti(sK1,i)),o))] : spm(10,17) 21 : :[++lit(ti(at(ti(a_truth,ft(i,o)),ti(X1,i)),o)),--lit(ti(at(ti(a_truth,ft(i,o)),ti(X2,i)),o)),--lit(ti(at(ti(a_truth,ft(i,o)),ti(X1,i)),o))] : spm(9,17) 22 : :[++lit(ti(at(ti(a_truth,ft(i,o)),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(X1,i)),ft(i,i)),ti(X2,i)),i)),o)),--lit(ti(at(ti(a_truth,ft(i,o)),ti(at(ti(not,ft(i,i)),ti(X1,i)),i)),o))] : spm(18,17) 23 : :[--lit(ti(at(ti(a_truth,ft(i,o)),ti(at(ti(not,ft(i,i)),ti(sK1,i)),i)),o))] : spm(10,22) 24 : :[++lit(ti(at(ti(a_truth,ft(i,o)),ti(X1,i)),o)),--lit(ti(at(ti(a_truth,ft(i,o)),ti(X2,i)),o)),--lit(ti(at(ti(a_truth,ft(i,o)),ti(at(ti(not,ft(i,i)),ti(X2,i)),i)),o))] : spm(9,22) 25 : :[++lit(ti(at(ti(a_truth,ft(i,o)),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(X1,i)),ft(i,i)),ti(X2,i)),i)),o)),--lit(ti(at(ti(a_truth,ft(i,o)),ti(at(ti(not,ft(i,i)),ti(at(ti(not,ft(i,i)),ti(X2,i)),i)),i)),o))] : spm(18,22) 26 : :[--lit(ti(at(ti(a_truth,ft(i,o)),ti(at(ti(not,ft(i,i)),ti(at(ti(not,ft(i,i)),ti(sK1,i)),i)),i)),o))] : spm(10,25) 27 : :[++lit(ti(at(ti(a_truth,ft(i,o)),ti(X1,i)),o)),--lit(ti(at(ti(a_truth,ft(i,o)),ti(X2,i)),o)),--lit(ti(at(ti(a_truth,ft(i,o)),ti(at(ti(not,ft(i,i)),ti(at(ti(not,ft(i,i)),ti(X1,i)),i)),i)),o))] : spm(9,25) 28 : :[++lit(ti(at(ti(a_truth,ft(i,o)),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(X1,i)),ft(i,i)),ti(X2,i)),i)),o)),--lit(ti(at(ti(a_truth,ft(i,o)),ti(at(ti(not,ft(i,i)),ti(at(ti(not,ft(i,i)),ti(at(ti(not,ft(i,i)),ti(X1,i)),i)),i)),i)),o))] : spm(18,25) 29 : :[++lit(ti(at(ti(a_truth,ft(i,o)),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(X1,i)),ft(i,i)),ti(X2,i)),i)),o)),--lit(ti(at(ti(a_truth,ft(i,o)),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(X1,i)),ft(i,i)),ti(X3,i)),i)),o)),--lit(ti(at(ti(a_truth,ft(i,o)),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(X1,i)),ft(i,i)),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(X3,i)),ft(i,i)),ti(X2,i)),i)),i)),o))] : spm(9,19) 30 : :[++lit(ti(at(ti(a_truth,ft(i,o)),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(X1,i)),ft(i,i)),ti(X2,i)),i)),o)),--lit(ti(at(ti(a_truth,ft(i,o)),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(X1,i)),ft(i,i)),ti(X3,i)),i)),o)),--lit(ti(at(ti(a_truth,ft(i,o)),ti(at(ti(not,ft(i,i)),ti(X1,i)),i)),o))] : spm(29,22) 31 : :[++lit(ti(at(ti(a_truth,ft(i,o)),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(X1,i)),ft(i,i)),ti(X2,i)),i)),o)),--lit(ti(at(ti(a_truth,ft(i,o)),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(X1,i)),ft(i,i)),ti(X3,i)),i)),o)),--lit(ti(at(ti(a_truth,ft(i,o)),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(X3,i)),ft(i,i)),ti(X2,i)),i)),o))] : spm(29,17) 32 : :[++lit(ti(at(ti(a_truth,ft(i,o)),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(X1,i)),ft(i,i)),ti(X2,i)),i)),o)),--lit(ti(at(ti(a_truth,ft(i,o)),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(X1,i)),ft(i,i)),ti(X3,i)),i)),o)),--lit(ti(at(ti(a_truth,ft(i,o)),ti(at(ti(not,ft(i,i)),ti(at(ti(not,ft(i,i)),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(X3,i)),ft(i,i)),ti(X2,i)),i)),i)),i)),o))] : spm(29,25) 33 : :[++lit(ti(at(ti(a_truth,ft(i,o)),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(X1,i)),ft(i,i)),ti(X1,i)),i)),o)),--lit(ti(at(ti(a_truth,ft(i,o)),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(X1,i)),ft(i,i)),ti(X2,i)),i)),o))] : spm(29,16) 34 : :[++lit(ti(at(ti(a_truth,ft(i,o)),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(at(ti(not,ft(i,i)),ti(X1,i)),i)),ft(i,i)),ti(at(ti(not,ft(i,i)),ti(X2,i)),i)),i)),ft(i,i)),ti(X1,i)),i)),o)),--lit(ti(at(ti(a_truth,ft(i,o)),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(at(ti(not,ft(i,i)),ti(X1,i)),i)),ft(i,i)),ti(at(ti(not,ft(i,i)),ti(X2,i)),i)),i)),ft(i,i)),ti(X2,i)),i)),o))] : spm(29,14) 35 : :[++lit(ti(at(ti(a_truth,ft(i,o)),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(X1,i)),ft(i,i)),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(X2,i)),ft(i,i)),ti(X3,i)),i)),i)),ft(i,i)),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(X1,i)),ft(i,i)),ti(X3,i)),i)),i)),o)),--lit(ti(at(ti(a_truth,ft(i,o)),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(X1,i)),ft(i,i)),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(X2,i)),ft(i,i)),ti(X3,i)),i)),i)),ft(i,i)),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(X1,i)),ft(i,i)),ti(X2,i)),i)),i)),o))] : spm(29,12) 36 : :[++lit(ti(at(ti(a_truth,ft(i,o)),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(X1,i)),ft(i,i)),ti(X2,i)),i)),ft(i,i)),ti(X3,i)),i)),o)),--lit(ti(at(ti(a_truth,ft(i,o)),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(X1,i)),ft(i,i)),ti(X2,i)),i)),ft(i,i)),ti(X1,i)),i)),o)),--lit(ti(at(ti(a_truth,ft(i,o)),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(X1,i)),ft(i,i)),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(X2,i)),ft(i,i)),ti(X3,i)),i)),i)),o))] : spm(29,19) 37 : :[++lit(ti(at(ti(a_truth,ft(i,o)),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(X1,i)),ft(i,i)),ti(X1,i)),i)),o)),--lit(ti(at(ti(a_truth,ft(i,o)),ti(at(ti(not,ft(i,i)),ti(X1,i)),i)),o))] : spm(33,22) 38 : :[++lit(ti(at(ti(a_truth,ft(i,o)),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(X1,i)),ft(i,i)),ti(X1,i)),i)),o)),--lit(ti(at(ti(a_truth,ft(i,o)),ti(X2,i)),o))] : spm(33,17) 39 : :[++lit(ti(at(ti(a_truth,ft(i,o)),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(X1,i)),ft(i,i)),ti(X1,i)),i)),o)),--lit(ti(at(ti(a_truth,ft(i,o)),ti(at(ti(not,ft(i,i)),ti(at(ti(not,ft(i,i)),ti(X2,i)),i)),i)),o))] : spm(33,25) 40 : :[++lit(ti(at(ti(a_truth,ft(i,o)),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(X1,i)),ft(i,i)),ti(X1,i)),i)),o))] : spm(33,16) 41 : :[++lit(ti(at(ti(a_truth,ft(i,o)),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(at(ti(not,ft(i,i)),ti(X1,i)),i)),ft(i,i)),ti(at(ti(not,ft(i,i)),ti(X2,i)),i)),i)),ft(i,i)),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(at(ti(not,ft(i,i)),ti(X1,i)),i)),ft(i,i)),ti(at(ti(not,ft(i,i)),ti(X2,i)),i)),i)),i)),o))] : spm(33,14) 42 : :[++lit(ti(at(ti(a_truth,ft(i,o)),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(X1,i)),ft(i,i)),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(X2,i)),ft(i,i)),ti(X3,i)),i)),i)),ft(i,i)),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(X1,i)),ft(i,i)),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(X2,i)),ft(i,i)),ti(X3,i)),i)),i)),i)),o))] : spm(33,12) 43 : :[++lit(ti(at(ti(a_truth,ft(i,o)),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(X1,i)),ft(i,i)),ti(X2,i)),i)),ft(i,i)),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(X1,i)),ft(i,i)),ti(X2,i)),i)),i)),o)),--lit(ti(at(ti(a_truth,ft(i,o)),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(X1,i)),ft(i,i)),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(X2,i)),ft(i,i)),ti(X3,i)),i)),i)),o))] : spm(33,19) 44 : :[++lit(ti(at(ti(a_truth,ft(i,o)),ti(X1,i)),o)),--lit(ti(at(ti(a_truth,ft(i,o)),ti(X1,i)),o))] : spm(9,40) 45 : :[++lit(ti(at(ti(a_truth,ft(i,o)),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(X1,i)),ft(i,i)),ti(X1,i)),i)),o))] : spm(18,40) 46 : :[++lit(ti(at(ti(a_truth,ft(i,o)),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(X1,i)),ft(i,i)),ti(X2,i)),i)),ft(i,i)),ti(X2,i)),i)),o)),--lit(ti(at(ti(a_truth,ft(i,o)),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(X1,i)),ft(i,i)),ti(X2,i)),i)),ft(i,i)),ti(X1,i)),i)),o))] : spm(29,40) 47 : :[++$true,--lit(ti(at(ti(a_truth,ft(i,o)),ti(at(ti(at(ti(implies,ft(i,ft(i,i))),ti(X1,i)),ft(i,i)),ti(X2,i)),i)),o))] : rw(33,40) 48 : :[--$true] : rw(10,40) 49 : :[] : cn(48) 50 : :[] : 49 : 'proof' # Proof found! # SZS intermediate status Unsatisfiable # Parsed axioms : 5 # Removed by relevancy pruning : 0 # Initial clauses : 5 # Removed in clause preprocessing : 0 # Initial clauses in saturation : 5 # Processed clauses : 24 # ...of these trivial : 0 # ...subsumed : 0 # ...remaining for further processing : 24 # Other redundant clauses eliminated : 0 # Clauses deleted for lack of memory : 0 # Backward-subsumed : 0 # Backward-rewritten : 2 # Generated clauses : 30 # ...of the previous two non-trivial : 26 # Contextual simplify-reflections : 0 # Paramodulations : 30 # Factorizations : 0 # Equation resolutions : 0 # Current number of processed clauses : 17 # Positive orientable unit clauses : 4 # Positive unorientable unit clauses: 0 # Negative unit clauses : 3 # Non-unit-clauses : 10 # Current number of unprocessed clauses: 6 # ...number of literals in the above : 16 # Clause-clause subsumption calls (NU) : 19 # Rec. Clause-clause subsumption calls : 19 # Unit Clause-clause subsumption calls : 8 # Rewrite failures with RHS unbound : 0 # Indexed BW rewrite attempts : 51 # Indexed BW rewrite successes : 2 # Unification attempts : 113 # Unification successes : 48 # Backwards rewriting index : 29 leaves, 4.76+/-6.532 terms/leaf # Paramod-from index : 1 leaves, 6.00+/-0.000 terms/leaf # Paramod-into index : 27 leaves, 4.33+/-5.354 terms/leaf # ------------------------------------------------- # User time : 0.007 s # System time : 0.003 s # Total time : 0.010 s # Maximum resident set size: 2804 pages ),[status(thm)],[41,37,18,29])). thf(43,plain,($false),inference(solved_all_splits,[solved_all_splits(join,[])],[42])). % SZS output end CNFRefutation %**** End of derivation protocol **** %**** no. of clauses in derivation: 39 **** WATCH: 0.03 CPU 0.06 WC FINAL WATCH: 0.03 CPU 0.06 WC