the tracing is not mesic.
sent1: something is a kind of a Lampyridae and it is fibrocalcific if it is not mesic. sent2: there is something such that it is an adverbial. sent3: something is a Lampyridae. sent4: the fact that the bolt is both penal and not a Lampyridae is not true. sent5: that the bolt is not mesic is right if that it is non-Britannic and it is not ergonomic is wrong. sent6: the fact that the consomme is not non-adverbial but it does not rig Capitonidae does not hold. sent7: that that the bolt is penal thing that is a kind of a Lampyridae is right does not hold. sent8: the bolt is a Lampyridae if that it is penal thing that is not a Lampyridae is incorrect. sent9: the fact that the bolt is a kind of a dashed and does freckle erroneousness does not hold. sent10: the bolt is Jacobinic if the consomme is a kind of non-adverbial thing that whooshes. sent11: if the bolt does freckle erroneousness then it is an adverbial. sent12: if something is a Lampyridae and is an adverbial then the consomme does not whoosh. sent13: the consomme is penal. sent14: the fact that the bolt is a kind of non-Britannic thing that is not ergonomic does not hold if the tracing is not a kind of an approach. sent15: that the bolt is a dashed but it does not freckle erroneousness is incorrect. sent16: if the consomme does not whoosh then the tracing is not mesic. sent17: the bolt is a kind of an adverbial if the fact that it does dash and it does not freckle erroneousness is not right.
sent17 & sent15 -> int1: the bolt is a kind of an adverbial.; sent8 & sent4 -> int2: the bolt is a Lampyridae.; int1 & int2 -> int3: the bolt is a Lampyridae that is adverbial.; int3 -> int4: there is something such that it is a kind of a Lampyridae and it is a kind of an adverbial.; int4 & sent12 -> int5: that the consomme does not whoosh is true.; int5 & sent16 -> hypothesis;
there exists something such that it is not non-Jacobinic but fibrocalcific.
sent1 -> int6: if that the bolt is not mesic is not false it is a Lampyridae and it is fibrocalcific.;
$hypothesis$ = the tracing is not mesic. ; $context$ = sent1: something is a kind of a Lampyridae and it is fibrocalcific if it is not mesic. sent2: there is something such that it is an adverbial. sent3: something is a Lampyridae. sent4: the fact that the bolt is both penal and not a Lampyridae is not true. sent5: that the bolt is not mesic is right if that it is non-Britannic and it is not ergonomic is wrong. sent6: the fact that the consomme is not non-adverbial but it does not rig Capitonidae does not hold. sent7: that that the bolt is penal thing that is a kind of a Lampyridae is right does not hold. sent8: the bolt is a Lampyridae if that it is penal thing that is not a Lampyridae is incorrect. sent9: the fact that the bolt is a kind of a dashed and does freckle erroneousness does not hold. sent10: the bolt is Jacobinic if the consomme is a kind of non-adverbial thing that whooshes. sent11: if the bolt does freckle erroneousness then it is an adverbial. sent12: if something is a Lampyridae and is an adverbial then the consomme does not whoosh. sent13: the consomme is penal. sent14: the fact that the bolt is a kind of non-Britannic thing that is not ergonomic does not hold if the tracing is not a kind of an approach. sent15: that the bolt is a dashed but it does not freckle erroneousness is incorrect. sent16: if the consomme does not whoosh then the tracing is not mesic. sent17: the bolt is a kind of an adverbial if the fact that it does dash and it does not freckle erroneousness is not right. ; $proof$ = 
sent17 & sent15 -> int1: the bolt is a kind of an adverbial.; sent8 & sent4 -> int2: the bolt is a Lampyridae.; int1 & int2 -> int3: the bolt is a Lampyridae that is adverbial.; int3 -> int4: there is something such that it is a kind of a Lampyridae and it is a kind of an adverbial.; int4 & sent12 -> int5: that the consomme does not whoosh is true.; int5 & sent16 -> hypothesis; __PROVED__