Non-Theorems: a
([P] F&d)
[P]- ( (e&F)+([P] a-> a)-> [P] e->F)&[F] (b& F)-> d))
[P] c
(a<-> -[F]- (( c)<->[P]- (e->c))+ [P] [P] [P] d))<-> -c
b
b-> - - (e& -T&(- [P] ((e<->b<->F<->e)&( [F] ([F] c&d + (a+b) -> a + b
a -> [F] a
a -> [P] e&( [F] ( - (( (e&a&[P] d)->( a->b + c)->[P] b)& -d))
[F] d&F->[F] [P] [P] [F] (e->(((T->e)+(T->b))&(-e+(d->c))<-> (b<->b)& - ([F] ([P] (c->c<->b->F)+( F->[P] d))+ [F] ( [P] ( ( ((( [F] [P] a
- -T
- e + [P]a)&((e->(c<->a))->[F] c& b)&([F] (a<->[P](d<->e))&(- ((d->e)&[P] a)-> (c&d)+ T&(T + d))))->T)
[F] ([P] [F] ( [P] e&[P] [F] b)+ [F] e)))
[F] (b<->b)
[P] [F] ([F]- (-[P] (T + d)->[P] [F] T
[P] [P] b +(e +a)))->(a<->([F] a<-> e)+- F))+ T)
T + F