----- SUMMARY FOR THEOREM AUG02A IN DIRECTORY D:\temp -----

% AUG02.IN                 1999 August 2
% Theorem needed to simplify some GOEDEL program examples.

formula_list(sos).
% negation of Lemma AUG02
-(all x y (subclass(U(R(x)),y) ->
           subclass(fix(x),fix(composite(x,IMAGE(id(y))))))).
end_of_list.


----- Otter 3.0.4, August 1995 -----
The job was started by ??? on ???, Mon Aug 02 13:43:08 1999

Length of proof is 11. Level of proof is 5.

---------------- 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).
82 [] -subclass(x,y) | -subclass(y,z) | subclass(x,z).
142 [] -subclass(x,y) | equal(intersection(x,y),x).
293 [] -member(u,x) | -member(v,y) | member(pair(u,v),cart(V,V)).
585 [] -member(x,y) | subclass(x,U(y)).
746 [] -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)).
1153 [] -member(x,V) | -member(pair(x,x),y) | member(x,fix(y)).
1154 [] -member(x,fix(y)) | member(pair(x,x),y).
1156 [] subclass(fix(x),R(x)).
2227 [] -member(x,V) | member(pair(x,intersection(x,y)),
          IMAGE(id(y))).
2816 [] subclass(U(R($c2)),$c1).
2817 [] -subclass(fix($c2),fix(composite($c2,IMAGE(id($c1))))).
3729 [] equal(notsub(fix(x),fix(composite(x,IMAGE(id(y))))),n$(x,y)).
3738 [ur,2817,3,demod,3729] 
          -member(n$($c2,$c1),fix(composite($c2,IMAGE(id($c1))))).
3739 [ur,2817,2,demod,3729] member(n$($c2,$c1),fix($c2)).
3757 [ur,3739,1154] member(pair(n$($c2,$c1),n$($c2,$c1)),$c2).
3760 [ur,3739,293,3739] 
          member(pair(n$($c2,$c1),n$($c2,$c1)),cart(V,V)).
3761 [ur,3739,1,1156] member(n$($c2,$c1),R($c2)).
3762 [ur,3739,1,4] member(n$($c2,$c1),V).
3787 [ur,3761,585] subclass(n$($c2,$c1),U(R($c2))).
3791 [ur,3762,1153,3738] 
          -member(pair(n$($c2,$c1),n$($c2,$c1)),
          composite($c2,IMAGE(id($c1)))).
3827 [ur,3787,82,2816] subclass(n$($c2,$c1),$c1).
3837 [ur,3791,746,3760,3757,3760] 
          -member(pair(n$($c2,$c1),n$($c2,$c1)),IMAGE(id($c1))).
3859 [ur,3827,142] equal(intersection(n$($c2,$c1),$c1),n$($c2,$c1)).
3897 [para_from,3859.1.1,2227.2.1.2,unit_del,3762,3837] $F.

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

clauses generated   57688
Kbytes malloced      2714
user CPU time           9.40  seconds