----- Mace4 Aug-2005A, 16 Aug 2005 ----- Built with library LADR July-2005, 16 Aug 2005. The process was started by mccune on theorem.mcs.anl.gov, Tue Aug 30 16:30:25 2005 The command was "mace4 -N -1 -t 15 -f LT CD-join H1". The process ID is 6543. % Reading from file LT clauses(sos). x v y = y v x. (x v y) v z = x v (y v z). x ^ y = y ^ x. (x ^ y) ^ z = x ^ (y ^ z). x ^ (x v y) = x. x v (x ^ y) = x. x v 0 = x. x ^ 1 = x. end_of_list. % Reading from file CD-join clauses(sos). A v B = A v C. (A ^ B) v (A ^ C) != A ^ (B v C). end_of_list. % Reading from file H1 clauses(sos). x ^ (y v (z ^ (x v u))) = x ^ (y v (z ^ (x v (z ^ u)))) # label(H1). end_of_list. % Finished reading the input. % From the command line: assign(iterate_up_to, -1). % From the command line: assign(max_seconds, 15). % The maximum domain element in the input is 1. === Starting model search for domain size 2. === === Starting model search for domain size 3. === === Starting model search for domain size 4. === === Starting model search for domain size 5. === === Starting model search for domain size 6. === === Starting model search for domain size 7. === -------- Model 1 at 0.03 seconds -------- A : 2 B : 3 C : 4 ^ : | 0 1 2 3 4 5 6 --+-------------- 0 | 0 0 0 0 0 0 0 1 | 0 1 2 3 4 5 6 2 | 0 2 2 0 5 5 0 3 | 0 3 0 3 6 0 6 4 | 0 4 5 6 4 5 6 5 | 0 5 5 0 5 5 0 6 | 0 6 0 6 6 0 6 v : | 0 1 2 3 4 5 6 --+-------------- 0 | 0 1 2 3 4 5 6 1 | 1 1 1 1 1 1 1 2 | 2 1 2 1 1 2 1 3 | 3 1 1 3 1 1 3 4 | 4 1 1 1 4 4 4 5 | 5 1 2 1 4 5 4 6 | 6 1 1 3 4 4 6 -------- end of model -------- User_CPU=0.03, System_CPU=0.01, Wall_clock=0. Exiting with 1 model. Process 6543 exit (max_models) Tue Aug 30 16:30:25 2005 The process finished Tue Aug 30 16:30:25 2005