Non-Theorems:

	a

        <P> ([P] F&d)

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

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

        [P] c

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

        [F] a

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

        <P> b

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

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

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

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

        <F> [P]-[P] e

Theorems:

        [F](a->b)   -> ([F]a -> [F]b)

        [P](a->b)   -> ([P]a -> [P]b)

        <F>(a+b) -> <F>a +<F>b

        <P>(a+b) -> <P>a +<P>b

        a -> [F]<P> a

        a -> [P]<F> a

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

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

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

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

        [F] T

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

        e->e

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

        - -T

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

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

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

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

        [F] (b<->b)

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

        [P]-F

        c + [F] <P> T

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

        T + F