----- 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 8586. assign(iterate_up_to,10). set(verbose). formulas(theory). (all x exists y (x < y)). (all x all y (x < y -> - (y < x))). (all x all y (x < y -> (exists z (x < z & z < y)))). end_of_list. % Finished reading the input. % There are no domain elements in the input. === Starting model search for domain size 2. === NOTE: unsatisfiability detected on input. Initial partial model: $f1 : 0 1 ------- 1 1 $f2 : | 0 1 --+---- 0 | - - 1 | - - < : | 0 1 --+---- 0 | 0 1 1 | 0 1 --------- statistics for domain size 2 --------- Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds). Ground clauses: seen=6, kept=4. Selections=0, assignments=0, propagations=6, current_models=0. Rewrite_terms=2, rewrite_bools=4, indexes=2. Rules_from_neg_clauses=2, cross_offs=2. === Starting model search for domain size 3. === Initial partial model: $f1 : 0 1 2 --------- - - - $f2 : | 0 1 2 --+------ 0 | - - - 1 | - - - 2 | - - - < : | 0 1 2 --+------ 0 | 0 - - 1 | - 0 - 2 | - - 0 --------- statistics for domain size 3 --------- Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds). Ground clauses: seen=30, kept=24. Selections=1, assignments=2, propagations=12, current_models=0. Rewrite_terms=5, rewrite_bools=32, indexes=3. Rules_from_neg_clauses=3, cross_offs=9. === Starting model search for domain size 4. === Initial partial model: $f1 : 0 1 2 3 ----------- - - - - $f2 : | 0 1 2 3 --+-------- 0 | - - - - 1 | - - - - 2 | - - - - 3 | - - - - < : | 0 1 2 3 --+-------- 0 | 0 - - - 1 | - 0 - - 2 | - - 0 - 3 | - - - 0 --------- statistics for domain size 4 --------- Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds). Ground clauses: seen=52, kept=44. Selections=2, assignments=5, propagations=22, current_models=0. Rewrite_terms=14, rewrite_bools=66, indexes=6. Rules_from_neg_clauses=6, cross_offs=23. === Starting model search for domain size 5. === Initial partial model: $f1 : 0 1 2 3 4 ------------- - - - - - $f2 : | 0 1 2 3 4 --+---------- 0 | - - - - - 1 | - - - - - 2 | - - - - - 3 | - - - - - 4 | - - - - - < : | 0 1 2 3 4 --+---------- 0 | 0 - - - - 1 | - 0 - - - 2 | - - 0 - - 3 | - - - 0 - 4 | - - - - 0 --------- statistics for domain size 5 --------- Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds). Ground clauses: seen=80, kept=70. Selections=3, assignments=9, propagations=19, current_models=0. Rewrite_terms=15, rewrite_bools=62, indexes=7. Rules_from_neg_clauses=2, cross_offs=24. === Starting model search for domain size 6. === Initial partial model: $f1 : 0 1 2 3 4 5 --------------- - - - - - - $f2 : | 0 1 2 3 4 5 --+------------ 0 | - - - - - - 1 | - - - - - - 2 | - - - - - - 3 | - - - - - - 4 | - - - - - - 5 | - - - - - - < : | 0 1 2 3 4 5 --+------------ 0 | 0 - - - - - 1 | - 0 - - - - 2 | - - 0 - - - 3 | - - - 0 - - 4 | - - - - 0 - 5 | - - - - - 0 --------- statistics for domain size 6 --------- Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds). Ground clauses: seen=114, kept=102. Selections=4, assignments=14, propagations=29, current_models=0. Rewrite_terms=26, rewrite_bools=96, indexes=12. Rules_from_neg_clauses=3, cross_offs=45. === Starting model search for domain size 7. === Initial partial model: $f1 : 0 1 2 3 4 5 6 ----------------- - - - - - - - $f2 : | 0 1 2 3 4 5 6 --+-------------- 0 | - - - - - - - 1 | - - - - - - - 2 | - - - - - - - 3 | - - - - - - - 4 | - - - - - - - 5 | - - - - - - - 6 | - - - - - - - < : | 0 1 2 3 4 5 6 --+-------------- 0 | 0 - - - - - - 1 | - 0 - - - - - 2 | - - 0 - - - - 3 | - - - 0 - - - 4 | - - - - 0 - - 5 | - - - - - 0 - 6 | - - - - - - 0 -------- Model 1 at 0.01 seconds -------- $f1 : 0 1 2 3 4 5 6 ----------------- 1 2 3 1 0 0 0 $f2 : | 0 1 2 3 4 5 6 --+-------------- 0 | 0 3 1 2 0 0 0 1 | 0 0 4 0 6 0 2 2 | 0 0 0 6 0 3 5 3 | 0 5 0 0 1 4 0 4 | 5 0 0 0 0 2 0 5 | 6 0 0 0 0 0 1 6 | 4 0 0 0 3 0 0 < : | 0 1 2 3 4 5 6 --+-------------- 0 | 0 1 1 1 0 0 0 1 | 0 0 1 0 1 0 1 2 | 0 0 0 1 0 1 1 3 | 0 1 0 0 1 1 0 4 | 1 0 1 0 0 1 0 5 | 1 1 0 0 0 0 1 6 | 1 0 0 1 1 0 0 -------- end of model -------- --------- statistics for domain size 7 --------- Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds). Ground clauses: seen=154, kept=140. Selections=39, assignments=60, propagations=68, current_models=1. Rewrite_terms=119, rewrite_bools=250, indexes=23. Rules_from_neg_clauses=17, cross_offs=137. ------------- memory usage (for entire run) ------------------- Total malloced: 20 megabytes type (bytes each) gets frees in use bytes chunk ( 104) 68 68 0 0.0 K string_buf ( 8) 58 58 0 0.0 K token ( 20) 104 104 0 0.0 K pterm ( 16) 54 54 0 0.0 K ilist ( 8) 12 12 0 0.0 K plist ( 8) 1219 1098 121 0.9 K mlist ( 12) 14 14 0 0.0 K term ( 16) 2920 2887 33 0.5 K term arg arrays: 0.1 K literal ( 12) 7 0 7 0.1 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) 384 384 0 0.0 K (3.8 K high) mstate ( 16) 96 96 0 0.0 K jnode ( 28) 603 603 0 0.0 K estack (3208) 96 96 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 141, 1.1 K List 4, length 27, 0.4 K List 5, length 23, 0.4 K List 6, length 515, 12.1 K List 7, length 147, 4.0 K List 26, length 18, 1.8 K User_CPU=0.01, System_CPU=0.01, Wall_clock=0. Exiting with 1 model. Process 8586 exit (max_models) Tue Jul 5 21:30:20 2005 The process finished Tue Jul 5 21:30:20 2005