----- 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 8583. assign(iterate_up_to,10). set(verbose). clauses(theory). a(a(L,x),y) = a(x,a(y,y)). a(a(a(Q,x),y),z) = a(y,a(x,z)). end_of_list. formulas(theory). - (exists F all x (a(F,x) = a(x,a(F,x)))). 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: L : - Q : - $f1 : 0 1 ------- - - a : | 0 1 --+---- 0 | - - 1 | - - --------- statistics for domain size 2 --------- Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). Ground clauses: seen=14, kept=14. Selections=20, assignments=39, propagations=29, current_models=0. Rewrite_terms=374, rewrite_bools=32, indexes=111. Rules_from_neg_clauses=14, cross_offs=14. === Starting model search for domain size 3. === Initial partial model: L : - Q : - $f1 : 0 1 2 --------- - - - a : | 0 1 2 --+------ 0 | - - - 1 | - - - 2 | - - - --------- statistics for domain size 3 --------- Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). Ground clauses: seen=39, kept=39. Selections=137, assignments=406, propagations=613, current_models=0. Rewrite_terms=9606, rewrite_bools=1080, indexes=3055. Rules_from_neg_clauses=75, cross_offs=303. === Starting model search for domain size 4. === Initial partial model: L : - Q : - $f1 : 0 1 2 3 ----------- - - - - a : | 0 1 2 3 --+-------- 0 | - - - - 1 | - - - - 2 | - - - - 3 | - - - - -------- Model 1 at 0.01 seconds -------- L : 0 Q : 0 $f1 : 0 1 2 3 ----------- 1 0 0 1 a : | 0 1 2 3 --+-------- 0 | 0 1 1 0 1 | 3 2 2 3 2 | 3 2 2 3 3 | 0 1 1 0 -------- end of model -------- --------- statistics for domain size 4 --------- Current CPU time: 0.01 seconds (total CPU time: 0.01 seconds). Ground clauses: seen=84, kept=84. Selections=19, assignments=51, propagations=75, current_models=1. Rewrite_terms=1841, rewrite_bools=171, indexes=542. Rules_from_neg_clauses=5, cross_offs=28. ------------- memory usage (for entire run) ------------------- Total malloced: 20 megabytes type (bytes each) gets frees in use bytes chunk ( 104) 76 76 0 0.0 K string_buf ( 8) 74 74 0 0.0 K token ( 20) 137 137 0 0.0 K pterm ( 16) 80 80 0 0.0 K ilist ( 8) 10 10 0 0.0 K plist ( 8) 400 274 126 1.0 K mlist ( 12) 15 15 0 0.0 K term ( 16) 1350 1320 30 0.5 K term arg arrays: 0.2 K literal ( 12) 4 1 3 0.0 K clause ( 32) 4 1 3 0.1 K clist_pos ( 20) 2 2 0 0.0 K clist ( 16) 1 1 0 0.0 K mclause ( 20) 137 137 0 0.0 K (2.0 K high) mstate ( 16) 499 499 0 0.0 K jnode ( 28) 3461 3461 0 0.0 K estack (3208) 498 498 0 0.0 K (avail=0, 0.0 K) Memory report, 1 @ 20 = 20 megs (0.02 megs used). List 1, length 7, 0.0 K List 2, length 84, 0.7 K List 3, length 6, 0.1 K List 4, length 84, 1.3 K List 5, length 27, 0.5 K List 6, length 596, 14.0 K List 7, length 28, 0.8 K List 26, length 16, 1.6 K User_CPU=0.01, System_CPU=0.00, Wall_clock=0. Exiting with 1 model. Process 8583 exit (max_models) Tue Jul 5 21:30:20 2005 The process finished Tue Jul 5 21:30:20 2005