semantic tableau is method of finding whether the given logic (propositional logic here) is consistent or inconsistent, whether it is valid (tautology) or not.
execute ./run.sh on terminal and follow rest of the instructions that would come on the screen.
If it shows error : permission denied,
then firstly execute chmod +x run.sh and then execute ./run.sh.