Non-Theorems: a

([P] F&d) [P]- ( (

(e&F)+([P] a->

a)->

[P] e->F)&[F] (b&

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

d)) [P] c (a<-> -[F]- ([F]- (F<->b)<->e))+ [F]-[P] b [F] a [P]- (b->

(( (e + d->

c)<->[P]- (e->c))+ [P]

[P] [P] d))<-> -c

b b-> - - (e& -T&(-

T-> - - (b->b<->-b))<->[P] b) -e +(

[P]

[P] ((e<->b<->F<->e)&( b->e))->[F] [P]

[F] ([F]

c&d + [F] (b&T)))

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

(a+b) ->

a +

b a -> [F]

a a -> [P] a T + [F]

e&( (d + [P]

[F] ( c& b))<->

- ((

(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)& (e<->a))) [F]-

- ([F] ([P] (c->c<->b->F)+(

F->[P] d))+ [F] ((a + T->[P] c)&(-a&(b + d)))) [F] [P] (- ([F] [F]- -[F] T +(

c + - (c->a))&[F]( b&(b<->F)<-> - T))->

(

[P] ( T&a)+(-[F](b<->d)+(d->b)))) [F] T T +

(

((( c<-> b)& (a->e)-> - (d&T+(b->a)))->

[P] (c&a))&([F] [F] (a +(c->c)<-> [P] a)->

[F] e))&d e->e [F] T +

[P]

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

e + [P]a)&((e->(c<->a))->[F] d)))->e - - ([F] ([F] ((e<->F)&

c&

b)&([F] (a<->[P](d<->e))&(- ((d->e)&[P] a)->

(c&d)+ T&(T + d))))->T) [F] ([P] [F]

[F] (b +-b +- (e<->b))+

( (d->( d<->F + b))+([P] (

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

T [P] [P] [F] (((-e +(a&e-> c)->[F] (

b +(e +a)))->(a<->([F] a<->

e)+-

F))+ T) T + F