============================== Mace4 ================================= Mace4 (32) version Dec-2007, Dec 2007. Process 3996 was started by Alexei on Alexei-PC, Sun Mar 17 13:18:11 2013 The command was "/cygdrive/c/Program Files (x86)/Prover9-Mace4/bin-win32/mace4 -c". ============================== end of head =========================== ============================== INPUT ================================= assign(report_stderr,2). set(ignore_option_dependencies). if(Prover9). % Conditional input omitted. end_if. if(Mace4). % Conditional input included. assign(max_seconds,-1). end_if. formulas(assumptions). x * x = x. (x * y) * y = x. (x * y) * z = (x * z) * (y * z). a2 = a1 * a10. a3 = a2 * a8. a4 = a3 * a6. a5 = a4 * a1. a6 = a5 * a9. a7 = a6 * a3. a8 = a7 * a2. a9 = a8 * a7. a10 = a9 * a5. a1 = a10 * a4. end_of_list. formulas(goals). a1 = a2 & a2 = a3 & a3 = a4 & a4 = a5 & a5 = a6 & a6 = a7 & a7 = a8 & a8 = a9 & a9 = a10. end_of_list. ============================== end of input ========================== % Enabling option dependencies (ignore applies only on input). ============================== PROCESS NON-CLAUSAL FORMULAS ========== % Formulas that are not ordinary clauses: 1 a1 = a2 & a2 = a3 & a3 = a4 & a4 = a5 & a5 = a6 & a6 = a7 & a7 = a8 & a8 = a9 & a9 = a10 # label(non_clause) # label(goal). [goal]. ============================== end of process non-clausal formulas === ============================== CLAUSES FOR SEARCH ==================== formulas(mace4_clauses). x * x = x. (x * y) * y = x. (x * y) * z = (x * z) * (y * z). a2 = a1 * a10. a3 = a2 * a8. a4 = a3 * a6. a5 = a4 * a1. a6 = a5 * a9. a7 = a6 * a3. a8 = a7 * a2. a9 = a8 * a7. a10 = a9 * a5. a1 = a10 * a4. a1 != a2 | a3 != a2 | a4 != a3 | a5 != a4 | a5 != a6 | a7 != a6 | a7 != a8 | a9 != a8 | a9 != a10. end_of_list. ============================== end of clauses for search ============= % There are no domain elements in the input. ============================== DOMAIN SIZE 2 ========================= ============================== STATISTICS ============================ For domain size 2. Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds). Ground clauses: seen=25, kept=15. Selections=4, assignments=7, propagations=15, current_models=0. Rewrite_terms=80, rewrite_bools=24, indexes=0. Rules_from_neg_clauses=6, cross_offs=6. ============================== end of statistics ===================== ============================== DOMAIN SIZE 3 ========================= ============================== STATISTICS ============================ For domain size 3. Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds). Ground clauses: seen=50, kept=44. Selections=6, assignments=13, propagations=61, current_models=0. Rewrite_terms=606, rewrite_bools=137, indexes=44. Rules_from_neg_clauses=19, cross_offs=41. ============================== end of statistics ===================== ============================== DOMAIN SIZE 4 ========================= ============================== STATISTICS ============================ For domain size 4. Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds). Ground clauses: seen=95, kept=87. Selections=10, assignments=28, propagations=101, current_models=0. Rewrite_terms=1333, rewrite_bools=276, indexes=147. Rules_from_neg_clauses=22, cross_offs=99. ============================== end of statistics ===================== ============================== DOMAIN SIZE 5 ========================= ============================== STATISTICS ============================ For domain size 5. Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds). Ground clauses: seen=166, kept=156. Selections=12, assignments=38, propagations=125, current_models=0. Rewrite_terms=1873, rewrite_bools=328, indexes=248. Rules_from_neg_clauses=22, cross_offs=187. ============================== end of statistics ===================== ============================== DOMAIN SIZE 6 ========================= ============================== STATISTICS ============================ For domain size 6. Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds). Ground clauses: seen=269, kept=257. Selections=14, assignments=50, propagations=197, current_models=0. Rewrite_terms=3898, rewrite_bools=701, indexes=488. Rules_from_neg_clauses=40, cross_offs=382. ============================== end of statistics ===================== ============================== DOMAIN SIZE 7 ========================= ============================== STATISTICS ============================ For domain size 7. Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds). Ground clauses: seen=410, kept=396. Selections=20, assignments=91, propagations=340, current_models=0. Rewrite_terms=7467, rewrite_bools=1380, indexes=1046. Rules_from_neg_clauses=56, cross_offs=632. ============================== end of statistics ===================== ============================== DOMAIN SIZE 8 ========================= ============================== STATISTICS ============================ For domain size 8. Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds). Ground clauses: seen=595, kept=579. Selections=21, assignments=101, propagations=479, current_models=0. Rewrite_terms=10895, rewrite_bools=1782, indexes=1551. Rules_from_neg_clauses=60, cross_offs=1111. ============================== end of statistics ===================== ============================== DOMAIN SIZE 9 ========================= ============================== STATISTICS ============================ For domain size 9. Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds). Ground clauses: seen=830, kept=812. Selections=30, assignments=180, propagations=912, current_models=0. Rewrite_terms=20767, rewrite_bools=3214, indexes=2997. Rules_from_neg_clauses=76, cross_offs=1981. ============================== end of statistics ===================== ============================== DOMAIN SIZE 10 ======================== ============================== STATISTICS ============================ For domain size 10. Current CPU time: 0.00 seconds (total CPU time: 0.03 seconds). Ground clauses: seen=1121, kept=1101. Selections=34, assignments=220, propagations=1129, current_models=0. Rewrite_terms=27981, rewrite_bools=4420, indexes=4202. Rules_from_neg_clauses=104, cross_offs=2870. ============================== end of statistics ===================== ============================== DOMAIN SIZE 11 ======================== ============================== STATISTICS ============================ For domain size 11. Current CPU time: 0.00 seconds (total CPU time: 0.03 seconds). Ground clauses: seen=1474, kept=1452. Selections=41, assignments=294, propagations=1439, current_models=0. Rewrite_terms=36788, rewrite_bools=5619, indexes=5473. Rules_from_neg_clauses=103, cross_offs=4130. ============================== end of statistics ===================== ============================== DOMAIN SIZE 12 ======================== ============================== STATISTICS ============================ For domain size 12. Current CPU time: 0.00 seconds (total CPU time: 0.05 seconds). Ground clauses: seen=1895, kept=1871. Selections=46, assignments=352, propagations=1947, current_models=0. Rewrite_terms=57259, rewrite_bools=9353, indexes=7644. Rules_from_neg_clauses=138, cross_offs=5788. ============================== end of statistics ===================== ============================== DOMAIN SIZE 13 ======================== ============================== STATISTICS ============================ For domain size 13. Current CPU time: 0.00 seconds (total CPU time: 0.06 seconds). Ground clauses: seen=2390, kept=2364. Selections=54, assignments=453, propagations=2698, current_models=0. Rewrite_terms=67758, rewrite_bools=9820, indexes=10186. Rules_from_neg_clauses=158, cross_offs=7369. ============================== end of statistics ===================== ============================== DOMAIN SIZE 14 ======================== ============================== STATISTICS ============================ For domain size 14. Current CPU time: 0.00 seconds (total CPU time: 0.08 seconds). Ground clauses: seen=2965, kept=2937. Selections=56, assignments=481, propagations=3027, current_models=0. Rewrite_terms=83321, rewrite_bools=11649, indexes=12186. Rules_from_neg_clauses=155, cross_offs=9441. ============================== end of statistics ===================== ============================== DOMAIN SIZE 15 ======================== ============================== STATISTICS ============================ For domain size 15. Current CPU time: 0.00 seconds (total CPU time: 0.11 seconds). Ground clauses: seen=3626, kept=3596. Selections=62, assignments=569, propagations=3777, current_models=0. Rewrite_terms=109377, rewrite_bools=16354, indexes=15282. Rules_from_neg_clauses=164, cross_offs=11709. ============================== end of statistics ===================== ============================== DOMAIN SIZE 16 ======================== ============================== STATISTICS ============================ For domain size 16. Current CPU time: 0.00 seconds (total CPU time: 0.16 seconds). Ground clauses: seen=4379, kept=4347. Selections=63, assignments=585, propagations=4013, current_models=0. Rewrite_terms=128835, rewrite_bools=19096, indexes=17332. Rules_from_neg_clauses=214, cross_offs=14268. ============================== end of statistics ===================== ============================== DOMAIN SIZE 17 ======================== ============================== STATISTICS ============================ For domain size 17. Current CPU time: 0.00 seconds (total CPU time: 0.22 seconds). Ground clauses: seen=5230, kept=5196. Selections=68, assignments=668, propagations=5069, current_models=0. Rewrite_terms=155089, rewrite_bools=23389, indexes=20516. Rules_from_neg_clauses=675, cross_offs=18127. ============================== end of statistics ===================== ============================== DOMAIN SIZE 18 ======================== ============================== STATISTICS ============================ For domain size 18. Current CPU time: 0.00 seconds (total CPU time: 0.30 seconds). Ground clauses: seen=6185, kept=6149. Selections=69, assignments=686, propagations=4980, current_models=0. Rewrite_terms=190809, rewrite_bools=31315, indexes=23779. Rules_from_neg_clauses=183, cross_offs=20726. ============================== end of statistics ===================== ============================== DOMAIN SIZE 19 ======================== ============================== STATISTICS ============================ For domain size 19. Current CPU time: 0.00 seconds (total CPU time: 0.42 seconds). Ground clauses: seen=7250, kept=7212. Selections=74, assignments=779, propagations=6460, current_models=0. Rewrite_terms=224637, rewrite_bools=35401, indexes=27935. Rules_from_neg_clauses=927, cross_offs=26125. ============================== end of statistics ===================== ============================== DOMAIN SIZE 20 ======================== ============================== STATISTICS ============================ For domain size 20. Current CPU time: 0.00 seconds (total CPU time: 0.56 seconds). Ground clauses: seen=8431, kept=8391. Selections=75, assignments=799, propagations=6108, current_models=0. Rewrite_terms=272751, rewrite_bools=45757, indexes=31725. Rules_from_neg_clauses=224, cross_offs=29872. ============================== end of statistics ===================== ============================== DOMAIN SIZE 21 ======================== ============================== STATISTICS ============================ For domain size 21. Current CPU time: 0.00 seconds (total CPU time: 0.73 seconds). Ground clauses: seen=9734, kept=9692. Selections=80, assignments=902, propagations=7871, current_models=0. Rewrite_terms=308302, rewrite_bools=50022, indexes=36759. Rules_from_neg_clauses=1058, cross_offs=35941. ============================== end of statistics ===================== ============================== DOMAIN SIZE 22 ======================== ============================== STATISTICS ============================ For domain size 22. Current CPU time: 0.00 seconds (total CPU time: 0.97 seconds). Ground clauses: seen=11165, kept=11121. Selections=81, assignments=924, propagations=7617, current_models=0. Rewrite_terms=374134, rewrite_bools=64407, indexes=41562. Rules_from_neg_clauses=280, cross_offs=40702. ============================== end of statistics ===================== ============================== DOMAIN SIZE 23 ======================== ============================== STATISTICS ============================ For domain size 23. Current CPU time: 0.00 seconds (total CPU time: 1.25 seconds). Ground clauses: seen=12730, kept=12684. Selections=86, assignments=1037, propagations=9519, current_models=0. Rewrite_terms=418994, rewrite_bools=69906, indexes=47529. Rules_from_neg_clauses=1105, cross_offs=48348. ============================== end of statistics ===================== ============================== DOMAIN SIZE 24 ======================== ============================== STATISTICS ============================ For domain size 24. Current CPU time: 0.00 seconds (total CPU time: 1.61 seconds). Ground clauses: seen=14435, kept=14387. Selections=88, assignments=1084, propagations=9562, current_models=0. Rewrite_terms=492042, rewrite_bools=86352, indexes=53581. Rules_from_neg_clauses=347, cross_offs=54029. ============================== end of statistics ===================== ============================== DOMAIN SIZE 25 ======================== ============================== STATISTICS ============================ For domain size 25. Current CPU time: 0.00 seconds (total CPU time: 2.02 seconds). Ground clauses: seen=16286, kept=16236. Selections=93, assignments=1207, propagations=12131, current_models=0. Rewrite_terms=551942, rewrite_bools=90452, indexes=61513. Rules_from_neg_clauses=1457, cross_offs=64505. ============================== end of statistics ===================== ============================== DOMAIN SIZE 26 ======================== ============================== STATISTICS ============================ For domain size 26. Current CPU time: 0.00 seconds (total CPU time: 2.53 seconds). Ground clauses: seen=18289, kept=18237. Selections=94, assignments=1233, propagations=11624, current_models=0. Rewrite_terms=630878, rewrite_bools=104994, indexes=67521. Rules_from_neg_clauses=388, cross_offs=72863. ============================== end of statistics ===================== ============================== DOMAIN SIZE 27 ======================== ============================== STATISTICS ============================ For domain size 27. Current CPU time: 0.00 seconds (total CPU time: 3.14 seconds). Ground clauses: seen=20450, kept=20396. Selections=99, assignments=1366, propagations=14642, current_models=0. Rewrite_terms=709354, rewrite_bools=116878, indexes=77162. Rules_from_neg_clauses=1913, cross_offs=84999. ============================== end of statistics ===================== ============================== DOMAIN SIZE 28 ======================== ============================== STATISTICS ============================ For domain size 28. Current CPU time: 0.00 seconds (total CPU time: 3.84 seconds). Ground clauses: seen=22775, kept=22719. Selections=100, assignments=1394, propagations=13907, current_models=0. Rewrite_terms=785116, rewrite_bools=127042, indexes=84428. Rules_from_neg_clauses=459, cross_offs=93359. ============================== end of statistics ===================== ============================== DOMAIN SIZE 29 ======================== ============================== STATISTICS ============================ For domain size 29. Current CPU time: 0.00 seconds (total CPU time: 4.69 seconds). Ground clauses: seen=25270, kept=25212. Selections=105, assignments=1537, propagations=17605, current_models=0. Rewrite_terms=889866, rewrite_bools=145529, indexes=95337. Rules_from_neg_clauses=2376, cross_offs=107521. ============================== end of statistics ===================== ============================== DOMAIN SIZE 30 ======================== ============================== STATISTICS ============================ For domain size 30. Current CPU time: 0.00 seconds (total CPU time: 5.59 seconds). Ground clauses: seen=27941, kept=27881. Selections=107, assignments=1596, propagations=16559, current_models=0. Rewrite_terms=934259, rewrite_bools=151686, indexes=103823. Rules_from_neg_clauses=492, cross_offs=118663. ============================== end of statistics ===================== ============================== DOMAIN SIZE 31 ======================== ============================== STATISTICS ============================ For domain size 31. Current CPU time: 0.00 seconds (total CPU time: 6.73 seconds). Ground clauses: seen=30794, kept=30732. Selections=111, assignments=1718, propagations=18739, current_models=0. Rewrite_terms=1099618, rewrite_bools=179933, indexes=116245. Rules_from_neg_clauses=819, cross_offs=134075. ============================== end of statistics ===================== ============================== DOMAIN SIZE 32 ======================== ============================== STATISTICS ============================ For domain size 32. Current CPU time: 0.00 seconds (total CPU time: 7.95 seconds). Ground clauses: seen=33835, kept=33771. Selections=114, assignments=1812, propagations=19067, current_models=0. Rewrite_terms=1142658, rewrite_bools=182192, indexes=125506. Rules_from_neg_clauses=599, cross_offs=149243. ============================== end of statistics ===================== ============================== DOMAIN SIZE 33 ======================== ============================== STATISTICS ============================ For domain size 33. Current CPU time: 0.00 seconds (total CPU time: 9.47 seconds). Ground clauses: seen=37070, kept=37004. Selections=117, assignments=1910, propagations=20847, current_models=0. Rewrite_terms=1320600, rewrite_bools=216239, indexes=138222. Rules_from_neg_clauses=619, cross_offs=165992. ============================== end of statistics ===================== ============================== DOMAIN SIZE 34 ======================== ============================== STATISTICS ============================ For domain size 34. Current CPU time: 0.00 seconds (total CPU time: 11.12 seconds). Ground clauses: seen=40505, kept=40437. Selections=119, assignments=1977, propagations=21243, current_models=0. Rewrite_terms=1400290, rewrite_bools=227545, indexes=149565. Rules_from_neg_clauses=508, cross_offs=180491. ============================== end of statistics ===================== ============================== DOMAIN SIZE 35 ======================== ============================== STATISTICS ============================ For domain size 35. Current CPU time: 0.00 seconds (total CPU time: 13.09 seconds). Ground clauses: seen=44146, kept=44076. Selections=123, assignments=2115, propagations=23741, current_models=0. Rewrite_terms=1572756, rewrite_bools=251165, indexes=164503. Rules_from_neg_clauses=878, cross_offs=209022. ============================== end of statistics ===================== ============================== DOMAIN SIZE 36 ======================== ============================== STATISTICS ============================ For domain size 36. Current CPU time: 0.00 seconds (total CPU time: 15.22 seconds). Ground clauses: seen=47999, kept=47927. Selections=125, assignments=2186, propagations=24408, current_models=0. Rewrite_terms=1635487, rewrite_bools=255331, indexes=178295. Rules_from_neg_clauses=939, cross_offs=238688. ============================== end of statistics ===================== ============================== DOMAIN SIZE 37 ======================== ============================== STATISTICS ============================ For domain size 37. Current CPU time: 0.00 seconds (total CPU time: 17.64 seconds). Ground clauses: seen=52070, kept=51996. Selections=128, assignments=2296, propagations=26654, current_models=0. Rewrite_terms=1800157, rewrite_bools=275035, indexes=194765. Rules_from_neg_clauses=669, cross_offs=260003. ============================== end of statistics ===================== ============================== DOMAIN SIZE 38 ======================== ============================== STATISTICS ============================ For domain size 38. Current CPU time: 0.00 seconds (total CPU time: 20.27 seconds). Ground clauses: seen=56365, kept=56289. Selections=128, assignments=2297, propagations=27057, current_models=0. Rewrite_terms=1882053, rewrite_bools=284857, indexes=207239. Rules_from_neg_clauses=679, cross_offs=281183. ============================== end of statistics ===================== ============================== DOMAIN SIZE 39 ======================== ============================== STATISTICS ============================ For domain size 39. Current CPU time: 0.00 seconds (total CPU time: 23.38 seconds). Ground clauses: seen=60890, kept=60812. Selections=131, assignments=2413, propagations=30437, current_models=0. Rewrite_terms=2123181, rewrite_bools=317252, indexes=225332. Rules_from_neg_clauses=1031, cross_offs=306778. ============================== end of statistics ===================== ============================== DOMAIN SIZE 40 ======================== ============================== STATISTICS ============================ For domain size 40. Current CPU time: 0.00 seconds (total CPU time: 26.75 seconds). Ground clauses: seen=65651, kept=65571. Selections=132, assignments=2453, propagations=30547, current_models=0. Rewrite_terms=2244095, rewrite_bools=340470, indexes=241289. Rules_from_neg_clauses=778, cross_offs=329503. ============================== end of statistics ===================== ============================== DOMAIN SIZE 41 ======================== ============================== STATISTICS ============================ For domain size 41. Current CPU time: 0.00 seconds (total CPU time: 30.66 seconds). Ground clauses: seen=70654, kept=70572. Selections=136, assignments=2615, propagations=33736, current_models=0. Rewrite_terms=2469422, rewrite_bools=369515, indexes=260604. Rules_from_neg_clauses=948, cross_offs=357353. ============================== end of statistics ===================== ============================== DOMAIN SIZE 42 ======================== ============================== STATISTICS ============================ For domain size 42. Current CPU time: 0.00 seconds (total CPU time: 34.88 seconds). Ground clauses: seen=75905, kept=75821. Selections=137, assignments=2657, propagations=34217, current_models=0. Rewrite_terms=2610688, rewrite_bools=398655, indexes=276446. Rules_from_neg_clauses=765, cross_offs=382183. ============================== end of statistics ===================== ============================== DOMAIN SIZE 43 ======================== ============================== STATISTICS ============================ For domain size 43. Current CPU time: 0.00 seconds (total CPU time: 39.55 seconds). Ground clauses: seen=81410, kept=81324. Selections=139, assignments=2743, propagations=37684, current_models=0. Rewrite_terms=2790805, rewrite_bools=411770, indexes=296767. Rules_from_neg_clauses=909, cross_offs=414326. ============================== end of statistics ===================== ============================== DOMAIN SIZE 44 ======================== ============================== STATISTICS ============================ For domain size 44. Current CPU time: 0.00 seconds (total CPU time: 44.81 seconds). Ground clauses: seen=87175, kept=87087. Selections=139, assignments=2744, propagations=38790, current_models=0. Rewrite_terms=3013271, rewrite_bools=439548, indexes=313888. Rules_from_neg_clauses=838, cross_offs=447087. ============================== end of statistics ===================== ============================== DOMAIN SIZE 45 ======================== ============================== STATISTICS ============================ For domain size 45. Current CPU time: 0.00 seconds (total CPU time: 50.75 seconds). Ground clauses: seen=93206, kept=93116. Selections=142, assignments=2878, propagations=42461, current_models=0. Rewrite_terms=3276922, rewrite_bools=476236, indexes=338445. Rules_from_neg_clauses=1299, cross_offs=480449. ============================== end of statistics ===================== ============================== DOMAIN SIZE 46 ======================== ============================== STATISTICS ============================ For domain size 46. Current CPU time: 0.00 seconds (total CPU time: 57.31 seconds). Ground clauses: seen=99509, kept=99417. Selections=144, assignments=2969, propagations=42659, current_models=0. Rewrite_terms=3497548, rewrite_bools=518245, indexes=359687. Rules_from_neg_clauses=941, cross_offs=512271. ============================== end of statistics ===================== ============================== DOMAIN SIZE 47 ======================== ============================== STATISTICS ============================ For domain size 47. Current CPU time: 0.00 seconds (total CPU time: 65.09 seconds). Ground clauses: seen=106090, kept=105996. Selections=148, assignments=3155, propagations=46962, current_models=0. Rewrite_terms=3937335, rewrite_bools=595771, indexes=385793. Rules_from_neg_clauses=1231, cross_offs=551769. ============================== end of statistics ===================== ============================== DOMAIN SIZE 48 ======================== ============================== STATISTICS ============================ For domain size 48. Current CPU time: 0.00 seconds (total CPU time: 73.41 seconds). Ground clauses: seen=112955, kept=112859. Selections=149, assignments=3203, propagations=47938, current_models=0. Rewrite_terms=4111731, rewrite_bools=635950, indexes=408061. Rules_from_neg_clauses=1000, cross_offs=595879. ============================== end of statistics ===================== ============================== DOMAIN SIZE 49 ======================== ============================== STATISTICS ============================ For domain size 49. Current CPU time: 0.00 seconds (total CPU time: 83.25 seconds). Ground clauses: seen=120110, kept=120012. Selections=151, assignments=3301, propagations=52238, current_models=0. Rewrite_terms=4621902, rewrite_bools=728827, indexes=436300. Rules_from_neg_clauses=1143, cross_offs=638625. ============================== end of statistics ===================== ============================== DOMAIN SIZE 50 ======================== ============================== STATISTICS ============================ For domain size 50. Current CPU time: 0.00 seconds (total CPU time: 93.16 seconds). Ground clauses: seen=127561, kept=127461. Selections=151, assignments=3302, propagations=52876, current_models=0. Rewrite_terms=4598826, rewrite_bools=696073, indexes=460551. Rules_from_neg_clauses=1251, cross_offs=683470. ============================== end of statistics ===================== ============================== DOMAIN SIZE 51 ======================== ============================== STATISTICS ============================ For domain size 51. Current CPU time: 0.00 seconds (total CPU time: 103.86 seconds). Ground clauses: seen=135314, kept=135212. Selections=153, assignments=3404, propagations=57191, current_models=0. Rewrite_terms=4860651, rewrite_bools=720577, indexes=491933. Rules_from_neg_clauses=1254, cross_offs=727224. ============================== end of statistics ===================== ============================== DOMAIN SIZE 52 ======================== ============================== STATISTICS ============================ For domain size 52. Current CPU time: 0.00 seconds (total CPU time: 115.23 seconds). Ground clauses: seen=143375, kept=143271. Selections=153, assignments=3405, propagations=58413, current_models=0. Rewrite_terms=5031846, rewrite_bools=747465, indexes=518676. Rules_from_neg_clauses=1219, cross_offs=777649. ============================== end of statistics ===================== ============================== DOMAIN SIZE 53 ======================== ============================== STATISTICS ============================ For domain size 53. Current CPU time: 0.00 seconds (total CPU time: 129.19 seconds). Ground clauses: seen=151750, kept=151644. Selections=155, assignments=3511, propagations=62859, current_models=0. Rewrite_terms=5798290, rewrite_bools=879334, indexes=552389. Rules_from_neg_clauses=1376, cross_offs=829092. ============================== end of statistics ===================== ============================== DOMAIN SIZE 54 ======================== ============================== STATISTICS ============================ For domain size 54. Current CPU time: 0.00 seconds (total CPU time: 142.86 seconds). Ground clauses: seen=160445, kept=160337. Selections=155, assignments=3512, propagations=62718, current_models=0. Rewrite_terms=5679678, rewrite_bools=835065, indexes=576821. Rules_from_neg_clauses=1150, cross_offs=874345. ============================== end of statistics ===================== ============================== DOMAIN SIZE 55 ======================== ============================== STATISTICS ============================ For domain size 55. Current CPU time: 0.00 seconds (total CPU time: 158.42 seconds). Ground clauses: seen=169466, kept=169356. Selections=157, assignments=3622, propagations=69050, current_models=0. Rewrite_terms=6195487, rewrite_bools=897970, indexes=618725. Rules_from_neg_clauses=1343, cross_offs=935249. ============================== end of statistics ===================== ============================== DOMAIN SIZE 56 ======================== ============================== STATISTICS ============================ For domain size 56. Current CPU time: 0.00 seconds (total CPU time: 174.48 seconds). Ground clauses: seen=178819, kept=178707. Selections=157, assignments=3623, propagations=69780, current_models=0. Rewrite_terms=6308872, rewrite_bools=900471, indexes=645064. Rules_from_neg_clauses=1268, cross_offs=991359. ============================== end of statistics ===================== ============================== DOMAIN SIZE 57 ======================== ============================== STATISTICS ============================ For domain size 57. Current CPU time: 0.00 seconds (total CPU time: 192.00 seconds). Ground clauses: seen=188510, kept=188396. Selections=159, assignments=3737, propagations=75596, current_models=0. Rewrite_terms=6681852, rewrite_bools=932378, indexes=681247. Rules_from_neg_clauses=1556, cross_offs=1051776. ============================== end of statistics ===================== ============================== DOMAIN SIZE 58 ======================== ============================== STATISTICS ============================ For domain size 58. Current CPU time: 0.00 seconds (total CPU time: 209.97 seconds). Ground clauses: seen=198545, kept=198429. Selections=159, assignments=3738, propagations=75778, current_models=0. Rewrite_terms=6757497, rewrite_bools=945690, indexes=711985. Rules_from_neg_clauses=1507, cross_offs=1112735. ============================== end of statistics ===================== ============================== DOMAIN SIZE 59 ======================== ============================== STATISTICS ============================ For domain size 59. Current CPU time: 0.00 seconds (total CPU time: 228.58 seconds). Ground clauses: seen=208930, kept=208812. Selections=161, assignments=3856, propagations=81502, current_models=0. Rewrite_terms=6922223, rewrite_bools=950553, indexes=749564. Rules_from_neg_clauses=1556, cross_offs=1173669. ============================== end of statistics ===================== ============================== DOMAIN SIZE 60 ======================== ============================== STATISTICS ============================ For domain size 60. Current CPU time: 0.00 seconds (total CPU time: 247.75 seconds). Ground clauses: seen=219671, kept=219551. Selections=161, assignments=3857, propagations=81894, current_models=0. Rewrite_terms=7034669, rewrite_bools=951910, indexes=776203. Rules_from_neg_clauses=1351, cross_offs=1231023. ============================== end of statistics ===================== ============================== DOMAIN SIZE 61 ======================== ============================== STATISTICS ============================ For domain size 61. Current CPU time: 0.00 seconds (total CPU time: 270.00 seconds). Ground clauses: seen=230774, kept=230652. Selections=163, assignments=3979, propagations=89471, current_models=0. Rewrite_terms=7818323, rewrite_bools=1078907, indexes=823319. Rules_from_neg_clauses=1543, cross_offs=1307180. ============================== end of statistics ===================== ============================== DOMAIN SIZE 62 ======================== ============================== STATISTICS ============================ For domain size 62. Current CPU time: 0.00 seconds (total CPU time: 293.69 seconds). Ground clauses: seen=242245, kept=242121. Selections=163, assignments=3980, propagations=89790, current_models=0. Rewrite_terms=8108145, rewrite_bools=1109421, indexes=856804. Rules_from_neg_clauses=1467, cross_offs=1370614. ============================== end of statistics ===================== ============================== DOMAIN SIZE 63 ======================== ============================== STATISTICS ============================ For domain size 63. Current CPU time: 0.00 seconds (total CPU time: 320.98 seconds). Ground clauses: seen=254090, kept=253964. Selections=165, assignments=4106, propagations=98865, current_models=0. Rewrite_terms=9010900, rewrite_bools=1247011, indexes=910893. Rules_from_neg_clauses=2068, cross_offs=1464732. ============================== end of statistics ===================== ============================== DOMAIN SIZE 64 ======================== ============================== STATISTICS ============================ For domain size 64. Current CPU time: 0.00 seconds (total CPU time: 350.20 seconds). Ground clauses: seen=266315, kept=266187. Selections=165, assignments=4107, propagations=97905, current_models=0. Rewrite_terms=9290950, rewrite_bools=1277971, indexes=945655. Rules_from_neg_clauses=1518, cross_offs=1532194. ============================== end of statistics ===================== ============================== DOMAIN SIZE 65 ======================== ============================== STATISTICS ============================ For domain size 65. Current CPU time: 0.00 seconds (total CPU time: 384.31 seconds). Ground clauses: seen=278926, kept=278796. Selections=167, assignments=4237, propagations=105468, current_models=0. Rewrite_terms=9864853, rewrite_bools=1324159, indexes=997118. Rules_from_neg_clauses=1638, cross_offs=1633617. ============================== end of statistics ===================== ============================== DOMAIN SIZE 66 ======================== ============================== STATISTICS ============================ For domain size 66. Current CPU time: 0.00 seconds (total CPU time: 417.51 seconds). Ground clauses: seen=291929, kept=291797. Selections=167, assignments=4238, propagations=107030, current_models=0. Rewrite_terms=10084221, rewrite_bools=1333136, indexes=1034155. Rules_from_neg_clauses=1800, cross_offs=1712148. ============================== end of statistics ===================== ============================== DOMAIN SIZE 67 ======================== ============================== STATISTICS ============================ For domain size 67. Current CPU time: 0.00 seconds (total CPU time: 453.19 seconds). Ground clauses: seen=305330, kept=305196. Selections=168, assignments=4305, propagations=112065, current_models=0. Rewrite_terms=10595981, rewrite_bools=1385061, indexes=1087662. Rules_from_neg_clauses=1549, cross_offs=1792087. ============================== end of statistics ===================== ============================== DOMAIN SIZE 68 ======================== ============================== STATISTICS ============================ For domain size 68. Current CPU time: 0.00 seconds (total CPU time: 491.62 seconds). Ground clauses: seen=319135, kept=318999. Selections=168, assignments=4305, propagations=113086, current_models=0. Rewrite_terms=11106315, rewrite_bools=1466678, indexes=1134427. Rules_from_neg_clauses=1601, cross_offs=1864298. ============================== end of statistics ===================== ============================== DOMAIN SIZE 69 ======================== ============================== STATISTICS ============================ For domain size 69. Current CPU time: 0.00 seconds (total CPU time: 534.69 seconds). Ground clauses: seen=333350, kept=333212. Selections=169, assignments=4373, propagations=119230, current_models=0. Rewrite_terms=11956971, rewrite_bools=1629391, indexes=1198361. Rules_from_neg_clauses=1864, cross_offs=1931345. ============================== end of statistics ===================== ============================== DOMAIN SIZE 70 ======================== ============================== STATISTICS ============================ For domain size 70. Current CPU time: 0.00 seconds (total CPU time: 578.80 seconds). Ground clauses: seen=347981, kept=347841. Selections=170, assignments=4442, propagations=123534, current_models=0. Rewrite_terms=12159661, rewrite_bools=1654137, indexes=1236966. Rules_from_neg_clauses=1813, cross_offs=1970296. ============================== end of statistics ===================== ============================== DOMAIN SIZE 71 ======================== ============================== STATISTICS ============================ For domain size 71. Current CPU time: 0.00 seconds (total CPU time: 625.66 seconds). Ground clauses: seen=363034, kept=362892. Selections=171, assignments=4512, propagations=127974, current_models=0. Rewrite_terms=12366346, rewrite_bools=1680236, indexes=1275532. Rules_from_neg_clauses=1766, cross_offs=2009560. ============================== end of statistics ===================== ============================== DOMAIN SIZE 72 ======================== ============================== STATISTICS ============================ For domain size 72. Current CPU time: 0.00 seconds (total CPU time: 677.06 seconds). Ground clauses: seen=378515, kept=378371. Selections=172, assignments=4583, propagations=132835, current_models=0. Rewrite_terms=12580311, rewrite_bools=1709491, indexes=1313757. Rules_from_neg_clauses=1709, cross_offs=2048699. ============================== end of statistics ===================== ============================== DOMAIN SIZE 73 ======================== ============================== MODEL ================================= interpretation( 73, [number=1, seconds=727], [ function(a1, [ 0 ]), function(a10, [ 1 ]), function(a2, [ 3 ]), function(a3, [35 ]), function(a4, [ 2 ]), function(a5, [ 6 ]), function(a6, [17 ]), function(a7, [47 ]), function(a8, [66 ]), function(a9, [ 7 ]), function(*(_,_), [ 0, 3, 1, 9, 8, 7, 5,15,22,27,16,25,13,21,19,33,32,28,30,39,37,45,44,43,38,51,49,64,55,58,69,67,65,61,52,57,72,70,59,68,63,71,62,60,54,50,66,53,56,46,47,40,42,41,48,31,36,26,34,29,35,18,24,10,20,11,23,14,17, 6, 2,12, 4, 5, 1, 0, 8, 3,13, 7,19,16,25, 9,22,15,28,21,37,30,33,27,43,39,52,38,45,32,49,44,58,57,51,67,64,72,63,55,61,69,71,62,66,70,68,65,53,56,48,60,50,59,47,54,41,36,46,42,29,31,24,35,26,40,11,18, 4,23,10,34,17,20,12, 6,14, 2, 6, 4, 2,11,10,14,12,20,24,29,18,26,17,34,23,40,36,35,31,46,41,54,48,47,42,53,50,66,59,60,71,68,63,65,56,62,70,69,57,64,72,67,61,51,52,44,58,49,55,43,45,37,32,39,38,27,30,22,28,25,33, 9,16, 3,19, 8,21,13,15, 5, 0, 7, 1, 7, 0, 5, 3, 1,15,13,21, 9,22, 8,16,19,33,28,39,27,37,25,45,43,55,32,52,30,44,38,51,61,49,64,58,69,70,57,63,67,68,65,60,71,66,72,50,59,42,53,48,62,54,56,46,31,47,36,26,29,18,40,24,41,10,11, 2,34, 4,35,20,23,14,12,17, 6, 12, 2, 6,10, 4,17,14,23,18,26,11,24,20,35,34,41,31,40,29,47,46,56,42,54,36,50,48,60,62,53,68,66,70,72,59,65,71,67,61,58,69,64,63,49,55,38,51,44,57,45,52,39,30,43,32,25,27,16,33,22,37, 8, 9, 1,21, 3,28,15,19, 7, 5,13, 0, 1, 8, 3,16, 9, 5, 0,13,25,30,22,27, 7,19,15,28,38,21,32,37,33,43,49,39,44,58,51,67,52,64,72,69,62,57,45,55,65,63,56,71,61,70,59,66,47,53,68,60,54,41,46,35,48,40,50,36,42,29,23,31,34,24,26,11,17,18,20,12,14, 2, 4, 6,10, 2,10, 4,18,11,12, 6,17,26,31,24,29,14,23,20,35,42,34,36,41,40,47,50,46,48,60,53,68,56,66,70,71,61,62,54,59,63,72,55,67,65,69,57,58,45,49,64,51,52,39,43,33,38,37,44,30,32,25,21,27,28,16,22, 8,15, 9,19, 7,13, 0, 1, 5, 3, 3, 9, 8,22,16, 0, 1, 7,27,32,25,30, 5,15,13,21,44,19,38,33,28,39,51,37,49,64,58,69,45,67,65,72,59,55,43,52,62,61,54,70,57,63,56,68,46,60,71,66,47,40,41,34,50,35,53,42,48,31,20,36,23,26,29,18,14,24,17, 6,12, 4,10, 2,11, 13, 5, 7, 1, 0,19,15,28, 8,16, 3, 9,21,37,33,43,25,39,22,52,45,57,30,55,27,38,32,49,63,44,58,51,67,71,61,70,64,66,72,53,68,60,69,48,62,36,50,42,65,56,59,47,29,54,31,24,26,11,41,18,46, 4,10, 6,35, 2,40,23,34,17,14,20,12, 15, 7,13, 0, 5,21,19,33, 3, 9, 1, 8,28,39,37,45,22,43,16,55,52,61,27,57,25,32,30,44,70,38,51,49,64,68,63,71,58,60,69,50,66,53,67,42,65,31,48,36,72,59,62,54,26,56,29,18,24,10,46,11,47, 2, 4,12,40, 6,41,34,35,20,17,23,14, 14, 6,12, 4, 2,20,17,34,11,24,10,18,23,40,35,46,29,41,26,54,47,59,36,56,31,48,42,53,65,50,66,60,71,69,62,72,68,64,63,51,67,58,70,44,57,32,49,38,61,52,55,43,27,45,30,22,25, 9,37,16,39, 3, 8, 0,28, 1,33,19,21,13, 7,15, 5, 17,12,14, 2, 6,23,20,35,10,18, 4,11,34,41,40,47,26,46,24,56,54,62,31,59,29,42,36,50,72,48,60,53,68,67,65,69,66,58,70,49,64,51,71,38,61,30,44,32,63,55,57,45,25,52,27,16,22, 8,39, 9,43, 1, 3, 5,33, 0,37,21,28,15,13,19, 7, 4,11,10,24,18, 6, 2,14,29,36,26,31,12,20,17,34,48,23,42,40,35,46,53,41,50,66,60,71,54,68,63,70,57,59,47,56,61,65,52,69,62,72,55,64,43,51,67,58,45,37,39,28,44,33,49,32,38,27,19,30,21,22,25, 9,13,16,15, 5, 7, 1, 3, 0, 8, 8,16, 9,25,22, 1, 3, 5,30,38,27,32, 0,13, 7,19,49,15,44,28,21,37,58,33,51,67,64,72,43,69,62,65,56,52,39,45,59,57,47,63,55,61,54,71,41,66,70,68,46,35,40,23,53,34,60,48,50,36,17,42,20,29,31,24,12,26,14, 2, 6,10,11, 4,18, 10,18,11,26,24, 2, 4,12,31,42,29,36, 6,17,14,23,50,20,48,35,34,41,60,40,53,68,66,70,47,71,61,63,55,56,46,54,57,62,45,72,59,65,52,67,39,58,69,64,43,33,37,21,49,28,51,38,44,30,15,32,19,25,27,16, 7,22,13, 0, 5, 3, 8, 1, 9, 9,22,16,27,25, 3, 8, 0,32,44,30,38, 1, 7, 5,15,51,13,49,21,19,33,64,28,58,69,67,65,39,72,59,62,54,45,37,43,56,55,46,61,52,57,47,70,40,68,63,71,41,34,35,20,60,23,66,50,53,42,14,48,17,31,36,26, 6,29,12, 4, 2,11,18,10,24, 19,13,15, 5, 7,28,21,37, 1, 8, 0, 3,33,43,39,52,16,45, 9,57,55,63,25,61,22,30,27,38,71,32,49,44,58,66,70,68,51,53,67,48,60,50,64,36,72,29,42,31,69,62,65,56,24,59,26,11,18, 4,47,10,54, 6, 2,14,41,12,46,35,40,23,20,34,17, 11,24,18,29,26, 4,10, 6,36,48,31,42, 2,14,12,20,53,17,50,34,23,40,66,35,60,71,68,63,46,70,57,61,52,54,41,47,55,59,43,65,56,62,45,69,37,64,72,67,39,28,33,19,51,21,58,44,49,32,13,38,15,27,30,22, 5,25, 7, 1, 0, 8, 9, 3,16, 20,14,17, 6,12,34,23,40, 4,11, 2,10,35,46,41,54,24,47,18,59,56,65,29,62,26,36,31,48,69,42,53,50,66,64,72,67,60,51,71,44,58,49,68,32,63,27,38,30,70,57,61,52,22,55,25, 9,16, 3,43, 8,45, 0, 1, 7,37, 5,39,28,33,19,15,21,13, 16,25,22,30,27, 8, 9, 1,38,49,32,44, 3, 5, 0,13,58, 7,51,19,15,28,67,21,64,72,69,62,37,65,56,59,47,43,33,39,54,52,41,57,45,55,46,63,35,71,61,70,40,23,34,17,66,20,68,53,60,48,12,50,14,36,42,29, 2,31, 6,10, 4,18,24,11,26, 18,26,24,31,29,10,11, 2,42,50,36,48, 4,12, 6,17,60,14,53,23,20,35,68,34,66,70,71,61,41,63,55,57,45,47,40,46,52,56,39,62,54,59,43,72,33,67,65,69,37,21,28,15,58,19,64,49,51,38, 7,44,13,30,32,25, 0,27, 5, 3, 1, 9,16, 8,22, 22,27,25,32,30, 9,16, 3,44,51,38,49, 8, 0, 1, 7,64, 5,58,15,13,21,69,19,67,65,72,59,33,62,54,56,46,39,28,37,47,45,40,55,43,52,41,61,34,70,57,63,35,20,23,14,68,17,71,60,66,50, 6,53,12,42,48,31, 4,36, 2,11,10,24,26,18,29, 21,15,19, 7,13,33,28,39, 0, 3, 5, 1,37,45,43,55, 9,52, 8,61,57,70,22,63,16,27,25,32,68,30,44,38,51,60,71,66,49,50,64,42,53,48,58,31,69,26,36,29,67,65,72,59,18,62,24,10,11, 2,54, 4,56,12, 6,17,46,14,47,40,41,34,23,35,20, 24,29,26,36,31,11,18, 4,48,53,42,50,10, 6, 2,14,66,12,60,20,17,34,71,23,68,63,70,57,40,61,52,55,43,46,35,41,45,54,37,59,47,56,39,65,28,69,62,72,33,19,21,13,64,15,67,51,58,44, 5,49, 7,32,38,27, 1,30, 0, 8, 3,16,22, 9,25, 23,17,20,12,14,35,34,41, 2,10, 6, 4,40,47,46,56,18,54,11,62,59,72,26,65,24,31,29,42,67,36,50,48,60,58,69,64,53,49,68,38,51,44,66,30,70,25,32,27,71,61,63,55,16,57,22, 8, 9, 1,45, 3,52, 5, 0,13,39, 7,43,33,37,21,19,28,15, 28,19,21,13,15,37,33,43, 5, 1, 7, 0,39,52,45,57, 8,55, 3,63,61,71,16,70, 9,25,22,30,66,27,38,32,49,53,68,60,44,48,58,36,50,42,51,29,67,24,31,26,64,72,69,62,11,65,18, 4,10, 6,56, 2,59,14,12,20,47,17,54,41,46,35,34,40,23, 34,20,23,14,17,40,35,46, 6, 4,12, 2,41,54,47,59,11,56,10,65,62,69,24,72,18,29,26,36,64,31,48,42,53,51,67,58,50,44,66,32,49,38,60,27,71,22,30,25,68,63,70,57, 9,61,16, 3, 8, 0,52, 1,55, 7, 5,15,43,13,45,37,39,28,21,33,19, 33,21,28,15,19,39,37,45, 7, 0,13, 5,43,55,52,61, 3,57, 1,70,63,68, 9,71, 8,22,16,27,60,25,32,30,44,50,66,53,38,42,51,31,48,36,49,26,64,18,29,24,58,69,67,65,10,72,11, 2, 4,12,59, 6,62,17,14,23,54,20,56,46,47,40,35,41,34, 25,30,27,38,32,16,22, 8,49,58,44,51, 9, 1, 3, 5,67, 0,64,13, 7,19,72,15,69,62,65,56,28,59,47,54,41,37,21,33,46,43,35,52,39,45,40,57,23,63,55,61,34,17,20,12,71,14,70,66,68,53, 2,60, 6,48,50,36,10,42, 4,18,11,26,29,24,31, 35,23,34,17,20,41,40,47,12, 2,14, 6,46,56,54,62,10,59, 4,72,65,67,18,69,11,26,24,31,58,29,42,36,50,49,64,51,48,38,60,30,44,32,53,25,68,16,27,22,66,70,71,61, 8,63, 9, 1, 3, 5,55, 0,57,13, 7,19,45,15,52,39,43,33,28,37,21, 37,28,33,19,21,43,39,52,13, 5,15, 7,45,57,55,63, 1,61, 0,71,70,66, 8,68, 3,16, 9,25,53,22,30,27,38,48,60,50,32,36,49,29,42,31,44,24,58,11,26,18,51,67,64,72, 4,69,10, 6, 2,14,62,12,65,20,17,34,56,23,59,47,54,41,40,46,35, 40,34,35,20,23,46,41,54,14, 6,17,12,47,59,56,65, 4,62, 2,69,72,64,11,67,10,24,18,29,51,26,36,31,48,44,58,49,42,32,53,27,38,30,50,22,66, 9,25,16,60,71,68,63, 3,70, 8, 0, 1, 7,57, 5,61,15,13,21,52,19,55,43,45,37,33,39,28, 39,33,37,21,28,45,43,55,15, 7,19,13,52,61,57,70, 0,63, 5,68,71,60, 3,66, 1, 9, 8,22,50,16,27,25,32,42,53,48,30,31,44,26,36,29,38,18,51,10,24,11,49,64,58,69, 2,67, 4,12, 6,17,65,14,72,23,20,35,59,34,62,54,56,46,41,47,40, 27,32,30,44,38,22,25, 9,51,64,49,58,16, 3, 8, 0,69, 1,67, 7, 5,15,65,13,72,59,62,54,21,56,46,47,40,33,19,28,41,39,34,45,37,43,35,55,20,61,52,57,23,14,17, 6,70,12,63,68,71,60, 4,66, 2,50,53,42,11,48,10,24,18,29,31,26,36, 26,31,29,42,36,18,24,10,50,60,48,53,11, 2, 4,12,68, 6,66,17,14,23,70,20,71,61,63,55,35,57,45,52,39,41,34,40,43,47,33,56,46,54,37,62,21,72,59,65,28,15,19, 7,67,13,69,58,64,49, 0,51, 5,38,44,30, 3,32, 1, 9, 8,22,25,16,27, 29,36,31,48,42,24,26,11,53,66,50,60,18, 4,10, 6,71, 2,68,14,12,20,63,17,70,57,61,52,34,55,43,45,37,40,23,35,39,46,28,54,41,47,33,59,19,65,56,62,21,13,15, 5,69, 7,72,64,67,51, 1,58, 0,44,49,32, 8,38, 3,16, 9,25,27,22,30, 41,35,40,23,34,47,46,56,17,12,20,14,54,62,59,72, 2,65, 6,67,69,58,10,64, 4,18,11,26,49,24,31,29,42,38,51,44,36,30,50,25,32,27,48,16,60, 8,22, 9,53,68,66,70, 1,71, 3, 5, 0,13,61, 7,63,19,15,28,55,21,57,45,52,39,37,43,33, 30,38,32,49,44,25,27,16,58,67,51,64,22, 8, 9, 1,72, 3,69, 5, 0,13,62, 7,65,56,59,47,19,54,41,46,35,28,15,21,40,37,23,43,33,39,34,52,17,57,45,55,20,12,14, 2,63, 6,61,71,70,66,10,68, 4,53,60,48,18,50,11,26,24,31,36,29,42, 43,37,39,28,33,52,45,57,19,13,21,15,55,63,61,71, 5,70, 7,66,68,53, 1,60, 0, 8, 3,16,48, 9,25,22,30,36,50,42,27,29,38,24,31,26,32,11,49, 4,18,10,44,58,51,67, 6,64, 2,14,12,20,72,17,69,34,23,40,62,35,65,56,59,47,46,54,41, 32,44,38,51,49,27,30,22,64,69,58,67,25, 9,16, 3,65, 8,72, 0, 1, 7,59, 5,62,54,56,46,15,47,40,41,34,21,13,19,35,33,20,39,28,37,23,45,14,55,43,52,17, 6,12, 4,61, 2,57,70,63,68,11,71,10,60,66,50,24,53,18,29,26,36,42,31,48, 31,42,36,50,48,26,29,18,60,68,53,66,24,10,11, 2,70, 4,71,12, 6,17,61,14,63,55,57,45,23,52,39,43,33,35,20,34,37,41,21,47,40,46,28,56,15,62,54,59,19, 7,13, 0,72, 5,65,67,69,58, 3,64, 1,49,51,38, 9,44, 8,22,16,27,30,25,32, 36,48,42,53,50,29,31,24,66,71,60,68,26,11,18, 4,63,10,70, 6, 2,14,57,12,61,52,55,43,20,45,37,39,28,34,17,23,33,40,19,46,35,41,21,54,13,59,47,56,15, 5, 7, 1,65, 0,62,69,72,64, 8,67, 3,51,58,44,16,49, 9,25,22,30,32,27,38, 46,40,41,34,35,54,47,59,20,14,23,17,56,65,62,69, 6,72,12,64,67,51, 4,58, 2,11,10,24,44,18,29,26,36,32,49,38,31,27,48,22,30,25,42, 9,53, 3,16, 8,50,66,60,71, 0,68, 1, 7, 5,15,63,13,70,21,19,33,57,28,61,52,55,43,39,45,37, 38,49,44,58,51,30,32,25,67,72,64,69,27,16,22, 8,62, 9,65, 1, 3, 5,56, 0,59,47,54,41,13,46,35,40,23,19, 7,15,34,28,17,37,21,33,20,43,12,52,39,45,14, 2, 6,10,57, 4,55,63,61,71,18,70,11,66,68,53,26,60,24,31,29,42,48,36,50, 45,39,43,33,37,55,52,61,21,15,28,19,57,70,63,68, 7,71,13,60,66,50, 0,53, 5, 3, 1, 9,42, 8,22,16,27,31,48,36,25,26,32,18,29,24,30,10,44, 2,11, 4,38,51,49,64,12,58, 6,17,14,23,69,20,67,35,34,41,65,40,72,59,62,54,47,56,46, 44,51,49,64,58,32,38,27,69,65,67,72,30,22,25, 9,59,16,62, 3, 8, 0,54, 1,56,46,47,40, 7,41,34,35,20,15, 5,13,23,21,14,33,19,28,17,39, 6,45,37,43,12, 4, 2,11,55,10,52,61,57,70,24,63,18,68,71,60,29,66,26,36,31,48,50,42,53, 42,50,48,60,53,31,36,26,68,70,66,71,29,18,24,10,61,11,63, 2, 4,12,55, 6,57,45,52,39,17,43,33,37,21,23,14,20,28,35,15,41,34,40,19,47, 7,56,46,54,13, 0, 5, 3,62, 1,59,72,65,67, 9,69, 8,58,64,49,22,51,16,27,25,32,38,30,44, 48,53,50,66,60,36,42,29,71,63,68,70,31,24,26,11,57,18,61, 4,10, 6,52, 2,55,43,45,37,14,39,28,33,19,20,12,17,21,34,13,40,23,35,15,46, 5,54,41,47, 7, 1, 0, 8,59, 3,56,65,62,69,16,72, 9,64,67,51,25,58,22,30,27,38,44,32,49, 47,41,46,35,40,56,54,62,23,17,34,20,59,72,65,67,12,69,14,58,64,49, 2,51, 6,10, 4,18,38,11,26,24,31,30,44,32,29,25,42,16,27,22,36, 8,50, 1, 9, 3,48,60,53,68, 5,66, 0,13, 7,19,70,15,71,28,21,37,61,33,63,55,57,45,43,52,39, 52,43,45,37,39,57,55,63,28,19,33,21,61,71,70,66,13,68,15,53,60,48, 5,50, 7, 1, 0, 8,36, 3,16, 9,25,29,42,31,22,24,30,11,26,18,27, 4,38, 6,10, 2,32,49,44,58,14,51,12,20,17,34,67,23,64,40,35,46,72,41,69,62,65,56,54,59,47, 54,46,47,40,41,59,56,65,34,20,35,23,62,69,72,64,14,67,17,51,58,44, 6,49,12, 4, 2,11,32,10,24,18,29,27,38,30,26,22,36, 9,25,16,31, 3,48, 0, 8, 1,42,53,50,66, 7,60, 5,15,13,21,71,19,68,33,28,39,63,37,70,57,61,52,45,55,43, 55,45,52,39,43,61,57,70,33,21,37,28,63,68,71,60,15,66,19,50,53,42, 7,48,13, 0, 5, 3,31, 1, 9, 8,22,26,36,29,16,18,27,10,24,11,25, 2,32,12, 4, 6,30,44,38,51,17,49,14,23,20,35,64,34,58,41,40,47,69,46,67,65,72,59,56,62,54, 49,58,51,67,64,38,44,30,72,62,69,65,32,25,27,16,56,22,59, 8, 9, 1,47, 3,54,41,46,35, 5,40,23,34,17,13, 0, 7,20,19,12,28,15,21,14,37, 2,43,33,39, 6,10, 4,18,52,11,45,57,55,63,26,61,24,71,70,66,31,68,29,42,36,50,53,48,60, 56,47,54,41,46,62,59,72,35,23,40,34,65,67,69,58,17,64,20,49,51,38,12,44,14, 2, 6,10,30, 4,18,11,26,25,32,27,24,16,31, 8,22, 9,29, 1,42, 5, 3, 0,36,50,48,60,13,53, 7,19,15,28,68,21,66,37,33,43,70,39,71,61,63,55,52,57,45, 50,60,53,68,66,42,48,31,70,61,71,63,36,26,29,18,55,24,57,10,11, 2,45, 4,52,39,43,33,12,37,21,28,15,17, 6,14,19,23, 7,35,20,34,13,41, 0,47,40,46, 5, 3, 1, 9,56, 8,54,62,59,72,22,65,16,67,69,58,27,64,25,32,30,44,49,38,51, 51,64,58,69,67,44,49,32,65,59,72,62,38,27,30,22,54,25,56, 9,16, 3,46, 8,47,40,41,34, 0,35,20,23,14, 7, 1, 5,17,15, 6,21,13,19,12,33, 4,39,28,37, 2,11,10,24,45,18,43,55,52,61,29,57,26,70,63,68,36,71,31,48,42,53,60,50,66, 53,66,60,71,68,48,50,36,63,57,70,61,42,29,31,24,52,26,55,11,18, 4,43,10,45,37,39,28, 6,33,19,21,13,14, 2,12,15,20, 5,34,17,23, 7,40, 1,46,35,41, 0, 8, 3,16,54, 9,47,59,56,65,25,62,22,69,72,64,30,67,27,38,32,49,51,44,58, 58,67,64,72,69,49,51,38,62,56,65,59,44,30,32,25,47,27,54,16,22, 8,41, 9,46,35,40,23, 1,34,17,20,12, 5, 3, 0,14,13, 2,19, 7,15, 6,28,10,37,21,33, 4,18,11,26,43,24,39,52,45,57,31,55,29,63,61,71,42,70,36,50,48,60,66,53,68, 57,52,55,43,45,63,61,71,37,28,39,33,70,66,68,53,19,60,21,48,50,36,13,42,15, 5, 7, 1,29, 0, 8, 3,16,24,31,26, 9,11,25, 4,18,10,22, 6,30,14, 2,12,27,38,32,49,20,44,17,34,23,40,58,35,51,46,41,54,67,47,64,72,69,62,59,65,56, 60,68,66,70,71,50,53,42,61,55,63,57,48,31,36,26,45,29,52,18,24,10,39,11,43,33,37,21, 2,28,15,19, 7,12, 4, 6,13,17, 0,23,14,20, 5,35, 3,41,34,40, 1, 9, 8,22,47,16,46,56,54,62,27,59,25,72,65,67,32,69,30,44,38,51,58,49,64, 59,54,56,46,47,65,62,69,40,34,41,35,72,64,67,51,20,58,23,44,49,32,14,38,17, 6,12, 4,27, 2,11,10,24,22,30,25,18, 9,29, 3,16, 8,26, 0,36, 7, 1, 5,31,48,42,53,15,50,13,21,19,33,66,28,60,39,37,45,71,43,68,63,70,57,55,61,52, 64,69,67,65,72,51,58,44,59,54,62,56,49,32,38,27,46,30,47,22,25, 9,40,16,41,34,35,20, 3,23,14,17, 6, 0, 8, 1,12, 7, 4,15, 5,13, 2,21,11,33,19,28,10,24,18,29,39,26,37,45,43,55,36,52,31,61,57,70,48,63,42,53,50,66,68,60,71, 66,71,68,63,70,53,60,48,57,52,61,55,50,36,42,29,43,31,45,24,26,11,37,18,39,28,33,19, 4,21,13,15, 5, 6,10, 2, 7,14, 1,20,12,17, 0,34, 8,40,23,35, 3,16, 9,25,46,22,41,54,47,59,30,56,27,65,62,69,38,72,32,49,44,58,64,51,67, 67,72,69,62,65,58,64,49,56,47,59,54,51,38,44,30,41,32,46,25,27,16,35,22,40,23,34,17, 8,20,12,14, 2, 1, 9, 3, 6, 5,10,13, 0, 7, 4,19,18,28,15,21,11,26,24,31,37,29,33,43,39,52,42,45,36,57,55,63,50,61,48,60,53,68,71,66,70, 61,55,57,45,52,70,63,68,39,33,43,37,71,60,66,50,21,53,28,42,48,31,15,36,19, 7,13, 0,26, 5, 3, 1, 9,18,29,24, 8,10,22, 2,11, 4,16,12,27,17, 6,14,25,32,30,44,23,38,20,35,34,41,51,40,49,47,46,56,64,54,58,69,67,65,62,72,59, 68,70,71,61,63,60,66,50,55,45,57,52,53,42,48,31,39,36,43,26,29,18,33,24,37,21,28,15,10,19, 7,13, 0, 2,11, 4, 5,12, 3,17, 6,14, 1,23, 9,35,20,34, 8,22,16,27,41,25,40,47,46,56,32,54,30,62,59,72,44,65,38,51,49,64,67,58,69, 62,56,59,47,54,72,65,67,41,35,46,40,69,58,64,49,23,51,34,38,44,30,17,32,20,12,14, 2,25, 6,10, 4,18,16,27,22,11, 8,26, 1, 9, 3,24, 5,31,13, 0, 7,29,42,36,50,19,48,15,28,21,37,60,33,53,43,39,52,68,45,66,70,71,61,57,63,55, 63,57,61,52,55,71,70,66,43,37,45,39,68,53,60,48,28,50,33,36,42,29,19,31,21,13,15, 5,24, 7, 1, 0, 8,11,26,18, 3, 4,16, 6,10, 2, 9,14,25,20,12,17,22,30,27,38,34,32,23,40,35,46,49,41,44,54,47,59,58,56,51,67,64,72,65,69,62, 65,59,62,54,56,69,72,64,46,40,47,41,67,51,58,44,34,49,35,32,38,27,20,30,23,14,17, 6,22,12, 4, 2,11, 9,25,16,10, 3,24, 0, 8, 1,18, 7,29,15, 5,13,26,36,31,48,21,42,19,33,28,39,53,37,50,45,43,55,66,52,60,71,68,63,61,70,57, 70,61,63,55,57,68,71,60,45,39,52,43,66,50,53,42,33,48,37,31,36,26,21,29,28,15,19, 7,18,13, 0, 5, 3,10,24,11, 1, 2, 9,12, 4, 6, 8,17,22,23,14,20,16,27,25,32,35,30,34,41,40,47,44,46,38,56,54,62,51,59,49,64,58,69,72,67,65, 69,65,72,59,62,64,67,51,54,46,56,47,58,44,49,32,40,38,41,27,30,22,34,25,35,20,23,14, 9,17, 6,12, 4, 3,16, 8, 2, 0,11, 7, 1, 5,10,15,24,21,13,19,18,29,26,36,33,31,28,39,37,45,48,43,42,55,52,61,53,57,50,66,60,71,70,68,63, 72,62,65,56,59,67,69,58,47,41,54,46,64,49,51,38,35,44,40,30,32,25,23,27,34,17,20,12,16,14, 2, 6,10, 8,22, 9, 4, 1,18, 5, 3, 0,11,13,26,19, 7,15,24,31,29,42,28,36,21,37,33,43,50,39,48,52,45,57,60,55,53,68,66,70,63,71,61, 71,63,70,57,61,66,68,53,52,43,55,45,60,48,50,36,37,42,39,29,31,24,28,26,33,19,21,13,11,15, 5, 7, 1, 4,18,10, 0, 6, 8,14, 2,12, 3,20,16,34,17,23, 9,25,22,30,40,27,35,46,41,54,38,47,32,59,56,65,49,62,44,58,51,67,69,64,72 ]) ]). ============================== end of model ========================== ============================== STATISTICS ============================ For domain size 73. Current CPU time: 0.00 seconds (total CPU time: 728.36 seconds). Ground clauses: seen=394430, kept=394284. Selections=173, assignments=4655, propagations=137894, current_models=1. Rewrite_terms=13001692, rewrite_bools=1809819, indexes=1351952. Rules_from_neg_clauses=1648, cross_offs=2088081. ============================== end of statistics ===================== User_CPU=728.36, System_CPU=0.14, Wall_clock=732. Exiting with 1 model. Process 3996 exit (max_models) Sun Mar 17 13:30:23 2013 The process finished Sun Mar 17 13:30:23 2013