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