[FOM] A question about semantic tableaux

[Jined]

Good evening !

I am a logic student and I am desperately looking for the LaTeX package mentioned in the 
following lines

'' There is also an "unreleased" package which tweaks proof.sty (described here) to turn 
things upside down, which therefore produces a tableau proof with inferences marked by 
horizontal lines rather than sloping lines. ''

which can be found on this web page :

http://www.phil.cam.ac.uk/teaching_staff/Smith/LaTeX/tableaux.html

and which I would like to use to type semantic tableaux instead of the "tree solution" which I 
found rather ugly and unpractical when it comes to long proofs. The following paper contains 
semantic tableaux typed as I would like to type them : "Local model checking for infinite state 
space" by Julian Bradfield and Colin Stirling of the university of Edinburgh. I already sent 
them an email but did not received any answers yet, probably because they are on vacation 
or because my email did not reach them in the first place. Anyway, I was wondering if 
someone on this list would be kind enough to take a few minutes of his (her) time to help me.

Thanks in advance.

Best regards,

Jined.