----- 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 8589. assign(iterate_up_to,10). set(verbose). clauses(theory). x ^ y = y ^ x. (x ^ y) ^ z = x ^ (y ^ z). x v y = y v x. (x v y) v z = x v (y v z). x v (x ^ y) = x. x ^ (x v y) = x. x ^ x = x. x v x = x. c(x) ^ x = 0. c(x) v x = 1. c(c(x)) = x. x ^ y = c(c(x) v c(y)). 1 v x = 1. 1 ^ x = x. 0 ^ x = 0. 0 v x = x. x v (c(x) ^ (x v y)) = x v y. A v (B ^ (A v C)) != (A v B) ^ (A v C). 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 : - C : - c : 0 1 ------- 1 0 ^ : | 0 1 --+---- 0 | 0 0 1 | 0 1 v : | 0 1 --+---- 0 | 0 1 1 | 1 1 --------- statistics for domain size 2 --------- Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds). Ground clauses: seen=59, kept=38. Selections=7, assignments=14, propagations=10, current_models=0. Rewrite_terms=180, rewrite_bools=45, indexes=14. Rules_from_neg_clauses=2, cross_offs=2. === Starting model search for domain size 3. === NOTE: unsatisfiability detected on input. Initial partial model: A : - B : - C : - c : 0 1 2 --------- - - - ^ : | 0 1 2 --+------ 0 | - - - 1 | - - - 2 | - - - v : | 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=117, kept=112. Selections=0, assignments=0, propagations=17, current_models=0. Rewrite_terms=216, rewrite_bools=62, indexes=44. Rules_from_neg_clauses=2, cross_offs=8. === Starting model search for domain size 4. === Initial partial model: A : - B : - C : - c : 0 1 2 3 ----------- 1 0 3 2 ^ : | 0 1 2 3 --+-------- 0 | 0 0 0 0 1 | 0 1 2 3 2 | 0 2 2 0 3 | 0 3 0 3 v : | 0 1 2 3 --+-------- 0 | 0 1 2 3 1 | 1 1 1 1 2 | 2 1 2 1 3 | 3 1 1 3 --------- statistics for domain size 4 --------- Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds). Ground clauses: seen=261, kept=228. Selections=14, assignments=49, propagations=36, current_models=0. Rewrite_terms=1041, rewrite_bools=263, indexes=109. Rules_from_neg_clauses=3, cross_offs=21. === Starting model search for domain size 5. === Initial partial model: A : - B : - C : - c : 0 1 2 3 4 ------------- 1 0 - - - ^ : | 0 1 2 3 4 --+---------- 0 | 0 0 0 0 0 1 | 0 1 2 3 4 2 | 0 2 2 - - 3 | 0 3 - 3 - 4 | 0 4 - - 4 v : | 0 1 2 3 4 --+---------- 0 | 0 1 2 3 4 1 | 1 1 1 1 1 2 | 2 1 2 - - 3 | 3 1 - 3 - 4 | 4 1 - - 4 --------- statistics for domain size 5 --------- Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds). Ground clauses: seen=446, kept=418. Selections=10, assignments=33, propagations=58, current_models=0. Rewrite_terms=1242, rewrite_bools=294, indexes=242. Rules_from_neg_clauses=4, cross_offs=44. === Starting model search for domain size 6. === Initial partial model: A : - B : - C : - c : 0 1 2 3 4 5 --------------- 1 0 - - - - ^ : | 0 1 2 3 4 5 --+------------ 0 | 0 0 0 0 0 0 1 | 0 1 2 3 4 5 2 | 0 2 2 - - - 3 | 0 3 - 3 - - 4 | 0 4 - - 4 - 5 | 0 5 - - - 5 v : | 0 1 2 3 4 5 --+------------ 0 | 0 1 2 3 4 5 1 | 1 1 1 1 1 1 2 | 2 1 2 - - - 3 | 3 1 - 3 - - 4 | 4 1 - - 4 - 5 | 5 1 - - - 5 --------- statistics for domain size 6 --------- Current CPU time: 0.01 seconds (total CPU time: 0.02 seconds). Ground clauses: seen=703, kept=670. Selections=31, assignments=152, propagations=283, current_models=0. Rewrite_terms=9025, rewrite_bools=2714, indexes=510. Rules_from_neg_clauses=49, cross_offs=307. === Starting model search for domain size 7. === Initial partial model: A : - B : - C : - c : 0 1 2 3 4 5 6 ----------------- 1 0 - - - - - ^ : | 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 2 - - - - 3 | 0 3 - 3 - - - 4 | 0 4 - - 4 - - 5 | 0 5 - - - 5 - 6 | 0 6 - - - - 6 v : | 0 1 2 3 4 5 6 --+-------------- 0 | 0 1 2 3 4 5 6 1 | 1 1 1 1 1 1 1 2 | 2 1 2 - - - - 3 | 3 1 - 3 - - - 4 | 4 1 - - 4 - - 5 | 5 1 - - - 5 - 6 | 6 1 - - - - 6 --------- statistics for domain size 7 --------- Current CPU time: 0.00 seconds (total CPU time: 0.02 seconds). Ground clauses: seen=1044, kept=1006. Selections=23, assignments=104, propagations=123, current_models=0. Rewrite_terms=3630, rewrite_bools=745, indexes=652. Rules_from_neg_clauses=7, cross_offs=193. === Starting model search for domain size 8. === Initial partial model: A : - B : - C : - c : 0 1 2 3 4 5 6 7 ------------------- 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 2 - - - - - 3 | 0 3 - 3 - - - - 4 | 0 4 - - 4 - - - 5 | 0 5 - - - 5 - - 6 | 0 6 - - - - 6 - 7 | 0 7 - - - - - 7 v : | 0 1 2 3 4 5 6 7 --+---------------- 0 | 0 1 2 3 4 5 6 7 1 | 1 1 1 1 1 1 1 1 2 | 2 1 2 - - - - - 3 | 3 1 - 3 - - - - 4 | 4 1 - - 4 - - - 5 | 5 1 - - - 5 - - 6 | 6 1 - - - - 6 - 7 | 7 1 - - - - - 7 --------- statistics for domain size 8 --------- Current CPU time: 0.02 seconds (total CPU time: 0.04 seconds). Ground clauses: seen=1481, kept=1438. Selections=46, assignments=271, propagations=911, current_models=0. Rewrite_terms=32276, rewrite_bools=9591, indexes=2191. Rules_from_neg_clauses=98, cross_offs=2215. === Starting model search for domain size 9. === Initial partial model: A : - B : - C : - c : 0 1 2 3 4 5 6 7 8 --------------------- 1 0 - - - - - - - ^ : | 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 - - - - - - 3 | 0 3 - 3 - - - - - 4 | 0 4 - - 4 - - - - 5 | 0 5 - - - 5 - - - 6 | 0 6 - - - - 6 - - 7 | 0 7 - - - - - 7 - 8 | 0 8 - - - - - - 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 - - - - - - 3 | 3 1 - 3 - - - - - 4 | 4 1 - - 4 - - - - 5 | 5 1 - - - 5 - - - 6 | 6 1 - - - - 6 - - 7 | 7 1 - - - - - 7 - 8 | 8 1 - - - - - - 8 --------- statistics for domain size 9 --------- Current CPU time: 0.02 seconds (total CPU time: 0.06 seconds). Ground clauses: seen=2026, kept=1978. Selections=52, assignments=319, propagations=776, current_models=0. Rewrite_terms=29175, rewrite_bools=7706, indexes=3336. Rules_from_neg_clauses=40, cross_offs=3285. === Starting model search for domain size 10. === Initial partial model: A : - B : - C : - c : 0 1 2 3 4 5 6 7 8 9 ----------------------- 1 0 - - - - - - - - ^ : | 0 1 2 3 4 5 6 7 8 9 --+-------------------- 0 | 0 0 0 0 0 0 0 0 0 0 1 | 0 1 2 3 4 5 6 7 8 9 2 | 0 2 2 - - - - - - - 3 | 0 3 - 3 - - - - - - 4 | 0 4 - - 4 - - - - - 5 | 0 5 - - - 5 - - - - 6 | 0 6 - - - - 6 - - - 7 | 0 7 - - - - - 7 - - 8 | 0 8 - - - - - - 8 - 9 | 0 9 - - - - - - - 9 v : | 0 1 2 3 4 5 6 7 8 9 --+-------------------- 0 | 0 1 2 3 4 5 6 7 8 9 1 | 1 1 1 1 1 1 1 1 1 1 2 | 2 1 2 - - - - - - - 3 | 3 1 - 3 - - - - - - 4 | 4 1 - - 4 - - - - - 5 | 5 1 - - - 5 - - - - 6 | 6 1 - - - - 6 - - - 7 | 7 1 - - - - - 7 - - 8 | 8 1 - - - - - - 8 - 9 | 9 1 - - - - - - - 9 -------- Model 1 at 0.08 seconds -------- A : 2 B : 4 C : 6 c : 0 1 2 3 4 5 6 7 8 9 ----------------------- 1 0 3 2 5 4 7 6 9 8 ^ : | 0 1 2 3 4 5 6 7 8 9 --+-------------------- 0 | 0 0 0 0 0 0 0 0 0 0 1 | 0 1 2 3 4 5 6 7 8 9 2 | 0 2 2 0 0 0 0 2 2 0 3 | 0 3 0 3 0 0 6 9 6 9 4 | 0 4 0 0 4 0 0 0 0 0 5 | 0 5 0 0 0 5 0 0 0 0 6 | 0 6 0 6 0 0 6 0 6 0 7 | 0 7 2 9 0 0 0 7 2 9 8 | 0 8 2 6 0 0 6 2 8 0 9 | 0 9 0 9 0 0 0 9 0 9 v : | 0 1 2 3 4 5 6 7 8 9 --+-------------------- 0 | 0 1 2 3 4 5 6 7 8 9 1 | 1 1 1 1 1 1 1 1 1 1 2 | 2 1 2 1 1 1 8 7 8 7 3 | 3 1 1 3 1 1 3 1 1 3 4 | 4 1 1 1 4 1 1 1 1 1 5 | 5 1 1 1 1 5 1 1 1 1 6 | 6 1 8 3 1 1 6 1 8 3 7 | 7 1 7 1 1 1 1 7 1 7 8 | 8 1 8 1 1 1 8 1 8 1 9 | 9 1 7 3 1 1 3 7 1 9 -------- end of model -------- --------- statistics for domain size 10 --------- Current CPU time: 0.03 seconds (total CPU time: 0.09 seconds). Ground clauses: seen=2691, kept=2638. Selections=51, assignments=290, propagations=831, current_models=1. Rewrite_terms=33975, rewrite_bools=8673, indexes=3737. Rules_from_neg_clauses=71, cross_offs=4282. ------------- memory usage (for entire run) ------------------- Total malloced: 20 megabytes type (bytes each) gets frees in use bytes chunk ( 104) 193 193 0 0.0 K string_buf ( 8) 193 193 0 0.0 K token ( 20) 335 335 0 0.0 K pterm ( 16) 166 166 0 0.0 K ilist ( 8) 18 18 0 0.0 K plist ( 8) 17185 17053 132 1.0 K mlist ( 12) 18 18 0 0.0 K term ( 16) 42967 42887 80 1.2 K term arg arrays: 0.5 K literal ( 12) 19 1 18 0.2 K clause ( 32) 19 1 18 0.6 K clist_pos ( 20) 18 18 0 0.0 K clist ( 16) 1 1 0 0.0 K mclause ( 20) 8527 8526 1 0.0 K (61.9 K high) mstate ( 16) 1241 1241 0 0.0 K jnode ( 28) 36484 36484 0 0.0 K estack (3208) 1732 1732 0 0.0 K (avail=0, 0.0 K) Memory report, 1 @ 20 = 20 megs (0.38 megs used). List 2, length 2638, 20.6 K List 3, length 17, 0.2 K List 4, length 19, 0.3 K List 5, length 431, 8.4 K List 6, length 14891, 349.0 K List 7, length 160, 4.4 K List 8, length 1, 0.0 K List 26, length 18, 1.8 K User_CPU=0.09, System_CPU=0.01, Wall_clock=0. Exiting with 1 model. Process 8589 exit (max_models) Tue Jul 5 21:30:21 2005 The process finished Tue Jul 5 21:30:21 2005