----- MACE4 2005-A, 30 June 2005 ----- Built with library LADR July-2005, 30 June 2005. The process was started by mccune on theorem.mcs.anl.gov, Tue Jul 5 21:30:21 2005 The command was "../bin/mace4". The process ID is 8588. assign(iterate_up_to,8). set(verbose). clauses(theory). 0 + x = x. x + 0 = x. - x + x = 0. x + - x = 0. (x + y) + z = x + (y + z). x + y = y + x. (x * y) * z = x * (y * z). x * (y + z) = (x * y) + (x * z). (x + y) * z = (x * z) + (y * z). - - x = x. - 0 = 0. 0 * x = 0. x * 0 = 0. 1 * x = x. x * 1 = x. a * b != b * a. end_of_list. % Finished reading the input. % The maximum domain element in the input is 1. === Starting model search for domain size 2. === Initial partial model: a : - b : - - : 0 1 ------- 0 1 + : | 0 1 --+---- 0 | 0 1 1 | 1 0 * : | 0 1 --+---- 0 | 0 0 1 | 0 1 --------- statistics for domain size 2 --------- Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). Ground clauses: seen=56, kept=34. Selections=3, assignments=6, propagations=10, current_models=0. Rewrite_terms=127, rewrite_bools=37, indexes=4. Rules_from_neg_clauses=2, cross_offs=2. === Starting model search for domain size 3. === Initial partial model: a : - b : - - : 0 1 2 --------- 0 - - + : | 0 1 2 --+------ 0 | 0 1 2 1 | 1 - - 2 | 2 - - * : | 0 1 2 --+------ 0 | 0 0 0 1 | 0 1 2 2 | 0 2 - --------- statistics for domain size 3 --------- Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). Ground clauses: seen=146, kept=126. Selections=5, assignments=15, propagations=25, current_models=0. Rewrite_terms=568, rewrite_bools=157, indexes=35. Rules_from_neg_clauses=4, cross_offs=11. === Starting model search for domain size 4. === Initial partial model: a : - b : - - : 0 1 2 3 ----------- 0 - - - + : | 0 1 2 3 --+-------- 0 | 0 1 2 3 1 | 1 - - - 2 | 2 - - - 3 | 3 - - - * : | 0 1 2 3 --+-------- 0 | 0 0 0 0 1 | 0 1 2 3 2 | 0 2 - - 3 | 0 3 - - --------- statistics for domain size 4 --------- Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). Ground clauses: seen=310, kept=285. Selections=12, assignments=44, propagations=54, current_models=0. Rewrite_terms=1781, rewrite_bools=469, indexes=103. Rules_from_neg_clauses=10, cross_offs=43. === Starting model search for domain size 5. === Initial partial model: a : - b : - - : 0 1 2 3 4 ------------- 0 - - - - + : | 0 1 2 3 4 --+---------- 0 | 0 1 2 3 4 1 | 1 - - - - 2 | 2 - - - - 3 | 3 - - - - 4 | 4 - - - - * : | 0 1 2 3 4 --+---------- 0 | 0 0 0 0 0 1 | 0 1 2 3 4 2 | 0 2 - - - 3 | 0 3 - - - 4 | 0 4 - - - --------- statistics for domain size 5 --------- Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). Ground clauses: seen=572, kept=542. Selections=19, assignments=81, propagations=147, current_models=0. Rewrite_terms=3588, rewrite_bools=850, indexes=324. Rules_from_neg_clauses=39, cross_offs=157. === Starting model search for domain size 6. === Initial partial model: a : - b : - - : 0 1 2 3 4 5 --------------- 0 - - - - - + : | 0 1 2 3 4 5 --+------------ 0 | 0 1 2 3 4 5 1 | 1 - - - - - 2 | 2 - - - - - 3 | 3 - - - - - 4 | 4 - - - - - 5 | 5 - - - - - * : | 0 1 2 3 4 5 --+------------ 0 | 0 0 0 0 0 0 1 | 0 1 2 3 4 5 2 | 0 2 - - - - 3 | 0 3 - - - - 4 | 0 4 - - - - 5 | 0 5 - - - - --------- statistics for domain size 6 --------- Current CPU time: 0.01 seconds (total CPU time: 0.01 seconds). Ground clauses: seen=956, kept=921. Selections=28, assignments=136, propagations=240, current_models=0. Rewrite_terms=6635, rewrite_bools=1516, indexes=584. Rules_from_neg_clauses=96, cross_offs=451. === Starting model search for domain size 7. === Initial partial model: a : - b : - - : 0 1 2 3 4 5 6 ----------------- 0 - - - - - - + : | 0 1 2 3 4 5 6 --+-------------- 0 | 0 1 2 3 4 5 6 1 | 1 - - - - - - 2 | 2 - - - - - - 3 | 3 - - - - - - 4 | 4 - - - - - - 5 | 5 - - - - - - 6 | 6 - - - - - - * : | 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 - - - - - 3 | 0 3 - - - - - 4 | 0 4 - - - - - 5 | 0 5 - - - - - 6 | 0 6 - - - - - --------- statistics for domain size 7 --------- Current CPU time: 0.01 seconds (total CPU time: 0.02 seconds). Ground clauses: seen=1486, kept=1446. Selections=48, assignments=266, propagations=553, current_models=0. Rewrite_terms=15529, rewrite_bools=3254, indexes=1918. Rules_from_neg_clauses=149, cross_offs=1059. === Starting model search for domain size 8. === Initial partial model: a : - b : - - : 0 1 2 3 4 5 6 7 ------------------- 0 - - - - - - - + : | 0 1 2 3 4 5 6 7 --+---------------- 0 | 0 1 2 3 4 5 6 7 1 | 1 - - - - - - - 2 | 2 - - - - - - - 3 | 3 - - - - - - - 4 | 4 - - - - - - - 5 | 5 - - - - - - - 6 | 6 - - - - - - - 7 | 7 - - - - - - - * : | 0 1 2 3 4 5 6 7 --+---------------- 0 | 0 0 0 0 0 0 0 0 1 | 0 1 2 3 4 5 6 7 2 | 0 2 - - - - - - 3 | 0 3 - - - - - - 4 | 0 4 - - - - - - 5 | 0 5 - - - - - - 6 | 0 6 - - - - - - 7 | 0 7 - - - - - - -------- Model 1 at 0.03 seconds -------- a : 2 b : 4 - : 0 1 2 3 4 5 6 7 ------------------- 0 1 2 3 4 5 6 7 + : | 0 1 2 3 4 5 6 7 --+---------------- 0 | 0 1 2 3 4 5 6 7 1 | 1 0 3 2 5 4 7 6 2 | 2 3 0 1 6 7 4 5 3 | 3 2 1 0 7 6 5 4 4 | 4 5 6 7 0 1 2 3 5 | 5 4 7 6 1 0 3 2 6 | 6 7 4 5 2 3 0 1 7 | 7 6 5 4 3 2 1 0 * : | 0 1 2 3 4 5 6 7 --+---------------- 0 | 0 0 0 0 0 0 0 0 1 | 0 1 2 3 4 5 6 7 2 | 0 2 0 2 0 2 0 2 3 | 0 3 2 1 4 7 6 5 4 | 0 4 2 6 4 0 6 2 5 | 0 5 0 5 0 5 0 5 6 | 0 6 2 4 4 2 6 0 7 | 0 7 0 7 0 7 0 7 -------- end of model -------- --------- statistics for domain size 8 --------- Current CPU time: 0.01 seconds (total CPU time: 0.03 seconds). Ground clauses: seen=2186, kept=2141. Selections=15, assignments=63, propagations=238, current_models=1. Rewrite_terms=11758, rewrite_bools=2551, indexes=1472. Rules_from_neg_clauses=20, cross_offs=561. ------------- memory usage (for entire run) ------------------- Total malloced: 20 megabytes type (bytes each) gets frees in use bytes chunk ( 104) 175 175 0 0.0 K string_buf ( 8) 173 173 0 0.0 K token ( 20) 196 196 0 0.0 K pterm ( 16) 135 135 0 0.0 K ilist ( 8) 16 16 0 0.0 K plist ( 8) 11116 10990 126 1.0 K mlist ( 12) 16 16 0 0.0 K term ( 16) 31483 31416 67 1.0 K term arg arrays: 0.4 K literal ( 12) 17 1 16 0.2 K clause ( 32) 17 1 16 0.5 K clist_pos ( 20) 16 16 0 0.0 K clist ( 16) 1 1 0 0.0 K mclause ( 20) 5495 5495 0 0.0 K (50.2 K high) mstate ( 16) 618 618 0 0.0 K jnode ( 28) 11143 11143 0 0.0 K estack (3208) 751 751 0 0.0 K (avail=0, 0.0 K) Memory report, 1 @ 20 = 20 megs (0.33 megs used). List 2, length 2141, 16.7 K List 3, length 15, 0.2 K List 4, length 15, 0.2 K List 5, length 38, 0.7 K List 6, length 13324, 312.3 K List 7, length 202, 5.5 K List 8, length 1, 0.0 K List 26, length 15, 1.5 K User_CPU=0.03, System_CPU=0.00, Wall_clock=0. Exiting with 1 model. Process 8588 exit (max_models) Tue Jul 5 21:30:21 2005 The process finished Tue Jul 5 21:30:21 2005