the glabellarness occurs.
sent1: if the fact that the circumscribing codex does not occur hold then that the glabellarness but not the providence happens is not right. sent2: if the circumscribing codex happens the providence occurs. sent3: the sinistralness happens. sent4: the circumscribing codex occurs. sent5: if the providence happens the glabellarness occurs.
sent2 & sent4 -> int1: that the providence occurs is right.; int1 & sent5 -> hypothesis;
the glabellarness does not occur.
$hypothesis$ = the glabellarness occurs. ; $context$ = sent1: if the fact that the circumscribing codex does not occur hold then that the glabellarness but not the providence happens is not right. sent2: if the circumscribing codex happens the providence occurs. sent3: the sinistralness happens. sent4: the circumscribing codex occurs. sent5: if the providence happens the glabellarness occurs. ; $proof$ = 
sent2 & sent4 -> int1: that the providence occurs is right.; int1 & sent5 -> hypothesis; __PROVED__