----- 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:22 2005 The command was "../bin/mace4". The process ID is 8591. assign(iterate_up_to,20). 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. (c(x) ^ (x v y)) v (c(y) v (x ^ y)) = 1. A ^ (B v (A ^ (c(A) v (A ^ B)))) != A ^ (c(A) v (A ^ B)). 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 : 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.02 seconds). Ground clauses: seen=59, kept=38. Selections=3, assignments=6, propagations=10, current_models=0. Rewrite_terms=166, rewrite_bools=41, 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 : 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.02 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 : 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.02 seconds). Ground clauses: seen=261, kept=228. Selections=4, assignments=13, propagations=36, current_models=0. Rewrite_terms=884, rewrite_bools=237, indexes=109. Rules_from_neg_clauses=3, cross_offs=21. === Starting model search for domain size 5. === Initial partial model: A : - B : - 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.02 seconds). Ground clauses: seen=446, kept=424. Selections=4, assignments=13, propagations=47, current_models=0. Rewrite_terms=1108, rewrite_bools=263, indexes=229. Rules_from_neg_clauses=2, cross_offs=42. === Starting model search for domain size 6. === Initial partial model: A : - B : - 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.03 seconds). Ground clauses: seen=703, kept=678. Selections=6, assignments=24, propagations=77, current_models=0. Rewrite_terms=2471, rewrite_bools=615, indexes=393. Rules_from_neg_clauses=6, cross_offs=115. === Starting model search for domain size 7. === Initial partial model: A : - B : - 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.03 seconds). Ground clauses: seen=1044, kept=1016. Selections=6, assignments=24, propagations=76, current_models=0. Rewrite_terms=2362, rewrite_bools=499, indexes=546. Rules_from_neg_clauses=2, cross_offs=128. === Starting model search for domain size 8. === Initial partial model: A : - B : - 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.01 seconds (total CPU time: 0.04 seconds). Ground clauses: seen=1481, kept=1450. Selections=9, assignments=46, propagations=206, current_models=0. Rewrite_terms=7743, rewrite_bools=2096, indexes=974. Rules_from_neg_clauses=24, cross_offs=453. === Starting model search for domain size 9. === Initial partial model: A : - B : - 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.01 seconds (total CPU time: 0.05 seconds). Ground clauses: seen=2026, kept=1992. Selections=10, assignments=54, propagations=184, current_models=0. Rewrite_terms=7289, rewrite_bools=1727, indexes=1360. Rules_from_neg_clauses=6, cross_offs=654. === Starting model search for domain size 10. === Initial partial model: A : - B : - 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 --------- statistics for domain size 10 --------- Current CPU time: 0.02 seconds (total CPU time: 0.07 seconds). Ground clauses: seen=2691, kept=2654. Selections=16, assignments=108, propagations=543, current_models=0. Rewrite_terms=21552, rewrite_bools=5910, indexes=2152. Rules_from_neg_clauses=50, cross_offs=1488. === Starting model search for domain size 11. === Initial partial model: A : - B : - c : 0 1 2 3 4 5 6 7 8 910 ------------------------- 1 0 - - - - - - - - - ^ : | 0 1 2 3 4 5 6 7 8 910 --+---------------------- 0 | 0 0 0 0 0 0 0 0 0 0 0 1 | 0 1 2 3 4 5 6 7 8 910 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 - 10 | 010 - - - - - - - -10 v : | 0 1 2 3 4 5 6 7 8 910 --+---------------------- 0 | 0 1 2 3 4 5 6 7 8 910 1 | 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 - 10 |10 1 - - - - - - - -10 --------- statistics for domain size 11 --------- Current CPU time: 0.02 seconds (total CPU time: 0.09 seconds). Ground clauses: seen=3488, kept=3448. Selections=19, assignments=138, propagations=456, current_models=0. Rewrite_terms=19192, rewrite_bools=4686, indexes=2897. Rules_from_neg_clauses=9, cross_offs=2010. === Starting model search for domain size 12. === Initial partial model: A : - B : - c : 0 1 2 3 4 5 6 7 8 91011 --------------------------- 1 0 - - - - - - - - - - ^ : | 0 1 2 3 4 5 6 7 8 91011 --+------------------------ 0 | 0 0 0 0 0 0 0 0 0 0 0 0 1 | 0 1 2 3 4 5 6 7 8 91011 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 - - 10 | 010 - - - - - - - -10 - 11 | 011 - - - - - - - - -11 v : | 0 1 2 3 4 5 6 7 8 91011 --+------------------------ 0 | 0 1 2 3 4 5 6 7 8 91011 1 | 1 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 - - 10 |10 1 - - - - - - - -10 - 11 |11 1 - - - - - - - - -11 --------- statistics for domain size 12 --------- Current CPU time: 0.03 seconds (total CPU time: 0.12 seconds). Ground clauses: seen=4429, kept=4386. Selections=24, assignments=193, propagations=738, current_models=0. Rewrite_terms=31231, rewrite_bools=7666, indexes=4086. Rules_from_neg_clauses=37, cross_offs=3358. === Starting model search for domain size 13. === Initial partial model: A : - B : - c : 0 1 2 3 4 5 6 7 8 9101112 ----------------------------- 1 0 - - - - - - - - - - - ^ : | 0 1 2 3 4 5 6 7 8 9101112 --+-------------------------- 0 | 0 0 0 0 0 0 0 0 0 0 0 0 0 1 | 0 1 2 3 4 5 6 7 8 9101112 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 - - - 10 | 010 - - - - - - - -10 - - 11 | 011 - - - - - - - - -11 - 12 | 012 - - - - - - - - - -12 v : | 0 1 2 3 4 5 6 7 8 9101112 --+-------------------------- 0 | 0 1 2 3 4 5 6 7 8 9101112 1 | 1 1 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 - - - 10 |10 1 - - - - - - - -10 - - 11 |11 1 - - - - - - - - -11 - 12 |12 1 - - - - - - - - - -12 --------- statistics for domain size 13 --------- Current CPU time: 0.04 seconds (total CPU time: 0.16 seconds). Ground clauses: seen=5526, kept=5480. Selections=29, assignments=253, propagations=812, current_models=0. Rewrite_terms=41463, rewrite_bools=10319, indexes=5396. Rules_from_neg_clauses=13, cross_offs=4719. === Starting model search for domain size 14. === Initial partial model: A : - B : - c : 0 1 2 3 4 5 6 7 8 910111213 ------------------------------- 1 0 - - - - - - - - - - - - ^ : | 0 1 2 3 4 5 6 7 8 910111213 --+---------------------------- 0 | 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 | 0 1 2 3 4 5 6 7 8 910111213 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 - - - - 10 | 010 - - - - - - - -10 - - - 11 | 011 - - - - - - - - -11 - - 12 | 012 - - - - - - - - - -12 - 13 | 013 - - - - - - - - - - -13 v : | 0 1 2 3 4 5 6 7 8 910111213 --+---------------------------- 0 | 0 1 2 3 4 5 6 7 8 910111213 1 | 1 1 1 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 - - - - 10 |10 1 - - - - - - - -10 - - - 11 |11 1 - - - - - - - - -11 - - 12 |12 1 - - - - - - - - - -12 - 13 |13 1 - - - - - - - - - - -13 --------- statistics for domain size 14 --------- Current CPU time: 0.08 seconds (total CPU time: 0.24 seconds). Ground clauses: seen=6791, kept=6742. Selections=41, assignments=410, propagations=1664, current_models=0. Rewrite_terms=81043, rewrite_bools=21492, indexes=8116. Rules_from_neg_clauses=105, cross_offs=7636. === Starting model search for domain size 15. === Initial partial model: A : - B : - c : 0 1 2 3 4 5 6 7 8 91011121314 --------------------------------- 1 0 - - - - - - - - - - - - - ^ : | 0 1 2 3 4 5 6 7 8 91011121314 --+------------------------------ 0 | 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 | 0 1 2 3 4 5 6 7 8 91011121314 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 - - - - - 10 | 010 - - - - - - - -10 - - - - 11 | 011 - - - - - - - - -11 - - - 12 | 012 - - - - - - - - - -12 - - 13 | 013 - - - - - - - - - - -13 - 14 | 014 - - - - - - - - - - - -14 v : | 0 1 2 3 4 5 6 7 8 91011121314 --+------------------------------ 0 | 0 1 2 3 4 5 6 7 8 91011121314 1 | 1 1 1 1 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 - - - - - 10 |10 1 - - - - - - - -10 - - - - 11 |11 1 - - - - - - - - -11 - - - 12 |12 1 - - - - - - - - - -12 - - 13 |13 1 - - - - - - - - - - -13 - 14 |14 1 - - - - - - - - - - - -14 --------- statistics for domain size 15 --------- Current CPU time: 0.09 seconds (total CPU time: 0.33 seconds). Ground clauses: seen=8236, kept=8184. Selections=51, assignments=550, propagations=1794, current_models=0. Rewrite_terms=93292, rewrite_bools=23567, indexes=10663. Rules_from_neg_clauses=30, cross_offs=10300. === Starting model search for domain size 16. === Initial partial model: A : - B : - c : 0 1 2 3 4 5 6 7 8 9101112131415 ----------------------------------- 1 0 - - - - - - - - - - - - - - ^ : | 0 1 2 3 4 5 6 7 8 9101112131415 --+-------------------------------- 0 | 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 | 0 1 2 3 4 5 6 7 8 9101112131415 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 - - - - - - 10 | 010 - - - - - - - -10 - - - - - 11 | 011 - - - - - - - - -11 - - - - 12 | 012 - - - - - - - - - -12 - - - 13 | 013 - - - - - - - - - - -13 - - 14 | 014 - - - - - - - - - - - -14 - 15 | 015 - - - - - - - - - - - - -15 v : | 0 1 2 3 4 5 6 7 8 9101112131415 --+-------------------------------- 0 | 0 1 2 3 4 5 6 7 8 9101112131415 1 | 1 1 1 1 1 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 - - - - - - 10 |10 1 - - - - - - - -10 - - - - - 11 |11 1 - - - - - - - - -11 - - - - 12 |12 1 - - - - - - - - - -12 - - - 13 |13 1 - - - - - - - - - - -13 - - 14 |14 1 - - - - - - - - - - - -14 - 15 |15 1 - - - - - - - - - - - - -15 --------- statistics for domain size 16 --------- Current CPU time: 0.21 seconds (total CPU time: 0.54 seconds). Ground clauses: seen=9873, kept=9818. Selections=77, assignments=943, propagations=4271, current_models=0. Rewrite_terms=219182, rewrite_bools=59450, indexes=18426. Rules_from_neg_clauses=299, cross_offs=19636. === Starting model search for domain size 17. === Initial partial model: A : - B : - c : 0 1 2 3 4 5 6 7 8 910111213141516 ------------------------------------- 1 0 - - - - - - - - - - - - - - - ^ : | 0 1 2 3 4 5 6 7 8 910111213141516 --+---------------------------------- 0 | 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 | 0 1 2 3 4 5 6 7 8 910111213141516 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 - - - - - - - 10 | 010 - - - - - - - -10 - - - - - - 11 | 011 - - - - - - - - -11 - - - - - 12 | 012 - - - - - - - - - -12 - - - - 13 | 013 - - - - - - - - - - -13 - - - 14 | 014 - - - - - - - - - - - -14 - - 15 | 015 - - - - - - - - - - - - -15 - 16 | 016 - - - - - - - - - - - - - -16 v : | 0 1 2 3 4 5 6 7 8 910111213141516 --+---------------------------------- 0 | 0 1 2 3 4 5 6 7 8 910111213141516 1 | 1 1 1 1 1 1 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 - - - - - - - 10 |10 1 - - - - - - - -10 - - - - - - 11 |11 1 - - - - - - - - -11 - - - - - 12 |12 1 - - - - - - - - - -12 - - - - 13 |13 1 - - - - - - - - - - -13 - - - 14 |14 1 - - - - - - - - - - - -14 - - 15 |15 1 - - - - - - - - - - - - -15 - 16 |16 1 - - - - - - - - - - - - - -16 --------- statistics for domain size 17 --------- Current CPU time: 0.28 seconds (total CPU time: 0.82 seconds). Ground clauses: seen=11714, kept=11656. Selections=97, assignments=1263, propagations=4471, current_models=0. Rewrite_terms=260852, rewrite_bools=69294, indexes=24742. Rules_from_neg_clauses=87, cross_offs=26113. === Starting model search for domain size 18. === Initial partial model: A : - B : - c : 0 1 2 3 4 5 6 7 8 91011121314151617 --------------------------------------- 1 0 - - - - - - - - - - - - - - - - ^ : | 0 1 2 3 4 5 6 7 8 91011121314151617 --+------------------------------------ 0 | 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 | 0 1 2 3 4 5 6 7 8 91011121314151617 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 - - - - - - - - 10 | 010 - - - - - - - -10 - - - - - - - 11 | 011 - - - - - - - - -11 - - - - - - 12 | 012 - - - - - - - - - -12 - - - - - 13 | 013 - - - - - - - - - - -13 - - - - 14 | 014 - - - - - - - - - - - -14 - - - 15 | 015 - - - - - - - - - - - - -15 - - 16 | 016 - - - - - - - - - - - - - -16 - 17 | 017 - - - - - - - - - - - - - - -17 v : | 0 1 2 3 4 5 6 7 8 91011121314151617 --+------------------------------------ 0 | 0 1 2 3 4 5 6 7 8 91011121314151617 1 | 1 1 1 1 1 1 1 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 - - - - - - - - 10 |10 1 - - - - - - - -10 - - - - - - - 11 |11 1 - - - - - - - - -11 - - - - - - 12 |12 1 - - - - - - - - - -12 - - - - - 13 |13 1 - - - - - - - - - - -13 - - - - 14 |14 1 - - - - - - - - - - - -14 - - - 15 |15 1 - - - - - - - - - - - - -15 - - 16 |16 1 - - - - - - - - - - - - - -16 - 17 |17 1 - - - - - - - - - - - - - - -17 --------- statistics for domain size 18 --------- Current CPU time: 0.67 seconds (total CPU time: 1.49 seconds). Ground clauses: seen=13771, kept=13710. Selections=157, assignments=2292, propagations=10983, current_models=0. Rewrite_terms=644765, rewrite_bools=182109, indexes=44581. Rules_from_neg_clauses=671, cross_offs=50581. === Starting model search for domain size 19. === Initial partial model: A : - B : - c : 0 1 2 3 4 5 6 7 8 9101112131415161718 ----------------------------------------- 1 0 - - - - - - - - - - - - - - - - - ^ : | 0 1 2 3 4 5 6 7 8 9101112131415161718 --+-------------------------------------- 0 | 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 | 0 1 2 3 4 5 6 7 8 9101112131415161718 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 - - - - - - - - - 10 | 010 - - - - - - - -10 - - - - - - - - 11 | 011 - - - - - - - - -11 - - - - - - - 12 | 012 - - - - - - - - - -12 - - - - - - 13 | 013 - - - - - - - - - - -13 - - - - - 14 | 014 - - - - - - - - - - - -14 - - - - 15 | 015 - - - - - - - - - - - - -15 - - - 16 | 016 - - - - - - - - - - - - - -16 - - 17 | 017 - - - - - - - - - - - - - - -17 - 18 | 018 - - - - - - - - - - - - - - - -18 v : | 0 1 2 3 4 5 6 7 8 9101112131415161718 --+-------------------------------------- 0 | 0 1 2 3 4 5 6 7 8 9101112131415161718 1 | 1 1 1 1 1 1 1 1 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 - - - - - - - - - 10 |10 1 - - - - - - - -10 - - - - - - - - 11 |11 1 - - - - - - - - -11 - - - - - - - 12 |12 1 - - - - - - - - - -12 - - - - - - 13 |13 1 - - - - - - - - - - -13 - - - - - 14 |14 1 - - - - - - - - - - - -14 - - - - 15 |15 1 - - - - - - - - - - - - -15 - - - 16 |16 1 - - - - - - - - - - - - - -16 - - 17 |17 1 - - - - - - - - - - - - - - -17 - 18 |18 1 - - - - - - - - - - - - - - - -18 --------- statistics for domain size 19 --------- Current CPU time: 0.78 seconds (total CPU time: 2.27 seconds). Ground clauses: seen=16056, kept=15992. Selections=197, assignments=3012, propagations=11320, current_models=0. Rewrite_terms=696762, rewrite_bools=187243, indexes=59577. Rules_from_neg_clauses=318, cross_offs=66099. === Starting model search for domain size 20. === Initial partial model: A : - B : - c : 0 1 2 3 4 5 6 7 8 910111213141516171819 ------------------------------------------- 1 0 - - - - - - - - - - - - - - - - - - ^ : | 0 1 2 3 4 5 6 7 8 910111213141516171819 --+---------------------------------------- 0 | 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 | 0 1 2 3 4 5 6 7 8 910111213141516171819 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 - - - - - - - - - - 10 | 010 - - - - - - - -10 - - - - - - - - - 11 | 011 - - - - - - - - -11 - - - - - - - - 12 | 012 - - - - - - - - - -12 - - - - - - - 13 | 013 - - - - - - - - - - -13 - - - - - - 14 | 014 - - - - - - - - - - - -14 - - - - - 15 | 015 - - - - - - - - - - - - -15 - - - - 16 | 016 - - - - - - - - - - - - - -16 - - - 17 | 017 - - - - - - - - - - - - - - -17 - - 18 | 018 - - - - - - - - - - - - - - - -18 - 19 | 019 - - - - - - - - - - - - - - - - -19 v : | 0 1 2 3 4 5 6 7 8 910111213141516171819 --+---------------------------------------- 0 | 0 1 2 3 4 5 6 7 8 910111213141516171819 1 | 1 1 1 1 1 1 1 1 1 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 - - - - - - - - - - 10 |10 1 - - - - - - - -10 - - - - - - - - - 11 |11 1 - - - - - - - - -11 - - - - - - - - 12 |12 1 - - - - - - - - - -12 - - - - - - - 13 |13 1 - - - - - - - - - - -13 - - - - - - 14 |14 1 - - - - - - - - - - - -14 - - - - - 15 |15 1 - - - - - - - - - - - - -15 - - - - 16 |16 1 - - - - - - - - - - - - - -16 - - - 17 |17 1 - - - - - - - - - - - - - - -17 - - 18 |18 1 - - - - - - - - - - - - - - - -18 - 19 |19 1 - - - - - - - - - - - - - - - - -19 -------- Model 1 at 2.40 seconds -------- A : 2 B : 4 c : 0 1 2 3 4 5 6 7 8 910111213141516171819 ------------------------------------------- 1 0 3 2 5 4 7 6 9 811101312151417161918 ^ : | 0 1 2 3 4 5 6 7 8 910111213141516171819 --+---------------------------------------- 0 | 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 | 0 1 2 3 4 5 6 7 8 910111213141516171819 2 | 0 2 2 0 6 0 6 912 916 012 916 016181816 3 | 0 3 0 3 0 0 0 3 3 0 0 0 0 3 0 0 0 3 0 3 4 | 0 4 6 0 4 0 611 6 0 611 611 4 0 611 0 6 5 | 0 5 0 0 0 5 0 5 0 0 5 0 015 015 015 0 0 6 | 0 6 6 0 6 0 6 0 6 0 6 0 6 0 6 0 6 0 0 6 7 | 0 7 9 311 5 0 7 3 9 511 0131115 01718 3 8 | 0 812 3 6 0 6 3 8 012 012 312 012 3 0 8 9 | 0 9 9 0 0 0 0 9 0 9 0 0 0 9 0 0 01818 0 10 | 01016 0 6 5 6 512 010 0121516151615 016 11 | 011 0 011 0 011 0 0 011 01111 0 011 0 0 12 | 01212 0 6 0 6 012 012 012 012 012 0 012 13 | 013 9 31115 013 3 91511 0131115 01718 3 14 | 01416 0 4 0 61112 01611121114 01611 016 15 | 015 0 0 015 015 0 015 0 015 015 015 0 0 16 | 01616 0 6 0 6 012 016 012 016 016 0 016 17 | 01718 31115 017 3181511 0171115 01718 3 18 | 01818 0 0 0 018 018 0 0 018 0 0 01818 0 19 | 01916 3 6 0 6 3 8 016 012 316 016 3 019 v : | 0 1 2 3 4 5 6 7 8 910111213141516171819 --+---------------------------------------- 0 | 0 1 2 3 4 5 6 7 8 910111213141516171819 1 | 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 2 | 2 1 2 1 1 1 2 1 1 2 1 1 2 1 1 1 2 1 2 1 3 | 3 1 1 3 1 7 8 7 813 117 813 11719171719 4 | 4 1 1 1 4 1 4 1 1 1 1 414 114 114 1 1 1 5 | 5 1 1 7 1 510 7 1 710 710 7 1 510 7 7 1 6 | 6 1 2 8 410 6 1 8 210 412 1141016 1 219 7 | 7 1 1 7 1 7 1 7 1 7 1 7 1 7 1 7 1 7 7 1 8 | 8 1 1 8 1 1 8 1 8 1 1 1 8 1 1 119 1 119 9 | 9 1 213 1 7 2 7 1 9 113 213 113 213 9 1 10 |10 1 1 1 11010 1 1 110 110 1 11010 1 1 1 11 |11 1 117 4 7 4 7 113 11114131417141717 1 12 |12 1 2 8141012 1 8 2101412 1141016 1 219 13 |13 1 113 1 7 1 7 113 113 113 113 11313 1 14 |14 1 1 114 114 1 1 1 11414 114 114 1 1 1 15 |15 1 117 1 510 7 11310171013 115101717 1 16 |16 1 219141016 119 2101416 1141016 1 219 17 |17 1 117 1 7 1 7 113 117 113 117 11717 1 18 |18 1 217 1 7 2 7 1 9 117 213 117 21718 1 19 |19 1 119 1 119 119 1 1 119 1 1 119 1 119 -------- end of model -------- --------- statistics for domain size 20 --------- Current CPU time: 0.15 seconds (total CPU time: 2.42 seconds). Ground clauses: seen=18581, kept=18514. Selections=34, assignments=305, propagations=1219, current_models=1. Rewrite_terms=92878, rewrite_bools=22938, indexes=12650. Rules_from_neg_clauses=59, cross_offs=11523. ------------- memory usage (for entire run) ------------------- Total malloced: 20 megabytes type (bytes each) gets frees in use bytes chunk ( 104) 202 202 0 0.0 K string_buf ( 8) 201 201 0 0.0 K token ( 20) 362 362 0 0.0 K pterm ( 16) 182 182 0 0.0 K ilist ( 8) 16 16 0 0.0 K plist ( 8) 213175 213045 130 1.0 K mlist ( 12) 16 16 0 0.0 K term ( 16) 534405 534316 89 1.4 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) 106523 106522 1 0.0 K (433.9 K high) mstate ( 16) 9666 9666 0 0.0 K jnode ( 28) 724058 724058 0 0.0 K estack (3208) 20902 20902 0 0.0 K (avail=0, 0.0 K) Memory report, 1 @ 20 = 20 megs (2.68 megs used). List 2, length 18514, 144.6 K List 3, length 15, 0.2 K List 4, length 21, 0.3 K List 5, length 2023, 39.5 K List 6, length 108041, 2532.2 K List 7, length 734, 20.1 K List 8, length 1, 0.0 K List 26, length 24, 2.4 K User_CPU=2.42, System_CPU=0.00, Wall_clock=2. Exiting with 1 model. Process 8591 exit (max_models) Tue Jul 5 21:30:24 2005 The process finished Tue Jul 5 21:30:24 2005