problem-set/algebra/boolean/prob1.desc created: 07/07/86 revised: 08/18/89 Natural Language Description: The files beginning with prob1 concern the proof of the statement that addition is associative. Versions: prob1.ver1: This version is from 'Problems and Experiments from and with Automated Theorem-Proving Programs' - McCharen, Overbeek and Wos. Hyper resolution is the inference rule and demodulators are not included. created by: E. Lusk verified for ITP: not yet translated for OTTER: TLH verified for OTTER: not yet prob1.ver2: This version is in equality representation. Paramodulation is the inference rule and demodulators are included. created: 08/04/89 verified for ITP: not yet translated for OTTER: tlh verified for OTTER: 08/04/89