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

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

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


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

Length of proof is 16. Level of proof is 8.

---------------- 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).
5 [] -subclass(x,y) | -subclass(y,x) | equal(x,y).
82 [] -subclass(x,y) | -subclass(y,z) | subclass(x,z).
142 [] -subclass(x,y) | equal(intersection(x,y),x).
585 [] -member(x,y) | subclass(x,U(y)).
779 [] -member(pair(x,y),composite(z,u))
           | member(pair(x,com(z,u,x,y)),u).
781 [] -member(pair(x,y),composite(z,u))
           | member(pair(com(z,u,x,y),y),z).
1153 [] -member(x,V) | -member(pair(x,x),y) | member(x,fix(y)).
1154 [] -member(x,fix(y)) | member(pair(x,x),y).
1355 [] subclass(fix(composite(x,y)),intersection(R(x),D(y))).
2225 [] -member(pair(x,y),IMAGE(id(z))) | equal(intersection(x,z),y).
2816 [] -subclass(U(R(x)),y) | subclass(fix(x),
          fix(composite(x,IMAGE(id(y))))).
2817 [] subclass(U(R($c2)),$c1).
2818 [] -equal(fix(composite($c2,IMAGE(id($c1)))),fix($c2)).
2846 [] equal(intersection(x,V),x).
3588 [] equal(D(IMAGE(id(x))),V).
3730 [] equal(notsub(fix(composite(x,IMAGE(id(y)))),fix(x)),n$(x,y)).
3731 [] equal(com(x,IMAGE(id(y)),n$(x,y),n$(x,y)),m$(x,y)).
3732 [ur,2817,2816] subclass(fix($c2),fix(composite($c2,
          IMAGE(id($c1))))).
3741 [ur,3732,5,2818] 
          -subclass(fix(composite($c2,IMAGE(id($c1)))),fix($c2)).
3751 [ur,3741,3,demod,3730] -member(n$($c2,$c1),fix($c2)).
3752 [ur,3741,2,demod,3730] 
          member(n$($c2,$c1),fix(composite($c2,IMAGE(id($c1))))).
3759 [ur,3752,1154] member(pair(n$($c2,$c1),n$($c2,$c1)),
          composite($c2,IMAGE(id($c1)))).
3761 [ur,3752,1,1355,demod,3588,2846] member(n$($c2,$c1),R($c2)).
3762 [ur,3752,1,4] member(n$($c2,$c1),V).
3767 [ur,3759,781,demod,3731] 
          member(pair(m$($c2,$c1),n$($c2,$c1)),$c2).
3769 [ur,3759,779,demod,3731] 
          member(pair(n$($c2,$c1),m$($c2,$c1)),IMAGE(id($c1))).
3771 [ur,3761,585] subclass(n$($c2,$c1),U(R($c2))).
3774 [ur,3762,1153,3751] -member(pair(n$($c2,$c1),n$($c2,$c1)),$c2).
3777 [ur,3769,2225] equal(intersection(n$($c2,$c1),$c1),m$($c2,$c1)).
3784 [ur,3771,82,2817] subclass(n$($c2,$c1),$c1).
3788,3787 [para_into,3777.1.1,142.2.1,unit_del,3784] 
          equal(n$($c2,$c1),m$($c2,$c1)).
3797 [back_demod,3774,demod,3788,3788] 
          -member(pair(m$($c2,$c1),m$($c2,$c1)),$c2).
3802 [back_demod,3767,demod,3788] 
          member(pair(m$($c2,$c1),m$($c2,$c1)),$c2).
3803 [binary,3802.1,3797.1] $F.

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

clauses generated   47363
Kbytes malloced      2650
user CPU time           5.93  seconds