the Bohemian happens if the Athenian occurs.
sent1: the Bohemianness happens if the acquainting nominal happens. sent2: the acquainting nominal happens if the caffeinicness happens. sent3: if the fact that the fact that the Athenian does not occur and the laving happens does not hold is correct then the caffeinicness occurs.
void -> assump1: Let's assume that the Athenianness occurs.; void -> assump2: Let's assume that both the non-Athenianness and the laving occurs.; assump2 -> int1: the Athenian does not occur.; assump1 & int1 -> int2: this is contradiction.; [assump2] & int2 -> int3: the fact that both the non-Athenianness and the laving happens is not correct.; sent3 & int3 -> int4: the caffeinicness happens.; sent2 & int4 -> int5: the acquainting nominal happens.; sent1 & int5 -> int6: that the Bohemianness occurs is not wrong.; [assump1] & int6 -> hypothesis;
$hypothesis$ = the Bohemian happens if the Athenian occurs. ; $context$ = sent1: the Bohemianness happens if the acquainting nominal happens. sent2: the acquainting nominal happens if the caffeinicness happens. sent3: if the fact that the fact that the Athenian does not occur and the laving happens does not hold is correct then the caffeinicness occurs. ; $proof$ = 
void -> assump1: Let's assume that the Athenianness occurs.; void -> assump2: Let's assume that both the non-Athenianness and the laving occurs.; assump2 -> int1: the Athenian does not occur.; assump1 & int1 -> int2: this is contradiction.; [assump2] & int2 -> int3: the fact that both the non-Athenianness and the laving happens is not correct.; sent3 & int3 -> int4: the caffeinicness happens.; sent2 & int4 -> int5: the acquainting nominal happens.; sent1 & int5 -> int6: that the Bohemianness occurs is not wrong.; [assump1] & int6 -> hypothesis; __PROVED__