-(skc0=skc1).
-skP0(X) | X=oskc0.
-(X=oskc1) | skP1(X).
-skA0 | skP0(oskc0).
X=skc1 | X=skc0.
-skP1(X) | skA0 | X=oskc1.
oskf0(X)=X | skP0(oskf0(X)).
oskf1(X)=X | skP1(oskf1(X)).
-skP1(X) | -f(X,Y) | Y=skf1(X).
-skP1(X) | f(X,skf1(X)).
-(oskf0(X)=X) | -skP0(oskf0(X)) | skA0.
-skP0(X) | -f(Y,X) | Y=skf3(X).
-skP0(X) | f(skf3(X),X).
-skA0 | -(oskf1(X)=X) | -skP1(oskf1(X)).
skP1(X) | skf0(Y,X)=Y | f(X,skf0(Y,X)).
-(skf0(X,Y)=X) | -f(Y,skf0(X,Y)) | skP1(Y).
skP0(X) | skf2(Y,X)=Y | f(skf2(Y,X),X).
-(skf2(X,Y)=X) | -f(skf2(X,Y),Y) | skP0(Y).