----- SUMMARY FOR THEOREM AC-FU-Q IN DIRECTORY Q:\choice -----

% AC-FU-Q.IN                 2000 June 6

formula_list(sos).
% negation of Theorem AC-FU-Q
-(AxCh -> (all x (FUNCTION(x) ->
           subclass(composite(IMAGE(x),id(P(D(x)))),composite(Q,inverse(S)))))).
end_of_list.


----- Otter 3.0.4, August 1995 -----
The job was started by ??? on ???, Tue Jun 06 13:55:17 2000

Length of proof is 20. Level of proof is 6.

---------------- PROOF ----------------

1 [] -member(x,y) | -subclass(y,z) | member(x,z).
2 [] member(notsub(x,y),x) | subclass(x,y).
3 [] -member(notsub(x,y),y) | subclass(x,y).
4 [] subclass(x,V).
15 [] -member(x,cart(y,z)) | equal(pair(first(x),second(x)),x).
20 [] -member(x,intersection(y,z)) | member(x,z).
280 [] -member(x,V) | member(first(x),V).
384 [] -member(x,y) | -member(x,cart(V,V)) | member(first(x),D(y)).
645 [] -member(x,P(y)) | subclass(x,y).
731 [] subclass(composite(x,y),cart(V,V)).
776 [] -subclass(R(x),D(y)) | equal(D(composite(y,x)),D(x)).
1162 [] subclass(composite(x,id(y)),x).
1220 [] -FUNCTION(x) | -subclass(y,x) | equal(composite(x,id(D(y))),
          y).
2368 [] -FUNCTION(x) | -member(y,V) | member(composite(x,id(y)),
          FUNS).
2405 [] -member(pair(x,y),IMAGE(z)) | equal(image(z,x),y).
2728 [] -AxCh | -member(x,FUNS) | member(pair(D(x),R(x)),
          composite(Q,inverse(S))).
2729 [] AxCh.
2730 [] FUNCTION($c1).
2731 [] -subclass(composite(IMAGE($c1),id(P(D($c1)))),
          composite(Q,inverse(S))).
2953 [] equal(R(composite(x,y)),image(x,R(y))).
3097 [] equal(D(id(x)),x).
3098 [] equal(R(id(x)),x).
3103 [] equal(D(composite(x,id(y))),intersection(D(x),y)).
3642 [] equal(notsub(composite(IMAGE(x),id(P(D(x)))),
          composite(Q,inverse(S))),n$(x)).
3643 [] equal(first(n$(x)),f$(x)).
3644 [] equal(second(n$(x)),s$(x)).
3645 [binary,2729.1,2728.1] 
          -member(x,FUNS) | member(pair(D(x),R(x)),
          composite(Q,inverse(S))).
3646 [binary,2730.1,2368.1] 
          -member(x,V) | member(composite($c1,id(x)),FUNS).
3658,3657 [ur,2730,1220,1162,demod,3103] 
          equal(composite($c1,id(intersection(D($c1),x))),
          composite($c1,id(x))).
3665 [binary,2731.1,3.2,demod,3642] 
          -member(n$($c1),composite(Q,inverse(S))).
3666 [binary,2731.1,2.2,demod,3642] 
          member(n$($c1),composite(IMAGE($c1),id(P(D($c1))))).
3750 [para_from,3657.1.2,776.2.1.1,demod,3098,3658,3103,3097] 
          -subclass(x,D($c1)) | equal(intersection(D($c1),x),x).
3786 [binary,3666.1,384.1,demod,3643,3103] 
          -member(n$($c1),cart(V,V)) | member(f$($c1),
          intersection(D(IMAGE($c1)),P(D($c1)))).
3789 [binary,3666.1,1.1] 
          -subclass(composite(IMAGE($c1),id(P(D($c1)))),x)
           | member(n$($c1),x).
3791 [ur,3666,1,1162] member(n$($c1),IMAGE($c1)).
3792 [ur,3666,1,731] member(n$($c1),cart(V,V)).
3924 [binary,3786.2,20.1,unit_del,3792] member(f$($c1),P(D($c1))).
3948 [binary,3789.2,280.1,demod,3643,unit_del,4] member(f$($c1),V).
3956,3955 [binary,3792.1,15.1,demod,3643,3644,flip.1] 
          equal(n$($c1),pair(f$($c1),s$($c1))).
3963 [back_demod,3791,demod,3956] 
          member(pair(f$($c1),s$($c1)),IMAGE($c1)).
3965 [back_demod,3665,demod,3956] 
          -member(pair(f$($c1),s$($c1)),composite(Q,inverse(S))).
4220 [binary,3924.1,645.1] subclass(f$($c1),D($c1)).
4283 [binary,3948.1,3646.1] member(composite($c1,id(f$($c1))),FUNS).
4307,4306 [binary,3963.1,2405.1] equal(image($c1,f$($c1)),s$($c1)).
4803,4802 [binary,4220.1,3750.1] 
          equal(intersection(D($c1),f$($c1)),f$($c1)).
5111 [binary,4283.1,3645.1,demod,3103,4803,2953,3098,4307] 
          member(pair(f$($c1),s$($c1)),composite(Q,inverse(S))).
5112 [binary,5111.1,3965.1] $F.

------------ end of proof -------------

clauses generated  413486
Kbytes malloced      3321
user CPU time          81.50  seconds