============================== Mace4 ================================= Mace4 (32) version Dec-2007, Dec 2007. Process 2788 was started by Alexei on Alexei-PC, Sun Mar 24 22:01:01 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). assign(max_megs,1200). end_if. formulas(assumptions). x * x = x. (x * y) * y = x. (x * y) * z = (x * z) * (y * z). a2 = a1 * a8. a3 = a2 * a10. a4 = a3 * a7. a5 = a4 * a1. a6 = a5 * a9. a7 = a6 * a2. a8 = a7 * a4. a9 = a8 * a5. a10 = a9 * a6. a1 = a10 * a3. 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 * a8. a3 = a2 * a10. a4 = a3 * a7. a5 = a4 * a1. a6 = a5 * a9. a7 = a6 * a2. a8 = a7 * a4. a9 = a8 * a5. a10 = a9 * a6. a1 = a10 * a3. a1 != a2 | a3 != a2 | a4 != a3 | a5 != a4 | a6 != a5 | a6 != a7 | 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.03 seconds). Ground clauses: seen=25, kept=15. Selections=5, assignments=9, propagations=16, current_models=0. Rewrite_terms=80, rewrite_bools=22, 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.03 seconds). Ground clauses: seen=50, kept=44. Selections=10, assignments=24, propagations=69, current_models=0. Rewrite_terms=787, rewrite_bools=182, indexes=64. Rules_from_neg_clauses=16, cross_offs=44. ============================== end of statistics ===================== ============================== DOMAIN SIZE 4 ========================= ============================== STATISTICS ============================ For domain size 4. Current CPU time: 0.00 seconds (total CPU time: 0.03 seconds). Ground clauses: seen=95, kept=87. Selections=18, assignments=57, propagations=146, current_models=0. Rewrite_terms=2066, rewrite_bools=424, indexes=201. Rules_from_neg_clauses=24, cross_offs=113. ============================== end of statistics ===================== ============================== DOMAIN SIZE 5 ========================= ============================== STATISTICS ============================ For domain size 5. Current CPU time: 0.00 seconds (total CPU time: 0.03 seconds). Ground clauses: seen=166, kept=156. Selections=28, assignments=108, propagations=268, current_models=0. Rewrite_terms=4560, rewrite_bools=865, indexes=525. Rules_from_neg_clauses=44, cross_offs=333. ============================== end of statistics ===================== ============================== DOMAIN SIZE 6 ========================= ============================== STATISTICS ============================ For domain size 6. Current CPU time: 0.00 seconds (total CPU time: 0.03 seconds). Ground clauses: seen=269, kept=257. Selections=39, assignments=176, propagations=528, current_models=0. Rewrite_terms=10716, rewrite_bools=2222, indexes=1042. Rules_from_neg_clauses=88, cross_offs=786. ============================== end of statistics ===================== ============================== DOMAIN SIZE 7 ========================= ============================== STATISTICS ============================ For domain size 7. Current CPU time: 0.00 seconds (total CPU time: 0.05 seconds). Ground clauses: seen=410, kept=396. Selections=57, assignments=301, propagations=971, current_models=0. Rewrite_terms=20344, rewrite_bools=3791, indexes=2450. Rules_from_neg_clauses=128, cross_offs=1609. ============================== end of statistics ===================== ============================== DOMAIN SIZE 8 ========================= ============================== STATISTICS ============================ For domain size 8. Current CPU time: 0.00 seconds (total CPU time: 0.05 seconds). Ground clauses: seen=595, kept=579. Selections=73, assignments=424, propagations=1419, current_models=0. Rewrite_terms=31513, rewrite_bools=5473, indexes=3938. Rules_from_neg_clauses=136, cross_offs=2922. ============================== end of statistics ===================== ============================== DOMAIN SIZE 9 ========================= ============================== STATISTICS ============================ For domain size 9. Current CPU time: 0.00 seconds (total CPU time: 0.06 seconds). Ground clauses: seen=830, kept=812. Selections=107, assignments=717, propagations=2450, current_models=0. Rewrite_terms=60734, rewrite_bools=11118, indexes=6962. Rules_from_neg_clauses=222, cross_offs=5327. ============================== end of statistics ===================== ============================== DOMAIN SIZE 10 ======================== ============================== STATISTICS ============================ For domain size 10. Current CPU time: 0.00 seconds (total CPU time: 0.08 seconds). Ground clauses: seen=1121, kept=1101. Selections=134, assignments=978, propagations=3412, current_models=0. Rewrite_terms=84609, rewrite_bools=14526, indexes=10931. Rules_from_neg_clauses=274, cross_offs=8073. ============================== end of statistics ===================== ============================== DOMAIN SIZE 11 ======================== ============================== STATISTICS ============================ For domain size 11. Current CPU time: 0.00 seconds (total CPU time: 0.08 seconds). Ground clauses: seen=1474, kept=1452. Selections=163, assignments=1280, propagations=4688, current_models=0. Rewrite_terms=114466, rewrite_bools=18196, indexes=15502. Rules_from_neg_clauses=309, cross_offs=11964. ============================== end of statistics ===================== ============================== DOMAIN SIZE 12 ======================== ============================== STATISTICS ============================ For domain size 12. Current CPU time: 0.00 seconds (total CPU time: 0.12 seconds). Ground clauses: seen=1895, kept=1871. Selections=214, assignments=1867, propagations=7596, current_models=0. Rewrite_terms=216686, rewrite_bools=38351, indexes=24790. Rules_from_neg_clauses=498, cross_offs=19981. ============================== end of statistics ===================== ============================== DOMAIN SIZE 13 ======================== ============================== STATISTICS ============================ For domain size 13. Current CPU time: 0.00 seconds (total CPU time: 0.20 seconds). Ground clauses: seen=2390, kept=2364. Selections=258, assignments=2428, propagations=10187, current_models=0. Rewrite_terms=276597, rewrite_bools=45152, indexes=36353. Rules_from_neg_clauses=548, cross_offs=28212. ============================== end of statistics ===================== ============================== DOMAIN SIZE 14 ======================== ============================== STATISTICS ============================ For domain size 14. Current CPU time: 0.00 seconds (total CPU time: 0.28 seconds). Ground clauses: seen=2965, kept=2937. Selections=290, assignments=2856, propagations=12819, current_models=0. Rewrite_terms=351712, rewrite_bools=54122, indexes=47453. Rules_from_neg_clauses=698, cross_offs=39414. ============================== end of statistics ===================== ============================== DOMAIN SIZE 15 ======================== ============================== STATISTICS ============================ For domain size 15. Current CPU time: 0.00 seconds (total CPU time: 0.44 seconds). Ground clauses: seen=3626, kept=3596. Selections=363, assignments=3905, propagations=18502, current_models=0. Rewrite_terms=531101, rewrite_bools=84626, indexes=69173. Rules_from_neg_clauses=1031, cross_offs=59400. ============================== end of statistics ===================== ============================== DOMAIN SIZE 16 ======================== ============================== STATISTICS ============================ For domain size 16. Current CPU time: 0.00 seconds (total CPU time: 0.66 seconds). Ground clauses: seen=4379, kept=4347. Selections=428, assignments=4909, propagations=24537, current_models=0. Rewrite_terms=679256, rewrite_bools=102912, indexes=92874. Rules_from_neg_clauses=1161, cross_offs=78555. ============================== end of statistics ===================== ============================== DOMAIN SIZE 17 ======================== ============================== STATISTICS ============================ For domain size 17. Current CPU time: 0.00 seconds (total CPU time: 0.95 seconds). Ground clauses: seen=5230, kept=5196. Selections=494, assignments=5985, propagations=31817, current_models=0. Rewrite_terms=878948, rewrite_bools=127658, indexes=124677. Rules_from_neg_clauses=1380, cross_offs=106351. ============================== end of statistics ===================== ============================== DOMAIN SIZE 18 ======================== ============================== STATISTICS ============================ For domain size 18. Current CPU time: 0.00 seconds (total CPU time: 1.58 seconds). Ground clauses: seen=6185, kept=6149. Selections=613, assignments=8066, propagations=46121, current_models=0. Rewrite_terms=1544525, rewrite_bools=272729, indexes=171857. Rules_from_neg_clauses=2497, cross_offs=158729. ============================== end of statistics ===================== ============================== DOMAIN SIZE 19 ======================== ============================== STATISTICS ============================ For domain size 19. Current CPU time: 0.00 seconds (total CPU time: 2.33 seconds). Ground clauses: seen=7250, kept=7212. Selections=713, assignments=9939, propagations=58444, current_models=0. Rewrite_terms=1836798, rewrite_bools=303300, indexes=233360. Rules_from_neg_clauses=2471, cross_offs=204588. ============================== end of statistics ===================== ============================== DOMAIN SIZE 20 ======================== ============================== STATISTICS ============================ For domain size 20. Current CPU time: 0.00 seconds (total CPU time: 3.27 seconds). Ground clauses: seen=8431, kept=8391. Selections=784, assignments=11308, propagations=68829, current_models=0. Rewrite_terms=2154996, rewrite_bools=339854, indexes=273959. Rules_from_neg_clauses=2774, cross_offs=261790. ============================== end of statistics ===================== ============================== DOMAIN SIZE 21 ======================== ============================== STATISTICS ============================ For domain size 21. Current CPU time: 0.00 seconds (total CPU time: 4.55 seconds). Ground clauses: seen=9734, kept=9692. Selections=915, assignments=13953, propagations=86155, current_models=0. Rewrite_terms=2679320, rewrite_bools=407984, indexes=354342. Rules_from_neg_clauses=3326, cross_offs=340897. ============================== end of statistics ===================== ============================== DOMAIN SIZE 22 ======================== ============================== STATISTICS ============================ For domain size 22. Current CPU time: 0.00 seconds (total CPU time: 6.17 seconds). Ground clauses: seen=11165, kept=11121. Selections=1054, assignments=16906, propagations=105556, current_models=0. Rewrite_terms=3193858, rewrite_bools=462668, indexes=433418. Rules_from_neg_clauses=3760, cross_offs=418376. ============================== end of statistics ===================== ============================== DOMAIN SIZE 23 ======================== ============================== STATISTICS ============================ For domain size 23. Current CPU time: 0.00 seconds (total CPU time: 8.22 seconds). Ground clauses: seen=12730, kept=12684. Selections=1180, assignments=19696, propagations=129569, current_models=0. Rewrite_terms=3852059, rewrite_bools=535156, indexes=535859. Rules_from_neg_clauses=4173, cross_offs=510898. ============================== end of statistics ===================== ============================== DOMAIN SIZE 24 ======================== ============================== STATISTICS ============================ For domain size 24. Current CPU time: 0.00 seconds (total CPU time: 11.70 seconds). Ground clauses: seen=14435, kept=14387. Selections=1384, assignments=24466, propagations=169233, current_models=0. Rewrite_terms=5855169, rewrite_bools=957473, indexes=687088. Rules_from_neg_clauses=6577, cross_offs=692257. ============================== end of statistics ===================== ============================== DOMAIN SIZE 25 ======================== ============================== STATISTICS ============================ For domain size 25. Current CPU time: 0.00 seconds (total CPU time: 15.91 seconds). Ground clauses: seen=16286, kept=16236. Selections=1541, assignments=28325, propagations=202721, current_models=0. Rewrite_terms=6819143, rewrite_bools=1070592, indexes=862210. Rules_from_neg_clauses=6191, cross_offs=838784. ============================== end of statistics ===================== ============================== DOMAIN SIZE 26 ======================== ============================== STATISTICS ============================ For domain size 26. Current CPU time: 0.00 seconds (total CPU time: 20.95 seconds). Ground clauses: seen=18289, kept=18237. Selections=1678, assignments=31777, propagations=234857, current_models=0. Rewrite_terms=7789982, rewrite_bools=1170275, indexes=1002729. Rules_from_neg_clauses=7017, cross_offs=1018233. ============================== end of statistics ===================== ============================== DOMAIN SIZE 27 ======================== ============================== STATISTICS ============================ For domain size 27. Current CPU time: 0.00 seconds (total CPU time: 27.53 seconds). Ground clauses: seen=20450, kept=20396. Selections=1909, assignments=37834, propagations=283705, current_models=0. Rewrite_terms=9655887, rewrite_bools=1455143, indexes=1233565. Rules_from_neg_clauses=8845, cross_offs=1274180. ============================== end of statistics ===================== ============================== DOMAIN SIZE 28 ======================== ============================== STATISTICS ============================ For domain size 28. Current CPU time: 0.00 seconds (total CPU time: 35.67 seconds). Ground clauses: seen=22775, kept=22719. Selections=2136, assignments=44024, propagations=337722, current_models=0. Rewrite_terms=11209983, rewrite_bools=1639926, indexes=1464716. Rules_from_neg_clauses=10088, cross_offs=1515202. ============================== end of statistics ===================== ============================== DOMAIN SIZE 29 ======================== ============================== STATISTICS ============================ For domain size 29. Current CPU time: 0.00 seconds (total CPU time: 45.39 seconds). Ground clauses: seen=25270, kept=25212. Selections=2334, assignments=49596, propagations=397361, current_models=0. Rewrite_terms=12984434, rewrite_bools=1831758, indexes=1731500. Rules_from_neg_clauses=10330, cross_offs=1779763. ============================== end of statistics ===================== ============================== DOMAIN SIZE 30 ======================== ============================== STATISTICS ============================ For domain size 30. Current CPU time: 0.00 seconds (total CPU time: 58.92 seconds). Ground clauses: seen=27941, kept=27881. Selections=2622, assignments=58022, propagations=484952, current_models=0. Rewrite_terms=16785123, rewrite_bools=2541562, indexes=2096253. Rules_from_neg_clauses=13813, cross_offs=2242930. ============================== end of statistics ===================== ============================== DOMAIN SIZE 31 ======================== ============================== STATISTICS ============================ For domain size 31. Current CPU time: 0.00 seconds (total CPU time: 74.55 seconds). Ground clauses: seen=30794, kept=30732. Selections=2898, assignments=66412, propagations=577065, current_models=0. Rewrite_terms=18989803, rewrite_bools=2764093, indexes=2495152. Rules_from_neg_clauses=13368, cross_offs=2614148. ============================== end of statistics ===================== ============================== DOMAIN SIZE 32 ======================== ============================== STATISTICS ============================ For domain size 32. Current CPU time: 0.00 seconds (total CPU time: 93.30 seconds). Ground clauses: seen=33835, kept=33771. Selections=3130, assignments=73639, propagations=656538, current_models=0. Rewrite_terms=21856077, rewrite_bools=3103772, indexes=2892385. Rules_from_neg_clauses=16396, cross_offs=3133209. ============================== end of statistics ===================== ============================== DOMAIN SIZE 33 ======================== ============================== STATISTICS ============================ For domain size 33. Current CPU time: 0.00 seconds (total CPU time: 115.62 seconds). Ground clauses: seen=37070, kept=37004. Selections=3448, assignments=83859, propagations=766209, current_models=0. Rewrite_terms=25050594, rewrite_bools=3458588, indexes=3391479. Rules_from_neg_clauses=18255, cross_offs=3713841. ============================== end of statistics ===================== ============================== DOMAIN SIZE 34 ======================== ============================== STATISTICS ============================ For domain size 34. Current CPU time: 0.00 seconds (total CPU time: 141.92 seconds). Ground clauses: seen=40505, kept=40437. Selections=3791, assignments=95245, propagations=890605, current_models=0. Rewrite_terms=28637867, rewrite_bools=3867609, indexes=3931503. Rules_from_neg_clauses=19906, cross_offs=4316574. ============================== end of statistics ===================== ============================== DOMAIN SIZE 35 ======================== ============================== STATISTICS ============================ For domain size 35. Current CPU time: 0.00 seconds (total CPU time: 173.45 seconds). Ground clauses: seen=44146, kept=44076. Selections=4120, assignments=106484, propagations=1035706, current_models=0. Rewrite_terms=33038476, rewrite_bools=4412366, indexes=4568668. Rules_from_neg_clauses=22007, cross_offs=4993418. ============================== end of statistics ===================== ============================== DOMAIN SIZE 36 ======================== ============================== STATISTICS ============================ For domain size 36. Current CPU time: 0.00 seconds (total CPU time: 223.47 seconds). Ground clauses: seen=47999, kept=47927. Selections=4642, assignments=124970, propagations=1271050, current_models=0. Rewrite_terms=47736579, rewrite_bools=7737245, indexes=5561973. Rules_from_neg_clauses=33290, cross_offs=6257775. ============================== end of statistics ===================== ============================== DOMAIN SIZE 37 ======================== ============================== STATISTICS ============================ For domain size 37. Current CPU time: 0.00 seconds (total CPU time: 279.17 seconds). Ground clauses: seen=52070, kept=51996. Selections=5047, assignments=139813, propagations=1465292, current_models=0. Rewrite_terms=52146294, rewrite_bools=8152396, indexes=6505034. Rules_from_neg_clauses=28626, cross_offs=7098907. ============================== end of statistics ===================== ============================== DOMAIN SIZE 38 ======================== ============================== STATISTICS ============================ For domain size 38. Current CPU time: 0.00 seconds (total CPU time: 341.55 seconds). Ground clauses: seen=56365, kept=56289. Selections=5342, assignments=150775, propagations=1605209, current_models=0. Rewrite_terms=56236180, rewrite_bools=8499002, indexes=7115171. Rules_from_neg_clauses=33032, cross_offs=8195801. ============================== end of statistics ===================== ============================== DOMAIN SIZE 39 ======================== ============================== STATISTICS ============================ For domain size 39. Current CPU time: 0.00 seconds (total CPU time: 414.28 seconds). Ground clauses: seen=60890, kept=60812. Selections=5850, assignments=170130, propagations=1821113, current_models=0. Rewrite_terms=62391102, rewrite_bools=9127828, indexes=8164451. Rules_from_neg_clauses=36417, cross_offs=9411735. ============================== end of statistics ===================== ============================== DOMAIN SIZE 40 ======================== ============================== STATISTICS ============================ For domain size 40. Current CPU time: 0.00 seconds (total CPU time: 496.81 seconds). Ground clauses: seen=65651, kept=65571. Selections=6394, assignments=191432, propagations=2062729, current_models=0. Rewrite_terms=69918092, rewrite_bools=9968772, indexes=9287800. Rules_from_neg_clauses=39609, cross_offs=10820270. ============================== end of statistics ===================== ============================== DOMAIN SIZE 41 ======================== ============================== STATISTICS ============================ For domain size 41. Current CPU time: 0.00 seconds (total CPU time: 590.64 seconds). Ground clauses: seen=70654, kept=70572. Selections=6908, assignments=212065, propagations=2341302, current_models=0. Rewrite_terms=78044091, rewrite_bools=10738379, indexes=10588106. Rules_from_neg_clauses=41350, cross_offs=12273632. ============================== end of statistics ===================== ============================== DOMAIN SIZE 42 ======================== ============================== STATISTICS ============================ For domain size 42. Current CPU time: 0.00 seconds (total CPU time: 700.91 seconds). Ground clauses: seen=75905, kept=75821. Selections=7494, assignments=236195, propagations=2661761, current_models=0. Rewrite_terms=89133523, rewrite_bools=12155493, indexes=12172694. Rules_from_neg_clauses=48760, cross_offs=14343932. ============================== end of statistics ===================== ============================== DOMAIN SIZE 43 ======================== ============================== STATISTICS ============================ For domain size 43. Current CPU time: 0.00 seconds (total CPU time: 824.06 seconds). Ground clauses: seen=81410, kept=81324. Selections=8069, assignments=260476, propagations=2993741, current_models=0. Rewrite_terms=98017871, rewrite_bools=13005347, indexes=13633714. Rules_from_neg_clauses=49636, cross_offs=16018575. ============================== end of statistics ===================== ============================== DOMAIN SIZE 44 ======================== ============================== STATISTICS ============================ For domain size 44. Current CPU time: 0.00 seconds (total CPU time: 969.98 seconds). Ground clauses: seen=87175, kept=87087. Selections=8640, assignments=285100, propagations=3346808, current_models=0. Rewrite_terms=110901505, rewrite_bools=14596126, indexes=15395132. Rules_from_neg_clauses=57428, cross_offs=18606271. ============================== end of statistics ===================== ============================== DOMAIN SIZE 45 ======================== ============================== STATISTICS ============================ For domain size 45. Current CPU time: 0.00 seconds (total CPU time: 1151.03 seconds). Ground clauses: seen=93206, kept=93116. Selections=9331, assignments=315644, propagations=3810973, current_models=0. Rewrite_terms=130581570, rewrite_bools=18008523, indexes=17466264. Rules_from_neg_clauses=66646, cross_offs=21398815. ============================== end of statistics ===================== ============================== DOMAIN SIZE 46 ======================== ============================== STATISTICS ============================ For domain size 46. Current CPU time: 0.00 seconds (total CPU time: 1356.30 seconds). Ground clauses: seen=99509, kept=99417. Selections=10051, assignments=348233, propagations=4309090, current_models=0. Rewrite_terms=144409188, rewrite_bools=19479021, indexes=19887175. Rules_from_neg_clauses=68737, cross_offs=24366954. ============================== end of statistics ===================== ============================== DOMAIN SIZE 47 ======================== ============================== STATISTICS ============================ For domain size 47. Current CPU time: 0.00 seconds (total CPU time: 1587.73 seconds). Ground clauses: seen=106090, kept=105996. Selections=10659, assignments=376273, propagations=4790296, current_models=0. Rewrite_terms=158844292, rewrite_bools=21100323, indexes=22055117. Rules_from_neg_clauses=73883, cross_offs=27254288. ============================== end of statistics ===================== ============================== DOMAIN SIZE 48 ======================== ============================== STATISTICS ============================ For domain size 48. Current CPU time: 0.00 seconds (total CPU time: 1891.22 seconds). Ground clauses: seen=112955, kept=112859. Selections=11601, assignments=420815, propagations=5484286, current_models=0. Rewrite_terms=196797699, rewrite_bools=29046106, indexes=25370046. Rules_from_neg_clauses=95249, cross_offs=32017839. ============================== end of statistics ===================== ============================== DOMAIN SIZE 49 ======================== ============================== STATISTICS ============================ For domain size 49. Current CPU time: 0.00 seconds (total CPU time: 2225.98 seconds). Ground clauses: seen=120110, kept=120012. Selections=12415, assignments=460233, propagations=6135512, current_models=0. Rewrite_terms=213132451, rewrite_bools=30696034, indexes=28410316. Rules_from_neg_clauses=87437, cross_offs=35217018. ============================== end of statistics ===================== ============================== DOMAIN SIZE 50 ======================== ============================== STATISTICS ============================ For domain size 50. Current CPU time: 0.00 seconds (total CPU time: 2610.89 seconds). Ground clauses: seen=127561, kept=127461. Selections=13152, assignments=496455, propagations=6717563, current_models=0. Rewrite_terms=234740820, rewrite_bools=33189867, indexes=31511836. Rules_from_neg_clauses=103914, cross_offs=40141021. ============================== end of statistics ===================== ============================== DOMAIN SIZE 51 ======================== ============================== STATISTICS ============================ For domain size 51. Current CPU time: 0.00 seconds (total CPU time: 3032.89 seconds). Ground clauses: seen=135314, kept=135212. Selections=14118, assignments=544872, propagations=7446016, current_models=0. Rewrite_terms=255072816, rewrite_bools=35198762, indexes=34990150. Rules_from_neg_clauses=110358, cross_offs=44739966. ============================== end of statistics ===================== ============================== DOMAIN SIZE 52 ======================== ============================== STATISTICS ============================ For domain size 52. Current CPU time: 0.00 seconds (total CPU time: 3498.30 seconds). Ground clauses: seen=143375, kept=143271. Selections=15162, assignments=598300, propagations=8238445, current_models=0. Rewrite_terms=278837178, rewrite_bools=37608600, indexes=38918242. Rules_from_neg_clauses=115890, cross_offs=50096952. ============================== end of statistics ===================== ============================== DOMAIN SIZE 53 ======================== ============================== STATISTICS ============================ For domain size 53. Current CPU time: 0.00 seconds (total CPU time: 4018.94 seconds). Ground clauses: seen=151750, kept=151644. Selections=16130, assignments=648780, propagations=9072921, current_models=0. Rewrite_terms=303948944, rewrite_bools=40100299, indexes=42917846. Rules_from_neg_clauses=122731, cross_offs=55131686. ============================== end of statistics ===================== ============================== DOMAIN SIZE 54 ======================== ============================== STATISTICS ============================ For domain size 54. Current CPU time: 0.00 seconds (total CPU time: 4664.81 seconds). Ground clauses: seen=160445, kept=160337. Selections=17348, assignments=713613, propagations=10162034, current_models=0. Rewrite_terms=358920882, rewrite_bools=50178120, indexes=48543746. Rules_from_neg_clauses=147158, cross_offs=63972708. ============================== end of statistics ===================== ============================== DOMAIN SIZE 55 ======================== ============================== STATISTICS ============================ For domain size 55. Current CPU time: 0.00 seconds (total CPU time: 5375.89 seconds). Ground clauses: seen=169466, kept=169356. Selections=18477, assignments=774943, propagations=11230449, current_models=0. Rewrite_terms=387545957, rewrite_bools=52914760, indexes=53677712. Rules_from_neg_clauses=142713, cross_offs=70110158. ============================== end of statistics ===================== ============================== DOMAIN SIZE 56 ======================== ============================== STATISTICS ============================ For domain size 56. Current CPU time: 0.00 seconds (total CPU time: 6157.61 seconds). Ground clauses: seen=178819, kept=178707. Selections=19568, assignments=835141, propagations=12251051, current_models=0. Rewrite_terms=422251431, rewrite_bools=56610187, indexes=59071519. Rules_from_neg_clauses=163613, cross_offs=79820792. ============================== end of statistics ===================== ============================== DOMAIN SIZE 57 ======================== ============================== STATISTICS ============================ For domain size 57. Current CPU time: 0.00 seconds (total CPU time: 7020.16 seconds). Ground clauses: seen=188510, kept=188396. Selections=20851, assignments=907211, propagations=13455452, current_models=0. Rewrite_terms=455893439, rewrite_bools=59723641, indexes=64930475. Rules_from_neg_clauses=175666, cross_offs=88879848. ============================== end of statistics ===================== ============================== DOMAIN SIZE 58 ======================== ============================== STATISTICS ============================ For domain size 58. Current CPU time: 0.00 seconds (total CPU time: 7965.84 seconds). Ground clauses: seen=198545, kept=198429. Selections=22127, assignments=980104, propagations=14695902, current_models=0. Rewrite_terms=493551213, rewrite_bools=63424731, indexes=71186159. Rules_from_neg_clauses=187509, cross_offs=97681444. ============================== end of statistics ===================== ============================== DOMAIN SIZE 59 ======================== ============================== STATISTICS ============================ For domain size 59. Current CPU time: 0.00 seconds (total CPU time: 9045.97 seconds). Ground clauses: seen=208930, kept=208812. Selections=23424, assignments=1055434, propagations=16054386, current_models=0. Rewrite_terms=536613167, rewrite_bools=67848843, indexes=78066701. Rules_from_neg_clauses=194392, cross_offs=107396694. ============================== end of statistics ===================== ============================== DOMAIN SIZE 60 ======================== ============================== STATISTICS ============================ For domain size 60. Current CPU time: 0.00 seconds (total CPU time: 10474.51 seconds). Ground clauses: seen=219671, kept=219551. Selections=25185, assignments=1159802, propagations=17996204, current_models=0. Rewrite_terms=640004181, rewrite_bools=88204796, indexes=88224949. Rules_from_neg_clauses=242534, cross_offs=125006672. ============================== end of statistics ===================== ============================== DOMAIN SIZE 61 ======================== ============================== STATISTICS ============================ For domain size 61. Current CPU time: 0.00 seconds (total CPU time: 11951.72 seconds). Ground clauses: seen=230774, kept=230652. Selections=26693, assignments=1250874, propagations=19785906, current_models=0. Rewrite_terms=686473513, rewrite_bools=92535661, indexes=96789798. Rules_from_neg_clauses=228046, cross_offs=135984011. ============================== end of statistics ===================== ============================== DOMAIN SIZE 62 ======================== ============================== STATISTICS ============================ For domain size 62. Current CPU time: 0.00 seconds (total CPU time: 13587.01 seconds). Ground clauses: seen=242245, kept=242121. Selections=28110, assignments=1337515, propagations=21443536, current_models=0. Rewrite_terms=752878492, rewrite_bools=100160929, indexes=106408419. Rules_from_neg_clauses=277204, cross_offs=155070685. ============================== end of statistics ===================== ============================== DOMAIN SIZE 63 ======================== ============================== STATISTICS ============================ For domain size 63. Current CPU time: 0.00 seconds (total CPU time: 15406.31 seconds). Ground clauses: seen=254090, kept=253964. Selections=30085, assignments=1460370, propagations=23652525, current_models=0. Rewrite_terms=820123151, rewrite_bools=107556456, indexes=117070224. Rules_from_neg_clauses=300905, cross_offs=174307103. ============================== end of statistics ===================== ============================== DOMAIN SIZE 64 ======================== ============================== STATISTICS ============================ For domain size 64. Current CPU time: 0.00 seconds (total CPU time: 17426.92 seconds). Ground clauses: seen=266315, kept=266187. Selections=32265, assignments=1598426, propagations=26153269, current_models=0. Rewrite_terms=890672992, rewrite_bools=114015982, indexes=129781356. Rules_from_neg_clauses=317567, cross_offs=199342276. ============================== end of statistics ===================== ============================== DOMAIN SIZE 65 ======================== ============================== STATISTICS ============================ For domain size 65. Current CPU time: 0.00 seconds (total CPU time: 19832.91 seconds). Ground clauses: seen=278926, kept=278796. Selections=34369, assignments=1733827, propagations=28765167, current_models=0. Rewrite_terms=967947640, rewrite_bools=121213677, indexes=142653473. Rules_from_neg_clauses=334620, cross_offs=226282743. ============================== end of statistics ===================== ============================== DOMAIN SIZE 66 ======================== ============================== STATISTICS ============================ For domain size 66. Current CPU time: 0.00 seconds (total CPU time: 22357.53 seconds). Ground clauses: seen=291929, kept=291797. Selections=37191, assignments=1918429, propagations=32226093, current_models=0. Rewrite_terms=1068851604, rewrite_bools=130447289, indexes=160669075. Rules_from_neg_clauses=376800, cross_offs=271410089. ============================== end of statistics ===================== ============================== DOMAIN SIZE 67 ======================== ============================== STATISTICS ============================ For domain size 67. Current CPU time: 0.00 seconds (total CPU time: 25152.09 seconds). Ground clauses: seen=305330, kept=305196. Selections=40093, assignments=2111486, propagations=35835869, current_models=0. Rewrite_terms=1164273774, rewrite_bools=137926827, indexes=178668450. Rules_from_neg_clauses=391841, cross_offs=315776603. ============================== end of statistics ===================== ============================== DOMAIN SIZE 68 ======================== ============================== STATISTICS ============================ For domain size 68. Current CPU time: 0.00 seconds (total CPU time: 28362.98 seconds). Ground clauses: seen=319135, kept=318999. Selections=44046, assignments=2378602, propagations=40685346, current_models=0. Rewrite_terms=1306660325, rewrite_bools=150006388, indexes=205753998. Rules_from_neg_clauses=443329, cross_offs=392466900. ============================== end of statistics ===================== ============================== DOMAIN SIZE 69 ======================== ============================== STATISTICS ============================ For domain size 69. Current CPU time: 0.00 seconds (total CPU time: 31959.62 seconds). Ground clauses: seen=333350, kept=333212. Selections=47923, assignments=2644789, propagations=45629257, current_models=0. Rewrite_terms=1438766900, rewrite_bools=160244300, indexes=231719658. Rules_from_neg_clauses=470940, cross_offs=461937598. ============================== end of statistics ===================== ============================== DOMAIN SIZE 70 ======================== ============================== STATISTICS ============================ For domain size 70. Current CPU time: 0.00 seconds (total CPU time: 36118.48 seconds). Ground clauses: seen=347981, kept=347841. Selections=53828, assignments=3055988, propagations=53134473, current_models=0. Rewrite_terms=1636702471, rewrite_bools=175424271, indexes=272019766. Rules_from_neg_clauses=541314, cross_offs=588191796. ============================== end of statistics ===================== ============================== DOMAIN SIZE 71 ======================== ============================== MODEL ================================= interpretation( 71, [number=1, seconds=40879], [ function(a1, [ 0 ]), function(a10, [ 1 ]), function(a2, [ 3 ]), function(a3, [ 2 ]), function(a4, [57 ]), function(a5, [40 ]), function(a6, [29 ]), function(a7, [41 ]), function(a8, [ 4 ]), function(a9, [67 ]), function(*(_,_), [ 0, 5, 1, 8, 3,19,10,20,32, 7,28,27,35,22, 9, 2,12,11,30,52,31,36,55,41,21,29,43,51,68,56,66,67,60,44,63,45,59,42,53,54,70,50,65,33,49,64,62,69,57,47,61,46,25,17,34,15,26,58,39,37,48,24,40, 6,18,14,38,16,13, 4,23, 7, 1, 0, 5, 2, 8, 3,27,28,20,19,31,32,12,11, 9,10,21,22,35,36,51,52,30,29,42,41,56,55,67,68,65,66,54,53,50,49,44,43,64,63,60,59,45,46,69,70,61,62,57,58,34,33,25,26,17,18,48,47,39,40,37,38,15,16,24,23, 4, 6,14,13, 9, 3, 2,10, 1,12, 5,21,30,11,22,29,41,19, 7, 0, 8,20,28,43,42,44,53,32,27,31,35,54,63,64,70,69,62,51,55,47,58,36,52,56,68,57,61,39,48,67,66,65,60,50,59,40,37,24,38,14,23,49,45,33,46,25,34, 4,13,17,26, 6,16,15,18, 11, 2, 9, 3, 0,10, 1,29,22,21,12,42,30, 8,20, 7, 5,27,19,41,44,54,43,28,31,36,32,64,53,69,63,61,70,56,52,57,48,51,35,67,55,62,58,47,40,65,68,59,66,60,49,38,39,37,23,24,13,46,50,45,34,33,26,14, 6,25,18,15, 4,17,16, 17, 6,15,13, 4,23,16,33,40,25,38,45,48,26,24,14,18,37,34,58,50,60,61,46,39,47,49,66,69,68,64,55,54,62,65,42,35,57,59,70,67,44,52,29,32,63,56,53,51,36,43,28,21,11,19, 9, 8,41,31,27,30,20,22, 2, 5, 7,12, 1, 3, 0,10, 20, 0, 7, 1, 9, 5, 2,31,19,27, 8,36,28,10,21,11, 3,29,12,32,51,56,35,22,42,44,30,67,52,65,55,59,68,64,43,60,46,54,41,69,53,66,49,50,34,61,63,58,70,62,48,26,45,33,18,25,16,40,57,47,38,39,23,17, 4,37,13,14,15,24, 6, 24, 4,14,16,15,18, 6,39,34,37,26,47,46,23,25,17,13,33,38,49,57,62,59,40,45,50,48,70,65,63,67,53,56,66,61,36,41,60,58,68,69,51,43,31,30,55,64,52,54,44,35,22,27,20,12, 7,10,32,42,29,28,21,19, 0, 3,11, 8, 2, 1, 9, 5, 1, 8, 5,19,10,28,12, 7,35, 0,32,20,52,30, 2, 3,22, 9,41,55,27,31,68,43,11,21,53,36,66,51,60,56,50,42,70,33,65,29,63,44,62,45,67,25,59,54,57,64,47,39,69,49,17,15,46, 6,34,61,37,24,58,14,48,13,26, 4,40,18,23,16,38, 27, 7,20, 0,11, 1, 9,36, 8,31, 5,51,19, 3,29,21, 2,42,10,28,56,67,32,12,44,54,22,65,35,59,52,49,55,69,41,66,34,64,30,61,43,68,46,60,26,58,53,48,63,70,40,18,50,45,16,33, 4,38,62,57,23,47,13,25,14,39, 6,24,17,37,15, 2,10, 3,12, 5,22, 8,11,41, 9,30,21,43,28, 0, 1,19, 7,32,53,29,42,63,35,20,27,52,44,70,54,62,64,57,36,68,39,61,31,55,51,66,47,69,37,58,56,60,67,50,45,65,48,24,14,40, 4,38,59,33,25,49,17,46,16,23,15,34,13,18, 6,26, 21, 9,11, 2, 7, 3, 0,42,12,29,10,44,22, 5,27,20, 1,31, 8,30,54,64,41,19,36,51,28,69,43,61,53,58,63,67,35,62,40,56,32,65,52,70,48,57,38,59,55,49,68,66,46,23,47,39,13,37, 6,34,60,50,26,45,18,24,15,33,16,17,14,25, 4, 3,12,10,22, 8,30,19, 9,43, 2,41,11,53,32, 1, 5,28, 0,35,63,21,29,70,52, 7,20,55,42,62,44,57,54,47,31,66,37,69,27,68,36,60,39,64,24,61,51,50,56,45,33,67,58,14, 4,48,16,40,65,25,17,59,15,49,18,38, 6,46,23,26,13,34, 29,11,21, 9,20, 2, 7,44,10,42, 3,54,12, 1,31,27, 0,36, 5,22,64,69,30, 8,51,56,19,61,41,58,43,48,53,65,32,70,38,67,28,59,35,63,40,62,23,49,52,46,55,68,34,13,57,47, 6,39,15,26,66,60,18,50,16,37,17,45, 4,25,24,33,14, 37,14,24, 4,17,16,15,47,26,39,18,57,34,13,33,25, 6,45,23,46,62,70,49,38,50,60,40,63,59,53,65,43,67,68,58,51,30,66,48,55,61,56,41,36,22,52,69,35,64,54,32,12,31,27,10,20, 3,28,44,42,19,29, 8, 7, 2,21, 5, 9, 0,11, 1, 15,13, 6,23,16,38,18,25,48,17,40,33,58,34,14, 4,26,24,46,61,45,50,69,49,37,39,59,60,64,66,54,68,44,57,67,29,52,47,65,62,56,42,55,21,35,70,51,63,36,31,53,32,11, 9,28, 2,19,43,27,20,41, 7,30, 3, 8, 0,22, 5,10, 1,12, 14,16, 4,18, 6,26,13,37,46,24,34,39,49,38,17,15,23,25,40,59,47,57,65,48,33,45,58,62,67,70,56,63,51,60,69,31,43,50,61,66,64,36,53,27,41,68,54,55,44,42,52,30,20, 7,22, 0,12,35,29,21,32,11,28, 1,10, 9,19, 3, 5, 2, 8, 25,15,17, 6,14,13, 4,45,38,33,23,50,40,18,37,24,16,39,26,48,60,66,58,34,47,57,46,68,61,55,69,52,64,70,59,44,32,62,49,63,65,54,35,42,28,53,67,43,56,51,41,19,29,21, 8,11, 5,30,36,31,22,27,12, 9, 1,20,10, 0, 2, 7, 3, 4,18,16,26,13,34,23,24,49,14,46,37,59,40,15, 6,38,17,48,65,39,47,67,58,25,33,61,57,56,62,51,70,36,50,64,27,53,45,69,60,54,31,63,20,43,66,44,68,42,29,55,41, 7, 0,30, 1,22,52,21,11,35, 9,32, 5,12, 2,28,10, 8, 3,19, 33,17,25,15,24, 6,14,50,23,45,13,60,38,16,39,37, 4,47,18,40,66,68,48,26,57,62,34,55,58,52,61,35,69,63,49,54,28,70,46,53,59,64,32,44,19,43,65,41,67,56,30, 8,42,29, 5,21, 1,22,51,36,12,31,10,11, 0,27, 3, 7, 9,20, 2, 31,20,27, 7,21, 0,11,51, 5,36, 1,56, 8, 2,42,29, 9,44, 3,19,67,65,28,10,54,64,12,59,32,49,35,46,52,61,30,68,26,69,22,58,41,55,34,66,18,48,43,40,53,63,38,16,60,50, 4,45,14,23,70,62,13,57, 6,33,24,47,15,37,25,39,17, 5,19, 8,28,12,32,22, 0,52, 1,35, 7,55,41, 3,10,30, 2,43,68,20,27,66,53, 9,11,63,31,60,36,50,51,45,29,62,25,67,21,70,42,57,33,56,17,65,44,47,54,39,37,64,59,15, 6,49,13,46,69,24,14,61, 4,58,23,34,16,48,26,38,18,40, 10,22,12,30,19,41,28, 2,53, 3,43, 9,63,35, 5, 8,32, 1,52,70,11,21,62,55, 0, 7,68,29,57,42,47,44,39,27,60,24,64,20,66,31,50,37,54,14,69,36,45,51,33,25,56,61, 4,16,58,18,48,67,17,15,65, 6,59,26,40,13,49,38,34,23,46, 42,21,29,11,27, 9,20,54, 3,44, 2,64,10, 0,36,31, 7,51, 1,12,69,61,22, 5,56,67, 8,58,30,48,41,40,43,59,28,63,23,65,19,49,32,53,38,70,13,46,35,34,52,55,26, 6,62,57,15,47,17,18,68,66,16,60, 4,39,25,50,14,33,37,45,24, 39,24,37,14,25, 4,17,57,18,47,16,62,26, 6,45,33,15,50,13,34,70,63,46,23,60,66,38,53,49,43,59,41,65,55,48,56,22,68,40,52,58,67,30,51,12,35,61,32,69,64,28,10,36,31, 3,27, 2,19,54,44, 8,42, 5,20, 9,29, 1,11, 7,21, 0, 6,23,13,38,18,40,26,17,58,15,48,25,61,46, 4,16,34,14,49,69,33,45,64,59,24,37,65,50,54,60,44,66,42,47,56,21,55,39,67,57,51,29,68,11,52,62,36,70,31,27,63,35, 9, 2,32, 3,28,53,20, 7,43, 0,41,10,19, 1,30, 8,12, 5,22, 16,26,18,34,23,46,38,14,59, 4,49,24,65,48, 6,13,40,15,58,67,37,39,56,61,17,25,69,47,51,57,36,62,31,45,54,20,63,33,64,50,44,27,70, 7,53,60,42,66,29,21,68,43, 0, 1,41, 5,30,55,11, 9,52, 2,35, 8,22, 3,32,12,19,10,28, 45,25,33,17,37,15,24,60,13,50, 6,66,23, 4,47,39,14,57,16,38,68,55,40,18,62,70,26,52,48,35,58,32,61,53,46,64,19,63,34,43,49,69,28,54, 8,41,59,30,65,67,22, 5,44,42, 1,29, 0,12,56,51,10,36, 3,21, 7,31, 2,20,11,27, 9, 8,28,19,32,22,35,30, 1,55, 5,52, 0,68,43,10,12,41, 3,53,66, 7,20,60,63, 2, 9,70,27,50,31,45,36,33,21,57,17,56,11,62,29,47,25,51,15,67,42,39,44,37,24,54,65, 6,13,59,23,49,64,14, 4,69,16,61,38,46,18,58,34,40,26,48, 36,27,31,20,29, 7,21,56, 1,51, 0,67, 5, 9,44,42,11,54, 2, 8,65,59,19, 3,64,69,10,49,28,46,32,34,35,58,22,55,18,61,12,48,30,52,26,68,16,40,41,38,43,53,23, 4,66,60,14,50,24,13,63,70, 6,62,15,45,37,57,17,39,33,47,25, 12,30,22,41,28,43,32, 3,63,10,53, 2,70,52, 8,19,35, 5,55,62, 9,11,57,68, 1, 0,66,21,47,29,39,42,37,20,50,14,54, 7,60,27,45,24,44, 4,64,31,33,36,25,17,51,69,16,18,61,26,58,56,15, 6,67,13,65,34,48,23,59,40,46,38,49, 44,29,42,21,31,11,27,64, 2,54, 9,69, 3, 7,51,36,20,56, 0,10,61,58,12, 1,67,65, 5,48,22,40,30,38,41,49,19,53,13,59, 8,46,28,43,23,63, 6,34,32,26,35,52,18,15,70,62,17,57,25,16,55,68, 4,66,14,47,33,60,24,45,39,50,37, 19,32,28,35,30,52,41, 5,68, 8,55, 1,66,53,12,22,43,10,63,60, 0, 7,50,70, 3, 2,62,20,45,27,33,31,25,11,47,15,51, 9,57,21,39,17,36, 6,56,29,37,42,24,14,44,67,13,23,65,38,59,54, 4,16,64,18,69,40,49,26,61,46,48,34,58, 51,31,36,27,42,20,29,67, 0,56, 7,65, 1,11,54,44,21,64, 9, 5,59,49, 8, 2,69,61, 3,46,19,34,28,26,32,48,12,52,16,58,10,40,22,35,18,55, 4,38,30,23,41,43,13,14,68,66,24,60,37, 6,53,63,15,70,17,50,39,62,25,47,45,57,33, 18,34,26,46,38,49,40, 4,65,16,59,14,67,58,13,23,48, 6,61,56,24,37,51,69,15,17,64,39,36,47,31,57,27,33,44, 7,70,25,54,45,42,20,62, 0,63,50,29,60,21,11,66,53, 1, 5,43, 8,41,68, 9, 2,55, 3,52,19,30,10,35,22,28,12,32, 50,33,45,25,39,17,37,66, 6,60,15,68,13,14,57,47,24,62, 4,23,55,52,38,16,70,63,18,35,40,32,48,28,58,43,34,69, 8,53,26,41,46,61,19,64, 5,30,49,22,59,65,12, 1,54,44, 0,42, 7,10,67,56, 3,51, 2,29,20,36, 9,27,21,31,11, 56,36,51,31,44,27,42,65, 7,67,20,59, 0,21,64,54,29,69,11, 1,49,46, 5, 9,61,58, 2,34, 8,26,19,18,28,40,10,35, 4,48, 3,38,12,32,16,52,14,23,22,13,30,41, 6,24,55,68,37,66,39,15,43,53,17,63,25,60,47,70,33,57,50,62,45, 28,35,32,52,41,55,43, 8,66,19,68, 5,60,63,22,30,53,12,70,50, 1, 0,45,62,10, 3,57, 7,33,20,25,27,17, 9,39, 6,36, 2,47,11,37,15,31,13,51,21,24,29,14, 4,42,56,23,38,67,40,65,44,16,18,54,26,64,48,59,34,69,49,58,46,61, 13,38,23,40,26,48,34,15,61, 6,58,17,69,49,16,18,46, 4,59,64,25,33,54,65,14,24,67,45,44,50,42,60,29,39,51,11,68,37,56,47,36,21,66, 9,55,57,31,62,27,20,70,52, 2, 3,35,10,32,63, 7, 0,53, 1,43,12,28, 5,41,19,22, 8,30, 47,37,39,24,33,14,25,62,16,57, 4,70,18,15,50,45,17,60, 6,26,63,53,34,13,66,68,23,43,46,41,49,30,59,52,40,67,12,55,38,35,48,65,22,56,10,32,58,28,61,69,19, 3,51,36, 2,31, 9, 8,64,54, 5,44, 1,27,11,42, 0,21,20,29, 7, 23,40,38,48,34,58,46, 6,69,13,61,15,64,59,18,26,49,16,65,54,17,25,44,67, 4,14,56,33,42,45,29,50,21,37,36, 9,66,24,51,39,31,11,60, 2,68,47,27,57,20, 7,62,55, 3,10,52,12,35,70, 0, 1,63, 5,53,22,32, 8,43,28,30,19,41, 57,39,47,37,45,24,33,70, 4,62,14,63,16,17,60,50,25,66,15,18,53,43,26, 6,68,55,13,41,34,30,46,22,49,35,38,65,10,52,23,32,40,59,12,67, 3,28,48,19,58,61, 8, 2,56,51, 9,36,11, 5,69,64, 1,54, 0,31,21,44, 7,29,27,42,20, 54,42,44,29,36,21,31,69, 9,64,11,61, 2,20,56,51,27,67, 7, 3,58,48,10, 0,65,59, 1,40,12,38,22,23,30,46, 8,43, 6,49, 5,34,19,41,13,53,15,26,28,18,32,35,16,17,63,70,25,62,33, 4,52,55,14,68,24,57,45,66,37,50,47,60,39, 22,41,30,43,32,53,35,10,70,12,63, 3,62,55,19,28,52, 8,68,57, 2, 9,47,66, 5, 1,60,11,39,21,37,29,24, 7,45, 4,44, 0,50,20,33,14,42,16,54,27,25,31,17,15,36,64,18,26,69,34,61,51, 6,13,56,23,67,46,58,38,65,48,49,40,59, 64,44,54,42,51,29,36,61,11,69,21,58, 9,27,67,56,31,65,20, 2,48,40, 3, 7,59,49, 0,38,10,23,12,13,22,34, 5,41,15,46, 1,26, 8,30, 6,43,17,18,19,16,28,32, 4,25,53,63,33,70,45,14,35,52,24,55,37,62,50,68,39,60,57,66,47, 30,43,41,53,35,63,52,12,62,22,70,10,57,68,28,32,55,19,66,47, 3, 2,39,60, 8, 5,50, 9,37,11,24,21,14, 0,33,16,42, 1,45, 7,25, 4,29,18,44,20,17,27,15, 6,31,54,26,34,64,46,69,36,13,23,51,38,56,49,61,40,67,58,59,48,65, 26,46,34,49,40,59,48,16,67,18,65, 4,56,61,23,38,58,13,69,51,14,24,36,64, 6,15,54,37,31,39,27,47,20,25,42, 0,62,17,44,33,29, 7,57, 1,70,45,21,50,11, 9,60,63, 5, 8,53,19,43,66, 2, 3,68,10,55,28,41,12,52,30,32,22,35, 60,45,50,33,47,25,39,68,15,66,17,55, 6,24,62,57,37,70,14,13,52,35,23, 4,63,53,16,32,38,28,40,19,48,41,26,61, 5,43,18,30,34,58, 8,69, 1,22,46,12,49,59,10, 0,64,54, 7,44,20, 3,65,67, 2,56, 9,42,27,51,11,31,29,36,21, 38,48,40,58,46,61,49,13,64,23,69, 6,54,65,26,34,59,18,67,44,15,17,42,56,16, 4,51,25,29,33,21,45,11,24,31, 2,60,14,36,37,27, 9,50, 3,66,39,20,47, 7, 0,57,68,10,12,55,22,52,62, 1, 5,70, 8,63,30,35,19,53,32,41,28,43, 62,47,57,39,50,37,45,63,14,70,24,53, 4,25,66,60,33,68,17,16,43,41,18,15,55,52, 6,30,26,22,34,12,46,32,23,59, 3,35,13,28,38,49,10,65, 2,19,40, 8,48,58, 5, 9,67,56,11,51,21, 1,61,69, 0,64, 7,36,29,54,20,42,31,44,27, 66,50,60,45,57,33,47,55,17,68,25,52,15,37,70,62,39,63,24, 6,35,32,13,14,53,43, 4,28,23,19,38, 8,40,30,18,58, 1,41,16,22,26,48, 5,61, 0,12,34,10,46,49, 3, 7,69,64,20,54,27, 2,59,65, 9,67,11,44,31,56,21,36,42,51,29, 34,49,46,59,48,65,58,18,56,26,67,16,51,69,38,40,61,23,64,36, 4,14,31,54,13, 6,44,24,27,37,20,39, 7,17,29, 1,57,15,42,25,21, 0,47, 5,62,33,11,45, 9, 2,50,70, 8,19,63,28,53,60, 3,10,66,12,68,32,43,22,55,41,35,30,52, 32,52,35,55,43,68,53,19,60,28,66, 8,50,70,30,41,63,22,62,45, 5, 1,33,57,12,10,47, 0,25, 7,17,20,15, 2,37,13,31, 3,39, 9,24, 6,27,23,36,11,14,21, 4,16,29,51,38,40,56,48,67,42,18,26,44,34,54,58,65,46,64,59,61,49,69, 67,51,56,36,54,31,44,59,20,65,27,49, 7,29,69,64,42,61,21, 0,46,34, 1,11,58,48, 9,26, 5,18, 8,16,19,38, 3,32,14,40, 2,23,10,28, 4,35,24,13,12, 6,22,30,15,37,52,55,39,68,47,17,41,43,25,53,33,66,57,63,45,62,60,70,50, 69,54,64,44,56,42,51,58,21,61,29,48,11,31,65,67,36,59,27, 9,40,38, 2,20,49,46, 7,23, 3,13,10, 6,12,26, 1,30,17,34, 0,18, 5,22,15,41,25,16, 8, 4,19,28,14,33,43,53,45,63,50,24,32,35,37,52,39,70,60,55,47,66,62,68,57, 41,53,43,63,52,70,55,22,57,30,62,12,47,66,32,35,68,28,60,39,10, 3,37,50,19, 8,45, 2,24, 9,14,11, 4, 1,25,18,29, 5,33, 0,17,16,21,26,42, 7,15,20, 6,13,27,44,34,46,54,49,64,31,23,38,36,40,51,59,69,48,56,61,65,58,67, 65,56,67,51,64,36,54,49,27,59,31,46,20,42,61,69,44,58,29, 7,34,26, 0,21,48,40,11,18, 1,16, 5, 4, 8,23, 2,28,24,38, 9,13, 3,19,14,32,37, 6,10,15,12,22,17,39,35,52,47,55,57,25,30,41,33,43,45,68,62,53,50,70,66,63,60, 35,55,52,68,53,66,63,28,50,32,60,19,45,62,41,43,70,30,57,33, 8, 5,25,47,22,12,39, 1,17, 0,15, 7, 6, 3,24,23,27,10,37, 2,14,13,20,38,31, 9, 4,11,16,18,21,36,40,48,51,58,56,29,26,34,42,46,44,61,67,49,54,65,69,59,64, 40,58,48,61,49,69,59,23,54,38,64,13,44,67,34,46,65,26,56,42, 6,15,29,51,18,16,36,17,21,25,11,33, 9,14,27, 3,50, 4,31,24,20, 2,45,10,60,37, 7,39, 0, 1,47,66,12,22,68,30,55,57, 5, 8,62,19,70,41,52,28,63,35,43,32,53, 70,57,62,47,60,39,50,53,24,63,37,43,14,33,68,66,45,55,25, 4,41,30,16,17,52,35,15,22,18,12,26,10,34,28,13,49, 2,32, 6,19,23,46, 3,59, 9, 8,38, 5,40,48, 1,11,65,67,21,56,29, 0,58,61, 7,69,20,51,42,64,27,44,36,54,31, 68,60,66,50,62,45,57,52,25,55,33,35,17,39,63,70,47,53,37,15,32,28, 6,24,43,41,14,19,13, 8,23, 5,38,22,16,48, 0,30, 4,12,18,40, 1,58, 7,10,26, 3,34,46, 2,20,61,69,27,64,31, 9,49,59,11,65,21,54,36,67,29,51,44,56,42, 46,59,49,65,58,67,61,26,51,34,56,18,36,64,40,48,69,38,54,31,16, 4,27,44,23,13,42,14,20,24, 7,37, 0,15,21, 5,47, 6,29,17,11, 1,39, 8,57,25, 9,33, 2, 3,45,62,19,28,70,32,63,50,10,12,60,22,66,35,53,30,68,43,52,41,55, 63,62,70,57,66,47,60,43,37,53,39,41,24,45,55,68,50,52,33,14,30,22, 4,25,35,32,17,12,16,10,18, 3,26,19, 6,46, 9,28,15, 8,13,34, 2,49,11, 5,23, 1,38,40, 0,21,59,65,29,67,42, 7,48,58,20,61,27,56,44,69,31,54,51,64,36, 48,61,58,69,59,64,65,38,44,40,54,23,42,56,46,49,67,34,51,29,13, 6,21,36,26,18,31,15,11,17, 9,25, 2, 4,20,10,45,16,27,14, 7, 3,33,12,50,24, 0,37, 1, 5,39,60,22,30,66,41,68,47, 8,19,57,28,62,43,55,32,70,52,53,35,63, 61,64,69,54,67,44,56,48,29,58,42,40,21,36,59,65,51,49,31,11,38,23, 9,27,46,34,20,13, 2, 6, 3,15,10,18, 0,22,25,26, 7,16, 1,12,17,30,33, 4, 5,14, 8,19,24,45,41,43,50,53,60,37,28,32,39,35,47,63,66,52,57,68,70,55,62, 43,63,53,70,55,62,68,30,47,41,57,22,39,60,35,52,66,32,50,37,12,10,24,45,28,19,33, 3,14, 2, 4, 9,16, 5,17,26,21, 8,25, 1,15,18,11,34,29, 0, 6, 7,13,23,20,42,46,49,44,59,54,27,38,40,31,48,36,65,64,58,51,69,67,61,56, 55,66,68,60,70,50,62,35,33,52,45,32,25,47,53,63,57,43,39,17,28,19,15,37,41,30,24, 8, 6, 5,13, 1,23,12, 4,40, 7,22,14,10,16,38, 0,48,20, 3,18, 2,26,34, 9,27,58,61,31,69,36,11,46,49,21,59,29,64,51,65,42,56,54,67,44, 49,65,59,67,61,56,69,34,36,46,51,26,31,54,48,58,64,40,44,27,18,16,20,42,38,23,29, 4, 7,14, 0,24, 1, 6,11, 8,39,13,21,15, 9, 5,37,19,47,17, 2,25, 3,10,33,57,28,32,62,35,70,45,12,22,50,30,60,52,63,41,66,53,55,43,68, 52,68,55,66,63,60,70,32,45,35,50,28,33,57,43,53,62,41,47,25,19, 8,17,39,30,22,37, 5,15, 1, 6, 0,13,10,14,38,20,12,24, 3, 4,23, 7,40,27, 2,16, 9,18,26,11,31,48,58,36,61,51,21,34,46,29,49,42,69,56,59,44,67,64,65,54, 59,67,65,56,69,51,64,46,31,49,36,34,27,44,58,61,54,48,42,20,26,18, 7,29,40,38,21,16, 0, 4, 1,14, 5,13, 9,19,37,23,11, 6, 2, 8,24,28,39,15, 3,17,10,12,25,47,32,35,57,52,62,33,22,30,45,41,50,55,70,43,60,63,68,53,66, 53,70,63,62,68,57,66,41,39,43,47,30,37,50,52,55,60,35,45,24,22,12,14,33,32,28,25,10, 4, 3,16, 2,18, 8,15,34,11,19,17, 5, 6,26, 9,46,21, 1,13, 0,23,38, 7,29,49,59,42,65,44,20,40,48,27,58,31,67,54,61,36,64,56,69,51, 58,69,61,64,65,54,67,40,42,48,44,38,29,51,49,59,56,46,36,21,23,13,11,31,34,26,27, 6, 9,15, 2,17, 3,16, 7,12,33,18,20, 4, 0,10,25,22,45,14, 1,24, 5, 8,37,50,30,41,60,43,66,39,19,28,47,32,57,53,68,35,62,55,63,52,70 ]) ]). ============================== end of model ========================== ============================== STATISTICS ============================ For domain size 71. Current CPU time: 0.00 seconds (total CPU time: 40879.72 seconds). Ground clauses: seen=363034, kept=362892. Selections=59492, assignments=3456678, propagations=60257317, current_models=1. Rewrite_terms=1827005142, rewrite_bools=188396795, indexes=312228393. Rules_from_neg_clauses=570253, cross_offs=718886773. ============================== end of statistics ===================== User_CPU=40879.72, System_CPU=7.33, Wall_clock=41087. Exiting with 1 model. Process 2788 exit (max_models) Mon Mar 25 09:25:48 2013 The process finished Mon Mar 25 09:25:48 2013