problem-set/set.theory/naive/compl.desc created : 07/16/86 revised : 08/10/88 Natural Language Description : Theorem: The complement of the complement of a set is that set; i.e., EQ(comp(comp(xs)),xs). Versions : compl.ver1.in: uses paramodulation and UR resolution, with a standard p-formulation. created : from McCharen, Overbeek, & Wos [Aug. 1976]. verified for ITP : 7/17/86. translated for OTTER by : caw. verified for OTTER : no proof in 5037 kept clauses.