%% clause labels for included files in standard.in
% ACL-I
-Aclosed(x) | -Aclosed(y) | Aclosed(intersection(x,y)).
% ACL-FP2
-Aclosed(x) | -member(x,V) | member(x,fix(ACLOSURE)).
% DEF-ACL2
-Aclosed(x) | equal(Aclosure(x),x).
% AC-FU-OO
-AxCh | -FUNCTION(x) | ONEONE(composite(CHOICE,VERTSECT(inverse(x)))).
% AC-FU-Q
-AxCh | -FUNCTION(x) | subclass(composite(IMAGE(x),id(P(D(x)))),composite(Q,inverse(S))).
% AC-MEM
-AxCh | -member(pair(x,y),CHOICE) | member(y,x).
% AC-FS-CO
-AxCh | -member(x,FUNS) | equal(composite(x,composite(CHOICE,VERTSECT(inverse(x)))),id(R(x))).
% AC-BIJ
-AxCh | -member(x,FUNS) | member(composite(CHOICE,VERTSECT(inverse(x))),BIJ).
% AC-FS-Q
-AxCh | -member(x,FUNS) | member(pair(D(x),R(x)),composite(Q,inverse(S))).
% AC-AP
-AxCh | -member(x,V) | equal(0,x) | member(apply(CHOICE,x),x).
% AC-SS-2
-AxCh | -member(x,V) | member(pair(singleton(x),x),CHOICE).
% AC-SS-1
-AxCh | -member(x,V) | member(singleton(x),D(CHOICE)).
% AC-Z
-AxCh | -member(x,y) | -subclass(cart(y,y),union(Id,DISJOINT)) | equal(x,0) | equal(intersection(x,image(CHOICE,y)),singleton(apply(CHOICE,x))).
% AC-Z-LEM
-AxCh | -member(x,y) | equal(x,0) | member(apply(CHOICE,x),image(CHOICE,y)).
% AC-Z-COR
-AxCh | -subclass(cart(x,x),union(Id,DISJOINT)) | member(0,x) | subclass(image(IMAGE(id(image(CHOICE,x))),x),R(SINGLETON)).
% AX-CH-1
-AxCh | FUNCTION(CHOICE).
% AX-CH-3
-AxCh | equal(D(CHOICE),complement(singleton(0))).
% AC-VS-DO
-AxCh | equal(D(composite(CHOICE,VERTSECT(x))),intersection(D(x),D(VERTSECT(x)))).
% AC-RA
-AxCh | equal(R(CHOICE),V).
% AC-SG-2
-AxCh | equal(composite(CHOICE,SINGLETON),Id).
% AC-FP
-AxCh | equal(fix(composite(E,CHOICE)),complement(singleton(0))).
% AC-V
-AxCh | subclass(CHOICE,cart(V,V)).
% AX-CH-2
-AxCh | subclass(CHOICE,inverse(E)).
% AC-VS
-AxCh | subclass(composite(CHOICE,VERTSECT(x)),x).
% AC-IM-SC
-AxCh | subclass(image(CHOICE,x),U(x)).
% AC-SG-1
-AxCh | subclass(inverse(SINGLETON),CHOICE).
% RE-FU
-AxReg | -FUNCTION(x) | -subclass(x,composite(inverse(E),x)) | equal(x,0).
% RE-AX-3
-AxReg | -disjoint(P(x),complement(x)) | equal(x,V).
% RE-3'
-AxReg | -equal(U(x),x) | -equal(singleton(U(x)),x).
% RE-6A
-AxReg | -equal(first(x),x) | -member(x,cart(V,V)).
% RE-8A
-AxReg | -equal(first(x),x) | equal(second(x),x).
% RE-H
-AxReg | -equal(intersection(x,P(y)),y) | equal(H(x),y).
% RE-3
-AxReg | -equal(memb(x),x) | -equal(singleton(memb(x)),x).
% RE-5A
-AxReg | -equal(pair(x,y),x).
% RE-5B
-AxReg | -equal(pair(x,y),y).
% RE-6B
-AxReg | -equal(second(x),x) | -member(x,cart(V,V)).
% RE-8B
-AxReg | -equal(second(x),x) | equal(first(x),x).
% RE-2
-AxReg | -equal(singleton(x),x).
% RE-FUL-2
-AxReg | -full(x) | -subclass(intersection(x,P(y)),y) | subclass(x,y).
% RE-PC-SC
-AxReg | -member(P(x),U(x)).
% RE-PC
-AxReg | -member(P(x),x).
% RE-3''
-AxReg | -member(x,R(SINGLETON)) | -equal(U(x),x).
% RE-4-B9
-AxReg | -member(x,U(U(x))).
% RE-4-A
-AxReg | -member(x,U(x)).
% RE-4-B1
-AxReg | -member(x,V) | -equal(regular(union(y,singleton(x))),x) | disjoint(y,x).
% RE-7
-AxReg | -member(x,V) | -member(complement(x),V).
% RE-0'''
-AxReg | -member(x,V) | member(regular(union(y,singleton(x))),union(y,singleton(x))).
% RE-4-B3
-AxReg | -member(x,V) | member(regular(union(y,singleton(x))),y) | disjoint(y,x).
% RE-1
-AxReg | -member(x,x).
% RE-4
-AxReg | -member(x,y) | -member(y,x).
% RE-4-B8
-AxReg | -member(x,y) | -member(y,z) | -member(z,x).
% RE-1-SU
-AxReg | -member(x,y) | -subclass(y,x).
% RE-0''
-AxReg | -member(x,y) | member(regular(y),y).
% RE-AX-4
-AxReg | -subclass(P(x),x) | equal(x,V).
% RE-FUL-1
-AxReg | -subclass(U(x),x) | equal(x,0) | member(0,x).
% RE-OM
-AxReg | -subclass(omega,D(x)) | -subclass(composite(x,inverse(SUCC)),composite(E,x)).
% RE-E
-AxReg | -subclass(x,E) | -subclass(D(x),R(x)) | equal(x,0).
% RE-CO
-AxReg | -subclass(x,composite(E,x)) | equal(x,0).
% RE-IM
-AxReg | -subclass(x,image(E,x)) | equal(x,0).
% RE-E-BC
-AxReg | disjoint(E,BIGCUP).
% RE-E-IN
-AxReg | disjoint(E,inverse(E)).
% RE-E-SR
-AxReg | disjoint(E,inverse(S)).
% RE-0'
-AxReg | disjoint(regular(x),x).
% RE-REG-1
-AxReg | equal(REGULAR,V).
% RE-RUS
-AxReg | equal(RUSSELL,V).
% RE-E-FP
-AxReg | equal(fix(E),0).
% RE-DJT-E
-AxReg | equal(fix(composite(E,DISJOINT)),complement(singleton(0))).
% RE-ON-EQ
-AxReg | equal(intersection(FULL,P(FULL)),OMEGA).
% RE-0
-AxReg | equal(intersection(regular(x),x),0).
% AX-RG-2
-AxReg | equal(x,0) | equal(intersection(regular(x),x),0).
% RE-AX-1
-AxReg | equal(x,0) | member(regular(x),P(complement(x))).
% AX-RG-1
-AxReg | equal(x,0) | member(regular(x),x).
% RE-AX-2
-AxReg | equal(x,V) | member(regular(complement(x)),P(x)).
% X-BH-3
-BINHOM(x,y,z) | -BINHOM(u,v,y) | BINHOM(composite(x,u),v,z).
% X-BH-2
-BINHOM(x,y,z) | -BINHOM(u,v,y) | equal(composite(composite(x,u),v),composite(z,cross(composite(x,u),composite(x,u)))).
% X-BH-1
-BINHOM(x,y,z) | -BINHOM(u,v,y) | subclass(R(composite(x,u)),D(D(z))).
% EQV-CP2
-EQUIVALENCE(cart(x,y)) | equal(x,y) | equal(cart(x,y),0).
% EQV-I
-EQUIVALENCE(x) | -EQUIVALENCE(y) | EQUIVALENCE(intersection(x,y)).
% EQV-MEM4
-EQUIVALENCE(x) | -member(pair(y,z),x) | -member(pair(z,u),x) | member(pair(y,u),x).
% EQV-IM1
-EQUIVALENCE(x) | -member(pair(y,z),x) | equal(image(x,singleton(y)),image(x,singleton(z))).
% EQV-MEM2
-EQUIVALENCE(x) | -member(pair(y,z),x) | member(pair(y,y),x).
% EQV-MEM1
-EQUIVALENCE(x) | -member(pair(y,z),x) | member(pair(z,y),x).
% EQV-MEM3
-EQUIVALENCE(x) | -member(pair(y,z),x) | member(pair(z,z),x).
% EQV-RS
-EQUIVALENCE(x) | EQUIVALENCE(restrict(x,y,y)).
% EQV-RFX
-EQUIVALENCE(x) | REFLEXIVE(x).
% EQV-SYM
-EQUIVALENCE(x) | SYMMETRIC(x).
% EQV-TRV
-EQUIVALENCE(x) | TRANSITIVE(x).
% EQV-DO1
-EQUIVALENCE(x) | equal(D(x),fix(x)).
% EQV-RA1
-EQUIVALENCE(x) | equal(R(x),fix(x)).
% EQV-ID
-EQUIVALENCE(x) | equal(composite(Id,x),x).
% DF-EQV-1
-EQUIVALENCE(x) | equal(composite(x,inverse(x)),x).
% EQV-DF3
-EQUIVALENCE(x) | equal(composite(x,x),x).
% EQV-CP3
-EQUIVALENCE(x) | equal(image(complement(x),y),V) | subclass(cart(y,y),x).
% EQV-IM3
-EQUIVALENCE(x) | equal(image(x,singleton(y)),image(x,singleton(z))) | disjoint(image(x,singleton(y)),image(x,singleton(z))).
% EQV-DF2
-EQUIVALENCE(x) | equal(inverse(x),x).
% EQV-IM2
-EQUIVALENCE(x) | member(pair(y,z),x) | disjoint(image(x,singleton(y)),image(x,singleton(z))).
% EQV-C1
-EQUIVALENCE(x) | subclass(composite(complement(x),x),complement(x)).
% EQV-C2
-EQUIVALENCE(x) | subclass(composite(x,complement(x)),complement(x)).
% EQV-DF1
-EQUIVALENCE(x) | subclass(x,cart(V,V)).
% EQV-FP1
-EQUIVALENCE(x) | subclass(x,cart(fix(x),fix(x))).
% SP-DJT-3
-FUNCTION(DISJOINT).
% SP-DI-FU
-FUNCTION(Di).
% PSM-E-FU
-FUNCTION(E).
% RFX-LT-2
-FUNCTION(LEAST(x)) | -REFLEXIVE(x) | subclass(intersection(x,inverse(x)),Id).
% ID-SR-FU
-FUNCTION(S).
% FS-PC-3
-FUNCTION(U(x)) | subclass(x,FUNS).
% SP-V-FU
-FUNCTION(V).
% X-SV
-FUNCTION(composite(Id,x)) | -FUNCTION(composite(Id,y)) | FUNCTION(cross(x,y)).
% AP-CO-SV
-FUNCTION(composite(Id,x)) | -member(pair(y,z),composite(u,x)) | member(pair(apply(x,y),z),u).
% AP-9
-FUNCTION(composite(Id,x)) | -member(pair(y,z),x) | -member(pair(y,z),cart(V,V)) | equal(apply(x,y),z).
% CUT-FS1
-FUNCTION(composite(Id,x)) | -member(x,V) | member(x,image(inverse(IMAGE(id(cart(V,V)))),FUNS)).
% AP-11B
-FUNCTION(composite(Id,x)) | -member(y,D(composite(z,x))) | equal(apply(composite(z,x),y),apply(z,apply(x,y))).
% AP-10C
-FUNCTION(composite(Id,x)) | -member(y,D(x)) | -member(apply(x,y),z) | member(y,image(inverse(x),z)).
% AP-11A
-FUNCTION(composite(Id,x)) | -member(y,D(x)) | equal(apply(composite(z,x),y),apply(z,apply(x,y))).
% AP-1B
-FUNCTION(composite(Id,x)) | -member(y,D(x)) | equal(image(x,singleton(y)),singleton(apply(x,y))).
% AP-1A
-FUNCTION(composite(Id,x)) | -member(y,D(x)) | equal(memb(image(x,singleton(y))),apply(x,y)).
% AP-0B
-FUNCTION(composite(Id,x)) | -member(y,D(x)) | equal(ran(x,y,V),apply(x,y)).
% AP-0A
-FUNCTION(composite(Id,x)) | -member(y,D(x)) | equal(singleton(ran(x,y,V)),image(x,singleton(y))).
% AP-2
-FUNCTION(composite(Id,x)) | -member(y,D(x)) | member(apply(x,y),R(x)).
% SG-SV
-FUNCTION(composite(Id,x)) | -member(y,D(x)) | member(image(x,singleton(y)),R(SINGLETON)).
% AP-10B
-FUNCTION(composite(Id,x)) | -member(y,D(x)) | member(pair(y,apply(x,y)),cart(V,V)).
% AP-10A
-FUNCTION(composite(Id,x)) | -member(y,D(x)) | member(pair(y,apply(x,y)),x).
% AP-3
-FUNCTION(composite(Id,x)) | -member(y,R(x)) | equal(apply(x,dom(x,V,y)),y).
% RP-7C
-FUNCTION(composite(Id,x)) | -member(y,V) | member(restrict(x,y,z),V).
% AP-9A
-FUNCTION(composite(Id,x)) | -member(y,image(inverse(x),z)) | member(apply(x,y),z).
% FU-IM-2
-FUNCTION(composite(Id,x)) | -subclass(y,image(x,z)) | equal(image(x,intersection(z,image(inverse(x),y))),y).
% RP-7A
-FUNCTION(composite(Id,x)) | FUNCTION(restrict(x,y,z)).
% 1ST-OO-2
-FUNCTION(composite(Id,x)) | ONEONE(composite(id(x),inverse(FIRST))).
% X-SV-DI2
-FUNCTION(composite(Id,x)) | disjoint(cart(x,x),cross(Id,Di)).
% X-SV-2
-FUNCTION(composite(Id,x)) | disjoint(cart(x,x),cross(Id,complement(Id))).
% AP-SV-C1
-FUNCTION(composite(Id,x)) | equal(complement(composite(y,x)),union(composite(complement(y),x),complement(cart(D(x),V)))).
% AP-SV-C2
-FUNCTION(composite(Id,x)) | equal(composite(complement(composite(y,x)),id(D(x))),composite(complement(y),x)).
% AP-SV-C3
-FUNCTION(composite(Id,x)) | equal(composite(complement(x),id(D(x))),composite(Di,x)).
% FU-IDX-1
-FUNCTION(composite(Id,x)) | equal(composite(x,inverse(x)),id(R(x))).
% AP-FUNP3
-FUNCTION(composite(Id,x)) | equal(funpart(x),composite(Id,x)).
% FU-IM-1
-FUNCTION(composite(Id,x)) | equal(image(x,image(inverse(x),y)),intersection(R(x),y)).
% AP-1C
-FUNCTION(composite(Id,x)) | equal(image(x,singleton(y)),intersection(singleton(apply(x,y)),image(V,intersection(D(x),singleton(y))))).
% AP-FU-I1
-FUNCTION(composite(Id,x)) | equal(intersection(composite(y,x),composite(z,x)),composite(intersection(y,z),x)).
% AP-8
-FUNCTION(composite(Id,x)) | member(apply(x,y),V).
% AP-13
-FUNCTION(composite(Id,x)) | subclass(apply(composite(y,x),z),apply(y,apply(x,z))).
% FU-DF-3
-FUNCTION(composite(Id,x)) | subclass(composite(x,inverse(x)),Id).
% PN-2
-FUNCTION(composite(id(x),E)) | subclass(cart(x,x),union(Id,DISJOINT)).
% ID-IN-E
-FUNCTION(inverse(E)).
% IMG1STFU
-FUNCTION(inverse(FIRST)).
% ID-IN-SR
-FUNCTION(inverse(S)).
% IMG2NDFU
-FUNCTION(inverse(SECOND)).
% IMG-OO3B
-FUNCTION(inverse(x)) | -equal(D(x),V) | ONEONE(IMAGE(x)).
% 2ND-RO-6
-FUNCTION(inverse(x)) | FUNCTION(rotate(x)).
% FU-C-IN
-FUNCTION(inverse(x)) | equal(image(x,complement(y)),intersection(R(x),complement(image(x,y)))).
% FU-I-IN
-FUNCTION(inverse(x)) | equal(image(x,intersection(y,z)),intersection(image(x,y),image(x,z))).
% AP-FU-I2
-FUNCTION(inverse(x)) | equal(intersection(composite(x,y),composite(x,z)),composite(x,intersection(y,z))).
% FU-UP-3
-FUNCTION(pairset(pair(x,y),pair(x,z))) | equal(y,z).
% FU-UP-1
-FUNCTION(pairset(x,y)) | -member(x,V) | member(x,cart(V,V)).
% FU-UP-2
-FUNCTION(pairset(x,y)) | -member(y,V) | member(y,cart(V,V)).
% DF-OO-3
-FUNCTION(x) | -FUNCTION(inverse(x)) | ONEONE(x).
% IMG-X-FS
-FUNCTION(x) | -FUNCTION(inverse(y)) | subclass(image(IMAGE(cross(y,x)),FUNS),FUNS).
% AP-EXT-1
-FUNCTION(x) | -FUNCTION(y) | -equal(apply(x,first(notsub(x,y))),apply(y,first(notsub(x,y)))) | -subclass(D(x),D(y)) | subclass(x,y).
% FU-U
-FUNCTION(x) | -FUNCTION(y) | -equal(intersection(D(x),D(y)),0) | FUNCTION(union(x,y)).
% X-AP-FU
-FUNCTION(x) | -FUNCTION(y) | -member(pair(z,u),cart(D(x),D(y))) | equal(apply(cross(x,y),pair(z,u)),pair(apply(x,z),apply(y,u))).
% AP-EXT-2
-FUNCTION(x) | -FUNCTION(y) | -subclass(D(x),D(y)) | member(first(notsub(x,y)),D(x)) | subclass(x,y).
% UO-CO1
-FUNCTION(x) | -FUNCTION(y) | -subclass(R(x),D(y)) | -subclass(R(y),D(x)) | UNOP(composite(x,y)).
% FU-3
-FUNCTION(x) | -FUNCTION(y) | FUNCTION(composite(x,y)).
% X-FU
-FUNCTION(x) | -FUNCTION(y) | FUNCTION(cross(x,y)).
% FP-FU-SU
-FUNCTION(x) | -equal(D(intersection(x,complement(y))),0) | subclass(x,y).
% UO-V
-FUNCTION(x) | -equal(D(x),V) | UNOP(x).
% AP-1PT
-FUNCTION(x) | -equal(D(x),singleton(y)) | equal(cart(singleton(y),singleton(apply(x,y))),x).
% FU-DO-CO
-FUNCTION(x) | -equal(D(y),V) | -subclass(composite(y,z),composite(u,x)) | subclass(composite(x,inverse(z)),composite(inverse(u),y)).
% IMG-OO3A
-FUNCTION(x) | -equal(R(x),V) | ONEONE(IMAGE(inverse(x))).
% FU-IDX-3
-FUNCTION(x) | -equal(composite(x,x),x) | equal(composite(x,id(R(x))),id(R(x))).
% FU-SV-2
-FUNCTION(x) | -equal(first(y),first(z)) | -member(pair(y,z),cart(x,x)) | equal(second(y),second(z)).
% FU-SV-3
-FUNCTION(x) | -equal(first(y),first(z)) | -member(pair(y,z),cart(x,x)) | equal(y,z).
% FU-U-RA
-FUNCTION(x) | -equal(image(inverse(x),y),image(inverse(x),z)) | -subclass(union(y,z),R(x)) | equal(y,z).
% ZER-4
-FUNCTION(x) | -member(A(fix(composite(S,x))),fix(composite(S,x))) | -subclass(composite(x,S),composite(S,x)) | member(A(fix(composite(S,x))),fix(x)).
% FIN-FU3
-FUNCTION(x) | -member(D(x),FINITE) | member(x,FINITE).
% ZER-8
-FUNCTION(x) | -member(D(x),R(POWER)) | -subclass(R(x),D(x)) | -subclass(composite(x,S),composite(S,x)) | member(A(fix(composite(S,x))),fix(x)).
% AP-FU-SS
-FUNCTION(x) | -member(D(x),R(SINGLETON)) | member(R(x),R(SINGLETON)).
% CA-4-FU
-FUNCTION(x) | -member(D(x),V) | -subclass(P(D(x)),R(x)).
% FS-FU-DO
-FUNCTION(x) | -member(D(x),V) | member(x,FUNS).
% RP-6
-FUNCTION(x) | -member(D(x),V) | member(x,V).
% SP-FU-C
-FUNCTION(x) | -member(complement(x),V).
% AP-CO-FU
-FUNCTION(x) | -member(pair(y,z),composite(u,x)) | member(pair(apply(x,y),z),u).
% FU-SV-1
-FUNCTION(x) | -member(pair(y,z),x) | -member(pair(y,u),x) | equal(z,u).
% AP-FU
-FUNCTION(x) | -member(pair(y,z),x) | equal(apply(x,y),z).
% FS-FU
-FUNCTION(x) | -member(x,V) | member(x,FUNS).
% AP-11
-FUNCTION(x) | -member(y,D(x)) | equal(apply(composite(z,x),y),apply(z,apply(x,y))).
% AP-1B'
-FUNCTION(x) | -member(y,D(x)) | equal(image(x,singleton(y)),singleton(apply(x,y))).
% AP-10B'
-FUNCTION(x) | -member(y,D(x)) | member(pair(y,apply(x,y)),cart(V,V)).
% AP-10A'
-FUNCTION(x) | -member(y,D(x)) | member(pair(y,apply(x,y)),x).
% FIN-CO1
-FUNCTION(x) | -member(y,FINITE) | member(composite(x,y),FINITE).
% FIN-CO2
-FUNCTION(x) | -member(y,FINITE) | member(composite(y,inverse(x)),FINITE).
% FIN-FU1
-FUNCTION(x) | -member(y,FINITE) | member(image(x,y),FINITE).
% IMG-AP6
-FUNCTION(x) | -member(y,V) | equal(apply(IMAGE(composite(id(x),inverse(FIRST))),y),composite(x,id(y))).
% IMG-FUIM
-FUNCTION(x) | -member(y,V) | equal(image(IMAGE(x),P(y)),P(image(x,y))).
% FS-RS2
-FUNCTION(x) | -member(y,V) | member(composite(x,id(y)),FUNS).
% AX-RP
-FUNCTION(x) | -member(y,V) | member(image(x,y),V).
% FS-RS1
-FUNCTION(x) | -member(y,V) | member(restrict(x,y,z),FUNS).
% FU-ADJ
-FUNCTION(x) | -member(y,cart(V,V)) | FUNCTION(union(x,singleton(y))) | member(first(y),D(x)).
% AP-10-FU
-FUNCTION(x) | -member(y,x) | equal(apply(x,first(y)),second(y)).
% FU-OP
-FUNCTION(x) | -member(y,x) | member(y,cart(V,V)).
% FU-EXT
-FUNCTION(x) | -subclass(D(x),D(intersection(x,y))) | subclass(x,y).
% DEF-UO3
-FUNCTION(x) | -subclass(R(x),D(x)) | UNOP(x).
% AP-FU-FP
-FUNCTION(x) | -subclass(composite(x,y),composite(z,x)) | subclass(image(x,fix(y)),fix(z)).
% FP-RA-FU
-FUNCTION(x) | -subclass(x,composite(y,x)) | subclass(R(x),fix(y)).
% FU-IM-4
-FUNCTION(x) | -subclass(y,R(x)) | -subclass(image(inverse(x),y),image(inverse(x),z)) | subclass(y,z).
% FU-CO1
-FUNCTION(x) | -subclass(y,composite(z,x)) | subclass(composite(y,inverse(x)),z).
% FP-FU-IM
-FUNCTION(x) | -subclass(y,fix(x)) | equal(image(x,y),y).
% FU-IM-3
-FUNCTION(x) | -subclass(y,image(inverse(x),z)) | subclass(image(x,y),z).
% FU-IN-SU
-FUNCTION(x) | -subclass(y,inverse(x)) | equal(composite(x,y),id(D(y))).
% FU-SU-DO
-FUNCTION(x) | -subclass(y,x) | -subclass(D(x),D(y)) | equal(x,y).
% FU-1A
-FUNCTION(x) | -subclass(y,x) | FUNCTION(y).
% IDX-FURS
-FUNCTION(x) | -subclass(y,x) | equal(composite(x,id(D(y))),y).
% FU-SU-RS
-FUNCTION(x) | -subclass(y,x) | equal(intersection(x,cart(D(y),V)),y).
% ST-FU
-FUNCTION(x) | -subcommute(x,y) | -equal(D(x),V) | subcommute(x,inverse(y)).
% EQV-FU
-FUNCTION(x) | EQUIVALENCE(composite(inverse(x),x)).
% FU-F-O
-FUNCTION(x) | FUNCTION(composite(Id,intersection(y,complement(composite(Di,intersection(y,complement(x))))))).
% FU-2
-FUNCTION(x) | FUNCTION(intersection(x,y)).
% FU-1B
-FUNCTION(x) | FUNCTION(restrict(x,y,z)).
% FF-CP-1
-FUNCTION(x) | FUNCTIONFAMILY(cart(y,x)).
% IMG-OO2
-FUNCTION(x) | ONEONE(composite(IMAGE(inverse(x)),id(P(R(x))))).
% PS-CO-3
-FUNCTION(x) | disjoint(composite(PS,x),x).
% FU-DJ-IM
-FUNCTION(x) | disjoint(image(inverse(x),complement(y)),image(inverse(x),y)).
% FU-DJ-1
-FUNCTION(x) | disjoint(x,composite(Di,x)).
% IMG-RP
-FUNCTION(x) | equal(D(IMAGE(x)),V).
% VS-DO-FU
-FUNCTION(x) | equal(D(VERTSECT(x)),V).
% PSM-3
-FUNCTION(x) | equal(PSM(composite(S,x)),x).
% VS-BA-FU
-FUNCTION(x) | equal(composite(BIGCAP,VERTSECT(x)),x).
% IMG-POW
-FUNCTION(x) | equal(composite(IMAGE(IMAGE(x)),POWER),composite(POWER,IMAGE(x))).
% IMG-SR-4
-FUNCTION(x) | equal(composite(IMAGE(x),inverse(S)),composite(inverse(S),IMAGE(x))).
% ID-CO-FU
-FUNCTION(x) | equal(composite(Id,x),x).
% VS-FU-3
-FUNCTION(x) | equal(composite(VERTSECT(x),id(D(x))),composite(SINGLETON,x)).
% X-FU-DUP
-FUNCTION(x) | equal(composite(cross(x,x),DUP),composite(DUP,x)).
% IDX-FUID
-FUNCTION(x) | equal(composite(id(y),x),composite(x,id(image(inverse(x),y)))).
% FP-FU-I
-FUNCTION(x) | equal(composite(x,id(D(intersection(x,y)))),intersection(x,y)).
% FP-CO-FU
-FUNCTION(x) | equal(composite(x,id(fix(x))),id(fix(x))).
% FU-CO2
-FUNCTION(x) | equal(composite(x,intersection(composite(inverse(x),y),z)),intersection(y,composite(x,z))).
% FU-IDX1A
-FUNCTION(x) | equal(composite(x,inverse(x)),id(R(x))).
% AP-FUNP1
-FUNCTION(x) | equal(funpart(composite(y,x)),composite(funpart(y),x)).
% FUNPART2
-FUNCTION(x) | equal(funpart(x),x).
% FP-IM-FU
-FUNCTION(x) | equal(image(x,fix(x)),fix(x)).
% FU-I-RA
-FUNCTION(x) | equal(image(x,image(inverse(x),y)),intersection(R(x),y)).
% AP-1D
-FUNCTION(x) | equal(image(x,singleton(y)),singleton(A(image(x,singleton(y))))).
% AP-C-FU1
-FUNCTION(x) | equal(intersection(composite(y,x),complement(composite(z,x))),composite(intersection(y,complement(z)),x)).
% AP-FU-I
-FUNCTION(x) | equal(intersection(composite(y,x),composite(z,x)),composite(intersection(y,z),x)).
% FU-4
-FUNCTION(x) | equal(restrict(x,V,V),x).
% SBV-FU2
-FUNCTION(x) | equal(subvar(inverse(x)),intersection(P(D(x)),invar(x))).
% VS-FU-4
-FUNCTION(x) | equal(union(cart(complement(D(x)),singleton(0)),composite(SINGLETON,x)),VERTSECT(x)).
% AP-FU-C
-FUNCTION(x) | equal(union(composite(Di,x),complement(cart(D(x),V))),complement(x)).
% IMGFU-FP
-FUNCTION(x) | subclass(P(fix(x)),fix(IMAGE(x))).
% FS-PC-1
-FUNCTION(x) | subclass(P(x),FUNS).
% IMG-SG-1
-FUNCTION(x) | subclass(composite(SINGLETON,x),composite(IMAGE(x),SINGLETON)).
% IMG-OO1
-FUNCTION(x) | subclass(composite(id(P(R(x))),inverse(IMAGE(inverse(x)))),IMAGE(x)).
% DI-FU
-FUNCTION(x) | subclass(composite(inverse(x),composite(Di,x)),Di).
% DF-FU-2
-FUNCTION(x) | subclass(composite(x,inverse(x)),Id).
% FIN-FU2
-FUNCTION(x) | subclass(image(IMAGE(x),FINITE),FINITE).
% ZER-3
-FUNCTION(x) | subclass(image(x,fix(composite(y,x))),fix(composite(x,y))).
% SBV-FU1
-FUNCTION(x) | subclass(subvar(inverse(x)),invar(x)).
% DF-FU-1
-FUNCTION(x) | subclass(x,cart(V,V)).
% FU-TR-1'
-FUNCTION(x) | subclass(x,composite(Id,complement(composite(Di,x)))).
% TH-FU
-FUNCTION(x) | thin(x).
% AX-CH-4
-FUNCTION(z) | -subclass(z,inverse(E)) | -equal(D(z),complement(singleton(0))) | AxCh.
% FF-CP-2
-FUNCTIONFAMILY(cart(x,y)) | FUNCTION(y) | equal(x,0).
% FF-FU-X1
-FUNCTIONFAMILY(x) | -FUNCTION(y) | FUNCTIONFAMILY(composite(cross(Id,y),x)).
% FF-FU-X2
-FUNCTIONFAMILY(x) | -FUNCTION(y) | FUNCTIONFAMILY(composite(cross(inverse(y),Id),x)).
% FF-FU-CO
-FUNCTIONFAMILY(x) | -FUNCTION(y) | FUNCTIONFAMILY(composite(x,y)).
% FF-2
-FUNCTIONFAMILY(x) | -member(y,V) | FUNCTION(image(x,singleton(y))).
% FF-SU
-FUNCTIONFAMILY(x) | -subclass(y,x) | FUNCTIONFAMILY(y).
% DF-FF-1
-FUNCTIONFAMILY(x) | subclass(R(complement(composite(E,complement(x)))),FUNS).
% FF-1
-FUNCTIONFAMILY(x) | subclass(R(x),cart(V,V)).
% IND-0
-INDUCTIVE(0).
% IND-SS
-INDUCTIVE(singleton(x)).
% IND-I-1
-INDUCTIVE(x) | -INDUCTIVE(y) | INDUCTIVE(intersection(y,x)).
% SUC-IND2
-INDUCTIVE(x) | -member(x,V) | member(x,fix(composite(S,IMAGE(SUCC)))).
% SUC-IND3
-INDUCTIVE(x) | -member(x,V) | member(x,intersection(complement(P(complement(singleton(0)))),fix(composite(S,IMAGE(SUCC))))).
% SUC-IND1
-INDUCTIVE(x) | -member(y,x) | member(succ(y),x).
% DF-IND-1
-INDUCTIVE(x) | member(0,x).
% DF-IND-2
-INDUCTIVE(x) | subclass(image(SUCC,x),x).
% AX-OM-3
-INDUCTIVE(x) | subclass(omega,x).
% IND-SC-1
-INDUCTIVE(x) | subclass(x,U(x)).
% 1ST-OO-1
-ONEONE(composite(id(x),inverse(FIRST))) | FUNCTION(composite(Id,x)).
% OO-U-DJ
-ONEONE(x) | -ONEONE(y) | -disjoint(D(x),D(y)) | -disjoint(R(x),R(y)) | ONEONE(union(x,y)).
% OO-CO
-ONEONE(x) | -ONEONE(y) | ONEONE(composite(x,y)).
% DK-PIG
-ONEONE(x) | -member(D(x),DEDEKIND) | -subclass(R(x),D(x)) | equal(R(x),D(x)).
% BIJ-1-DO
-ONEONE(x) | -member(D(x),V) | member(x,BIJ).
% BIJ-1
-ONEONE(x) | -member(x,V) | member(x,BIJ).
% BIJ-OO2
-ONEONE(x) | -member(y,V) | member(composite(x,id(y)),BIJ).
% OO-SU
-ONEONE(x) | -subclass(y,x) | ONEONE(y).
% DF-OO-2
-ONEONE(x) | FUNCTION(inverse(x)).
% DF-OO-1
-ONEONE(x) | FUNCTION(x).
% OO-IN
-ONEONE(x) | ONEONE(inverse(x)).
% FU-IDX-2
-ONEONE(x) | equal(composite(inverse(x),x),id(D(x))).
% BIJ-OO1
-ONEONE(x) | subclass(P(x),BIJ).
% Q-OO
-ONEONE(x) | subclass(composite(IMAGE(x),id(P(D(x)))),Q).
% POR-I
-PARTIALORDER(x) | -REFLEXIVE(y) | -TRANSITIVE(y) | PARTIALORDER(intersection(x,y)).
% TO-DF-2
-PARTIALORDER(x) | -equal(union(x,inverse(x)),cart(fix(x),fix(x))) | TOTALORDER(x).
% WO-POR-2
-PARTIALORDER(x) | -subclass(P(fix(x)),union(singleton(0),D(LEAST(x)))) | WELLORDER(x).
% POR-RS
-PARTIALORDER(x) | PARTIALORDER(intersection(x,cart(y,y))).
% POR-IN
-PARTIALORDER(x) | PARTIALORDER(inverse(x)).
% POR-U-ID
-PARTIALORDER(x) | PARTIALORDER(union(x,id(y))).
% DEF-POR1
-PARTIALORDER(x) | REFLEXIVE(x).
% DEF-POR2
-PARTIALORDER(x) | TRANSITIVE(intersection(x,Di)).
% POR-DF-2
-PARTIALORDER(x) | TRANSITIVE(x).
% SBV-PO
-PARTIALORDER(x) | disjoint(D(LEAST(x)),subvar(intersection(Di,x))).
% POR-DF-5
-PARTIALORDER(x) | equal(composite(x,x),x).
% POR-DF-4
-PARTIALORDER(x) | equal(intersection(x,inverse(x)),id(fix(x))).
% POR-DF-1
-PARTIALORDER(x) | subclass(intersection(x,inverse(x)),Id).
% DEF-PN1
-PARTITION(x) | -member(0,x).
% DEF-PN2
-PARTITION(x) | subclass(cart(x,x),union(Id,DISJOINT)).
% RFX-CP2
-REFLEXIVE(cart(x,y)) | equal(x,y) | equal(cart(x,y),0).
% RFX-I
-REFLEXIVE(x) | -REFLEXIVE(y) | REFLEXIVE(intersection(x,y)).
% RFX-U
-REFLEXIVE(x) | -REFLEXIVE(y) | REFLEXIVE(union(x,y)).
% DEF-POR3
-REFLEXIVE(x) | -TRANSITIVE(intersection(x,Di)) | PARTIALORDER(x).
% RFX-V
-REFLEXIVE(x) | -member(fix(x),V) | member(x,V).
% RFX-UP
-REFLEXIVE(x) | -member(pair(y,z),x) | member(pair(pairset(y,z),y),LEAST(x)).
% RFX-1
-REFLEXIVE(x) | -member(pair(y,z),x) | member(pair(y,y),x).
% RFX-2
-REFLEXIVE(x) | -member(pair(y,z),x) | member(pair(z,z),x).
% DEF-WO-3
-REFLEXIVE(x) | -subclass(P(fix(x)),union(singleton(0),D(funpart(LEAST(x))))) | WELLORDER(x).
% POR-DF-3
-REFLEXIVE(x) | -subclass(intersection(x,inverse(x)),Id) | -TRANSITIVE(x) | PARTIALORDER(x).
% RFX-IN
-REFLEXIVE(x) | REFLEXIVE(inverse(x)).
% RFX-RS
-REFLEXIVE(x) | REFLEXIVE(restrict(x,y,y)).
% RFX-DO
-REFLEXIVE(x) | equal(D(x),fix(x)).
% RFX-RA
-REFLEXIVE(x) | equal(R(x),fix(x)).
% RFX-ID
-REFLEXIVE(x) | equal(composite(Id,x),x).
% SBV-RFX
-REFLEXIVE(x) | equal(subvar(x),P(fix(x))).
% RFX-LT-1
-REFLEXIVE(x) | subclass(intersection(x,inverse(x)),composite(LEAST(x),inverse(LEAST(x)))).
% DF-RFX-1
-REFLEXIVE(x) | subclass(x,cart(fix(x),fix(x))).
% RFX-CO
-REFLEXIVE(x) | subclass(x,composite(x,x)).
% SYM-CP2
-SYMMETRIC(cart(x,y)) | equal(x,y) | equal(cart(x,y),0).
% SYM-I
-SYMMETRIC(x) | -SYMMETRIC(y) | SYMMETRIC(intersection(x,y)).
% SYM-U
-SYMMETRIC(x) | -SYMMETRIC(y) | SYMMETRIC(union(x,y)).
% EQV-RST2
-SYMMETRIC(x) | -TRANSITIVE(x) | EQUIVALENCE(x).
% EQV-RST1
-SYMMETRIC(x) | -TRANSITIVE(x) | REFLEXIVE(x).
% SYM-V
-SYMMETRIC(x) | -member(D(x),V) | member(x,V).
% SYM-MEM
-SYMMETRIC(x) | -member(pair(y,z),x) | member(pair(z,y),x).
% SYM-RS
-SYMMETRIC(x) | SYMMETRIC(restrict(x,y,y)).
% SYM-RA
-SYMMETRIC(x) | equal(R(x),D(x)).
% SYM-ID
-SYMMETRIC(x) | equal(composite(Id,x),x).
% SYM-DF2
-SYMMETRIC(x) | equal(inverse(x),x).
% SYM-DF1
-SYMMETRIC(x) | subclass(x,cart(V,V)).
% DF-SYM-1
-SYMMETRIC(x) | subclass(x,inverse(x)).
% TO-DF-3
-TOTALORDER(x) | -member(pair(y,z),cart(fix(x),fix(x))) | member(pair(y,z),x) | member(pair(z,y),x).
% DEF-TO-1
-TOTALORDER(x) | PARTIALORDER(x).
% TO-RS
-TOTALORDER(x) | TOTALORDER(intersection(x,cart(y,y))).
% TO-IN
-TOTALORDER(x) | TOTALORDER(inverse(x)).
% DEF-TO-2
-TOTALORDER(x) | TRANSITIVE(intersection(Di,x)).
% DEF-TO-3
-TOTALORDER(x) | equal(union(x,inverse(x)),cart(fix(x),fix(x))).
% TO-DF-1
-TRANSITIVE(intersection(Di,x)) | -equal(union(x,inverse(x)),cart(fix(x),fix(x))) | TOTALORDER(x).
% TRV-DI-1
-TRANSITIVE(intersection(x,Di)) | TRANSITIVE(composite(Id,x)).
% TRV-DI-2
-TRANSITIVE(intersection(x,Di)) | subclass(intersection(x,inverse(x)),Id).
% TRV-I
-TRANSITIVE(x) | -TRANSITIVE(y) | TRANSITIVE(intersection(x,y)).
% TRV-MEM
-TRANSITIVE(x) | -member(pair(y,z),x) | -member(pair(z,u),x) | member(pair(y,u),x).
% TRV-IMSS
-TRANSITIVE(x) | -member(pair(y,z),x) | subclass(image(x,singleton(z)),image(x,singleton(y))).
% TRV-DI-3
-TRANSITIVE(x) | -subclass(intersection(x,inverse(x)),Id) | TRANSITIVE(intersection(x,Di)).
% TC-CLOS
-TRANSITIVE(x) | -subclass(inverse(E),x) | subclass(composite(inverse(E),TC),x).
% POR-DI
-TRANSITIVE(x) | -subclass(x,intersection(Di,cart(y,y))) | PARTIALORDER(union(x,id(y))).
% TRV-U-ID
-TRANSITIVE(x) | -subclass(y,Id) | TRANSITIVE(union(x,y)).
% TH-TRV
-TRANSITIVE(x) | -thin(x) | subclass(composite(VERTSECT(x),x),composite(inverse(S),VERTSECT(x))).
% TRV-IN
-TRANSITIVE(x) | TRANSITIVE(inverse(x)).
% TRV-RS
-TRANSITIVE(x) | TRANSITIVE(restrict(x,y,z)).
% TRV-ID
-TRANSITIVE(x) | equal(composite(Id,x),x).
% TRV-DF2
-TRANSITIVE(x) | subclass(composite(x,x),x).
% TRV-DF1
-TRANSITIVE(x) | subclass(x,cart(V,V)).
% DF-TRV-1
-TRANSITIVE(x) | subclass(x,composite(Id,complement(composite(complement(x),inverse(x))))).
% UNOPS-5
-UNOP(x) | -member(D(x),V) | member(x,UNOPS).
% UNOPS-4
-UNOP(x) | -member(x,V) | member(x,UNOPS).
% UO-RS2
-UNOP(x) | -member(y,invar(x)) | member(composite(x,id(y)),UNOPS).
% UO-RS1
-UNOP(x) | -subclass(image(x,y),y) | UNOP(composite(x,id(y))).
% DEF-UO1
-UNOP(x) | FUNCTION(x).
% UO-CO2
-UNOP(x) | UNOP(composite(x,x)).
% DEF-UO2
-UNOP(x) | subclass(R(x),D(x)).
% UCL-I
-Uclosed(x) | -Uclosed(y) | Uclosed(intersection(x,y)).
% UCL-FP2
-Uclosed(x) | -member(x,V) | member(x,fix(UCLOSURE)).
% DEF-UCL2
-Uclosed(x) | equal(Uclosure(x),x).
% WO-TRV-2
-WELLORDER(x) | -member(pair(y,z),x) | -member(pair(z,u),x) | member(pair(y,u),x).
% WO-SU-2
-WELLORDER(x) | -member(y,P(fix(x))) | -member(apply(LEAST(x),y),z) | -subclass(z,y) | equal(apply(LEAST(x),z),apply(LEAST(x),y)).
% WO-TRV-1
-WELLORDER(x) | -member(y,P(fix(x))) | -member(z,P(fix(x))) | -member(pair(apply(LEAST(x),y),apply(LEAST(x),z)),x) | equal(y,0) | equal(apply(LEAST(x),union(y,z)),apply(LEAST(x),y)).
% WO-SU-1
-WELLORDER(x) | -member(y,P(fix(x))) | -subclass(z,y) | equal(z,0) | member(pair(apply(LEAST(x),y),apply(LEAST(x),z)),x).
% WO-AP-1
-WELLORDER(x) | -member(y,P(fix(x))) | equal(y,0) | member(apply(LEAST(x),y),y).
% WO-AP-2
-WELLORDER(x) | -member(y,z) | -member(z,P(fix(x))) | member(pair(apply(LEAST(x),z),y),x).
% WO-FU-LT
-WELLORDER(x) | FUNCTION(LEAST(x)).
% WO-POR-1
-WELLORDER(x) | PARTIALORDER(x).
% DEF-WO-1
-WELLORDER(x) | REFLEXIVE(x).
% WO-TO-2
-WELLORDER(x) | TOTALORDER(x).
% WO-RS
-WELLORDER(x) | WELLORDER(intersection(x,cart(y,y))).
% WO-DO-LT
-WELLORDER(x) | equal(D(LEAST(x)),intersection(complement(singleton(0)),P(fix(x)))).
% WO-CO-ID
-WELLORDER(x) | equal(composite(Id,x),x).
% SBV-WO
-WELLORDER(x) | equal(subvar(intersection(Di,x)),singleton(0)).
% WO-TO-1
-WELLORDER(x) | equal(union(x,inverse(x)),cart(fix(x),fix(x))).
% DEF-WO-2
-WELLORDER(x) | subclass(P(fix(x)),union(singleton(0),D(funpart(LEAST(x))))).
% WO-TRV-3
-WELLORDER(x) | subclass(composite(x,x),x).
% WO-V
-WELLORDER(x) | subclass(x,cart(V,V)).
% CO-DO-DJ
-disjoint(D(x),D(y)) | equal(composite(x,inverse(y)),0).
% CO-DJ
-disjoint(D(x),R(y)) | equal(composite(x,y),0).
% IM-DJ-2
-disjoint(D(x),y) | equal(image(x,y),0).
% VS-11COR
-disjoint(D(x),y) | subclass(cart(y,singleton(0)),VERTSECT(x)).
% REG-20
-disjoint(DESCENDING,image(E,x)) | subclass(x,REGULAR).
% CO-DJ-DO
-disjoint(cart(V,D(x)),y) | equal(composite(x,y),0).
% X-SV-DI1
-disjoint(cart(x,x),cross(Id,Di)) | FUNCTION(composite(Id,x)).
% X-SV-1
-disjoint(cart(x,x),cross(Id,complement(Id))) | FUNCTION(composite(Id,x)).
% IM-CP-4'
-disjoint(cart(x,y),z) | disjoint(x,image(inverse(z),y)).
% IM-CP-4
-disjoint(cart(x,y),z) | disjoint(y,image(z,x)).
% CO-DJ-RO
-disjoint(composite(x,y),inverse(z)) | disjoint(composite(y,z),inverse(x)).
% CO-TR-DJ
-disjoint(composite(x,y),z) | disjoint(composite(z,inverse(y)),x).
% E-IM-DJ
-disjoint(image(E,x),image(E,y)) | equal(x,0) | equal(y,0).
% IMV-DJ
-disjoint(image(V,x),image(V,y)) | equal(x,0) | equal(y,0).
% DJ-ASS
-disjoint(intersection(x,y),z) | disjoint(x,intersection(y,z)).
% RE-AX-6E
-disjoint(x,IRREG) | AxReg | disjoint(P(x),IRREG).
% CO-DJ-RA
-disjoint(x,cart(R(y),V)) | equal(composite(x,y),0).
% DJ-9A
-disjoint(x,cart(y,z)) | equal(restrict(x,y,z),0).
% DJ-5B
-disjoint(x,complement(y)) | subclass(x,y).
% SV-DJ-2
-disjoint(x,composite(Di,x)) | subclass(composite(x,inverse(x)),Id).
% IM-CP-2'
-disjoint(x,image(inverse(y),z)) | disjoint(cart(x,z),y).
% IM-CP-2
-disjoint(x,image(y,z)) | disjoint(cart(z,x),y).
% IM-DJ-IN
-disjoint(x,image(y,z)) | disjoint(z,image(inverse(y),x)).
% IN-DJ-2
-disjoint(x,inverse(y)) | disjoint(y,inverse(x)).
% FP-DJ4
-disjoint(x,inverse(y)) | equal(fix(composite(x,y)),0).
% DJ-3A
-disjoint(x,x) | equal(x,0).
% DJ-7
-disjoint(x,y) | -disjoint(z,y) | disjoint(union(x,z),y).
% DJ-EQ
-disjoint(x,y) | -subclass(complement(x),y) | equal(complement(x),y).
% IN-DJ-1
-disjoint(x,y) | disjoint(inverse(x),inverse(y)).
% DJ-4
-disjoint(x,y) | disjoint(y,x).
% DJ-DEF-2
-disjoint(x,y) | equal(intersection(x,y),0).
% DI-DJ1
-disjoint(x,y) | subclass(composite(x,inverse(y)),Di).
% DJ-5C
-disjoint(x,y) | subclass(x,complement(y)).
% SP-SS-2
-equal(A(x),U(x)) | member(x,R(SINGLETON)).
% SP-A-C-B
-equal(A(x),complement(x)) | equal(x,0) | equal(x,V).
% DEF-ACL3
-equal(Aclosure(x),x) | Aclosed(x).
% IMG-DO-X
-equal(D(IMAGE(x)),V) | -equal(D(IMAGE(y)),V) | equal(D(IMAGE(cross(x,y))),V).
% IMG-CO-2
-equal(D(IMAGE(x)),V) | equal(composite(IMAGE(y),IMAGE(x)),IMAGE(composite(y,x))).
% IMG-SR-2
-equal(D(IMAGE(x)),V) | subclass(composite(IMAGE(x),inverse(S)),composite(inverse(S),IMAGE(x))).
% IVR-IMG3
-equal(D(IMAGE(x)),V) | subclass(image(BIGCUP,invar(IMAGE(x))),invar(x)).
% IMG-TH-2
-equal(D(IMAGE(x)),V) | thin(x).
% IMG-SS0
-equal(D(IMAGE(x)),singleton(0)) | equal(IMAGE(x),id(singleton(0))).
% X-VS-DO
-equal(D(VERTSECT(x)),V) | -equal(D(VERTSECT(y)),V) | equal(D(VERTSECT(cross(x,y))),V).
% DEF-TH-2
-equal(D(VERTSECT(x)),V) | thin(x).
% FUNP-RS3
-equal(D(funpart(x)),D(x)) | FUNCTION(composite(Id,x)).
% RE-E-LEM
-equal(D(x),0) | -subclass(x,E) | equal(x,0).
% RA-DO-1
-equal(D(x),0) | equal(R(x),0).
% X-DO-0A
-equal(D(x),0) | equal(cross(x,y),0).
% X-DO-0B
-equal(D(x),0) | equal(cross(y,x),0).
% DO-4G
-equal(D(x),0) | equal(intersection(x,cart(V,V)),0).
% DO-4F
-equal(D(x),0) | equal(restrict(x,V,V),0).
% ID-5I
-equal(D(x),D(y)) | -subclass(x,Id) | -subclass(y,Id) | equal(x,y).
% IDX-IN
-equal(D(x),R(y)) | -subclass(composite(x,y),Id) | equal(composite(Id,x),inverse(y)).
% PC-4B
-equal(P(x),0).
% RA-DO-2
-equal(R(x),0) | equal(D(x),0).
% RC-V-2
-equal(RC(x),0) | -member(x,V).
% RE-REG-2
-equal(REGULAR,V) | AxReg.
% SG-DO-B
-equal(U(intersection(x,R(SINGLETON))),V) | subclass(R(SINGLETON),x).
% PC-0-SC
-equal(U(x),0) | equal(x,0) | equal(x,singleton(0)).
% ON-SUC-5
-equal(U(x),x) | -member(x,OMEGA) | -member(y,x) | member(succ(y),x).
% ON-SUC-7
-equal(U(x),x) | -member(x,OMEGA) | equal(x,0) | subclass(omega,x).
% ON-SUC-6
-equal(U(x),x) | -member(x,OMEGA) | subclass(image(SUCC,x),x).
% IND-RUS5
-equal(U(x),x) | -member(x,omega) | equal(x,0).
% DEF-UCL3
-equal(Uclosure(x),x) | Uclosed(x).
% SP-7
-equal(V,0).
% VS-12COR
-equal(VERTSECT(x),0) | -member(image(x,y),V) | equal(y,0).
% CARD-0B
-equal(card(x),0) | equal(x,0).
% CP-V-0
-equal(cart(V,V),0).
% ID-CP-V
-equal(cart(V,V),Id).
% CP-SS-7
-equal(cart(singleton(x),singleton(y)),0) | -member(pair(x,y),cart(V,V)).
% CP-SS-3
-equal(cart(singleton(x),singleton(y)),singleton(pair(x,y))) | member(pair(x,y),cart(V,V)).
% CP-13
-equal(cart(x,x),cart(y,y)) | equal(x,y).
% CP-3C
-equal(cart(x,y),0) | equal(x,0) | equal(y,0).
% C-1C
-equal(complement(x),complement(y)) | equal(x,y).
% SG-4I
-equal(composite(E,x),composite(E,y)) | equal(composite(Id,x),composite(Id,y)).
% E-CO7
-equal(composite(E,x),composite(E,y)) | equal(composite(z,x),composite(z,y)).
% E-CO5
-equal(composite(E,x),composite(E,y)) | equal(restrict(x,V,V),restrict(y,V,V)).
% SP-E-CO
-equal(composite(E,x),composite(x,E)) | -member(x,V) | equal(composite(Id,x),0).
% IMG-RS3
-equal(composite(x,id(D(y))),y) | -member(y,V) | member(y,image(IMAGE(cross(Id,x)),P(Id))).
% SG-4G
-equal(composite(x,inverse(E)),composite(y,inverse(E))) | equal(composite(Id,x),composite(Id,y)).
% DF-EQV-2
-equal(composite(x,inverse(x)),x) | EQUIVALENCE(x).
% IMG-CO-3
-equal(composite(x,x),x) | equal(composite(IMAGE(x),IMAGE(x)),IMAGE(x)).
% IVR-FP
-equal(composite(x,y),composite(y,x)) | -member(R(y),V) | member(fix(IMAGE(y)),invar(IMAGE(x))).
% IMG-IVR
-equal(composite(x,y),composite(z,x)) | subclass(image(IMAGE(x),fix(IMAGE(y))),fix(IMAGE(z))).
% X-DO-0C
-equal(cross(x,y),0) | equal(D(x),0) | equal(D(y),0).
% FP-DJ3
-equal(fix(composite(x,y)),0) | disjoint(x,inverse(y)).
% FP-CO9
-equal(fix(composite(x,y)),0) | equal(fix(composite(y,x)),0).
% FP-DJ2
-equal(fix(composite(x,y)),0) | subclass(inverse(x),complement(y)).
% AP-FUNP4
-equal(funpart(x),composite(Id,x)) | FUNCTION(composite(Id,x)).
% FUNPART1
-equal(funpart(x),x) | FUNCTION(x).
% Q-C-IM
-equal(image(Q,x),x) | equal(image(Q,complement(x)),complement(x)).
% SR-HER2
-equal(image(S,complement(x)),complement(x)) | equal(image(inverse(S),x),x).
% SR-0-IM2
-equal(image(S,x),V) | member(0,x).
% SG-IM-SS
-equal(image(SINGLETON,x),singleton(x)) | member(x,R(SINGLETON)).
% IM-CP-5
-equal(image(complement(x),y),V) | -subclass(cart(y,y),x).
% POW-5A
-equal(image(inverse(POWER),x),V) | subclass(R(POWER),x).
% ZER-2
-equal(image(inverse(S),D(x)),D(x)) | -subclass(composite(composite(x,S),inverse(x)),S) | subclass(composite(x,S),composite(S,x)).
% SR-IM-2D
-equal(image(inverse(S),x),V) | equal(U(x),V).
% SR-HER1
-equal(image(inverse(S),x),x) | equal(image(S,complement(x)),complement(x)).
% ISB5HER1
-equal(image(inverse(S),x),x) | member(intersection(OMEGA,x),OMEGA) | subclass(OMEGA,x).
% IMG-BIN2
-equal(image(x,cart(y,y)),y) | -member(y,V) | member(y,fix(composite(IMAGE(x),composite(CART,DUP)))).
% IMG-OP-1
-equal(image(x,first(y)),second(y)) | -member(y,cart(V,V)) | member(y,IMAGE(x)).
% VS-MEM
-equal(image(x,singleton(first(y))),second(y)) | -member(y,cart(V,V)) | member(y,VERTSECT(x)).
% IM-7COR3
-equal(image(x,singleton(y)),0) | -member(y,D(x)).
% IM-DJ-1
-equal(image(x,y),0) | disjoint(y,D(x)).
% IM-7CONV
-equal(image(x,y),0) | equal(intersection(y,D(x)),0).
% FUL-LIM1
-equal(intersection(FULL,P(x)),x) | equal(U(x),x).
% ON-IND-D
-equal(intersection(OMEGA,P(x)),succ(x)) | equal(x,OMEGA) | member(x,OMEGA).
% ON-IND-C
-equal(intersection(OMEGA,P(x)),x) | equal(x,OMEGA).
% FIN-PP2
-equal(intersection(P(P(x)),subvar(PS)),singleton(0)) | -member(x,V) | member(x,FINITE).
% SU-6
-equal(intersection(complement(x),y),0) | subclass(y,x).
% CUT-3
-equal(intersection(first(x),y),second(x)) | -member(x,cart(V,V)) | member(x,IMAGE(id(y))).
% CO-IM6
-equal(intersection(image(inverse(x),singleton(y)),image(z,singleton(u))),0) | -member(pair(u,y),composite(x,z)).
% IM-7
-equal(intersection(x,D(y)),0) | equal(image(y,x),0).
% E-CO-IN4
-equal(intersection(x,y),0) | -member(pair(x,y),composite(E,inverse(E))).
% SPECIAL
-equal(intersection(x,y),0) | -subclass(x,union(z,y)) | subclass(x,z).
% DJ-DEF-1
-equal(intersection(x,y),0) | disjoint(x,y).
% D-DJ
-equal(intersection(x,y),0) | equal(intersection(y,complement(x)),y).
% SU-6A
-equal(intersection(x,y),0) | subclass(x,complement(y)).
% SU-2
-equal(intersection(x,y),x) | subclass(x,y).
% INV-3
-equal(inverse(first(x)),second(x)) | -member(x,cart(V,V)) | member(x,IMAGE(SWAP)).
% RL-3-U
-equal(inverse(x),inverse(y)) | -subclass(union(x,y),cart(V,V)) | equal(x,y).
% RL-3-EQ
-equal(inverse(x),inverse(y)) | -subclass(x,cart(V,V)) | -subclass(y,cart(V,V)) | equal(x,y).
% INV-FP2
-equal(inverse(x),x) | -member(x,V) | member(x,fix(IMAGE(SWAP))).
% SS-13-A
-equal(notsub(intersection(x,complement(singleton(notsub(x,0)))),0),notsub(x,0)) | equal(x,0) | equal(singleton(notsub(x,0)),x).
% ID-10-B
-equal(notsub(intersection(x,complement(singleton(y))),0),y) | -member(y,x) | subclass(cart(x,x),Id).
% RE-10A
-equal(pair(first(pair(x,y)),second(pair(x,y))),pair(x,y)) | member(x,V).
% RE-10B
-equal(pair(first(pair(x,y)),second(pair(x,y))),pair(x,y)) | member(y,V).
% RE-9A'
-equal(pair(first(x),second(x)),x) | member(first(x),V).
% RE-9B
-equal(pair(first(x),second(x)),x) | member(second(x),V).
% OP-9
-equal(pair(first(x),second(x)),x) | member(x,V).
% OP-9A
-equal(pair(first(x),second(x)),x) | member(x,cart(V,V)).
% OP-2C
-equal(pair(x,y),0).
% OP-5B
-equal(pair(x,y),pair(z,u)) | -member(x,V) | -member(u,V) | equal(y,u) | member(z,V).
% OP-5D
-equal(pair(x,y),pair(z,u)) | -member(x,V) | -member(y,V) | equal(y,u).
% OP-10
-equal(pair(x,y),pair(z,u)) | -member(x,V) | equal(x,z).
% OP-5
-equal(pair(x,y),pair(z,u)) | -member(y,V) | -member(u,V) | equal(y,u).
% OP-5A
-equal(pair(x,y),pair(z,u)) | -member(y,V) | equal(y,u) | member(x,V) | member(z,V).
% OP-11
-equal(pair(x,y),pair(z,u)) | -member(y,V) | equal(y,u).
% OP-4A
-equal(pair(x,y),pair(z,u)) | -member(z,V) | equal(x,z).
% OP-SS-2
-equal(pair(x,y),pair(z,u)) | equal(singleton(x),singleton(z)).
% OP-SS-4
-equal(pair(x,y),pair(z,u)) | equal(singleton(y),singleton(u)).
% UP-6A
-equal(pairset(x,y),0) | -member(x,V).
% UP-6B
-equal(pairset(x,y),0) | -member(y,V).
% UP-4
-equal(pairset(x,y),pairset(x,z)) | -member(pair(y,z),cart(V,V)) | equal(y,z).
% UP-5
-equal(pairset(x,y),pairset(z,y)) | -member(pair(x,z),cart(V,V)) | equal(x,z).
% RK-6B
-equal(rank(x),0) | equal(x,0).
% RA-0A
-equal(restrict(x,V,singleton(y)),0) | -member(y,R(x)).
% DJ-9B
-equal(restrict(x,y,z),0) | disjoint(x,cart(y,z)).
% ID-3'
-equal(second(x),first(x)) | -member(x,cart(V,V)) | member(x,Id).
% SS-2B
-equal(singleton(0),0).
% SS-3-COR
-equal(singleton(0),V).
% SG-IM-3
-equal(singleton(U(x)),x) | -member(U(x),y) | member(x,image(SINGLETON,y)).
% SG-IM-3'
-equal(singleton(U(x)),x) | -member(U(x),y) | member(x,intersection(P(y),R(SINGLETON))).
% SG-RA4
-equal(singleton(U(x)),x) | member(x,R(SINGLETON)).
% RP-SS-IN
-equal(singleton(inverse(x)),0) | equal(singleton(x),0).
% SS-10
-equal(singleton(memb(x)),x) | -member(y,x) | equal(memb(x),y).
% SS-9
-equal(singleton(memb(x)),x) | member(x,V).
% SS-2A
-equal(singleton(x),0) | -member(x,V).
% PC-7-SS
-equal(singleton(x),0) | equal(singleton(P(x)),0).
% UP-SS-4
-equal(singleton(x),singleton(y)) | -equal(singleton(z),singleton(u)) | equal(pairset(x,singleton(z)),pairset(y,singleton(u))).
% SS-5A
-equal(singleton(x),singleton(y)) | -member(x,V) | equal(x,y).
% SS-5B
-equal(singleton(x),singleton(y)) | -member(y,V) | equal(x,y).
% OP-SS-7
-equal(singleton(x),singleton(y)) | equal(pair(x,z),pair(y,z)).
% OP-SS-6
-equal(singleton(x),singleton(y)) | equal(pair(z,x),pair(z,y)).
% UP-SS-3
-equal(singleton(x),singleton(y)) | equal(pairset(x,z),pairset(y,z)).
% SUC-0-B
-equal(succ(x),0).
% OM-SC-1'
-equal(succ(x),succ(y)) | -member(x,omega) | equal(x,y).
% SUC-EQ-1
-equal(succ(x),succ(y)) | equal(x,y) | member(x,U(x)).
% SUC-EQ-2
-equal(succ(x),succ(y)) | equal(x,y) | member(x,y).
% SUC-FP-2
-equal(succ(x),x) | -member(x,V) | member(x,x).
% SV-CO3
-equal(sv2(composite(x,y)),sv1(composite(x,y))) | FUNCTION(composite(x,y)).
% OO-SV-6
-equal(sv2(inverse(x)),sv1(inverse(x))) | subclass(composite(inverse(x),x),Id).
% SV-2D
-equal(sv2(x),sv1(x)) | subclass(composite(x,inverse(x)),Id).
% E-PC-U-V
-equal(union(P(x),P(y)),V) | equal(x,V) | equal(y,V).
% SU-8
-equal(union(complement(x),y),V) | subclass(x,y).
% C-EQ-0
-equal(union(intersection(x,complement(y)),intersection(complement(x),y)),0) | equal(x,y).
% D-4-EXT
-equal(union(intersection(x,complement(y)),intersection(y,complement(x))),0) | equal(x,y).
% D-EQ-V
-equal(union(intersection(x,y),intersection(complement(x),complement(y))),V) | equal(x,y).
% TC-FUL-5
-equal(union(x,U(y)),y) | subclass(tc(x),y).
% U-EQ-0A
-equal(union(x,y),0) | equal(x,0).
% U-EQ-0B
-equal(union(x,y),0) | equal(y,0).
% C-5
-equal(union(x,y),V) | -equal(intersection(x,y),0) | equal(x,complement(y)).
% SU-8A
-equal(union(x,y),V) | subclass(complement(x),y).
% SU-8B
-equal(union(x,y),V) | subclass(complement(y),x).
% SU-4
-equal(union(x,y),y) | subclass(x,y).
% SS-0-C
-equal(x,0) | -member(x,complement(singleton(0))).
% DJ-3B
-equal(x,0) | disjoint(x,x).
% FUL-C
-full(complement(x)) | -member(x,V) | equal(x,0).
% FUL-U-V
-full(x) | -full(y) | -equal(union(x,y),V) | equal(x,V) | equal(y,V).
% FUL-I-1
-full(x) | -full(y) | full(intersection(x,y)).
% FUL-U-1
-full(x) | -full(y) | full(union(x,y)).
% FUL-DF09
-full(x) | -member(pair(y,x),intersection(E,complement(S))).
% FUL-DF10
-full(x) | -member(x,R(intersection(E,complement(S)))).
% FUL-DF11
-full(x) | -member(x,V) | member(x,FULL).
% FUL-DESC
-full(x) | -member(y,DESCENDING) | member(intersection(x,y),DESCENDING).
% ON-ORD-8
-full(x) | -member(y,OMEGA) | -subclass(x,OMEGA) | member(y,x) | subclass(x,y).
% FULSUC-H
-full(x) | -member(y,x) | member(succ(y),P(x)).
% FUL-DF01
-full(x) | -member(y,x) | subclass(y,x).
% FUL-DF04
-full(x) | -member(y,z) | -member(z,x) | member(y,x).
% TC-REG-2
-full(x) | -subclass(intersection(x,P(y)),y) | subclass(intersection(REGULAR,x),y).
% ISB4-SU
-full(x) | -subclass(x,OMEGA) | equal(x,OMEGA) | member(x,OMEGA).
% FULSUC-F
-full(x) | -subclass(x,succ(y)) | equal(x,succ(y)) | subclass(x,y).
% H-6
-full(x) | -subclass(x,y) | subclass(x,H(y)).
% TC-FUL-4
-full(x) | -subclass(y,x) | subclass(tc(y),x).
% H-4
-full(x) | equal(H(x),x).
% TC-FUL-3
-full(x) | equal(tc(x),x).
% FUL-PC-1
-full(x) | full(P(x)).
% FUL-SC-1
-full(x) | full(U(x)).
% FULSUC-B
-full(x) | full(succ(x)).
% ISB5FUL1
-full(x) | member(intersection(OMEGA,x),OMEGA) | subclass(OMEGA,x).
% TC-LEM-4
-full(x) | subclass(P(complement(image(inverse(U(subvar(union(cross(E,inverse(E)),id(cart(V,x)))))),complement(x)))),complement(image(inverse(U(subvar(union(cross(E,inverse(E)),id(cart(V,x)))))),complement(x)))).
% DF-FUL-1
-full(x) | subclass(U(x),x).
% FUL-BC-4
-full(x) | subclass(image(BIGCUP,P(x)),P(x)).
% FUL-DF05
-full(x) | subclass(x,P(x)).
% LT-DO-0
-member(0,D(LEAST(x))).
% CARTIM0A
-member(0,D(x)) | member(0,image(CART,x)).
% RE-AX-6C
-member(0,IRREG) | AxReg.
% E-RA1
-member(0,R(E)).
% POW-RA-3
-member(0,R(POWER)).
% SG-RA1
-member(0,R(SINGLETON)).
% SUC-RA-1
-member(0,R(SUCC)).
% CARTIM0B
-member(0,R(x)) | member(0,image(CART,x)).
% SP-UV2
-member(0,U(cart(V,V))).
% SP-V2
-member(0,cart(V,V)).
% CARTIM0C
-member(0,image(CART,x)) | member(0,D(x)) | member(0,R(x)).
% E-IM3
-member(0,image(E,x)).
% SR-IM-3D
-member(0,image(S,x)) | member(0,x).
% SP-OP
-member(0,pair(x,y)) | -member(pair(x,y),cart(V,V)).
% IND-4
-member(0,x) | -member(succ(ind(x)),x) | INDUCTIVE(x).
% FIN-IND1
-member(0,x) | -subclass(image(CUP,cart(x,R(SINGLETON))),x) | subclass(FINITE,x).
% FIN-IND2
-member(0,x) | -subclass(image(CUP,cart(x,image(SINGLETON,y))),x) | subclass(intersection(FINITE,P(y)),x).
% SBV-PS3B
-member(0,x) | -subclass(image(CUP,cart(x,image(SINGLETON,y))),x) | subclass(intersection(P(y),complement(x)),image(PS,intersection(P(y),complement(x)))).
% FIN-K-1
-member(0,x) | -subclass(image(K,x),x) | subclass(FINITE,x).
% IND-I-3
-member(0,x) | -subclass(image(SUCC,intersection(omega,x)),x) | subclass(omega,x).
% DF-IND-3
-member(0,x) | -subclass(image(SUCC,x),x) | INDUCTIVE(x).
% IND-3
-member(0,x) | INDUCTIVE(x) | member(ind(x),x).
% A-1B
-member(0,x) | equal(A(x),0).
% DJT-0
-member(0,x) | equal(image(DISJOINT,x),V).
% SR-0-IM1
-member(0,x) | equal(image(S,x),V).
% SR-IM-3E
-member(0,x) | member(0,image(S,x)).
% ON-A-1'
-member(A(intersection(OMEGA,x)),complement(OMEGA)).
% ACL-RP
-member(ACLOSURE,x).
% ACL-V-1
-member(Aclosure(x),V) | member(x,V).
% BA-MEM
-member(BIGCAP,x).
% BC-MEM
-member(BIGCUP,x).
% CART-MEM
-member(CART,x).
% IMG-V-RP
-member(D(IMAGE(x)),V) | member(IMAGE(x),V).
% ZER-6
-member(D(x),R(POWER)) | -subclass(R(x),D(x)) | member(A(fix(composite(S,x))),D(x)).
% ZER-5
-member(D(x),R(POWER)) | -subclass(R(x),D(x)) | member(U(D(x)),fix(composite(S,x))).
% IVR-V
-member(D(x),V) | -member(invar(x),V).
% CA-4-SV
-member(D(x),V) | -subclass(P(D(x)),R(x)) | -subclass(composite(x,inverse(x)),Id).
% IVR-DO2
-member(D(x),V) | -subclass(R(x),D(x)) | member(D(x),invar(x)).
% IVR-RA
-member(D(x),invar(x)) | member(R(x),invar(x)).
% IVR-DO1
-member(D(x),invar(x)) | subclass(R(x),D(x)).
% REG-C-V
-member(DESCENDING,V) | equal(REGULAR,V).
% SP-DESC
-member(DESCENDING,V) | equal(singleton(0),DESCENDING).
% SP-DJT-4
-member(DISJOINT,x).
% DUP-MEM
-member(DUP,x).
% SP-DI
-member(Di,x).
% SP-E
-member(E,x).
% FIN-MEM
-member(FINITE,x).
% 1ST-MEM
-member(FIRST,x).
% IND-FUL1
-member(FULL,x).
% FS-RP-1
-member(FUNS,x).
% IMG-SC2B
-member(IMAGE(x),V) | member(D(VERTSECT(x)),P(D(VERTSECT(x)))).
% IMG-SC2C
-member(IMAGE(x),V) | member(P(D(VERTSECT(x))),R(POWER)).
% RE-REG-3
-member(IRREG,REGULAR) | AxReg.
% SP-ID
-member(Id,x).
% ON-BF-2
-member(OMEGA,x).
% RUS-3B
-member(P(RUSSELL),x).
% POW-RA-8
-member(P(U(x)),P(x)) | member(x,R(POWER)).
% FIN-PCSS
-member(P(x),FINITE) | member(P(union(x,singleton(y))),FINITE).
% FIN-PC1
-member(P(x),FINITE) | member(x,FINITE).
% RUS-PC-2
-member(P(x),P(x)).
% REG-14
-member(P(x),REGULAR) | member(x,REGULAR).
% RP-9
-member(P(x),V) | member(x,V).
% POW-IN2
-member(P(x),y) | member(x,image(inverse(POWER),y)).
% POW-RP
-member(POWER,x).
% SP-RA-SG
-member(R(SINGLETON),x).
% SUC-RA-4
-member(R(SUCC),x).
% IMG-DO-R
-member(R(x),V) | equal(D(IMAGE(x)),V).
% VS-12-DO
-member(R(x),V) | equal(D(VERTSECT(x)),V).
% SBV-RA3
-member(R(x),V) | member(U(subvar(x)),fix(IMAGE(x))).
% SBV-RA2
-member(R(x),V) | member(U(subvar(x)),invar(x)).
% SBV-RA1
-member(R(x),V) | member(subvar(x),V).
% TH-RA
-member(R(x),V) | thin(x).
% REG-28
-member(REGULAR,x).
% RUS-3A
-member(RUSSELL,x).
% SP-SR
-member(S,x).
% 2ND-MEM
-member(SECOND,x).
% SP-SG
-member(SINGLETON,x).
% SUC-MEM1
-member(SUCC,x).
% FUL-IND-5
-member(U(intersection(FULL,P(x))),x) | -subclass(x,RUSSELL).
% FIN-SC6
-member(U(x),FINITE) | member(x,FINITE).
% FIN-SC2
-member(U(x),FINITE) | member(x,P(FINITE)).
% ON-PC-1'
-member(U(x),OMEGA) | member(x,P(P(OMEGA))).
% RUS-SC-3
-member(U(x),P(RUSSELL)) | member(x,P(RUSSELL)).
% FUL-DF14
-member(U(x),P(x)) | member(x,FULL).
% REG-15
-member(U(x),REGULAR) | member(x,REGULAR).
% RP-8
-member(U(x),V) | member(x,V).
% ON-SUC5C
-member(U(x),omega) | -subclass(x,omega) | member(x,image(inverse(S),omega)).
% SUC-IM-2
-member(U(x),x) | -subclass(image(SUCC,x),x) | member(U(x),U(x)).
% BC-FP-1
-member(U(x),x) | member(x,fix(composite(E,BIGCUP))).
% BC-IM-8
-member(U(x),y) | member(x,image(inverse(BIGCUP),y)).
% UCL-V-3
-member(Uclosure(x),V) | member(x,V).
% SP-6
-member(V,x).
% CARD-OP4
-member(card(x),V) | member(pair(x,card(x)),CARD).
% CARD-IM2
-member(card(x),y) | member(x,image(inverse(CARD),y)).
% REG-CP-V
-member(cart(REGULAR,REGULAR),x).
% SP-11
-member(cart(V,V),x).
% FIN-CP0B
-member(cart(x,y),FINITE) | equal(x,0) | member(y,FINITE).
% FIN-CP0A
-member(cart(x,y),FINITE) | equal(y,0) | member(x,FINITE).
% RP-11B
-member(cart(x,y),V) | equal(x,0) | member(y,V).
% RP-11A
-member(cart(x,y),V) | equal(y,0) | member(x,V).
% FINC-MEM
-member(complement(FINITE),x).
% FULC-MEM
-member(complement(FULL),x).
% ON-C-SP
-member(complement(OMEGA),x).
% SP-PC-C
-member(complement(P(x)),V) | equal(x,V).
% POW-RA-C
-member(complement(R(POWER)),x).
% SP-REG-C
-member(complement(REGULAR),V) | equal(REGULAR,V).
% SP-CP-C2
-member(complement(cart(x,y)),z).
% FP-E3
-member(complement(fix(E)),V).
% RP-RS-3
-member(composite(id(x),y),V) | member(image(inverse(y),x),V).
% RP-RS-1
-member(composite(x,id(y)),V) | member(image(x,y),V).
% RP-CO2
-member(composite(x,y),V) | member(image(inverse(y),D(x)),V).
% RP-CO1
-member(composite(x,y),V) | member(image(x,R(y)),V).
% RP-IDX-2
-member(id(x),V) | member(x,V).
% IDP-IM-5
-member(id(x),y) | member(x,image(inverse(IDP),y)).
% SP-IM-DI
-member(image(Di,x),V) | equal(x,0).
% SP-E-IM
-member(image(E,x),V) | equal(x,0).
% SP-SR-IM
-member(image(S,x),V) | equal(x,0).
% SG-IM-V
-member(image(SINGLETON,x),V) | member(x,V).
% IMG-IN3
-member(image(SINGLETON,x),y) | member(x,image(inverse(IMAGE(SINGLETON)),y)).
% RP-1-HER
-member(image(inverse(S),x),V) | member(x,V).
% RP-CO3
-member(image(x,R(y)),V) | -member(image(inverse(y),D(x)),V) | member(composite(x,y),V).
% VS-DO-3
-member(image(x,singleton(y)),complement(singleton(0))) | member(y,D(VERTSECT(x))).
% IMG-DO-P
-member(image(x,y),V) | subclass(P(y),D(IMAGE(x))).
% IND-ISB
-member(intersection(FULL,P(RUSSELL)),V).
% ON-SC-4B
-member(intersection(OMEGA,R(SUCC)),x).
% SG-IM-V'
-member(intersection(P(x),R(SINGLETON)),V) | member(x,V).
% RUS-8
-member(intersection(RUSSELL,x),x).
% FIN-C-SS
-member(intersection(complement(singleton(x)),y),FINITE) | member(y,FINITE).
% RP-C-SS
-member(intersection(complement(singleton(x)),y),V) | member(y,V).
% RP-I-C
-member(intersection(x,y),V) | -member(complement(x),V) | member(y,V).
% FUL-DF02
-member(notsub(U(x),x),x) | full(x).
% FUL-DF08
-member(notsub(x,P(x)),P(x)) | full(x).
% C-0B
-member(notsub(x,y),complement(x)) | subclass(x,y).
% EQ-2D
-member(notsub(x,y),y) | -member(notsub(y,x),x) | equal(x,y).
% EQ-2B
-member(notsub(x,y),y) | equal(x,y) | member(notsub(y,x),y).
% DF-SU-3
-member(notsub(x,y),y) | subclass(x,y).
% EQ-2C
-member(notsub(y,x),x) | equal(x,y) | member(notsub(x,y),x).
% DK-C-OM
-member(omega,DEDEKIND).
% FIN-C-OM
-member(omega,FINITE).
% IND-SUC
-member(omega,R(SUCC)).
% IND-OM-S
-member(omega,image(inverse(S),omega)).
% Q-0-OP
-member(pair(0,x),Q) | equal(x,0).
% RP-4
-member(pair(D(x),R(x)),cart(V,V)) | -subclass(x,cart(V,V)) | member(x,V).
% SP-6C
-member(pair(V,x),cart(V,V)).
% AX-FL-3
-member(pair(pair(u,v),w),cart(cart(V,V),V)) | -member(pair(pair(v,u),w),x) | member(pair(pair(u,v),w),flip(x)).
% AX-RO-3
-member(pair(pair(u,v),w),cart(cart(V,V),V)) | -member(pair(pair(v,w),u),x) | member(pair(pair(u,v),w),rotate(x)).
% CP-2A
-member(pair(pair(u,v),w),cart(cart(x,y),z)) | member(pair(pair(v,u),w),cart(cart(y,x),z)).
% CP-2C
-member(pair(pair(u,v),w),cart(cart(x,y),z)) | member(pair(pair(v,w),u),cart(cart(y,z),x)).
% CP-2B
-member(pair(pair(u,v),w),cart(cart(x,y),z)) | member(pair(pair(w,u),v),cart(cart(z,x),y)).
% AX-FL-2
-member(pair(pair(u,v),w),flip(x)) | member(pair(pair(v,u),w),x).
% AX-RO-2
-member(pair(pair(u,v),w),rotate(x)) | member(pair(pair(v,w),u),x).
% TW-AP1
-member(pair(pair(x,y),pair(z,u)),cart(cart(V,V),cart(V,V))) | equal(apply(TWIST,pair(pair(x,y),pair(z,u))),pair(pair(x,z),pair(y,u))).
% TW-LEM1
-member(pair(pair(x,y),pair(z,u)),cart(cart(V,V),cart(V,V))) | equal(cart(cart(singleton(x),singleton(y)),cart(singleton(z),singleton(u))),singleton(pair(pair(x,y),pair(z,u)))).
% TW-OP
-member(pair(pair(x,y),pair(z,u)),cart(cart(V,V),cart(V,V))) | equal(image(TWIST,singleton(pair(pair(x,y),pair(z,u)))),singleton(pair(pair(x,z),pair(y,u)))).
% X-OP-2
-member(pair(pair(x,y),pair(z,u)),cross(v,w)) | member(pair(x,z),v).
% X-OP-3
-member(pair(pair(x,y),pair(z,u)),cross(v,w)) | member(pair(y,u),w).
% CAP-OP1A
-member(pair(pair(x,y),z),CAP) | equal(intersection(x,y),z).
% CUP-OP3A
-member(pair(pair(x,y),z),CUP) | equal(union(x,y),z).
% 1ST-DF-4
-member(pair(pair(x,y),z),FIRST) | equal(x,z).
% SW-OP-2
-member(pair(pair(x,y),z),SWAP) | equal(pair(y,x),z).
% ASS-AP1
-member(pair(pair(x,y),z),cart(cart(V,V),V)) | equal(apply(ASSOC,pair(pair(x,y),z)),pair(x,pair(y,z))).
% REV-AP
-member(pair(pair(x,y),z),cart(cart(V,V),V)) | equal(apply(REVERSE,pair(pair(x,y),z)),pair(pair(z,y),x)).
% ROT-AP1
-member(pair(pair(x,y),z),cart(cart(V,V),V)) | equal(apply(ROT,pair(pair(x,y),z)),pair(pair(z,x),y)).
% ASS-AP2
-member(pair(pair(x,y),z),cart(cart(V,V),V)) | equal(apply(inverse(ASSOC),pair(x,pair(y,z))),pair(pair(x,y),z)).
% CUP-OP2
-member(pair(pair(x,y),z),composite(inverse(DUP),cross(S,S))) | subclass(union(x,y),z).
% CP-2
-member(pair(u,v),cart(x,y)) | member(pair(v,u),cart(y,x)).
% AX-CP-1
-member(pair(u,v),cart(x,y)) | member(u,x).
% AX-CP-2
-member(pair(u,v),cart(x,y)) | member(v,y).
% SP-6B
-member(pair(x,V),cart(V,V)).
% VS-11
-member(pair(x,image(y,singleton(x))),cart(V,V)) | member(pair(x,image(y,singleton(x))),VERTSECT(y)).
% VS-12
-member(pair(x,image(y,singleton(x))),cart(V,V)) | member(x,D(VERTSECT(y))).
% IMG-LEM7
-member(pair(x,image(y,x)),cart(V,V)) | member(pair(x,image(y,x)),IMAGE(y)).
% IMG-LEM8
-member(pair(x,image(y,x)),cart(V,V)) | member(x,D(IMAGE(y))).
% CO-E-6
-member(pair(x,image(y,x)),composite(E,complement(composite(y,inverse(E))))).
% CO-E-5
-member(pair(x,image(y,x)),composite(complement(E),composite(y,inverse(E)))).
% PS-DF-2
-member(pair(x,x),PS).
% ACL-OP2
-member(pair(x,y),ACLOSURE) | equal(Aclosure(x),y).
% ADJ-MEM2
-member(pair(x,y),ADJOIN(z)) | equal(y,union(z,x)).
% ADJ-MEM1
-member(pair(x,y),ADJOIN(z)) | subclass(y,union(z,x)).
% BA-4
-member(pair(x,y),BIGCAP) | equal(A(x),y).
% BC-4
-member(pair(x,y),BIGCUP) | equal(U(x),y).
% CAP-OP1B
-member(pair(x,y),CAP) | equal(y,intersection(first(x),second(x))).
% CARD-OP2
-member(pair(x,y),CARD) | equal(card(x),y).
% CART-OP1
-member(pair(x,y),CART) | equal(y,cart(first(x),second(x))).
% CUP-OP3B
-member(pair(x,y),CUP) | equal(union(first(x),second(x)),y).
% DJT-DF-1
-member(pair(x,y),DISJOINT) | disjoint(x,y).
% DUP-2
-member(pair(x,y),DUP) | equal(pair(x,x),y).
% E-V1
-member(pair(x,y),E) | member(pair(x,y),cart(V,V)).
% AX-E-2
-member(pair(x,y),E) | member(x,y).
% ES-DF-2
-member(pair(x,y),ES) | subclass(succ(x),y).
% 1ST-DF-2
-member(pair(x,y),FIRST) | equal(first(x),y).
% FIX-2
-member(pair(x,y),FIX) | equal(y,fix(x)).
% GT-DF-2
-member(pair(x,y),GREATEST(z)) | member(y,x).
% GT-DF-1
-member(pair(x,y),GREATEST(z)) | subclass(cart(x,singleton(y)),z).
% HC-OP-2
-member(pair(x,y),HC) | equal(y,H(x)).
% IDP-2
-member(pair(x,y),IDP) | equal(y,id(x)).
% IMG-IM2A
-member(pair(x,y),IMAGE(composite(id(z),inverse(FIRST)))) | equal(y,composite(z,id(x))).
% IMG-IM2B
-member(pair(x,y),IMAGE(composite(id(z),inverse(SECOND)))) | equal(y,composite(id(x),z)).
% CUT-1A
-member(pair(x,y),IMAGE(id(z))) | equal(intersection(x,z),y).
% IMG-U-2
-member(pair(x,y),IMAGE(z)) | -member(pair(x,u),IMAGE(v)) | member(pair(x,union(y,u)),IMAGE(union(z,v))).
% IMG-IM2
-member(pair(x,y),IMAGE(z)) | equal(image(z,x),y).
% IMG-IM1
-member(pair(x,y),IMAGE(z)) | subclass(image(z,x),y).
% ID-2
-member(pair(x,y),Id) | equal(x,y).
% K-SU2
-member(pair(x,y),K) | -subclass(y,x).
% K-SS6
-member(pair(x,y),K) | equal(intersection(y,complement(singleton(U(intersection(y,complement(x)))))),x).
% K-SS5
-member(pair(x,y),K) | equal(union(x,singleton(U(intersection(y,complement(x))))),y).
% K-SS4
-member(pair(x,y),K) | member(intersection(y,complement(x)),R(SINGLETON)).
% K-SU1
-member(pair(x,y),K) | subclass(x,y).
% LB-DF-1
-member(pair(x,y),LB(z)) | subclass(cart(singleton(y),x),z).
% LT-DF-2
-member(pair(x,y),LEAST(z)) | member(y,x).
% LT-DF-1
-member(pair(x,y),LEAST(z)) | subclass(cart(singleton(y),x),z).
% LB-2
-member(pair(x,y),LOWERBOUND) | subclass(x,A(y)).
% POW-4
-member(pair(x,y),POWER) | equal(P(x),y).
% PS-DF-3'
-member(pair(x,y),PS) | -subclass(y,x).
% PS-I-C
-member(pair(x,y),PS) | -subclass(z,x) | member(pair(intersection(x,complement(z)),intersection(y,complement(z))),PS).
% PS-DF-3
-member(pair(x,y),PS) | subclass(x,y).
% Q-DJ-I
-member(pair(x,y),Q) | -member(pair(z,intersection(u,complement(y))),Q) | -disjoint(x,z) | member(pair(union(x,z),union(y,u)),Q).
% Q-DJ-U
-member(pair(x,y),Q) | -member(pair(z,u),Q) | -disjoint(x,z) | -disjoint(y,u) | member(pair(union(x,z),union(y,u)),Q).
% Q-BIJ-2
-member(pair(x,y),Q) | -subclass(z,x) | member(pair(z,image(bij(x,y),z)),Q).
% Q-4B
-member(pair(x,y),Q) | equal(D(bij(x,y)),x).
% Q-4C
-member(pair(x,y),Q) | equal(R(bij(x,y)),y).
% Q-4A
-member(pair(x,y),Q) | member(bij(x,y),BIJ).
% Q-IMG
-member(pair(x,y),Q) | member(pair(x,y),IMAGE(bij(x,y))).
% RK-OP1
-member(pair(x,y),RANK) | equal(y,rank(x)).
% RC-OP1
-member(pair(x,y),RC(z)) | equal(y,intersection(z,complement(x))).
% REV-OP
-member(pair(x,y),REVERSE) | equal(y,pair(pair(second(x),second(first(x))),first(first(x)))).
% RT-OP-2
-member(pair(x,y),RIGHT(z)) | equal(y,pair(x,z)).
% K-SS2
-member(pair(x,y),S) | member(pair(x,y),K) | -member(intersection(y,complement(x)),R(SINGLETON)).
% SR-2
-member(pair(x,y),S) | subclass(x,y).
% 2ND-DF-2
-member(pair(x,y),SECOND) | equal(second(x),y).
% SG-2D
-member(pair(x,y),SINGLETON) | equal(singleton(x),y).
% SG-2A
-member(pair(x,y),SINGLETON) | member(x,y).
% SUC-DF-4
-member(pair(x,y),SUCC) | equal(succ(x),y).
% SUC-DF-2
-member(pair(x,y),SUCC) | member(pair(x,y),cart(V,V)).
% SPW-2
-member(pair(x,y),SUPERPOWER) | -subclass(z,x) | member(z,y).
% SPW-3
-member(pair(x,y),SUPERPOWER) | subclass(P(x),y).
% SW-SW
-member(pair(x,y),SWAP) | -member(pair(y,z),SWAP) | equal(x,z).
% SW-DF-1
-member(pair(x,y),SWAP) | equal(swap(x),y).
% TC-OP2
-member(pair(x,y),TC) | equal(tc(x),y).
% GT-UB-U
-member(pair(x,y),UB(z)) | -member(pair(u,y),GREATEST(z)) | member(pair(union(x,u),y),GREATEST(z)).
% UB-U
-member(pair(x,y),UB(z)) | -member(pair(u,y),UB(z)) | member(pair(union(x,u),y),UB(z)).
% UB-DF-1
-member(pair(x,y),UB(z)) | subclass(cart(x,singleton(y)),z).
% UCL-OP2
-member(pair(x,y),UCLOSURE) | equal(Uclosure(x),y).
% UB-4
-member(pair(x,y),UPPERBOUND) | subclass(U(x),y).
% UB-3
-member(pair(x,y),UPPERBOUND) | subclass(x,P(y)).
% VS-10
-member(pair(x,y),VERTSECT(z)) | equal(image(z,singleton(x)),y).
% BIJ-U-DJ
-member(pair(x,y),cart(BIJ,BIJ)) | -disjoint(D(x),D(y)) | -disjoint(R(x),R(y)) | member(union(x,y),BIJ).
% BIJ-CO1
-member(pair(x,y),cart(BIJ,BIJ)) | member(composite(x,y),BIJ).
% FIN-CP2
-member(pair(x,y),cart(FINITE,FINITE)) | member(cart(x,y),FINITE).
% FIN-U
-member(pair(x,y),cart(FINITE,FINITE)) | member(union(x,y),FINITE).
% FULSUC-D
-member(pair(x,y),cart(FULL,FULL)) | -equal(succ(x),succ(y)) | equal(x,y).
% ZN-RS1
-member(pair(x,y),cart(FULL,FULL)) | -subclass(composite(inverse(E),z),composite(z,inverse(E))) | member(restrict(z,x,y),subcommutant(inverse(E))).
% FUL-I-2
-member(pair(x,y),cart(FULL,FULL)) | member(intersection(x,y),FULL).
% FUL-U-2
-member(pair(x,y),cart(FULL,FULL)) | member(union(x,y),FULL).
% FS-CO
-member(pair(x,y),cart(FUNS,FUNS)) | member(composite(x,y),FUNS).
% FS-X
-member(pair(x,y),cart(FUNS,FUNS)) | member(cross(x,y),FUNS).
% HF-CP
-member(pair(x,y),cart(H(FINITE),H(FINITE))) | member(cart(x,y),H(FINITE)).
% HF-UP
-member(pair(x,y),cart(H(FINITE),H(FINITE))) | member(pairset(x,y),H(FINITE)).
% HF-U
-member(pair(x,y),cart(H(FINITE),H(FINITE))) | member(union(x,y),H(FINITE)).
% ON-SC-SC
-member(pair(x,y),cart(OMEGA,OMEGA)) | -member(U(x),U(y)) | member(x,y).
% ON-ORD-4
-member(pair(x,y),cart(OMEGA,OMEGA)) | -subclass(x,y) | member(x,succ(y)).
% ON-ORD-7
-member(pair(x,y),cart(OMEGA,OMEGA)) | member(x,y) | member(y,x) | equal(x,y).
% ON-ORD-6
-member(pair(x,y),cart(OMEGA,OMEGA)) | member(x,y) | subclass(y,x).
% ON-ORD-5
-member(pair(x,y),cart(OMEGA,OMEGA)) | subclass(x,y) | subclass(y,x).
% REG-CP
-member(pair(x,y),cart(REGULAR,REGULAR)) | member(cart(x,y),REGULAR).
% UO-X
-member(pair(x,y),cart(UNOPS,UNOPS)) | member(cross(x,y),UNOPS).
% K-SS-1B
-member(pair(x,y),cart(V,R(SINGLETON))) | member(pair(x,union(x,y)),union(Id,K)).
% DJT-DF-2
-member(pair(x,y),cart(V,V)) | -disjoint(x,y) | member(pair(x,y),DISJOINT).
% FU-UP-4
-member(pair(x,y),cart(V,V)) | -member(pair(z,u),cart(V,V)) | FUNCTION(pairset(pair(x,y),pair(z,u))) | equal(x,z).
% GT-UP
-member(pair(x,y),cart(V,V)) | -member(pairset(x,y),D(GREATEST(z))) | member(pair(x,y),union(z,inverse(z))).
% LT-UP
-member(pair(x,y),cart(V,V)) | -member(pairset(x,y),D(LEAST(z))) | member(pair(x,y),union(z,inverse(z))).
% AX-E-3
-member(pair(x,y),cart(V,V)) | -member(x,y) | member(pair(x,y),E).
% SPW-4
-member(pair(x,y),cart(V,V)) | -subclass(P(x),y) | member(pair(x,y),SUPERPOWER).
% UB-5
-member(pair(x,y),cart(V,V)) | -subclass(U(x),y) | member(pair(x,y),UPPERBOUND).
% LB-DF-2
-member(pair(x,y),cart(V,V)) | -subclass(cart(singleton(y),x),z) | member(pair(x,y),LB(z)).
% UB-DF-2
-member(pair(x,y),cart(V,V)) | -subclass(cart(x,singleton(y)),z) | member(pair(x,y),UB(z)).
% ES-DF-1
-member(pair(x,y),cart(V,V)) | -subclass(succ(x),y) | member(pair(x,y),ES).
% LB-3
-member(pair(x,y),cart(V,V)) | -subclass(x,A(y)) | member(pair(x,y),LOWERBOUND).
% SR-3
-member(pair(x,y),cart(V,V)) | -subclass(x,y) | member(pair(x,y),S).
% FU-TP-3
-member(pair(x,y),cart(V,V)) | FUNCTION(transposition(x,y)).
% A-UP-1
-member(pair(x,y),cart(V,V)) | equal(A(pairset(x,y)),intersection(x,y)).
% SC-5
-member(pair(x,y),cart(V,V)) | equal(U(pairset(x,y)),union(x,y)).
% ADJ-AP
-member(pair(x,y),cart(V,V)) | equal(apply(ADJOIN(x),y),union(x,y)).
% CAP-AP2
-member(pair(x,y),cart(V,V)) | equal(apply(CAP,pair(x,y)),intersection(x,y)).
% CART-AP2
-member(pair(x,y),cart(V,V)) | equal(apply(CART,pair(x,y)),cart(x,y)).
% CPS-AP
-member(pair(x,y),cart(V,V)) | equal(apply(COMPOSE,pair(x,y)),composite(x,y)).
% CRS-AP2
-member(pair(x,y),cart(V,V)) | equal(apply(CROSS,pair(x,y)),cross(x,y)).
% CUP-AP1
-member(pair(x,y),cart(V,V)) | equal(apply(CUP,pair(x,y)),union(x,y)).
% MG-AP-1
-member(pair(x,y),cart(V,V)) | equal(apply(IMG,pair(x,y)),image(x,y)).
% PRS-AP2
-member(pair(x,y),cart(V,V)) | equal(apply(PAIRSET,pair(x,y)),pairset(x,y)).
% CP-SS-5
-member(pair(x,y),cart(V,V)) | equal(cart(singleton(x),singleton(y)),singleton(pair(x,y))).
% OP-7A
-member(pair(x,y),cart(V,V)) | equal(first(pair(x,y)),x).
% CPS-VS
-member(pair(x,y),cart(V,V)) | equal(image(COMPOSE,singleton(pair(x,y))),singleton(composite(x,y))).
% E-CO-IN3
-member(pair(x,y),cart(V,V)) | equal(intersection(x,y),0) | member(pair(x,y),composite(E,inverse(E))).
% IN-SS-1
-member(pair(x,y),cart(V,V)) | equal(inverse(singleton(pair(x,y))),singleton(pair(y,x))).
% FU-TP-4
-member(pair(x,y),cart(V,V)) | equal(inverse(transposition(x,y)),transposition(x,y)).
% OP-7B
-member(pair(x,y),cart(V,V)) | equal(second(pair(x,y)),y).
% SW-0C
-member(pair(x,y),cart(V,V)) | equal(swap(pair(x,y)),pair(y,x)).
% DI-OP2
-member(pair(x,y),cart(V,V)) | equal(x,y) | member(pair(x,y),Di).
% E-IN-C4
-member(pair(x,y),cart(V,V)) | equal(x,y) | member(pair(x,y),composite(inverse(complement(E)),E)).
% CART-RA2
-member(pair(x,y),cart(V,V)) | member(cart(x,y),R(CART)).
% RP-3
-member(pair(x,y),cart(V,V)) | member(cart(x,y),V).
% CPS-RA1'
-member(pair(x,y),cart(V,V)) | member(composite(x,y),P(cart(V,V))).
% RP-CO4
-member(pair(x,y),cart(V,V)) | member(composite(x,y),V).
% MAP-MEM
-member(pair(x,y),cart(V,V)) | member(map(x,y),V).
% Q-RT-2
-member(pair(x,y),cart(V,V)) | member(pair(cart(x,singleton(y)),x),Q).
% INV-CP
-member(pair(x,y),cart(V,V)) | member(pair(cart(x,y),cart(y,x)),IMAGE(SWAP)).
% CART-OP3
-member(pair(x,y),cart(V,V)) | member(pair(pair(x,y),cart(x,y)),CART).
% CPS-OP
-member(pair(x,y),cart(V,V)) | member(pair(pair(x,y),composite(x,y)),COMPOSE).
% MG-OP-1
-member(pair(x,y),cart(V,V)) | member(pair(pair(x,y),image(x,y)),IMG).
% CAP-OP2
-member(pair(x,y),cart(V,V)) | member(pair(pair(x,y),intersection(x,y)),CAP).
% SW-OP-1
-member(pair(x,y),cart(V,V)) | member(pair(pair(x,y),pair(y,x)),SWAP).
% CUP-OP4
-member(pair(x,y),cart(V,V)) | member(pair(pair(x,y),union(x,y)),CUP).
% 1ST-DF-3
-member(pair(x,y),cart(V,V)) | member(pair(pair(x,y),x),FIRST).
% 2ND-DF-4
-member(pair(x,y),cart(V,V)) | member(pair(pair(x,y),y),SECOND).
% Q-SS
-member(pair(x,y),cart(V,V)) | member(pair(singleton(x),singleton(y)),Q).
% INV-U
-member(pair(x,y),cart(V,V)) | member(pair(union(x,y),union(inverse(x),inverse(y))),IMAGE(SWAP)).
% ADJ-MEM3
-member(pair(x,y),cart(V,V)) | member(pair(union(x,y),x),composite(S,IMAGE(id(complement(y))))).
% IMG-RT1
-member(pair(x,y),cart(V,V)) | member(pair(x,cart(x,singleton(y))),IMAGE(RIGHT(y))).
% RT-OP-1
-member(pair(x,y),cart(V,V)) | member(pair(x,pair(x,y)),RIGHT(y)).
% E-UP1
-member(pair(x,y),cart(V,V)) | member(pair(x,pairset(x,y)),E).
% ADJ-MEM4
-member(pair(x,y),cart(V,V)) | member(pair(x,union(x,y)),ADJOIN(y)).
% CP-SS-6
-member(pair(x,y),cart(V,V)) | member(pair(x,y),cart(singleton(x),singleton(y))).
% SR-C-A2
-member(pair(x,y),cart(V,V)) | member(pair(x,y),composite(E,complement(S))) | subclass(x,A(y)).
% IMG-X
-member(pair(x,y),cart(V,V)) | member(pair(y,composite(x,y)),IMAGE(cross(Id,x))).
% E-UP2
-member(pair(x,y),cart(V,V)) | member(pair(y,pairset(x,y)),E).
% RP-3-RS
-member(pair(x,y),cart(V,V)) | member(restrict(z,x,y),V).
% SC-5-COR
-member(pair(x,y),cart(V,V)) | member(union(x,y),V).
% IM-10A1
-member(pair(x,y),cart(V,V)) | member(x,image(V,singleton(y))).
% E-IN-C3
-member(pair(x,y),cart(V,V)) | member(y,x) | member(pair(x,y),inverse(complement(E))).
% CP-UP-SU
-member(pair(x,y),cart(V,V)) | subclass(cart(singleton(z),pairset(x,y)),pairset(pair(z,x),pair(z,y))).
% FU-TP-1
-member(pair(x,y),cart(V,V)) | subclass(transposition(x,y),cart(V,V)).
% SG-2B
-member(pair(x,y),cart(V,V)) | subclass(y,singleton(x)) | member(pair(x,y),composite(E,complement(Id))).
% CO-DF'
-member(pair(x,y),cart(cart(V,V),V)) | -member(pair(y,second(x)),z) | -member(pair(first(x),y),u) | member(x,composite(z,u)).
% ON-OM-I1
-member(pair(x,y),cart(omega,omega)) | member(intersection(x,y),omega).
% ON-OM-U1
-member(pair(x,y),cart(omega,omega)) | member(union(x,y),omega).
% ST-CO3
-member(pair(x,y),cart(subcommutant(z),subcommutant(z))) | member(composite(x,y),subcommutant(z)).
% SBV-X
-member(pair(x,y),cart(subvar(z),subvar(u))) | member(cart(x,y),subvar(cross(z,u))).
% Q-SUB
-member(pair(x,y),cart(z,complement(u))) | -member(pair(intersection(z,complement(singleton(x))),u),Q) | member(pair(z,union(u,singleton(y))),Q).
% E-CO1
-member(pair(x,y),composite(E,E)) | member(x,U(y)).
% E-C-A-1
-member(pair(x,y),composite(E,complement(E))) | member(x,complement(A(y))).
% SG-2C
-member(pair(x,y),composite(E,complement(Id))) | -subclass(y,singleton(x)).
% SR-C-A1
-member(pair(x,y),composite(E,complement(S))) | -subclass(x,A(y)).
% CO-E-4
-member(pair(x,y),composite(E,complement(composite(z,inverse(E))))) | -subclass(y,image(z,x)).
% VS-8
-member(pair(x,y),composite(E,complement(z))) | -subclass(y,image(z,singleton(x))).
% VS-9
-member(pair(x,y),composite(Id,complement(composite(E,complement(z))))) | subclass(y,image(z,singleton(x))).
% VS-7
-member(pair(x,y),composite(Id,complement(composite(complement(E),z)))) | subclass(image(z,singleton(x)),y).
% ID-IM-SS
-member(pair(x,y),composite(Id,z)) | -subclass(composite(u,z),v) | subclass(image(u,singleton(y)),image(v,singleton(x))).
% UB-SS
-member(pair(x,y),composite(Id,z)) | member(pair(singleton(x),y),UB(z)).
% INV-SR1
-member(pair(x,y),composite(S,IMAGE(SWAP))) | subclass(inverse(x),y).
% CO-E-3
-member(pair(x,y),composite(complement(E),composite(z,inverse(E)))) | -subclass(image(z,x),y).
% VS-6
-member(pair(x,y),composite(complement(E),z)) | -subclass(image(z,singleton(x)),y).
% IDX-OP-4
-member(pair(x,y),composite(id(z),u)) | member(y,z).
% IMG-SR-3
-member(pair(x,y),composite(inverse(S),IMAGE(z))) | subclass(y,image(z,x)).
% IDX-OP-3
-member(pair(x,y),composite(z,id(u))) | member(x,u).
% CO-E-2
-member(pair(x,y),composite(z,inverse(E))) | member(y,image(z,x)).
% CO-COM-V
-member(pair(x,y),composite(z,u)) | member(com(z,u,x,y),V).
% CO-1D'
-member(pair(x,y),composite(z,u)) | member(pair(com(z,u,x,y),y),cart(V,V)).
% CO-1C'
-member(pair(x,y),composite(z,u)) | member(pair(com(z,u,x,y),y),z).
% CO-1B'
-member(pair(x,y),composite(z,u)) | member(pair(x,com(z,u,x,y)),cart(V,V)).
% CO-1A'
-member(pair(x,y),composite(z,u)) | member(pair(x,com(z,u,x,y)),u).
% CO-IM5
-member(pair(x,y),composite(z,u)) | member(y,image(z,image(u,singleton(x)))).
% X-OP-4
-member(pair(x,y),cross(z,u)) | member(pair(first(x),first(y)),z).
% X-OP-5
-member(pair(x,y),cross(z,u)) | member(pair(second(x),second(y)),u).
% SW-0F
-member(pair(x,y),flip(z)) | member(pair(swap(x),y),z).
% FUNP-MEM
-member(pair(x,y),funpart(z)) | -member(pair(x,u),composite(Id,z)) | equal(y,u).
% SG-FNP2
-member(pair(x,y),funpart(z)) | equal(image(z,singleton(x)),singleton(y)).
% IDX-EQ
-member(pair(x,y),id(z)) | equal(x,y).
% IDX-OP-1
-member(pair(x,y),id(z)) | member(x,z).
% IDX-OP-2
-member(pair(x,y),id(z)) | member(y,z).
% CUP-IN3
-member(pair(x,y),image(inverse(CUP),singleton(z))) | equal(union(x,y),z).
% CUP-IN1
-member(pair(x,y),image(inverse(CUP),z)) | member(union(x,y),z).
% LB-SS
-member(pair(x,y),inverse(z)) | member(pair(singleton(x),y),LB(z)).
% IN-2
-member(pair(x,y),inverse(z)) | member(pair(y,x),z).
% E-CO3
-member(pair(x,y),restrict(z,V,V)) | -subclass(composite(E,z),composite(E,u)) | member(pair(x,y),u).
% RS-1
-member(pair(x,y),restrict(z,u,v)) | member(pair(x,y),z).
% RS-2
-member(pair(x,y),restrict(z,u,v)) | member(x,u).
% RS-3
-member(pair(x,y),restrict(z,u,v)) | member(y,v).
% X-OP-1
-member(pair(x,y),z) | -member(pair(x,y),cart(V,V)) | -member(pair(u,v),w) | -member(pair(u,v),cart(V,V)) | member(pair(pair(x,u),pair(y,v)),cross(z,w)).
% SV-1
-member(pair(x,y),z) | -member(pair(x,y),cart(V,V)) | -member(pair(x,u),z) | -member(pair(x,u),cart(V,V)) | -subclass(composite(z,inverse(z)),Id) | equal(y,u).
% CO-DF1
-member(pair(x,y),z) | -member(pair(x,y),cart(V,V)) | -member(pair(y,u),v) | -member(pair(y,u),cart(V,V)) | member(pair(x,u),composite(v,z)).
% SV-5
-member(pair(x,y),z) | -member(pair(x,y),cart(V,V)) | -subclass(composite(z,inverse(z)),Id) | equal(image(z,singleton(x)),singleton(y)).
% CO-4-LEM
-member(pair(x,y),z) | -member(pair(x,y),cart(V,V)) | member(pair(x,x),composite(inverse(z),z)).
% ID-CO3
-member(pair(x,y),z) | -member(pair(x,y),cart(V,V)) | member(pair(x,y),composite(Id,z)).
% IN-3
-member(pair(x,y),z) | -member(pair(x,y),cart(V,V)) | member(pair(y,x),inverse(z)).
% DO-1C
-member(pair(x,y),z) | -member(pair(x,y),cart(V,V)) | member(x,D(z)).
% RA-1C
-member(pair(x,y),z) | -member(pair(x,y),cart(V,V)) | member(y,R(z)).
% IM-2A
-member(pair(x,y),z) | -member(pair(x,y),cart(V,V)) | member(y,image(z,singleton(x))).
% AP-4C
-member(pair(x,y),z) | -member(pair(x,y),cart(V,V)) | subclass(y,apply(z,x)).
% SW-0G
-member(pair(x,y),z) | -member(pair(x,y),cart(cart(V,V),V)) | member(pair(swap(x),y),flip(z)).
% RS-4
-member(pair(x,y),z) | -member(pair(x,y),cart(u,v)) | member(pair(x,y),restrict(z,u,v)).
% CO-DF2
-member(pair(x,y),z) | -member(pair(y,u),v) | -member(pair(pair(x,u),y),cart(cart(V,V),V)) | member(pair(x,u),composite(v,z)).
% IN-3-COR
-member(pair(x,y),z) | -subclass(z,cart(V,V)) | member(pair(y,x),inverse(z)).
% DO-1D
-member(pair(x,y),z) | -subclass(z,cart(V,V)) | member(x,D(z)).
% EQV-MEM5
-member(pair(x,y),z) | -subclass(z,inverse(z)) | -subclass(composite(z,z),z) | member(pair(x,x),z).
% EQV-MEM6
-member(pair(x,y),z) | -subclass(z,inverse(z)) | -subclass(composite(z,z),z) | member(pair(y,y),z).
% Q-ADJ
-member(pair(z,u),cart(complement(x),complement(y))) | -member(pair(x,y),Q) | member(pair(union(x,singleton(z)),union(y,singleton(u))),Q).
% RK-AP
-member(rank(x),OMEGA) | equal(apply(RANK,x),rank(x)).
% RK-4
-member(rank(x),OMEGA) | member(pair(rank(x),x),ZN).
% RK-OP2
-member(rank(x),OMEGA) | member(pair(x,rank(x)),RANK).
% RK-DO1
-member(rank(x),OMEGA) | member(x,D(RANK)).
% RK-2
-member(rank(x),OMEGA) | member(x,image(ZN,OMEGA)).
% RK-MEMB
-member(rank(x),x).
% IND-SS-0
-member(singleton(0),x) | -subclass(image(SUCC,x),x) | subclass(omega,union(x,singleton(0))).
% FUL-0-4
-member(singleton(singleton(0)),FULL).
% OM-SS-1
-member(singleton(singleton(0)),omega).
% E-SS3
-member(singleton(x),image(E,y)) | member(x,y).
% IND-2
-member(succ(ind(x)),x) | subclass(image(SUCC,x),x).
% ON-5C
-member(succ(x),OMEGA) | member(x,OMEGA).
% SUC-V-3
-member(succ(x),V) | member(x,V).
% OM-PC-8
-member(succ(x),omega) | member(x,omega).
% SUC-SC-2
-member(succ(x),y) | member(x,U(y)).
% TC-ON1
-member(tc(x),OMEGA) | member(x,P(OMEGA)).
% TC-IMS
-member(tc(x),y) | member(x,image(inverse(S),y)).
% TC-IMIN1
-member(tc(x),y) | member(x,image(inverse(TC),y)).
% CP-1A
-member(u,x) | -member(v,y) | member(pair(u,v),cart(V,V)).
% RP-10-OP
-member(union(x,y),V) | member(pair(x,y),cart(V,V)).
% RP-10
-member(union(x,y),V) | member(x,V).
% CUP-IN2
-member(union(x,y),z) | member(pair(x,y),image(inverse(CUP),z)).
% ADJ-IN2
-member(union(x,y),z) | member(x,image(inverse(ADJOIN(y)),z)).
% SP-2
-member(x,0).
% A-1
-member(x,A(y)) | -member(z,y) | member(x,z).
% SR-A-DJ
-member(x,A(y)) | disjoint(y,P(complement(singleton(x)))).
% Q-BIJ-1
-member(x,BIJ) | -subclass(y,D(x)) | member(pair(y,image(x,y)),Q).
% BIJ-SU
-member(x,BIJ) | -subclass(y,x) | member(y,BIJ).
% BIJ-2
-member(x,BIJ) | ONEONE(x).
% BIJ-RS-1
-member(x,BIJ) | member(composite(id(y),x),BIJ).
% BIJ-RS-2
-member(x,BIJ) | member(composite(x,id(y)),BIJ).
% BIJ-3
-member(x,BIJ) | member(inverse(x),BIJ).
% Q-2
-member(x,BIJ) | member(pair(D(x),R(x)),Q).
% IMG-FP2
-member(x,D(IMAGE(y))) | -subclass(x,image(y,x)) | member(x,fix(composite(inverse(S),IMAGE(y)))).
% IMG-DO-H
-member(x,D(IMAGE(y))) | -subclass(z,x) | member(z,D(IMAGE(y))).
% IMG-DO
-member(x,D(IMAGE(y))) | member(image(y,x),V).
% RK-DO2
-member(x,D(RANK)) | member(rank(x),OMEGA).
% VS-AP
-member(x,D(VERTSECT(y))) | equal(image(y,singleton(x)),apply(VERTSECT(y),x)).
% VS-DO-1
-member(x,D(VERTSECT(y))) | member(image(y,singleton(x)),V).
% IMG-VS-4
-member(x,D(VERTSECT(y))) | member(singleton(x),D(IMAGE(y))).
% SG-FNP1
-member(x,D(funpart(y))) | member(image(y,singleton(x)),R(SINGLETON)).
% UNOPS-1
-member(x,D(intersection(IMAGE(FIRST),composite(S,IMAGE(SECOND))))) | subclass(R(x),D(x)).
% TC-I-E-1
-member(x,D(intersection(TC,E))) | member(x,tc(x)).
% RS-9A
-member(x,D(restrict(E,y,singleton(z)))) | member(x,intersection(y,z)).
% DJ-10B
-member(x,D(y)) | -disjoint(y,cart(singleton(x),V)).
% CO-BOY1'
-member(x,D(y)) | -subclass(R(y),D(z)) | member(x,image(inverse(y),D(z))).
% ID-3-COR
-member(x,D(y)) | -subclass(y,Id) | member(pair(x,x),y).
% DO-0C
-member(x,D(y)) | equal(first(notsub(restrict(y,singleton(x),V),0)),x).
% DO-0D
-member(x,D(y)) | equal(notsub(restrict(y,singleton(x),V),0),pair(x,ran(y,x,V))).
% DO-0B
-member(x,D(y)) | member(notsub(restrict(y,singleton(x),V),0),y).
% DO-1A
-member(x,D(y)) | member(pair(x,ran(y,x,V)),cart(V,V)).
% DO-1B
-member(x,D(y)) | member(pair(x,ran(y,x,V)),y).
% RA-9B
-member(x,D(y)) | member(ran(y,x,V),R(y)).
% DO-1A'
-member(x,D(y)) | member(ran(y,x,V),V).
% CA-3
-member(x,D(y)) | member(x,cantor(y)) | member(x,apply(y,x)).
% AX-DO-1
-member(x,D(z)) | -equal(restrict(z,singleton(x),V),0).
% DK-MEM-1
-member(x,DEDEKIND) | -member(pair(x,y),Q) | -subclass(x,y) | equal(x,y).
% DK-MEM-2
-member(x,DEDEKIND) | -member(pair(x,y),Q) | -subclass(y,x) | equal(x,y).
% REG-17
-member(x,DESCENDING) | -member(y,REGULAR) | disjoint(x,y).
% REG-16
-member(x,DESCENDING) | disjoint(x,REGULAR).
% DESC-5
-member(x,DESCENDING) | member(union(x,singleton(y)),DESCENDING) | disjoint(x,y).
% DESC-1
-member(x,DESCENDING) | subclass(x,image(E,x)).
% DJT-DF1'
-member(x,DISJOINT) | disjoint(first(x),second(x)).
% E-MEM1
-member(x,E) | member(first(x),second(x)).
% FIN-DJ2
-member(x,FINITE) | -member(y,subvar(PS)) | disjoint(y,P(x)).
% FIN-DCC
-member(x,FINITE) | -subclass(cart(x,x),union(S,inverse(S))) | equal(x,0) | member(A(x),x).
% FIN-SC4
-member(x,FINITE) | -subclass(x,FINITE) | member(U(x),FINITE).
% FIN-PS3
-member(x,FINITE) | -subclass(x,image(PS,x)) | equal(x,0).
% FIN-OM4
-member(x,FINITE) | -subclass(x,omega) | equal(x,0) | member(U(x),x).
% FIN-OM5
-member(x,FINITE) | -subclass(x,omega) | member(tc(x),omega).
% FIN-SU
-member(x,FINITE) | -subclass(y,x) | member(y,FINITE).
% FIN-PP3
-member(x,FINITE) | equal(intersection(P(P(x)),subvar(PS)),singleton(0)).
% FIN-DO1
-member(x,FINITE) | member(D(x),FINITE).
% FIN-PC3
-member(x,FINITE) | member(P(x),FINITE).
% FIN-RA1
-member(x,FINITE) | member(R(x),FINITE).
% FIN-FP1
-member(x,FINITE) | member(fix(x),FINITE).
% FIN-IDX
-member(x,FINITE) | member(id(x),FINITE).
% FIN-IN1
-member(x,FINITE) | member(inverse(x),FINITE).
% FIN-SBV
-member(x,FINITE) | member(subvar(x),FINITE).
% FIN-U-SS
-member(x,FINITE) | member(union(x,singleton(y)),FINITE).
% FIN-ADJ
-member(x,FINITE) | subclass(FINITE,image(inverse(ADJOIN(x)),FINITE)).
% FIN-SUPC
-member(x,FINITE) | subclass(P(x),FINITE).
% ON-1
-member(x,FULL) | -member(y,OMEGA) | -subclass(x,y) | member(x,succ(y)).
% FUL-REG1
-member(x,FULL) | -subclass(P(y),y) | subclass(intersection(REGULAR,x),y).
% ISBELL-4
-member(x,FULL) | -subclass(x,OMEGA) | member(x,OMEGA).
% FULDESC1
-member(x,FULL) | -subclass(y,image(E,y)) | member(intersection(x,y),DESCENDING).
% FUL-SC-9
-member(x,FULL) | equal(U(intersection(FULL,P(x))),x).
% FULSUC-A
-member(x,FULL) | equal(U(succ(x)),x).
% FUL-DF12
-member(x,FULL) | full(x).
% FUL-PC-2
-member(x,FULL) | member(P(x),FULL).
% IVR-BC2
-member(x,FULL) | member(P(x),invar(BIGCUP)).
% FUL-SC-2
-member(x,FULL) | member(U(x),FULL).
% FUL-DF13
-member(x,FULL) | member(U(x),P(x)).
% ZN-IDX
-member(x,FULL) | member(id(x),subcommutant(inverse(E))).
% FUL-PC-5
-member(x,FULL) | member(singleton(x),U(FULL)).
% FULSUC-C
-member(x,FULL) | member(succ(x),FULL).
% FULDESC2
-member(x,FULL) | member(x,DESCENDING) | member(0,x).
% FUL-DF15
-member(x,FULL) | member(x,P(P(x))).
% FIN-FS
-member(x,FUNS) | -member(D(x),FINITE) | member(R(x),FINITE).
% FS-PS-1
-member(x,FUNS) | -member(pair(y,z),PS) | -subclass(z,R(x)) | member(pair(image(inverse(x),y),image(inverse(x),z)),PS).
% FS-4
-member(x,FUNS) | -member(x,fix(composite(E,composite(cross(Id,complement(Id)),inverse(E))))).
% SBV-PS4
-member(x,FUNS) | -member(y,intersection(subvar(PS),P(P(R(x))))) | member(image(IMAGE(inverse(x)),y),subvar(PS)).
% UNOPS-7
-member(x,FUNS) | -subclass(R(x),D(x)) | member(x,UNOPS).
% MAP-FU4
-member(x,FUNS) | -subclass(R(x),y) | member(x,map(D(x),y)).
% IMGFURS1
-member(x,FUNS) | -subclass(y,x) | member(pair(id(D(y)),y),IMAGE(cross(Id,x))).
% FS-6
-member(x,FUNS) | FUNCTION(x).
% FS-5
-member(x,FUNS) | disjoint(cart(x,x),cross(Id,complement(Id))).
% IMGFURS2
-member(x,FUNS) | equal(image(IMAGE(cross(Id,x)),P(Id)),P(x)).
% SBV-SC3
-member(x,FUNS) | member(U(subvar(inverse(x))),invar(x)).
% BIJ-FS
-member(x,FUNS) | member(composite(FIRST,id(x)),BIJ).
% MAP-FU3
-member(x,FUNS) | member(x,map(D(x),V)).
% FS-3
-member(x,FUNS) | subclass(x,cart(V,V)).
% H-A
-member(x,H(A(y))) | -member(z,y) | member(x,H(z)).
% HF-SU
-member(x,H(FINITE)) | -subclass(y,x) | member(y,H(FINITE)).
% HF-DO
-member(x,H(FINITE)) | member(D(x),H(FINITE)).
% HF-PC
-member(x,H(FINITE)) | member(P(x),H(FINITE)).
% HF-RA
-member(x,H(FINITE)) | member(R(x),H(FINITE)).
% HF-SC
-member(x,H(FINITE)) | member(U(x),H(FINITE)).
% HF-IN
-member(x,H(FINITE)) | member(inverse(x),H(FINITE)).
% HF-SS-1
-member(x,H(FINITE)) | member(singleton(x),H(FINITE)).
% H-MEM-1
-member(x,H(y)) | subclass(tc(x),y).
% INV-1
-member(x,IMAGE(SWAP)) | equal(inverse(first(x)),second(x)).
% CUT-1B
-member(x,IMAGE(id(y))) | equal(intersection(first(x),y),second(x)).
% DUP-AP2
-member(x,Id) | equal(apply(inverse(DUP),x),first(x)).
% ID-2B
-member(x,Id) | equal(pair(first(x),first(x)),x).
% ID-2A
-member(x,Id) | equal(second(x),first(x)).
% ON-SC-2
-member(x,OMEGA) | -member(U(x),x) | equal(succ(U(x)),x).
% RK-5
-member(x,OMEGA) | -member(pair(x,y),ZN) | subclass(rank(y),x).
% CARD-ON3
-member(x,OMEGA) | -member(pair(y,x),Q) | subclass(card(y),x).
% ON-ORD-2
-member(x,OMEGA) | -member(x,U(x)).
% ON-1-C
-member(x,OMEGA) | -member(x,cart(V,V)).
% ON-SUC-1
-member(x,OMEGA) | -member(y,x) | member(succ(y),succ(x)).
% ON-IND-B
-member(x,OMEGA) | -subclass(intersection(x,P(y)),y) | subclass(x,y).
% RK-5-SU
-member(x,OMEGA) | -subclass(y,image(ZN,x)) | subclass(rank(y),x).
% ON-SC-5
-member(x,OMEGA) | -subclass(y,x) | member(U(y),succ(x)).
% ON-1-B
-member(x,OMEGA) | equal(0,x) | member(0,x).
% ON-A-5
-member(x,OMEGA) | equal(A(intersection(OMEGA,complement(x))),x).
% ON-SC-3
-member(x,OMEGA) | equal(U(succ(x)),x).
% ON-SUC-3
-member(x,OMEGA) | equal(U(x),x) | member(x,R(SUCC)).
% ON-SUC11
-member(x,OMEGA) | equal(composite(SUCC,id(U(x))),composite(id(x),SUCC)).
% ON-SUC13
-member(x,OMEGA) | equal(composite(SUCC,id(x)),composite(id(succ(x)),SUCC)).
% ON-BA4
-member(x,OMEGA) | equal(image(BIGCAP,P(x)),x).
% ON-SC-8
-member(x,OMEGA) | equal(image(BIGCUP,P(x)),succ(U(x))).
% ON-SUC14
-member(x,OMEGA) | equal(image(SUCC,x),intersection(succ(x),R(SUCC))).
% ON-HER-1
-member(x,OMEGA) | equal(image(inverse(S),succ(x)),P(x)).
% ON-SUC-9
-member(x,OMEGA) | equal(image(inverse(SUCC),x),U(x)).
% ISB5-SUC
-member(x,OMEGA) | equal(intersection(FULL,P(x)),succ(x)).
% ISB5HER2
-member(x,OMEGA) | equal(intersection(FULL,image(inverse(S),x)),x).
% ON-I-PC
-member(x,OMEGA) | equal(intersection(OMEGA,P(x)),succ(x)).
% ISB5-CP
-member(x,OMEGA) | equal(intersection(x,cart(V,V)),0).
% RK-ON
-member(x,OMEGA) | equal(rank(x),x).
% ON-A-2
-member(x,OMEGA) | equal(x,0) | equal(A(x),0).
% ON-1-A
-member(x,OMEGA) | member(0,succ(x)).
% ON-FUL-A
-member(x,OMEGA) | member(U(intersection(FULL,P(x))),succ(x)).
% ON-PC-2
-member(x,OMEGA) | member(U(x),OMEGA).
% ON-SC-1
-member(x,OMEGA) | member(U(x),succ(x)).
% ISB5-LEM
-member(x,OMEGA) | member(intersection(OMEGA,x),OMEGA).
% ON-RUS-1
-member(x,OMEGA) | member(intersection(RUSSELL,x),OMEGA).
% RK-ZN2
-member(x,OMEGA) | member(pair(image(ZN,x),x),RANK).
% ON-5
-member(x,OMEGA) | member(succ(x),OMEGA).
% ON-SUC-2
-member(x,OMEGA) | member(x,R(SUCC)) | subclass(image(SUCC,x),x).
% CARD-ON1
-member(x,OMEGA) | subclass(card(x),x).
% ON-SC-7
-member(x,OMEGA) | subclass(image(BIGCUP,P(x)),succ(U(x))).
% ON-SC-6
-member(x,OMEGA) | subclass(image(BIGCUP,P(x)),succ(x)).
% ON-SUC10
-member(x,OMEGA) | subclass(image(SUCC,U(x)),x).
% ON-SUC12
-member(x,OMEGA) | subclass(image(SUCC,x),succ(x)).
% ON-2
-member(x,OMEGA) | subclass(intersection(FULL,P(x)),succ(x)).
% ISBELL-5
-member(x,OMEGA) | subclass(x,OMEGA).
% ON-SC-2'
-member(x,OMEGA) | subclass(x,succ(U(x))).
% ON-A-4
-member(x,OMEGA) | subclass(x,y) | subclass(A(intersection(x,complement(y))),y).
% DESC-4
-member(x,P(DESCENDING)) | member(U(x),DESCENDING).
% FUL-SC-5
-member(x,P(FULL)) | member(U(x),FULL).
% TC-ON3
-member(x,P(OMEGA)) | equal(A(intersection(OMEGA,image(S,singleton(x)))),tc(x)).
% RK-ON-TC
-member(x,P(OMEGA)) | equal(rank(x),tc(x)).
% ON-PC-1
-member(x,P(OMEGA)) | member(U(x),OMEGA).
% TC-ON2
-member(x,P(OMEGA)) | member(tc(x),OMEGA).
% ON-HER-2
-member(x,P(OMEGA)) | subclass(x,succ(U(x))).
% IMG-DO-U
-member(x,P(P(D(VERTSECT(y))))) | member(U(x),P(D(VERTSECT(y)))).
% IMG-SC-4
-member(x,P(P(D(VERTSECT(y))))) | member(image(y,U(x)),V).
% FUL-DF16
-member(x,P(P(x))) | member(x,FULL).
% PC-SC-3
-member(x,P(P(y))) | member(U(x),P(y)).
% RUS-PC-1
-member(x,P(RUSSELL)) | member(P(x),P(RUSSELL)).
% RUS-6
-member(x,P(RUSSELL)) | member(singleton(x),P(RUSSELL)).
% RUS-7
-member(x,P(RUSSELL)) | member(succ(x),P(RUSSELL)).
% FUL-SC-8
-member(x,P(intersection(FULL,P(y)))) | member(U(x),intersection(FULL,P(y))).
% IVR-SC1
-member(x,P(invar(y))) | member(U(x),invar(y)).
% ST-SC2
-member(x,P(subcommutant(y))) | member(U(x),subcommutant(y)).
% SBV-PC
-member(x,P(subvar(y))) | member(U(x),subvar(y)).
% RP-1D
-member(x,P(union(y,z))) | member(intersection(complement(y),x),P(z)).
% RP-1C
-member(x,P(union(y,z))) | member(intersection(complement(z),x),P(y)).
% PC-U-1
-member(x,P(y)) | -member(z,P(y)) | member(union(x,z),P(y)).
% ACL-MEM
-member(x,P(y)) | equal(x,0) | member(A(x),Aclosure(y)).
% UCL-MEM
-member(x,P(y)) | member(U(x),Uclosure(y)).
% PC-1
-member(x,P(y)) | subclass(x,y).
% CART-RA1
-member(x,R(CART)) | equal(cart(D(x),R(x)),x).
% POW-RA-7
-member(x,R(POWER)) | equal(P(U(x)),x).
% POW-RA-9
-member(x,R(POWER)) | member(P(U(x)),P(x)).
% POW-BC4B
-member(x,R(POWER)) | member(U(x),x).
% K-SS-1A
-member(x,R(SINGLETON)) | -member(pair(y,x),DISJOINT) | member(pair(y,union(y,x)),K).
% SP-SS-1
-member(x,R(SINGLETON)) | equal(A(x),U(x)).
% AP-SG-3
-member(x,R(SINGLETON)) | equal(apply(inverse(SINGLETON),x),U(x)).
% AP-SG-1'
-member(x,R(SINGLETON)) | equal(image(SINGLETON,x),singleton(x)).
% SG-RA-DI
-member(x,R(SINGLETON)) | equal(image(complement(Id),x),complement(x)).
% SG-MEMB
-member(x,R(SINGLETON)) | equal(memb(x),U(x)).
% SG-RA3
-member(x,R(SINGLETON)) | equal(singleton(U(x)),x).
% SG-RA3A
-member(x,R(SINGLETON)) | member(U(x),x).
% SG-SU-DJ
-member(x,R(SINGLETON)) | subclass(x,y) | disjoint(x,y).
% RA-0E
-member(x,R(y)) | equal(pair(dom(y,V,x),x),notsub(restrict(y,V,singleton(x)),0)).
% RA-0D
-member(x,R(y)) | equal(second(notsub(restrict(y,V,singleton(x)),0)),x).
% RA-9A
-member(x,R(y)) | member(dom(y,V,x),D(y)).
% RA-1A'
-member(x,R(y)) | member(dom(y,V,x),V).
% RA-0C
-member(x,R(y)) | member(notsub(restrict(y,V,singleton(x)),0),y).
% RA-1A
-member(x,R(y)) | member(pair(dom(y,V,x),x),cart(V,V)).
% RA-1B
-member(x,R(y)) | member(pair(dom(y,V,x),x),y).
% E-SS7
-member(x,R(y)) | member(singleton(x),R(complement(composite(E,complement(y))))).
% TC-I-E-5
-member(x,REGULAR) | -member(x,tc(x)).
% REG-13
-member(x,REGULAR) | -member(y,REGULAR) | member(pairset(x,y),REGULAR).
% REG-10
-member(x,REGULAR) | -member(y,REGULAR) | member(union(x,y),REGULAR).
% REG-27
-member(x,REGULAR) | -subclass(x,image(E,x)) | equal(x,0).
% REG-8
-member(x,REGULAR) | -subclass(y,x) | member(y,REGULAR).
% RK-TC-3
-member(x,REGULAR) | equal(tc(image(RANK,x)),rank(x)).
% REG-22
-member(x,REGULAR) | member(D(x),REGULAR).
% REG-6
-member(x,REGULAR) | member(P(x),REGULAR).
% REG-23
-member(x,REGULAR) | member(R(x),REGULAR).
% REG-7
-member(x,REGULAR) | member(U(x),REGULAR).
% REG-FST
-member(x,REGULAR) | member(first(x),REGULAR).
% REG-FL
-member(x,REGULAR) | member(flip(x),REGULAR).
% ZN-FUL4
-member(x,REGULAR) | member(image(ZN,x),FULL).
% REG-11
-member(x,REGULAR) | member(intersection(x,y),REGULAR).
% REG-IN
-member(x,REGULAR) | member(inverse(x),REGULAR).
% REG-RO
-member(x,REGULAR) | member(rotate(x),REGULAR).
% REG-SEC
-member(x,REGULAR) | member(second(x),REGULAR).
% REG-12
-member(x,REGULAR) | member(singleton(x),REGULAR).
% TC-REG-4
-member(x,REGULAR) | member(tc(x),REGULAR).
% REG-4
-member(x,REGULAR) | subclass(x,REGULAR).
% RT-OP-3
-member(x,RIGHT(y)) | equal(second(x),pair(first(x),y)).
% RUS-SS
-member(x,RUSSELL) | member(singleton(x),RUSSELL).
% SR-2-COR
-member(x,S) | subclass(first(x),second(x)).
% 2ND-DF-3
-member(x,SECOND) | equal(second(first(x)),second(x)).
% SW-V-4
-member(x,SWAP) | member(first(x),cart(V,V)).
% SW-V-2
-member(x,SWAP) | member(second(x),cart(V,V)).
% SW-V-3
-member(x,SWAP) | member(x,cart(cart(V,V),cart(V,V))).
% SGIMIN-1
-member(x,U(intersection(y,R(SINGLETON)))) | member(singleton(x),y).
% ON-SUC-8
-member(x,U(y)) | -member(y,OMEGA) | member(succ(x),y).
% E-CO2
-member(x,U(y)) | -member(y,V) | member(pair(x,y),composite(E,E)).
% FUL-SC-3
-member(x,U(y)) | -subclass(y,FULL) | subclass(x,U(y)).
% SC-1B
-member(x,U(y)) | member(ran(E,x,y),y).
% SC-1A
-member(x,U(y)) | member(x,ran(E,x,y)).
% UNOPS-2
-member(x,UNOPS) | UNOP(x).
% UNOPS-6
-member(x,UNOPS) | subclass(R(x),D(x)).
% SBV-PS3
-member(x,V) | -member(0,y) | -subclass(image(CUP,cart(y,R(SINGLETON))),y) | member(intersection(P(x),complement(y)),subvar(PS)).
% SBV-PS3A
-member(x,V) | -member(0,y) | -subclass(image(CUP,cart(y,image(SINGLETON,x))),y) | member(intersection(P(x),complement(y)),subvar(PS)).
% SBV-PS3K
-member(x,V) | -member(0,y) | -subclass(image(K,y),y) | member(intersection(P(x),complement(y)),subvar(PS)).
% BA-IN-IM
-member(x,V) | -member(A(x),y) | member(x,image(inverse(BIGCAP),y)).
% SP-C
-member(x,V) | -member(complement(x),V).
% FIX-IM-5
-member(x,V) | -member(fix(x),y) | member(x,image(inverse(FIX),y)).
% RP-RS-4
-member(x,V) | -member(image(y,x),V) | member(composite(id(x),inverse(y)),V).
% RP-RS-2
-member(x,V) | -member(image(y,x),V) | member(composite(y,id(x)),V).
% IMG-IN2
-member(x,V) | -member(image(y,x),z) | member(x,image(inverse(IMAGE(y)),z)).
% ADJ-IM1A
-member(x,V) | -member(intersection(x,complement(y)),z) | -subclass(y,x) | member(x,image(ADJOIN(y),z)).
% CUT-IM2
-member(x,V) | -member(intersection(x,y),z) | member(x,image(inverse(IMAGE(id(y))),z)).
% DI-OP1
-member(x,V) | -member(pair(x,x),Di).
% K-FP1
-member(x,V) | -member(pair(x,x),K).
% FP-DF1
-member(x,V) | -member(pair(x,x),y) | member(x,fix(y)).
% IMG-RT2
-member(x,V) | -member(pair(y,z),IMAGE(RIGHT(x))) | equal(cart(y,singleton(x)),z).
% IMG-VS-6
-member(x,V) | -member(singleton(x),D(IMAGE(y))) | member(x,D(VERTSECT(y))).
% HF-SS-2
-member(x,V) | -member(singleton(x),H(FINITE)) | member(x,H(FINITE)).
% ON-1-SS
-member(x,V) | -member(singleton(x),OMEGA) | equal(x,0).
% IND-RUS4
-member(x,V) | -member(singleton(x),omega) | equal(x,0).
% SGIMIN-2
-member(x,V) | -member(singleton(x),y) | member(x,U(intersection(y,R(SINGLETON)))).
% K-SS1
-member(x,V) | -member(y,complement(x)) | member(pair(x,union(x,singleton(y))),K).
% RS-9B
-member(x,V) | -member(y,intersection(z,x)) | member(y,D(restrict(E,z,singleton(x)))).
% OP-1ST
-member(x,V) | -member(y,pair(x,z)) | member(x,y).
% GT-DF-3
-member(x,V) | -member(y,x) | -subclass(cart(x,singleton(y)),z) | member(pair(x,y),GREATEST(z)).
% MAP-CP
-member(x,V) | -member(y,z) | member(cart(x,singleton(y)),map(x,z)).
% ADJ-IM1
-member(x,V) | -member(y,z) | member(union(x,y),image(ADJOIN(x),z)).
% RUS-PC-3
-member(x,V) | -subclass(P(x),x).
% UNOPS-3
-member(x,V) | -subclass(R(x),D(x)) | member(x,D(intersection(IMAGE(FIRST),composite(S,IMAGE(SECOND))))).
% ST-2
-member(x,V) | -subclass(composite(y,x),composite(x,y)) | member(x,subcommutant(y)).
% IVR-2
-member(x,V) | -subclass(image(y,x),x) | member(x,invar(y)).
% ON-3
-member(x,V) | -subclass(intersection(FULL,P(x)),succ(x)) | member(x,OMEGA).
% ISB5FUL2
-member(x,V) | -subclass(intersection(FULL,P(x)),x).
% SS-SU
-member(x,V) | -subclass(singleton(x),y) | member(x,y).
% CUP-OP1
-member(x,V) | -subclass(union(y,z),x) | member(pair(pair(y,z),x),composite(inverse(DUP),cross(S,S))).
% DESC-2
-member(x,V) | -subclass(x,image(E,x)) | member(x,DESCENDING).
% SBV-2
-member(x,V) | -subclass(x,image(y,x)) | member(x,subvar(y)).
% SBV-U-2
-member(x,V) | -subclass(x,union(y,image(z,x))) | member(x,subvar(union(id(y),z))).
% A-UP-2
-member(x,V) | -subclass(x,y) | equal(A(pairset(x,y)),x).
% PC-2
-member(x,V) | -subclass(x,y) | member(x,P(y)).
% IM-9
-member(x,V) | -subclass(x,y) | member(x,complement(image(E,complement(y)))).
% TC-LEM1C
-member(x,V) | -subclass(y,union(composite(inverse(E),composite(y,inverse(E))),cart(V,x))) | member(image(y,omega),V).
% TC-LEM1B
-member(x,V) | -subclass(y,union(composite(inverse(E),composite(y,inverse(E))),cart(V,x))) | subclass(P(D(VERTSECT(y))),D(VERTSECT(y))).
% PS-DF-4
-member(x,V) | -subclass(y,x) | equal(y,x) | member(pair(y,x),PS).
% RC-OP2
-member(x,V) | -subclass(y,x) | member(pair(y,intersection(x,complement(y))),RC(x)).
% RP-SR
-member(x,V) | -subclass(y,x) | member(pair(y,x),S).
% RP-IM-SR
-member(x,V) | -subclass(y,x) | member(x,image(S,singleton(y))).
% RP-PC
-member(x,V) | -subclass(y,x) | member(y,P(x)).
% RP-1B
-member(x,V) | -subclass(y,x) | member(y,V).
% IMG-RT3
-member(x,V) | ONEONE(IMAGE(RIGHT(x))).
% SP-A-C
-member(x,V) | equal(A(complement(x)),0).
% TC-FP-2
-member(x,V) | equal(A(fix(composite(ADJOIN(x),BIGCUP))),tc(x)).
% A-SS-2
-member(x,V) | equal(A(image(E,singleton(x))),singleton(x)).
% TC-A-2
-member(x,V) | equal(A(intersection(FULL,image(S,singleton(x)))),tc(x)).
% A-5
-member(x,V) | equal(A(singleton(x)),x).
% ACL-ACL2
-member(x,V) | equal(Aclosure(Aclosure(x)),Aclosure(x)).
% IMG-DO-V
-member(x,V) | equal(D(IMAGE(x)),V).
% RC-DO
-member(x,V) | equal(D(RC(x)),P(x)).
% VS-DO-V
-member(x,V) | equal(D(VERTSECT(x)),V).
% SP-DO-C
-member(x,V) | equal(D(complement(x)),V).
% RS-9
-member(x,V) | equal(D(restrict(E,y,singleton(x))),intersection(y,x)).
% RC-RA
-member(x,V) | equal(R(RC(x)),P(x)).
% SP-RA-C
-member(x,V) | equal(R(complement(x)),V).
% SP-SC-C
-member(x,V) | equal(U(complement(x)),V).
% ZN-IM-3
-member(x,V) | equal(U(image(ZN,singleton(x))),image(ZN,x)).
% MAP-SC2
-member(x,V) | equal(U(map(x,y)),cart(x,y)).
% SC-4
-member(x,V) | equal(U(singleton(x)),x).
% SUC-SC-1
-member(x,V) | equal(U(succ(x)),union(x,U(x))).
% TC-SS-2
-member(x,V) | equal(U(tc(singleton(x))),tc(x)).
% UCL-UCL2
-member(x,V) | equal(Uclosure(Uclosure(x)),Uclosure(x)).
% ACL-AP
-member(x,V) | equal(apply(ACLOSURE,x),Aclosure(x)).
% DUP-AP1
-member(x,V) | equal(apply(DUP,x),pair(x,x)).
% FIX-AP
-member(x,V) | equal(apply(FIX,x),fix(x)).
% HC-AP
-member(x,V) | equal(apply(HC,x),H(x)).
% INV-AP
-member(x,V) | equal(apply(IMAGE(SWAP),x),inverse(x)).
% CUT-AP
-member(x,V) | equal(apply(IMAGE(id(y)),x),intersection(y,x)).
% HER-AP2
-member(x,V) | equal(apply(IMAGE(inverse(S)),singleton(x)),P(x)).
% POW-AP
-member(x,V) | equal(apply(POWER,x),P(x)).
% SUC-AP1
-member(x,V) | equal(apply(SUCC,x),succ(x)).
% TC-AP
-member(x,V) | equal(apply(TC,x),tc(x)).
% UCL-AP
-member(x,V) | equal(apply(UCLOSURE,x),Uclosure(x)).
% AP-14A
-member(x,V) | equal(apply(V,x),V).
% IMG-RT4
-member(x,V) | equal(composite(IMAGE(FIRST),IMAGE(RIGHT(x))),Id).
% DI-IM-SS
-member(x,V) | equal(image(Di,singleton(x)),complement(singleton(x))).
% HER-AP3
-member(x,V) | equal(image(IMAGE(inverse(S)),singleton(singleton(x))),singleton(P(x))).
% AP-SG-1
-member(x,V) | equal(image(SINGLETON,singleton(x)),singleton(singleton(x))).
% IM-10A
-member(x,V) | equal(image(V,singleton(x)),V).
% ZN-PC
-member(x,V) | equal(image(ZN,P(x)),P(image(ZN,x))).
% ZN-IM-2
-member(x,V) | equal(image(ZN,singleton(x)),P(image(ZN,x))).
% ZN-SUC
-member(x,V) | equal(image(ZN,succ(x)),image(ZN,singleton(x))).
% SG-SS-DI
-member(x,V) | equal(image(complement(Id),singleton(x)),complement(singleton(x))).
% PC-5
-member(x,V) | equal(image(inverse(S),singleton(x)),P(x)).
% SS-7
-member(x,V) | equal(memb(singleton(x)),x).
% RK-SS
-member(x,V) | equal(rank(singleton(x)),succ(rank(x))).
% IDX-SS-2
-member(x,V) | equal(singleton(pair(x,x)),id(singleton(x))).
% TC-SS-3
-member(x,V) | equal(tc(singleton(x)),union(singleton(x),tc(x))).
% RP-A-5
-member(x,V) | equal(union(complement(image(V,singleton(x))),x),x).
% E-RA2
-member(x,V) | equal(x,0) | member(x,R(E)).
% ACL-V-2
-member(x,V) | member(Aclosure(x),V).
% RP-FL-DO
-member(x,V) | member(D(flip(x)),V).
% RP-7B
-member(x,V) | member(D(restrict(y,x,z)),V).
% RP-2A
-member(x,V) | member(D(x),V).
% POW-RA-4
-member(x,V) | member(P(x),R(POWER)).
% RUS-PC-4
-member(x,V) | member(P(x),RUSSELL).
% AX-PC
-member(x,V) | member(P(x),V).
% RP-2B
-member(x,V) | member(R(x),V).
% FUL-SC-6
-member(x,V) | member(U(intersection(FULL,P(x))),intersection(FULL,P(x))).
% AX-SC
-member(x,V) | member(U(x),V).
% UCL-V-2
-member(x,V) | member(Uclosure(x),V).
% FS-CP
-member(x,V) | member(cart(x,singleton(y)),FUNS).
% RP-E-2
-member(x,V) | member(composite(id(x),E),V).
% OP-13A
-member(x,V) | member(first(x),V).
% RP-FP
-member(x,V) | member(fix(x),V).
% RP-FL
-member(x,V) | member(flip(x),V).
% BIJ-IDX1
-member(x,V) | member(id(x),BIJ).
% UO-IDX
-member(x,V) | member(id(x),UNOPS).
% RP-IDX-1
-member(x,V) | member(id(x),V).
% RP-8-COR
-member(x,V) | member(image(inverse(S),x),V).
% SUC-IN6
-member(x,V) | member(image(inverse(SUCC),x),V).
% RP-2C
-member(x,V) | member(image(x,y),V).
% FIN-PC2
-member(x,V) | member(intersection(P(x),complement(FINITE)),subvar(PS)).
% REG-2_I
-member(x,V) | member(intersection(REGULAR,x),REGULAR).
% RUS-9
-member(x,V) | member(intersection(RUSSELL,x),P(RUSSELL)).
% RP-1A
-member(x,V) | member(intersection(y,x),V).
% RP-5
-member(x,V) | member(inverse(x),V).
% SS-6-COR
-member(x,V) | member(memb(x),V).
% IMG-OP1A
-member(x,V) | member(pair(D(x),R(x)),IMAGE(x)).
% BC-3C
-member(x,V) | member(pair(P(x),x),BIGCUP).
% HER-AP1
-member(x,V) | member(pair(singleton(x),P(x)),IMAGE(inverse(S))).
% BA-SS
-member(x,V) | member(pair(singleton(x),x),BIGCAP).
% BC-3B
-member(x,V) | member(pair(singleton(x),x),BIGCUP).
% LB-0
-member(x,V) | member(pair(x,0),LOWERBOUND).
% ACL-OP1
-member(x,V) | member(pair(x,Aclosure(x)),ACLOSURE).
% IMG-OP-2
-member(x,V) | member(pair(x,D(x)),IMAGE(FIRST)).
% HC-OP-1
-member(x,V) | member(pair(x,H(x)),HC).
% POW-3
-member(x,V) | member(pair(x,P(x)),POWER).
% IMG-OP-3
-member(x,V) | member(pair(x,R(x)),IMAGE(SECOND)).
% BC-3
-member(x,V) | member(pair(x,U(x)),BIGCUP).
% UCL-OP1
-member(x,V) | member(pair(x,Uclosure(x)),UCLOSURE).
% FIX-1
-member(x,V) | member(pair(x,fix(x)),FIX).
% IDP-1
-member(x,V) | member(pair(x,id(x)),IDP).
% CUT-2
-member(x,V) | member(pair(x,intersection(x,y)),IMAGE(id(y))).
% INV-2
-member(x,V) | member(pair(x,inverse(x)),IMAGE(SWAP)).
% DUP-1
-member(x,V) | member(pair(x,pair(x,x)),DUP).
% E-SS1
-member(x,V) | member(pair(x,singleton(x)),E).
% LB-5
-member(x,V) | member(pair(x,singleton(x)),LOWERBOUND).
% SG-3
-member(x,V) | member(pair(x,singleton(x)),SINGLETON).
% ES-DF-4
-member(x,V) | member(pair(x,succ(x)),ES).
% SUC-DF-5
-member(x,V) | member(pair(x,succ(x)),SUCC).
% TC-OP1
-member(x,V) | member(pair(x,tc(x)),TC).
% ID-3
-member(x,V) | member(pair(x,x),Id).
% RP-1-RS
-member(x,V) | member(restrict(x,y,z),V).
% RP-RO
-member(x,V) | member(rotate(x),V).
% OP-13B
-member(x,V) | member(second(x),V).
% SG-RA2
-member(x,V) | member(singleton(x),R(SINGLETON)).
% SBV-MEM
-member(x,V) | member(subvar(x),V).
% SUC-V-1
-member(x,V) | member(succ(x),V).
% RK-TC-2
-member(x,V) | member(tc(image(RANK,x)),OMEGA).
% TC-V
-member(x,V) | member(tc(x),V).
% TC-FP-1
-member(x,V) | member(tc(x),fix(composite(ADJOIN(x),BIGCUP))).
% SC-U-SS
-member(x,V) | member(union(x,singleton(y)),V).
% A-2B
-member(x,V) | member(x,A(y)) | member(ran(complement(E),x,y),y).
% PC-2-COR
-member(x,V) | member(x,P(x)).
% AP-6D
-member(x,V) | member(x,apply(y,x)) | member(x,fix(complement(composite(inverse(E),y)))).
% FP-UB1
-member(x,V) | member(x,fix(composite(E,composite(inverse(y),UB(complement(z)))))) | subclass(image(y,x),image(z,x)).
% FP-UB2
-member(x,V) | member(x,fix(composite(E,composite(y,UB(z))))) | subclass(image(inverse(y),x),image(complement(z),x)).
% SG-DI-SS
-member(x,V) | member(x,image(Di,y)) | subclass(y,singleton(x)).
% E-IM2
-member(x,V) | member(x,image(E,y)) | disjoint(x,y).
% RK-4-SUC
-member(x,V) | member(x,image(ZN,succ(rank(x)))).
% DF-UP-2
-member(x,V) | member(x,pairset(x,y)).
% DF-UP-3
-member(x,V) | member(x,pairset(y,x)).
% SS-2
-member(x,V) | member(x,singleton(x)).
% SUC-DF2
-member(x,V) | member(x,succ(x)).
% RUS-2
-member(x,V) | member(x,x) | member(x,RUSSELL).
% FP-E2
-member(x,V) | member(x,x) | member(x,complement(fix(E))).
% AX-C-2
-member(x,V) | member(x,y) | member(x,complement(y)).
% Q-RT-1
-member(x,V) | subclass(IMAGE(RIGHT(x)),Q).
% E-SS-PC
-member(x,V) | subclass(P(image(y,singleton(x))),R(complement(composite(E,complement(y))))).
% RK-DO3'
-member(x,V) | subclass(rank(intersection(REGULAR,x)),tc(image(RANK,x))).
% SC-4-LEM
-member(x,V) | subclass(x,U(singleton(x))).
% TH-CP
-member(x,V) | thin(cart(y,x)).
% TH-V
-member(x,V) | thin(x).
% AP-6A
-member(x,apply(y,x)) | member(x,fix(composite(inverse(E),y))).
% CA-2
-member(x,cantor(y)) | -member(x,apply(y,x)).
% E-MEM2
-member(x,cart(V,V)) | -member(first(x),second(x)) | member(x,E).
% FU-SS
-member(x,cart(V,V)) | FUNCTION(singleton(x)).
% A-OP-2
-member(x,cart(V,V)) | equal(A(A(x)),first(x)).
% A-OP-1'
-member(x,cart(V,V)) | equal(A(x),singleton(first(x))).
% DO-SS-1
-member(x,cart(V,V)) | equal(D(singleton(x)),singleton(first(x))).
% RA-SS-1
-member(x,cart(V,V)) | equal(R(singleton(x)),singleton(second(x))).
% SC-1ST
-member(x,cart(V,V)) | equal(U(D(singleton(x))),first(x)).
% SC-2ND
-member(x,cart(V,V)) | equal(U(R(singleton(x))),second(x)).
% CAP-AP1
-member(x,cart(V,V)) | equal(apply(CAP,x),intersection(first(x),second(x))).
% CART-AP1
-member(x,cart(V,V)) | equal(apply(CART,x),cart(first(x),second(x))).
% CRS-AP1
-member(x,cart(V,V)) | equal(apply(CROSS,x),cross(first(x),second(x))).
% CUP-AP2
-member(x,cart(V,V)) | equal(apply(CUP,x),union(first(x),second(x))).
% 1ST-AP
-member(x,cart(V,V)) | equal(apply(FIRST,x),first(x)).
% MG-AP-2
-member(x,cart(V,V)) | equal(apply(IMG,x),image(first(x),second(x))).
% PRS-AP1
-member(x,cart(V,V)) | equal(apply(PAIRSET,x),pairset(first(x),second(x))).
% 2ND-AP
-member(x,cart(V,V)) | equal(apply(SECOND,x),second(x)).
% SDF-AP1
-member(x,cart(V,V)) | equal(apply(SYMDIF,x),union(intersection(second(x),complement(first(x))),intersection(first(x),complement(second(x))))).
% CP-SS-5'
-member(x,cart(V,V)) | equal(cart(singleton(first(x)),singleton(second(x))),singleton(x)).
% SW-1ST
-member(x,cart(V,V)) | equal(first(swap(x)),second(x)).
% SW-SS
-member(x,cart(V,V)) | equal(inverse(singleton(x)),singleton(swap(x))).
% SW-2ND
-member(x,cart(V,V)) | equal(second(swap(x)),first(x)).
% SW-0B
-member(x,cart(V,V)) | equal(swap(swap(x)),x).
% CART-OP2
-member(x,cart(V,V)) | member(pair(x,cart(first(x),second(x))),CART).
% 1ST-DF-1
-member(x,cart(V,V)) | member(pair(x,first(x)),FIRST).
% 2ND-DF-1
-member(x,cart(V,V)) | member(pair(x,second(x)),SECOND).
% SW-DF-2
-member(x,cart(V,V)) | member(pair(x,swap(x)),SWAP).
% SDF-OP1
-member(x,cart(V,V)) | member(pair(x,union(intersection(second(x),complement(first(x))),intersection(first(x),complement(second(x))))),SYMDIF).
% BIJ-SS
-member(x,cart(V,V)) | member(singleton(x),BIJ).
% FS-SS
-member(x,cart(V,V)) | member(singleton(x),FUNS).
% CART-RA4
-member(x,cart(V,V)) | member(singleton(x),R(CART)).
% SDF-LEM1
-member(x,cart(V,V)) | member(union(intersection(second(x),complement(first(x))),intersection(first(x),complement(second(x)))),V).
% COMPRELN
-member(x,cart(V,V)) | member(x,y) | member(x,composite(Id,complement(y))).
% SPW-LEM
-member(x,cart(V,V)) | member(x,y) | member(x,restrict(complement(y),V,V)).
% OP-15
-member(x,cart(cart(V,V),V)) | equal(pair(pair(first(first(x)),second(first(x))),second(x)),x).
% TW-AP2
-member(x,cart(cart(V,V),cart(V,V))) | equal(apply(TWIST,x),pair(pair(first(first(x)),first(second(x))),pair(second(first(x)),second(second(x))))).
% BIJ-ADJ
-member(x,cart(complement(D(y)),complement(R(y)))) | -member(y,BIJ) | member(union(singleton(x),y),BIJ).
% CP-SS-1
-member(x,cart(singleton(y),singleton(z))) | equal(x,pair(y,z)).
% AX-CP-4
-member(x,cart(y,z)) | equal(pair(first(x),second(x)),x).
% CP-4A
-member(x,cart(y,z)) | member(first(x),y).
% CP-4B
-member(x,cart(y,z)) | member(second(x),z).
% SW-0A
-member(x,cart(y,z)) | member(swap(x),cart(z,y)).
% PC-6LEM5
-member(x,cart(y,z)) | member(x,P(P(union(y,P(z))))).
% SR-C-A
-member(x,complement(A(y))) | -disjoint(y,P(complement(singleton(x)))).
% E-C-A-2
-member(x,complement(A(y))) | -member(y,V) | member(pair(x,y),composite(E,complement(E))).
% FIN-PP1
-member(x,complement(FINITE)) | member(x,U(intersection(P(P(x)),subvar(PS)))).
% IM-8
-member(x,complement(image(E,complement(y)))) | subclass(x,y).
% Q-AP-RA
-member(x,complement(singleton(0))) | equal(R(apply(Q,x)),V).
% BA-AP-1
-member(x,complement(singleton(0))) | equal(apply(BIGCAP,x),A(x)).
% LB-4
-member(x,complement(singleton(0))) | member(pair(A(x),x),LOWERBOUND).
% BA-3
-member(x,complement(singleton(0))) | member(pair(x,A(x)),BIGCAP).
% SS-C
-member(x,complement(singleton(x))).
% DESC-9
-member(x,complement(x)) | -member(singleton(x),DESCENDING).
% AX-C-1
-member(x,complement(y)) | -member(x,y).
% ACL-FP1
-member(x,fix(ACLOSURE)) | Aclosed(x).
% INV-FP1
-member(x,fix(IMAGE(SWAP))) | equal(inverse(x),x).
% UCL-FP1
-member(x,fix(UCLOSURE)) | Uclosed(x).
% X-CO-FP5
-member(x,fix(complement(composite(complement(composite(E,cross(Id,inverse(y)))),composite(cross(inverse(z),Id),inverse(E)))))) | subclass(composite(x,z),composite(y,x)).
% X-CO-FP2
-member(x,fix(complement(composite(complement(composite(E,cross(Id,y))),composite(cross(z,Id),inverse(E)))))) | subclass(composite(x,inverse(z)),composite(inverse(y),x)).
% FP-IM-E2
-member(x,fix(complement(composite(complement(composite(E,y)),composite(z,inverse(E)))))) | subclass(image(z,x),image(inverse(y),x)).
% AP-6C
-member(x,fix(complement(composite(inverse(E),y)))) | -member(x,apply(y,x)).
% BC-FP-2
-member(x,fix(composite(E,BIGCUP))) | member(U(x),x).
% FP-UB4
-member(x,fix(composite(E,composite(inverse(y),UB(complement(z)))))) | -subclass(image(y,x),image(z,x)).
% FP-UB3
-member(x,fix(composite(E,composite(y,UB(z))))) | -subclass(image(inverse(y),x),image(complement(z),x)).
% IMG-BIN1
-member(x,fix(composite(IMAGE(y),composite(CART,DUP)))) | equal(image(y,cart(x,x)),x).
% X-CO-FP4
-member(x,fix(composite(complement(composite(E,cross(Id,inverse(y)))),composite(cross(inverse(z),Id),inverse(E))))) | -subclass(composite(x,z),composite(y,x)).
% X-CO-FP1
-member(x,fix(composite(complement(composite(E,cross(Id,y))),composite(cross(z,Id),inverse(E))))) | -subclass(composite(x,inverse(z)),composite(inverse(y),x)).
% FP-IM-E1
-member(x,fix(composite(complement(composite(E,inverse(y))),composite(z,inverse(E))))) | -subclass(image(z,x),image(y,x)).
% FP-IM-E4
-member(x,fix(composite(complement(composite(E,y)),composite(z,inverse(E))))) | -subclass(image(z,x),image(inverse(y),x)).
% AP-6B
-member(x,fix(composite(inverse(E),y))) | member(x,apply(y,x)).
% IMG-FP1
-member(x,fix(composite(inverse(S),IMAGE(y)))) | subclass(x,image(y,x)).
% GT-SS
-member(x,fix(y)) | member(pair(singleton(x),x),GREATEST(y)).
% LT-SS
-member(x,fix(y)) | member(pair(singleton(x),x),LEAST(y)).
% FP-DF2
-member(x,fix(y)) | member(pair(x,x),y).
% IDX-7
-member(x,id(y)) | equal(second(x),first(x)).
% IDX-8
-member(x,id(y)) | member(first(x),y).
% BC-IM-0
-member(x,image(BIGCUP,y)) | equal(U(dom(BIGCUP,y,x)),x).
% E-IM-SS1
-member(x,image(E,singleton(y))) | member(y,x).
% E-IM1
-member(x,image(E,y)) | -disjoint(x,y).
% SUC-IM-E
-member(x,image(E,y)) | member(succ(x),image(E,y)).
% IMG-RS2
-member(x,image(IMAGE(cross(Id,y)),P(Id))) | equal(composite(y,id(D(x))),x).
% CARD-AP
-member(x,image(Q,OMEGA)) | equal(apply(CARD,x),card(x)).
% CARD-ON2
-member(x,image(Q,OMEGA)) | member(card(x),OMEGA).
% CARD-VS1
-member(x,image(Q,OMEGA)) | member(card(x),image(Q,singleton(x))).
% CARD-OP3
-member(x,image(Q,OMEGA)) | member(pair(x,card(x)),CARD).
% CARD-OP1
-member(x,image(Q,OMEGA)) | member(pair(x,card(x)),Q).
% IND-Q
-member(x,image(Q,omega)) | member(union(x,singleton(y)),image(Q,omega)).
% SR-SS-PC
-member(x,image(S,singleton(y))) | member(y,P(x)).
% SR-SS-IM
-member(x,image(S,singleton(y))) | subclass(y,x).
% SG-IM-1
-member(x,image(SINGLETON,y)) | equal(singleton(U(x)),x).
% SG-IM-2
-member(x,image(SINGLETON,y)) | member(U(x),y).
% FULSUCA1
-member(x,image(SUCC,FULL)) | equal(succ(U(x)),x).
% OM-SC-2
-member(x,image(SUCC,omega)) | equal(succ(U(x)),x).
% FULSUCA2
-member(x,image(SUCC,y)) | -subclass(y,FULL) | member(U(x),y).
% IM-10A2
-member(x,image(V,singleton(y))) | member(pair(x,y),cart(V,V)).
% RK-3
-member(x,image(ZN,OMEGA)) | member(rank(x),OMEGA).
% RK-5-IM
-member(x,image(ZN,rank(x))) | -member(rank(x),OMEGA).
% RK-9
-member(x,image(ZN,y)) | -member(y,OMEGA) | member(rank(x),y).
% ADJ-IN1
-member(x,image(inverse(ADJOIN(y)),z)) | member(union(x,y),z).
% BA-IM-IN
-member(x,image(inverse(BIGCAP),y)) | member(A(x),y).
% BC-IM-7
-member(x,image(inverse(BIGCUP),y)) | member(U(x),y).
% CARD-IM1
-member(x,image(inverse(CARD),y)) | member(card(x),y).
% FIX-IM-4
-member(x,image(inverse(FIX),y)) | member(fix(x),y).
% IDP-IM-4
-member(x,image(inverse(IDP),y)) | member(id(x),y).
% CUT-FS2
-member(x,image(inverse(IMAGE(id(cart(V,V)))),FUNS)) | FUNCTION(composite(Id,x)).
% CUT-IM1
-member(x,image(inverse(IMAGE(id(y))),z)) | member(intersection(x,y),z).
% IMG-IN1
-member(x,image(inverse(IMAGE(y)),z)) | member(image(y,x),z).
% POW-IN1
-member(x,image(inverse(POWER),y)) | member(P(x),y).
% ON-SUC7B
-member(x,image(inverse(S),omega)) | equal(0,x) | member(U(x),x).
% SR-2-IMS
-member(x,image(inverse(S),y)) | subclass(x,dom(inverse(S),y,x)).
% TC-IMIN2
-member(x,image(inverse(TC),y)) | member(tc(x),y).
% E-SS4
-member(x,image(inverse(y),singleton(z))) | member(pair(x,singleton(z)),complement(composite(E,complement(y)))).
% IM-0B'
-member(x,image(inverse(y),z)) | -equal(restrict(y,singleton(x),z),0).
% IM-0E'
-member(x,image(inverse(y),z)) | equal(first(notsub(restrict(y,singleton(x),z),0)),x).
% IM-0F'
-member(x,image(inverse(y),z)) | equal(notsub(restrict(y,singleton(x),z),0),pair(x,ran(y,x,z))).
% IM-0D'
-member(x,image(inverse(y),z)) | member(notsub(restrict(y,singleton(x),z),0),y).
% IM-3'
-member(x,image(inverse(y),z)) | member(pair(x,ran(y,x,z)),cart(V,V)).
% IM-4'
-member(x,image(inverse(y),z)) | member(pair(x,ran(y,x,z)),y).
% IM-1'
-member(x,image(inverse(y),z)) | member(ran(y,x,z),z).
% CO-IM2
-member(x,image(y,image(z,singleton(u)))) | member(pair(u,x),cart(V,V)).
% CO-IM3
-member(x,image(y,image(z,singleton(u)))) | member(pair(u,x),composite(y,z)).
% IM-SS-2
-member(x,image(y,singleton(z))) | -member(z,image(u,singleton(v))) | member(x,image(y,image(u,singleton(v)))).
% IM-SS-1
-member(x,image(y,singleton(z))) | member(pair(x,z),cart(V,V)).
% IM-1-COR
-member(x,image(y,singleton(z))) | member(pair(z,x),y).
% AP-4A
-member(x,image(y,singleton(z))) | subclass(x,apply(y,z)).
% IM-0B
-member(x,image(y,z)) | -equal(restrict(y,z,singleton(x)),0).
% CO-E-1
-member(x,image(y,z)) | -member(z,V) | member(pair(z,x),composite(y,inverse(E))).
% IM-0F
-member(x,image(y,z)) | equal(notsub(restrict(y,z,singleton(x)),0),pair(dom(y,z,x),x)).
% IM-0E
-member(x,image(y,z)) | equal(second(notsub(restrict(y,z,singleton(x)),0)),x).
% IM-7-LEM
-member(x,image(y,z)) | member(dom(y,z,x),D(y)).
% IM-1
-member(x,image(y,z)) | member(dom(y,z,x),z).
% IM-0D
-member(x,image(y,z)) | member(notsub(restrict(y,z,singleton(x)),0),y).
% IM-3
-member(x,image(y,z)) | member(pair(dom(y,z,x),x),cart(V,V)).
% IM-4
-member(x,image(y,z)) | member(pair(dom(y,z,x),x),y).
% SBV-U-3
-member(x,intersection(D(IMAGE(y)),subvar(union(id(z),y)))) | member(union(x,image(y,x)),subvar(union(id(z),y))).
% SBV-IMG4
-member(x,intersection(D(IMAGE(y)),subvar(y))) | member(image(y,x),subvar(y)).
% FUL-SC-7
-member(x,intersection(FULL,P(y))) | member(U(x),intersection(FULL,P(y))).
% FUL-REG3
-member(x,intersection(FULL,REGULAR)) | equal(x,0) | member(0,x).
% ON-SUC5A
-member(x,intersection(OMEGA,R(SUCC))) | equal(succ(U(x)),x).
% SG-IM-2'
-member(x,intersection(P(y),R(SINGLETON))) | member(U(x),y).
% SUC-IND4
-member(x,intersection(complement(P(complement(singleton(0)))),fix(composite(S,IMAGE(SUCC))))) | INDUCTIVE(x).
% OM-PC-1
-member(x,intersection(omega,P(omega))) | member(succ(x),intersection(omega,P(omega))).
% IND-LEM2
-member(x,intersection(omega,P(y))) | -subclass(intersection(omega,P(y)),y) | member(succ(x),intersection(omega,P(y))).
% ON-IND-1
-member(x,intersection(omega,y)) | -subclass(image(SUCC,y),y) | member(0,union(x,y)).
% ON-IND-2
-member(x,intersection(omega,y)) | -subclass(image(SUCC,y),y) | subclass(omega,union(x,y)).
% SP-1
-member(x,intersection(y,complement(y))).
% AX-I-1
-member(x,intersection(y,z)) | member(x,y).
% AX-I-2
-member(x,intersection(y,z)) | member(x,z).
% IVR-BC1A
-member(x,invar(BIGCUP)) | member(U(x),FULL).
% IVR-BC1B
-member(x,invar(BIGCUP)) | member(image(inverse(S),x),FULL).
% IVR-BC-S
-member(x,invar(BIGCUP)) | member(image(inverse(S),x),invar(BIGCUP)).
% IVR-IM
-member(x,invar(y)) | member(image(y,x),invar(y)).
% IVR-1
-member(x,invar(y)) | subclass(image(y,x),x).
% SW-0D
-member(x,inverse(y)) | member(swap(x),y).
% MAP-FU2
-member(x,map(y,z)) | FUNCTION(x).
% MAP-DO
-member(x,map(y,z)) | equal(D(x),y).
% MAP-RA
-member(x,map(y,z)) | subclass(R(x),z).
% OM-FUL-6
-member(x,omega) | -member(succ(y),succ(x)) | member(y,x).
% ON-OM-AD
-member(x,omega) | -member(y,image(inverse(S),omega)) | member(union(y,singleton(x)),image(inverse(S),omega)).
% IND-SC-2
-member(x,omega) | -subclass(x,U(x)) | equal(x,0).
% ON-SC-5B
-member(x,omega) | -subclass(y,x) | equal(x,0) | member(U(y),x).
% OM-SC-1
-member(x,omega) | equal(U(succ(x)),x).
% CN-OM-1A
-member(x,omega) | equal(card(x),x).
% ON-SUC15
-member(x,omega) | equal(image(SUCC,x),intersection(succ(x),complement(singleton(0)))).
% ON-OM-1'
-member(x,omega) | equal(intersection(omega,P(x)),succ(x)).
% OM-SC-2A
-member(x,omega) | equal(x,0) | equal(succ(U(x)),x).
% ON-7-A
-member(x,omega) | member(0,succ(x)).
% OM-SC-3
-member(x,omega) | member(U(x),omega).
% HF-ZN-2
-member(x,omega) | member(image(ZN,x),FINITE).
% IVR-OM-C
-member(x,omega) | member(intersection(omega,complement(x)),invar(SUCC)).
% IND-PS
-member(x,omega) | member(pair(x,succ(x)),PS).
% OM-DF-1
-member(x,omega) | member(succ(x),omega).
% OM-FUL-2
-member(x,omega) | subclass(U(x),x).
% IND-C
-member(x,omega) | subclass(image(SUCC,complement(x)),complement(x)).
% OM-SUC13
-member(x,omega) | subclass(intersection(x,complement(singleton(0))),R(SUCC)).
% OM-PC-7
-member(x,omega) | subclass(x,omega).
% ON-SUC16
-member(x,omega) | subclass(x,union(singleton(0),image(SUCC,x))).
% DF-UP-1
-member(x,pairset(y,z)) | equal(x,y) | equal(x,z).
% A-2A
-member(x,ran(complement(E),x,y)) | member(x,A(y)).
% DO-7LEM1
-member(x,restrict(y,z,u)) | member(first(x),intersection(z,D(y))).
% OP-RO
-member(x,rotate(y)) | member(pair(pair(second(first(x)),second(x)),first(first(x))),y).
% SS-3
-member(x,singleton(y)) | equal(x,y).
% ZN-RA1
-member(x,subcommutant(inverse(E))) | member(R(x),FULL).
% ZN-ST-1
-member(x,subcommutant(inverse(E))) | subclass(composite(Id,x),ZN).
% ST-1
-member(x,subcommutant(y)) | subclass(composite(y,x),composite(x,y)).
% ST-1'
-member(x,subcommutant(y)) | subcommute(y,x).
% SBV-PS2
-member(x,subvar(PS)) | -subclass(y,A(x)) | member(image(IMAGE(id(complement(y))),x),subvar(PS)).
% FIN-DJ1
-member(x,subvar(PS)) | disjoint(x,FINITE).
% SBV-U-1
-member(x,subvar(union(id(y),z))) | subclass(x,union(y,image(z,x))).
% SBV-SS
-member(x,subvar(y)) | -member(z,image(y,x)) | member(union(x,singleton(z)),subvar(y)).
% SBV-1
-member(x,subvar(y)) | subclass(x,image(y,x)).
% ON-3-LEM
-member(x,succ(y)) | -member(pair(x,y),cart(V,V)) | -member(pair(x,y),complement(Id)) | -member(pair(x,y),complement(E)).
% SUC-DF3
-member(x,succ(y)) | equal(x,y) | member(x,y).
% TC-I-E-2
-member(x,tc(x)) | member(x,D(intersection(TC,E))).
% TC-SU-4
-member(x,tc(y)) | -member(y,tc(z)) | member(x,tc(z)).
% RA-3LEM2
-member(x,union(R(y),R(z))) | member(x,R(y)) | member(x,R(z)).
% U-7A
-member(x,union(y,z)) | member(x,y) | member(x,z).
% RUS-1
-member(x,x) | -member(x,RUSSELL).
% FP-E1
-member(x,x) | -member(x,complement(fix(E))).
% SUC-FP-1
-member(x,x) | equal(succ(x),x).
% DESC-8
-member(x,x) | member(singleton(x),DESCENDING).
% RUS-SC-1
-member(x,x) | subclass(x,U(x)).
% DJ-6A
-member(x,y) | -disjoint(singleton(x),y).
% ON-OM-SB
-member(x,y) | -member(intersection(y,complement(singleton(x))),image(inverse(S),omega)) | -subclass(y,omega) | member(y,image(inverse(S),omega)).
% CUP-SUB
-member(x,y) | -member(intersection(y,complement(singleton(x))),z) | -subclass(image(CUP,cart(z,R(SINGLETON))),z) | member(y,z).
% IM-2
-member(x,y) | -member(pair(x,z),u) | -member(pair(x,z),cart(V,V)) | member(z,image(u,y)).
% IM-2B
-member(x,y) | -member(pair(x,z),u) | -subclass(u,cart(V,V)) | member(z,image(u,y)).
% E-IN-C2
-member(x,y) | -member(pair(y,x),inverse(complement(E))).
% LT-DF-4
-member(x,y) | -member(pair(y,z),LEAST(u)) | member(pair(z,x),u).
% UB-2
-member(x,y) | -member(pair(y,z),UPPERBOUND) | subclass(x,z).
% PC-6LEM3
-member(x,y) | -member(singleton(z),y) | member(pair(x,z),P(P(y))).
% ON-ORD-3
-member(x,y) | -member(x,OMEGA) | -member(y,x).
% DESC-6
-member(x,y) | -member(x,U(DESCENDING)) | -member(y,V) | member(y,U(DESCENDING)).
% DO-4B
-member(x,y) | -member(x,cart(V,V)) | member(first(x),D(y)).
% RA-4X
-member(x,y) | -member(x,cart(V,V)) | member(second(x),R(y)).
% SW-0E
-member(x,y) | -member(x,cart(V,V)) | member(swap(x),inverse(y)).
% DO-4C
-member(x,y) | -member(x,cart(V,V)) | member(x,cart(D(y),V)).
% RA-4Y
-member(x,y) | -member(x,cart(V,V)) | member(x,cart(V,R(y))).
% DO-4A2
-member(x,y) | -member(x,cart(complement(D(y)),V)).
% IND-RUS6
-member(x,y) | -member(x,omega) | -member(y,x).
% IND-RUS7
-member(x,y) | -member(x,omega) | -subclass(y,x).
% DJ-MEM
-member(x,y) | -member(x,z) | -disjoint(y,z).
% AX-I-3
-member(x,y) | -member(x,z) | member(x,intersection(y,z)).
% ON-FUL-D
-member(x,y) | -member(y,OMEGA) | subclass(x,y).
% SG-RA-SS
-member(x,y) | -member(y,R(SINGLETON)) | equal(singleton(x),y).
% REG-5
-member(x,y) | -member(y,REGULAR) | member(x,REGULAR).
% LT-DF-3
-member(x,y) | -member(y,V) | -subclass(cart(singleton(x),y),z) | member(pair(y,x),LEAST(z)).
% K-SS3
-member(x,y) | -member(y,V) | member(pair(intersection(y,complement(singleton(x))),y),K).
% PS-SS-C
-member(x,y) | -member(y,V) | member(pair(intersection(y,complement(singleton(x))),y),PS).
% E-V2
-member(x,y) | -member(y,V) | member(pair(x,y),E).
% IVR-BC1
-member(x,y) | -member(y,invar(BIGCUP)) | member(U(x),y).
% OM-SC-2B
-member(x,y) | -member(y,omega) | equal(x,0) | member(U(x),U(y)).
% ON-OM-2
-member(x,y) | -member(y,omega) | member(succ(x),succ(y)).
% OM-PC-6
-member(x,y) | -member(y,omega) | member(x,omega).
% OM-FUL-4
-member(x,y) | -member(y,omega) | subclass(succ(x),y).
% OM-FUL-3
-member(x,y) | -member(y,omega) | subclass(x,y).
% SBV-PS1
-member(x,y) | -member(y,subvar(PS)) | member(intersection(y,P(x)),subvar(PS)).
% DESC-10
-member(x,y) | -member(y,x) | member(pairset(x,y),DESCENDING).
% OM-FUL-5
-member(x,y) | -member(y,z) | -member(z,omega) | member(x,z).
% SC-2
-member(x,y) | -member(y,z) | member(x,U(z)).
% IM-C-1
-member(x,y) | -member(z,complement(image(u,y))) | -member(pair(x,z),u).
% IM-C-2
-member(x,y) | -member(z,complement(image(u,y))) | member(pair(x,z),complement(u)).
% FIN-PP4
-member(x,y) | -member(z,intersection(P(P(y)),subvar(PS))) | -member(intersection(y,complement(singleton(x))),FINITE) | member(x,A(z)).
% CUP-ADJ'
-member(x,y) | -member(z,u) | member(union(x,singleton(z)),y) | -subclass(image(CUP,cart(y,image(SINGLETON,u))),y).
% ID-9C
-member(x,y) | -member(z,y) | -subclass(cart(y,y),Id) | equal(x,z).
% PC-6LEM2
-member(x,y) | -member(z,y) | member(pairset(x,z),P(y)).
% UP-7
-member(x,y) | -member(z,y) | subclass(pairset(x,z),y).
% CUP-ADJ
-member(x,y) | -subclass(image(CUP,cart(y,R(SINGLETON))),y) | member(union(x,singleton(z)),y).
% H-MEM-2
-member(x,y) | -subclass(tc(x),y) | member(x,H(y)).
% SUC-SU
-member(x,y) | -subclass(x,y) | subclass(succ(x),y).
% ON-WO-DJ
-member(x,y) | -subclass(y,OMEGA) | -disjoint(x,y) | equal(x,A(y)).
% SBV-PS1'
-member(x,y) | -subclass(y,image(PS,y)) | member(intersection(y,P(x)),subvar(PS)).
% SS-12-A
-member(x,y) | -subclass(y,singleton(x)) | equal(singleton(x),y).
% CUP-SUB'
-member(x,y) | -subclass(y,u) | member(y,z) | -member(intersection(y,complement(singleton(x))),z) | -subclass(image(CUP,cart(z,image(SINGLETON,u))),z).
% DF-SU-1
-member(x,y) | -subclass(y,z) | member(x,z).
% RP-SR-IN
-member(x,y) | -subclass(z,x) | member(z,image(inverse(S),y)).
% AP10-IDX
-member(x,y) | equal(apply(id(y),x),x).
% RK-9-MEM
-member(x,y) | equal(rank(x),V) | member(rank(x),rank(y)).
% ADJ-IN0
-member(x,y) | member(0,image(inverse(ADJOIN(x)),y)).
% RP-A-PC
-member(x,y) | member(A(y),P(x)).
% HC-IM
-member(x,y) | member(H(x),image(HC,y)).
% PC-PC-SC
-member(x,y) | member(P(x),P(P(U(y)))).
% PC-SC-SC
-member(x,y) | member(U(x),P(U(U(y)))).
% BC-IM-1
-member(x,y) | member(U(x),image(BIGCUP,y)).
% CUT-2-IM
-member(x,y) | member(intersection(z,x),image(IMAGE(id(z)),y)).
% IDX-6
-member(x,y) | member(pair(x,x),id(y)).
% PC-6LEM1
-member(x,y) | member(singleton(x),P(y)).
% SG-3-IM
-member(x,y) | member(singleton(x),image(SINGLETON,y)).
% SUC-SUC
-member(x,y) | member(succ(x),image(SUCC,y)).
% U-7B
-member(x,y) | member(x,union(y,z)).
% U-7C
-member(x,y) | member(x,union(z,y)).
% A-1A
-member(x,y) | subclass(A(y),x).
% ID-10-A
-member(x,y) | subclass(cart(y,y),Id) | member(notsub(intersection(y,complement(singleton(x))),0),y).
% RK-8
-member(x,y) | subclass(rank(x),rank(y)).
% SS-11
-member(x,y) | subclass(singleton(x),y).
% TC-SU-3
-member(x,y) | subclass(tc(x),tc(y)).
% SC-7
-member(x,y) | subclass(x,U(y)).
% SW-0D'
-member(x,y)| -member(x,cart(V,V))|member(swap(x),inverse(y)).
% ACL-SU3
-subclass(Aclosure(x),x) | Aclosed(x).
% IDX-CO4D
-subclass(D(x),y) | equal(composite(x,id(y)),composite(Id,x)).
% IM-5B
-subclass(D(x),y) | equal(image(x,y),R(x)).
% VS-FU-U
-subclass(D(x),y) | equal(union(cart(complement(y),singleton(0)),composite(VERTSECT(x),id(y))),VERTSECT(x)).
% ID-E
-subclass(E,Id).
% ID-CO-SU
-subclass(Id,composite(x,y)) | -subclass(composite(z,x),composite(u,v)) | -subclass(composite(w,u),Id) | subclass(composite(w,z),composite(v,y)).
% BIJ-OO3
-subclass(P(x),BIJ) | ONEONE(x).
% FS-PC-2
-subclass(P(x),FUNS) | FUNCTION(x).
% REG3-SU
-subclass(P(x),REGULAR) | subclass(x,REGULAR).
% PC-0-SS1
-subclass(P(x),singleton(y)) | equal(x,0).
% PC-0-SS2
-subclass(P(x),singleton(y)) | equal(y,0).
% IND-PC
-subclass(P(x),x) | INDUCTIVE(P(x)).
% ON-PC-SU
-subclass(P(x),x) | subclass(OMEGA,x).
% TC-REG-1
-subclass(P(x),x) | subclass(REGULAR,x).
% FUL-REG2
-subclass(P(x),x) | subclass(intersection(REGULAR,U(FULL)),x).
% PC-SC-4
-subclass(P(x),y) | subclass(x,U(y)).
% POW-5B
-subclass(R(POWER),x) | equal(image(inverse(POWER),x),V).
% SG-PC-V
-subclass(R(SINGLETON),P(x)) | equal(x,V).
% SG-DO-A
-subclass(R(SINGLETON),x) | equal(U(intersection(x,R(SINGLETON))),V).
% DF-FF-2
-subclass(R(complement(composite(E,complement(x)))),FUNS) | FUNCTIONFAMILY(x).
% FU-IN-CO
-subclass(R(x),D(y)) | -subclass(composite(y,x),Id) | FUNCTION(inverse(x)).
% CO-BOY2
-subclass(R(x),D(y)) | equal(D(composite(y,x)),D(x)).
% ON-BA-VS
-subclass(R(x),OMEGA) | subclass(composite(BIGCAP,VERTSECT(x)),x).
% IDX-CO3C
-subclass(R(x),y) | equal(composite(id(y),x),composite(Id,x)).
% RUS-PCSU
-subclass(RUSSELL,x) | subclass(P(x),x).
% FUL-FUL
-subclass(U(FULL),FULL).
% REG2-SU2
-subclass(U(x),REGULAR) | subclass(x,REGULAR).
% RUS-SC-2
-subclass(U(x),RUSSELL) | subclass(x,RUSSELL).
% IDX-ZN
-subclass(U(x),x) | subclass(composite(inverse(E),id(x)),composite(id(x),inverse(E))).
% PC-SC-2
-subclass(U(x),y) | subclass(x,P(y)).
% UCL-SU3
-subclass(Uclosure(x),x) | Uclosed(x).
% SP-7-COR
-subclass(V,0).
% SP-VXV
-subclass(V,cart(V,V)).
% ID-V-CP
-subclass(V,image(x,singleton(first(notsub(cart(V,V),x))))) | subclass(cart(V,V),x).
% SP-V-SU
-subclass(V,x) | equal(x,V).
% E-CP-V
-subclass(cart(V,V),E).
% SV-V
-subclass(cart(V,V),Id).
% CP-11
-subclass(cart(u,v),cart(x,y)) | equal(u,0) | subclass(v,y).
% CP-12
-subclass(cart(u,v),cart(x,y)) | equal(v,0) | subclass(u,x).
% ID-9E'
-subclass(cart(x,x),Id) | equal(x,0) | equal(singleton(U(x)),x).
% ID-9E-Q1
-subclass(cart(x,x),Id) | equal(x,0) | equal(singleton(memb(x)),x).
% ID-9E
-subclass(cart(x,x),Id) | equal(x,0) | equal(singleton(notsub(x,0)),x).
% ID-9F
-subclass(cart(x,x),Id) | member(x,V).
% ID-9D
-subclass(cart(x,x),Id) | subclass(x,singleton(notsub(x,0))).
% CP-13A
-subclass(cart(x,x),cart(y,y)) | subclass(x,y).
% PN-1
-subclass(cart(x,x),union(Id,DISJOINT)) | FUNCTION(composite(id(x),E)).
% DEF-PN3
-subclass(cart(x,x),union(Id,DISJOINT)) | PARTITION(x) | member(0,x).
% ID-CP
-subclass(cart(x,y),Id) | equal(x,y) | equal(x,0) | equal(y,0).
% ID-9G
-subclass(cart(x,y),Id) | member(x,V) | member(y,V).
% IM-CP-0
-subclass(cart(x,y),z) | equal(x,0) | subclass(y,image(z,x)).
% IM-CP-3
-subclass(cart(x,y),z) | subclass(y,complement(image(complement(z),x))).
% SU-10
-subclass(complement(x),complement(y)) | subclass(y,x).
% SG-4H
-subclass(composite(E,x),composite(E,y)) | subclass(composite(Id,x),composite(Id,y)).
% E-CO6
-subclass(composite(E,x),composite(E,y)) | subclass(composite(z,x),composite(z,y)).
% E-CO4
-subclass(composite(E,x),composite(E,y)) | subclass(restrict(x,V,V),y).
% ID-CO-C
-subclass(composite(Id,x),y) | subclass(composite(Id,complement(y)),complement(x)).
% CO-TR-1
-subclass(composite(complement(x),inverse(y)),complement(z)) | subclass(composite(z,y),x).
% IDX-IM-4
-subclass(composite(id(x),y),composite(y,id(z))) | subclass(image(inverse(y),x),z).
% ZN-SU1
-subclass(composite(inverse(E),x),composite(x,inverse(E))) | subclass(composite(Id,x),ZN).
% ZN-RS2
-subclass(composite(inverse(E),x),composite(x,inverse(E))) | subclass(image(IMAGE(id(x)),image(CART,cart(FULL,FULL))),subcommutant(inverse(E))).
% CO-IN3
-subclass(composite(inverse(x),inverse(y)),inverse(z)) | subclass(composite(y,x),z).
% FU-IN
-subclass(composite(inverse(x),x),Id) | FUNCTION(inverse(x)).
% ZN-IN1
-subclass(composite(x,E),composite(E,x)) | subclass(inverse(x),ZN).
% UB-SU
-subclass(composite(x,E),y) | subclass(composite(Id,x),UB(y)).
% ZER-1
-subclass(composite(x,S),composite(S,x)) | equal(image(inverse(S),D(x)),D(x)).
% IDX-IM-2
-subclass(composite(x,id(y)),composite(id(z),x)) | subclass(image(x,y),z).
% SG-4F
-subclass(composite(x,inverse(E)),composite(y,inverse(E))) | subclass(composite(Id,x),composite(Id,y)).
% SV-6B
-subclass(composite(x,inverse(x)),Id) | -subclass(composite(y,inverse(y)),Id) | subclass(composite(x,composite(y,composite(inverse(y),inverse(x)))),Id).
% DF-FU-3
-subclass(composite(x,inverse(x)),Id) | -subclass(x,cart(V,V)) | FUNCTION(x).
% FU-DF-4
-subclass(composite(x,inverse(x)),Id) | FUNCTION(composite(Id,x)).
% SV-DJ-1
-subclass(composite(x,inverse(x)),Id) | disjoint(x,composite(Di,x)).
% SV-C-CO
-subclass(composite(x,inverse(x)),Id) | subclass(composite(complement(y),x),complement(composite(y,x))).
% SV-6A
-subclass(composite(x,inverse(x)),Id) | subclass(composite(composite(y,x),inverse(x)),y).
% SV-4B
-subclass(composite(x,inverse(x)),Id) | subclass(composite(intersection(x,y),inverse(intersection(x,y))),Id).
% DI-DJ2
-subclass(composite(x,y),Di) | disjoint(x,inverse(y)).
% CO-DO5A
-subclass(composite(x,y),composite(y,x)) | subclass(image(inverse(y),D(x)),D(x)).
% DEF-ST2
-subclass(composite(x,y),composite(y,x)) | subcommute(x,y).
% IVR-IMG1
-subclass(composite(x,y),composite(y,z)) | subclass(image(IMAGE(y),invar(z)),invar(x)).
% SBV-IMG6
-subclass(composite(x,y),composite(z,x)) | subclass(image(IMAGE(x),subvar(y)),subvar(z)).
% CO-TR-2
-subclass(composite(x,y),z) | subclass(composite(complement(z),inverse(y)),complement(x)).
% IDX-FP-4
-subclass(id(x),y) | subclass(x,fix(y)).
% FUL-BC-3
-subclass(image(BIGCUP,P(x)),P(x)) | full(x).
% FUL-BC-5
-subclass(