# KEY # - not # + and # / or # > implies # = if and only if # a-z and A-J represent variables -(a=a) -(a>a) (-a^a) (-a=a) (a^-a) (a=-a) -(-ava) -(av-a) ---(a=a) ---(a>a) --(-a^a) --(-a=a) --(a^-a) --(a=-a) -(--a=a) -(--a>a) -(-a=-a) -(-a>-a) -(a=--a) -(a>--a) (---a^a) (---a=a) (--a^-a) (--a=-a) (-a^--a) (-a=--a) (a^---a) (a=---a) ---(-ava) ---(av-a) -(---ava) -(--av-a) -(-av--a) -(av---a) -----(a=a) -----(a>a) ----(-a^a) ----(-a=a) ----(a^-a) ----(a=-a) ---(--a=a) ---(--a>a) ---(-a=-a) ---(-a>-a) ---(a=--a) ---(a>--a) --(---a^a) --(---a=a) --(--a^-a) --(--a=-a) --(-a^--a) --(-a=--a) --(a^---a) --(a=---a) -(----a=a) -(----a>a) -(---a=-a) -(---a>-a) -(--a=--a) -(--a>--a) -(-a=---a) -(-a>---a) -((a^a)=a) -((a^a)>a) -((a^b)>a) -((a^b)>b) -((ava)=a) -((ava)>a) -((a=a)va) -((a=a)vb) -((a>a)va) -((a>a)vb) -((a>b)va) -(av(a=a)) -(av(a>a)) -(av(a>b)) -(av(b=b)) -(av(b>b)) -(a=----a) -(a=(a^a)) -(a=(ava)) -(a>----a) -(a>(a^a)) -(a>(ava)) -(a>(avb)) -(a>(a=a)) -(a>(a>a)) -(a>(bva)) -(a>(b=b)) -(a>(b>a)) -(a>(b>b)) (-----a^a) (-----a=a) (----a^-a) (----a=-a) (---a^--a) (---a=--a) (--a^---a) (--a=---a) (-(a^a)^a) (-(a^a)=a) (-(ava)^a) (-(ava)=a) (-(avb)^a) (-(avb)^b) (-(a=a)^a) (-(a=a)^b) (-(a>a)^a) (-(a>a)^b) (-(a>b)^b) (-a^----a) (-a^(a^a)) (-a^(a^b)) (-a^(ava)) (-a^(b^a)) (-a=----a) (-a=(a^a)) (-a=(ava)) ((-a^a)^a) ((-a^a)^b) ((-a^b)^a) ((-a=a)^a) ((-a=a)^b) ((a^-a)^a) ((a^-a)^b) ((a^-b)^b) ((a^a)^-a) ((a^a)=-a) ((a^b)^-a) ((a^b)^-b) ((ava)^-a) ((ava)=-a) ((a=-a)^a) ((a=-a)^b) ((a>-a)^a) ((a>-a)=a) (a^-----a) (a^-(a^a)) (a^-(ava)) (a^-(avb)) (a^-(a=a)) (a^-(a>a)) (a^-(bva)) (a^-(b=b)) (a^-(b>a)) (a^-(b>b)) (a^(-a^a)) (a^(-a^b)) (a^(-a=a)) (a^(-b^b)) (a^(-b=b)) (a^(a^-a)) (a^(a=-a)) (a^(a>-a)) (a^(b^-a)) (a^(b^-b)) (a^(b=-b)) (a=-----a) (a=-(a^a)) (a=-(ava)) (a=(a>-a)) -----(-ava) -----(av-a) ---(---ava) ---(--av-a) ---(-av--a) ---(av---a) -(-----ava) -(----av-a) -(---av--a) -(--av---a) -(-(a^a)va) -(-(a^b)va) -(-(a^b)vb) -(-(ava)va) -(-(a=a)>a) -(-(a=a)>b) -(-(a>a)>a) -(-(a>a)>b) -(-(a>b)>a) -(-av----a) -(-av(a^a)) -(-av(ava)) -(-av(avb)) -(-av(a=a)) -(-av(a>a)) -(-av(bva)) -(-av(b=b)) -(-av(b>a)) -(-av(b>b)) -(-a>(a=a)) -(-a>(a>a)) -(-a>(a>b)) -(-a>(b=b)) -(-a>(b>b)) -((-a^a)>a) -((-a^a)>b) -((-a^b)>b) -((-ava)va) -((-ava)vb) -((-avb)va) -((-a=a)>a) -((-a=a)>b) -((-a>a)=a) -((-a>a)>a) -((a^-a)>a) -((a^-a)>b) -((a^-b)>a) -((a^a)v-a) -((av-a)va) -((av-a)vb) -((av-b)vb) -((ava)v-a) -((avb)v-a) -((avb)v-b) -((a=-a)>a) -((a=-a)>b) -((a=a)v-a) -((a=a)v-b) -((a>-a)va) -((a>-b)va) -((a>-b)vb) -((a>a)v-a) -((a>a)v-b) -((a>b)v-b) -(av-----a) -(av-(a^a)) -(av-(a^b)) -(av-(ava)) -(av-(b^a)) -(av(-ava)) -(av(-avb)) -(av(-bvb)) -(av(av-a)) -(av(a>-a)) -(av(a>-b)) -(av(bv-a)) -(av(bv-b)) -(av(b>-a)) -(a=(-a>a)) -(a>(-ava)) -(a>(-a>a)) -(a>(-a>b)) -(a>(-bva)) -(a>(-bvb)) -(a>(-b>a)) -(a>(av-a)) -(a>(av-b)) -(a>(bv-b))