----- 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:20 2005 The command was "../bin/mace4". The process ID is 8585. assign(iterate_up_to,12). set(verbose). formulas(theory). (all x all y all z ((x * y) * z = x * (y * z))). (exists e ((all x (e * x = x)) & (all x exists y (y * x = e)))). (exists a exists b (a * b != b * a)). end_of_list. % Finished reading the input. % There are no domain elements in the input. === Starting model search for domain size 2. === Initial partial model: $c1 : - $c2 : - $c3 : - $f1 : 0 1 ------- - - * : | 0 1 --+---- 0 | - - 1 | - - --------- statistics for domain size 2 --------- Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds). Ground clauses: seen=13, kept=13. Selections=4, assignments=7, propagations=6, current_models=0. Rewrite_terms=62, rewrite_bools=16, indexes=8. Rules_from_neg_clauses=2, cross_offs=2. === Starting model search for domain size 3. === Initial partial model: $c1 : - $c2 : - $c3 : - $f1 : 0 1 2 --------- - - - * : | 0 1 2 --+------ 0 | - - - 1 | - - - 2 | - - - --------- statistics for domain size 3 --------- Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds). Ground clauses: seen=34, kept=34. Selections=7, assignments=17, propagations=32, current_models=0. Rewrite_terms=310, rewrite_bools=73, indexes=48. Rules_from_neg_clauses=8, cross_offs=24. === Starting model search for domain size 4. === Initial partial model: $c1 : - $c2 : - $c3 : - $f1 : 0 1 2 3 ----------- - - - - * : | 0 1 2 3 --+-------- 0 | - - - - 1 | - - - - 2 | - - - - 3 | - - - - --------- statistics for domain size 4 --------- Current CPU time: 0.01 seconds (total CPU time: 0.02 seconds). Ground clauses: seen=73, kept=73. Selections=14, assignments=45, propagations=111, current_models=0. Rewrite_terms=1151, rewrite_bools=243, indexes=212. Rules_from_neg_clauses=20, cross_offs=101. === Starting model search for domain size 5. === Initial partial model: $c1 : - $c2 : - $c3 : - $f1 : 0 1 2 3 4 ------------- - - - - - * : | 0 1 2 3 4 --+---------- 0 | - - - - - 1 | - - - - - 2 | - - - - - 3 | - - - - - 4 | - - - - - --------- statistics for domain size 5 --------- Current CPU time: 0.00 seconds (total CPU time: 0.02 seconds). Ground clauses: seen=136, kept=136. Selections=24, assignments=91, propagations=220, current_models=0. Rewrite_terms=2532, rewrite_bools=493, indexes=630. Rules_from_neg_clauses=34, cross_offs=249. === Starting model search for domain size 6. === Initial partial model: $c1 : - $c2 : - $c3 : - $f1 : 0 1 2 3 4 5 --------------- - - - - - - * : | 0 1 2 3 4 5 --+------------ 0 | - - - - - - 1 | - - - - - - 2 | - - - - - - 3 | - - - - - - 4 | - - - - - - 5 | - - - - - - -------- Model 1 at 0.02 seconds -------- $c1 : 0 $c2 : 1 $c3 : 2 $f1 : 0 1 2 3 4 5 --------------- 0 1 2 4 3 5 * : | 0 1 2 3 4 5 --+------------ 0 | 0 1 2 3 4 5 1 | 1 0 3 2 5 4 2 | 2 4 0 5 1 3 3 | 3 5 1 4 0 2 4 | 4 2 5 0 3 1 5 | 5 3 4 1 2 0 -------- end of model -------- --------- statistics for domain size 6 --------- Current CPU time: 0.00 seconds (total CPU time: 0.02 seconds). Ground clauses: seen=229, kept=229. Selections=14, assignments=44, propagations=95, current_models=1. Rewrite_terms=1596, rewrite_bools=347, indexes=379. Rules_from_neg_clauses=9, cross_offs=141. ------------- memory usage (for entire run) ------------------- Total malloced: 20 megabytes type (bytes each) gets frees in use bytes chunk ( 104) 81 81 0 0.0 K string_buf ( 8) 77 77 0 0.0 K token ( 20) 149 149 0 0.0 K pterm ( 16) 68 68 0 0.0 K ilist ( 8) 14 14 0 0.0 K plist ( 8) 1103 970 133 1.0 K mlist ( 12) 30 30 0 0.0 K term ( 16) 3117 3065 52 0.8 K term arg arrays: 0.2 K literal ( 12) 4 0 4 0.0 K clause ( 32) 4 0 4 0.1 K clist_pos ( 20) 0 0 0 0.0 K clist ( 16) 0 0 0 0.0 K mclause ( 20) 485 485 0 0.0 K (5.4 K high) mstate ( 16) 209 209 0 0.0 K jnode ( 28) 2479 2479 0 0.0 K estack (3208) 214 214 0 0.0 K (avail=0, 0.0 K) Memory report, 1 @ 20 = 20 megs (0.04 megs used). List 1, length 4, 0.0 K List 2, length 229, 1.8 K List 3, length 1, 0.0 K List 4, length 23, 0.4 K List 5, length 30, 0.6 K List 6, length 1408, 33.0 K List 7, length 91, 2.5 K List 26, length 22, 2.2 K User_CPU=0.02, System_CPU=0.00, Wall_clock=0. Exiting with 1 model. Process 8585 exit (max_models) Tue Jul 5 21:30:20 2005 The process finished Tue Jul 5 21:30:20 2005