Expression is: p
1:  => p fail

1:  =>  not p
1.1: p =>  fail
Expression is satisfiable

Expression is: (p or  not p)

1:  => (p or  not p)
1.1: p => p succeed
Expression is a tautlogy

Expression is: (p and  not p)

1:  => (p and  not p)
1.1:  => p fail
1.2:  =>  not p
1.2.1: p =>  fail


1:  =>  not (p and  not p)
1.1: (p and  not p) => 
1.1.1: p => p succeed
Expression is a contradiction

Expression is: ((p and (p->q))->q)

1:  => ((p and (p->q))->q)
1.1:  => ( not (p and (p->q)) or q)
1.1.1: (p and (p->q)) => q
1.1.1.1: (( not p or q) and p) => q
1.1.1.1.1: ( not p and p) => q
1.1.1.1.1.1: p => (p or q) succeed
1.1.1.1.2: (q and p) => q succeed
Expression is a tautlogy