----- Mace4 July-2005D, 18 July 2005 ----- Built with library LADR July-2005, 18 July 2005. The process was started by mccune on theorem.mcs.anl.gov, Fri Aug 5 13:48:26 2005 The command was "mace4 -N100 -f H2-H3.in". The process ID is 29458. % Reading from file H2-H3.in clauses(sos). x v y = y v x. x ^ y = y ^ x. (x v y) v z = x v (y v z). (x ^ y) ^ z = x ^ (y ^ z). x ^ (x v y) = x. x v (x ^ y) = x. x v 0 = x. x ^ 1 = x. x ^ (y v (z ^ ((x ^ (y v z)) v (y ^ z)))) = x ^ (y v (x ^ z)) # label(H2). A ^ (B v (C ^ (B v (A ^ (C v (A ^ B)))))) != A ^ (B v (A ^ C)) # label(H3_denial). end_of_list. % Finished reading the input. % From the command line: assign(iterate_up_to, 100). % 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. === === Starting model search for domain size 8. === === Starting model search for domain size 9. === -------- Model 1 at 0.30 seconds -------- A : 2 B : 3 C : 6 ^ : | 0 1 2 3 4 5 6 7 8 --+------------------ 0 | 0 0 0 0 0 0 0 0 0 1 | 0 1 2 3 4 5 6 7 8 2 | 0 2 2 4 4 2 0 0 4 3 | 0 3 4 3 4 3 0 0 4 4 | 0 4 4 4 4 4 0 0 4 5 | 0 5 2 3 4 5 7 7 8 6 | 0 6 0 0 0 7 6 7 7 7 | 0 7 0 0 0 7 7 7 7 8 | 0 8 4 4 4 8 7 7 8 v : | 0 1 2 3 4 5 6 7 8 --+------------------ 0 | 0 1 2 3 4 5 6 7 8 1 | 1 1 1 1 1 1 1 1 1 2 | 2 1 2 5 2 5 1 5 5 3 | 3 1 5 3 3 5 1 5 5 4 | 4 1 2 3 4 5 1 8 8 5 | 5 1 5 5 5 5 1 5 5 6 | 6 1 1 1 1 1 6 6 1 7 | 7 1 5 5 8 5 6 7 8 8 | 8 1 5 5 8 5 1 8 8 -------- end of model -------- User_CPU=0.30, System_CPU=0.01, Wall_clock=0. Exiting with 1 model. Process 29458 exit (max_models) Fri Aug 5 13:48:26 2005 The process finished Fri Aug 5 13:48:26 2005