============================== Mace4 ================================= Mace4 (32) version Dec-2007, Dec 2007. Process 2336 was started by Alexei on Alexei-PC, Sun Mar 17 16:22:00 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 * a9. a4 = a3 * a8. a5 = a4 * a1. a6 = a5 * a2. a7 = a6 * a3. a8 = a7 * a4. a9 = a8 * a7. a10 = a9 * a6. a1 = a10 * a5. 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 * a9. a4 = a3 * a8. a5 = a4 * a1. a6 = a5 * a2. a7 = a6 * a3. a8 = a7 * a4. a9 = a8 * a7. a10 = a9 * a6. a1 = a10 * a5. a1 != a2 | a3 != a2 | a4 != a3 | a5 != a4 | a6 != a5 | a7 != a6 | a7 != a8 | a8 != a9 | 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=79, rewrite_bools=23, indexes=0. Rules_from_neg_clauses=5, cross_offs=5. ============================== 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=55, current_models=0. Rewrite_terms=551, rewrite_bools=126, indexes=44. Rules_from_neg_clauses=11, cross_offs=31. ============================== 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=96, current_models=0. Rewrite_terms=1122, rewrite_bools=220, indexes=142. Rules_from_neg_clauses=18, cross_offs=80. ============================== 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=13, assignments=43, propagations=152, current_models=0. Rewrite_terms=2111, rewrite_bools=377, indexes=277. Rules_from_neg_clauses=21, cross_offs=188. ============================== 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=212, current_models=0. Rewrite_terms=4126, rewrite_bools=819, indexes=466. Rules_from_neg_clauses=35, cross_offs=360. ============================== 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=18, assignments=77, propagations=321, current_models=0. Rewrite_terms=5823, rewrite_bools=963, indexes=797. Rules_from_neg_clauses=33, cross_offs=547. ============================== 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=18, assignments=78, propagations=349, current_models=0. Rewrite_terms=6977, rewrite_bools=1038, indexes=1019. Rules_from_neg_clauses=35, cross_offs=790. ============================== 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=23, assignments=121, propagations=641, current_models=0. Rewrite_terms=13396, rewrite_bools=2066, indexes=1654. Rules_from_neg_clauses=67, cross_offs=1330. ============================== end of statistics ===================== ============================== DOMAIN SIZE 10 ======================== ============================== STATISTICS ============================ For domain size 10. Current CPU time: 0.00 seconds (total CPU time: 0.01 seconds). Ground clauses: seen=1121, kept=1101. Selections=24, assignments=131, propagations=750, current_models=0. Rewrite_terms=17998, rewrite_bools=2875, indexes=2213. Rules_from_neg_clauses=62, cross_offs=1783. ============================== 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=29, assignments=184, propagations=1145, current_models=0. Rewrite_terms=26283, rewrite_bools=4089, indexes=3245. Rules_from_neg_clauses=80, cross_offs=2589. ============================== 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=30, assignments=196, propagations=1371, current_models=0. Rewrite_terms=37022, rewrite_bools=5937, indexes=4132. Rules_from_neg_clauses=96, cross_offs=3576. ============================== 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=35, assignments=259, propagations=1952, current_models=0. Rewrite_terms=48358, rewrite_bools=7631, indexes=5797. Rules_from_neg_clauses=118, cross_offs=4818. ============================== 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=37, assignments=286, propagations=2142, current_models=0. Rewrite_terms=59540, rewrite_bools=8973, indexes=7117. Rules_from_neg_clauses=166, cross_offs=6451. ============================== 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=41, assignments=344, propagations=2630, current_models=0. Rewrite_terms=75996, rewrite_bools=11884, indexes=8831. Rules_from_neg_clauses=208, cross_offs=8419. ============================== 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=43, assignments=375, propagations=2853, current_models=0. Rewrite_terms=97981, rewrite_bools=16213, indexes=10798. Rules_from_neg_clauses=167, cross_offs=10439. ============================== end of statistics ===================== ============================== DOMAIN SIZE 17 ======================== ============================== STATISTICS ============================ For domain size 17. Current CPU time: 0.00 seconds (total CPU time: 0.20 seconds). Ground clauses: seen=5230, kept=5196. Selections=46, assignments=425, propagations=3361, current_models=0. Rewrite_terms=108496, rewrite_bools=15639, indexes=13042. Rules_from_neg_clauses=267, cross_offs=13606. ============================== end of statistics ===================== ============================== DOMAIN SIZE 18 ======================== ============================== STATISTICS ============================ For domain size 18. Current CPU time: 0.00 seconds (total CPU time: 0.27 seconds). Ground clauses: seen=6185, kept=6149. Selections=47, assignments=443, propagations=3639, current_models=0. Rewrite_terms=137942, rewrite_bools=22025, indexes=15024. Rules_from_neg_clauses=198, cross_offs=16453. ============================== end of statistics ===================== ============================== DOMAIN SIZE 19 ======================== ============================== STATISTICS ============================ For domain size 19. Current CPU time: 0.00 seconds (total CPU time: 0.36 seconds). Ground clauses: seen=7250, kept=7212. Selections=50, assignments=499, propagations=4403, current_models=0. Rewrite_terms=155747, rewrite_bools=23183, indexes=18212. Rules_from_neg_clauses=204, cross_offs=19640. ============================== end of statistics ===================== ============================== DOMAIN SIZE 20 ======================== ============================== STATISTICS ============================ For domain size 20. Current CPU time: 0.00 seconds (total CPU time: 0.45 seconds). Ground clauses: seen=8431, kept=8391. Selections=51, assignments=519, propagations=4519, current_models=0. Rewrite_terms=159792, rewrite_bools=22030, indexes=20436. Rules_from_neg_clauses=188, cross_offs=22751. ============================== end of statistics ===================== ============================== DOMAIN SIZE 21 ======================== ============================== STATISTICS ============================ For domain size 21. Current CPU time: 0.00 seconds (total CPU time: 0.58 seconds). Ground clauses: seen=9734, kept=9692. Selections=55, assignments=601, propagations=5889, current_models=0. Rewrite_terms=205618, rewrite_bools=28332, indexes=25125. Rules_from_neg_clauses=271, cross_offs=27553. ============================== end of statistics ===================== ============================== DOMAIN SIZE 22 ======================== ============================== STATISTICS ============================ For domain size 22. Current CPU time: 0.00 seconds (total CPU time: 0.73 seconds). Ground clauses: seen=11165, kept=11121. Selections=57, assignments=644, propagations=6332, current_models=0. Rewrite_terms=227093, rewrite_bools=31232, indexes=28381. Rules_from_neg_clauses=253, cross_offs=31446. ============================== end of statistics ===================== ============================== DOMAIN SIZE 23 ======================== ============================== STATISTICS ============================ For domain size 23. Current CPU time: 0.00 seconds (total CPU time: 0.92 seconds). Ground clauses: seen=12730, kept=12684. Selections=61, assignments=734, propagations=7610, current_models=0. Rewrite_terms=280722, rewrite_bools=38494, indexes=34029. Rules_from_neg_clauses=275, cross_offs=37140. ============================== end of statistics ===================== ============================== DOMAIN SIZE 24 ======================== ============================== STATISTICS ============================ For domain size 24. Current CPU time: 0.00 seconds (total CPU time: 1.19 seconds). Ground clauses: seen=14435, kept=14387. Selections=63, assignments=781, propagations=8232, current_models=0. Rewrite_terms=333749, rewrite_bools=49205, indexes=38878. Rules_from_neg_clauses=299, cross_offs=42475. ============================== end of statistics ===================== ============================== DOMAIN SIZE 25 ======================== ============================== STATISTICS ============================ For domain size 25. Current CPU time: 0.00 seconds (total CPU time: 1.51 seconds). Ground clauses: seen=16286, kept=16236. Selections=67, assignments=879, propagations=10139, current_models=0. Rewrite_terms=418835, rewrite_bools=62827, indexes=45827. Rules_from_neg_clauses=373, cross_offs=49442. ============================== end of statistics ===================== ============================== DOMAIN SIZE 26 ======================== ============================== STATISTICS ============================ For domain size 26. Current CPU time: 0.00 seconds (total CPU time: 1.89 seconds). Ground clauses: seen=18289, kept=18237. Selections=70, assignments=955, propagations=11887, current_models=0. Rewrite_terms=478204, rewrite_bools=69291, indexes=53002. Rules_from_neg_clauses=430, cross_offs=57647. ============================== end of statistics ===================== ============================== DOMAIN SIZE 27 ======================== ============================== STATISTICS ============================ For domain size 27. Current CPU time: 0.00 seconds (total CPU time: 2.41 seconds). Ground clauses: seen=20450, kept=20396. Selections=76, assignments=1113, propagations=14518, current_models=0. Rewrite_terms=569622, rewrite_bools=83557, indexes=61792. Rules_from_neg_clauses=569, cross_offs=67313. ============================== end of statistics ===================== ============================== DOMAIN SIZE 28 ======================== ============================== STATISTICS ============================ For domain size 28. Current CPU time: 0.00 seconds (total CPU time: 3.09 seconds). Ground clauses: seen=22775, kept=22719. Selections=79, assignments=1195, propagations=16333, current_models=0. Rewrite_terms=715449, rewrite_bools=112736, indexes=71797. Rules_from_neg_clauses=507, cross_offs=78098. ============================== end of statistics ===================== ============================== DOMAIN SIZE 29 ======================== ============================== STATISTICS ============================ For domain size 29. Current CPU time: 0.00 seconds (total CPU time: 3.91 seconds). Ground clauses: seen=25270, kept=25212. Selections=85, assignments=1365, propagations=19802, current_models=0. Rewrite_terms=815137, rewrite_bools=124702, indexes=82872. Rules_from_neg_clauses=639, cross_offs=91339. ============================== end of statistics ===================== ============================== DOMAIN SIZE 30 ======================== ============================== STATISTICS ============================ For domain size 30. Current CPU time: 0.00 seconds (total CPU time: 4.91 seconds). Ground clauses: seen=27941, kept=27881. Selections=90, assignments=1511, propagations=22501, current_models=0. Rewrite_terms=963901, rewrite_bools=154423, indexes=94102. Rules_from_neg_clauses=718, cross_offs=104169. ============================== end of statistics ===================== ============================== DOMAIN SIZE 31 ======================== ============================== STATISTICS ============================ For domain size 31. Current CPU time: 0.00 seconds (total CPU time: 6.06 seconds). Ground clauses: seen=30794, kept=30732. Selections=98, assignments=1753, propagations=26656, current_models=0. Rewrite_terms=1068373, rewrite_bools=168910, indexes=109168. Rules_from_neg_clauses=794, cross_offs=117664. ============================== end of statistics ===================== ============================== DOMAIN SIZE 32 ======================== ============================== STATISTICS ============================ For domain size 32. Current CPU time: 0.00 seconds (total CPU time: 7.47 seconds). Ground clauses: seen=33835, kept=33771. Selections=103, assignments=1909, propagations=29668, current_models=0. Rewrite_terms=1225772, rewrite_bools=194688, indexes=121021. Rules_from_neg_clauses=784, cross_offs=134875. ============================== end of statistics ===================== ============================== DOMAIN SIZE 33 ======================== ============================== STATISTICS ============================ For domain size 33. Current CPU time: 0.00 seconds (total CPU time: 9.05 seconds). Ground clauses: seen=37070, kept=37004. Selections=109, assignments=2103, propagations=33278, current_models=0. Rewrite_terms=1343034, rewrite_bools=207799, indexes=136338. Rules_from_neg_clauses=893, cross_offs=151854. ============================== end of statistics ===================== ============================== DOMAIN SIZE 34 ======================== ============================== STATISTICS ============================ For domain size 34. Current CPU time: 0.00 seconds (total CPU time: 10.92 seconds). Ground clauses: seen=40505, kept=40437. Selections=113, assignments=2236, propagations=35859, current_models=0. Rewrite_terms=1511028, rewrite_bools=236703, indexes=152508. Rules_from_neg_clauses=867, cross_offs=171760. ============================== end of statistics ===================== ============================== DOMAIN SIZE 35 ======================== ============================== STATISTICS ============================ For domain size 35. Current CPU time: 0.00 seconds (total CPU time: 13.20 seconds). Ground clauses: seen=44146, kept=44076. Selections=118, assignments=2408, propagations=39763, current_models=0. Rewrite_terms=1752328, rewrite_bools=276999, indexes=170770. Rules_from_neg_clauses=938, cross_offs=196306. ============================== end of statistics ===================== ============================== DOMAIN SIZE 36 ======================== ============================== STATISTICS ============================ For domain size 36. Current CPU time: 0.00 seconds (total CPU time: 15.84 seconds). Ground clauses: seen=47999, kept=47927. Selections=121, assignments=2514, propagations=41650, current_models=0. Rewrite_terms=1943280, rewrite_bools=310111, indexes=187412. Rules_from_neg_clauses=874, cross_offs=215110. ============================== end of statistics ===================== ============================== DOMAIN SIZE 37 ======================== ============================== STATISTICS ============================ For domain size 37. Current CPU time: 0.00 seconds (total CPU time: 18.77 seconds). Ground clauses: seen=52070, kept=51996. Selections=126, assignments=2696, propagations=44543, current_models=0. Rewrite_terms=2090416, rewrite_bools=336525, indexes=206289. Rules_from_neg_clauses=1020, cross_offs=237425. ============================== end of statistics ===================== ============================== DOMAIN SIZE 38 ======================== ============================== STATISTICS ============================ For domain size 38. Current CPU time: 0.00 seconds (total CPU time: 22.22 seconds). Ground clauses: seen=56365, kept=56289. Selections=128, assignments=2771, propagations=45988, current_models=0. Rewrite_terms=2380864, rewrite_bools=399197, indexes=224344. Rules_from_neg_clauses=958, cross_offs=263314. ============================== end of statistics ===================== ============================== DOMAIN SIZE 39 ======================== ============================== STATISTICS ============================ For domain size 39. Current CPU time: 0.00 seconds (total CPU time: 26.00 seconds). Ground clauses: seen=60890, kept=60812. Selections=131, assignments=2887, propagations=48331, current_models=0. Rewrite_terms=2509902, rewrite_bools=406739, indexes=243147. Rules_from_neg_clauses=935, cross_offs=287861. ============================== end of statistics ===================== ============================== DOMAIN SIZE 40 ======================== ============================== STATISTICS ============================ For domain size 40. Current CPU time: 0.00 seconds (total CPU time: 30.12 seconds). Ground clauses: seen=65651, kept=65571. Selections=132, assignments=2927, propagations=49210, current_models=0. Rewrite_terms=2657916, rewrite_bools=429710, indexes=261169. Rules_from_neg_clauses=1041, cross_offs=315908. ============================== end of statistics ===================== ============================== DOMAIN SIZE 41 ======================== ============================== STATISTICS ============================ For domain size 41. Current CPU time: 0.00 seconds (total CPU time: 34.69 seconds). Ground clauses: seen=70654, kept=70572. Selections=135, assignments=3049, propagations=51737, current_models=0. Rewrite_terms=2837059, rewrite_bools=451402, indexes=280797. Rules_from_neg_clauses=1085, cross_offs=341977. ============================== end of statistics ===================== ============================== DOMAIN SIZE 42 ======================== ============================== STATISTICS ============================ For domain size 42. Current CPU time: 0.00 seconds (total CPU time: 39.53 seconds). Ground clauses: seen=75905, kept=75821. Selections=137, assignments=3132, propagations=52326, current_models=0. Rewrite_terms=2948612, rewrite_bools=467965, indexes=298225. Rules_from_neg_clauses=1027, cross_offs=371447. ============================== end of statistics ===================== ============================== DOMAIN SIZE 43 ======================== ============================== STATISTICS ============================ For domain size 43. Current CPU time: 0.00 seconds (total CPU time: 45.03 seconds). Ground clauses: seen=81410, kept=81324. Selections=139, assignments=3218, propagations=55461, current_models=0. Rewrite_terms=3247028, rewrite_bools=509964, indexes=325940. Rules_from_neg_clauses=859, cross_offs=403248. ============================== end of statistics ===================== ============================== DOMAIN SIZE 44 ======================== ============================== STATISTICS ============================ For domain size 44. Current CPU time: 0.00 seconds (total CPU time: 51.28 seconds). Ground clauses: seen=87175, kept=87087. Selections=139, assignments=3219, propagations=56773, current_models=0. Rewrite_terms=3529944, rewrite_bools=548665, indexes=346745. Rules_from_neg_clauses=922, cross_offs=439639. ============================== end of statistics ===================== ============================== DOMAIN SIZE 45 ======================== ============================== STATISTICS ============================ For domain size 45. Current CPU time: 0.00 seconds (total CPU time: 57.77 seconds). Ground clauses: seen=93206, kept=93116. Selections=142, assignments=3353, propagations=60162, current_models=0. Rewrite_terms=3633883, rewrite_bools=558396, indexes=373266. Rules_from_neg_clauses=1179, cross_offs=472655. ============================== end of statistics ===================== ============================== DOMAIN SIZE 46 ======================== ============================== STATISTICS ============================ For domain size 46. Current CPU time: 0.00 seconds (total CPU time: 64.81 seconds). Ground clauses: seen=99509, kept=99417. Selections=143, assignments=3399, propagations=61353, current_models=0. Rewrite_terms=3801936, rewrite_bools=568577, indexes=392177. Rules_from_neg_clauses=1166, cross_offs=509618. ============================== end of statistics ===================== ============================== DOMAIN SIZE 47 ======================== ============================== STATISTICS ============================ For domain size 47. Current CPU time: 0.00 seconds (total CPU time: 72.30 seconds). Ground clauses: seen=106090, kept=105996. Selections=145, assignments=3493, propagations=65402, current_models=0. Rewrite_terms=3972716, rewrite_bools=578800, indexes=418774. Rules_from_neg_clauses=1121, cross_offs=553483. ============================== end of statistics ===================== ============================== DOMAIN SIZE 48 ======================== ============================== STATISTICS ============================ For domain size 48. Current CPU time: 0.00 seconds (total CPU time: 81.23 seconds). Ground clauses: seen=112955, kept=112859. Selections=146, assignments=3541, propagations=66531, current_models=0. Rewrite_terms=4452679, rewrite_bools=672860, indexes=442530. Rules_from_neg_clauses=1304, cross_offs=590765. ============================== end of statistics ===================== ============================== DOMAIN SIZE 49 ======================== ============================== STATISTICS ============================ For domain size 49. Current CPU time: 0.00 seconds (total CPU time: 90.88 seconds). Ground clauses: seen=120110, kept=120012. Selections=150, assignments=3735, propagations=70491, current_models=0. Rewrite_terms=4705096, rewrite_bools=710223, indexes=473149. Rules_from_neg_clauses=1639, cross_offs=630507. ============================== end of statistics ===================== ============================== DOMAIN SIZE 50 ======================== ============================== STATISTICS ============================ For domain size 50. Current CPU time: 0.00 seconds (total CPU time: 100.80 seconds). Ground clauses: seen=127561, kept=127461. Selections=151, assignments=3785, propagations=70596, current_models=0. Rewrite_terms=4727425, rewrite_bools=701100, indexes=496543. Rules_from_neg_clauses=1218, cross_offs=678065. ============================== end of statistics ===================== ============================== DOMAIN SIZE 51 ======================== ============================== STATISTICS ============================ For domain size 51. Current CPU time: 0.00 seconds (total CPU time: 111.88 seconds). Ground clauses: seen=135314, kept=135212. Selections=154, assignments=3937, propagations=75909, current_models=0. Rewrite_terms=5118276, rewrite_bools=749448, indexes=531842. Rules_from_neg_clauses=1589, cross_offs=728530. ============================== end of statistics ===================== ============================== DOMAIN SIZE 52 ======================== ============================== STATISTICS ============================ For domain size 52. Current CPU time: 0.00 seconds (total CPU time: 123.44 seconds). Ground clauses: seen=143375, kept=143271. Selections=155, assignments=3989, propagations=76287, current_models=0. Rewrite_terms=5217037, rewrite_bools=751215, indexes=555692. Rules_from_neg_clauses=1302, cross_offs=775305. ============================== end of statistics ===================== ============================== DOMAIN SIZE 53 ======================== ============================== STATISTICS ============================ For domain size 53. Current CPU time: 0.00 seconds (total CPU time: 136.69 seconds). Ground clauses: seen=151750, kept=151644. Selections=158, assignments=4147, propagations=81956, current_models=0. Rewrite_terms=5747392, rewrite_bools=825658, indexes=593752. Rules_from_neg_clauses=1636, cross_offs=829880. ============================== end of statistics ===================== ============================== DOMAIN SIZE 54 ======================== ============================== STATISTICS ============================ For domain size 54. Current CPU time: 0.00 seconds (total CPU time: 151.28 seconds). Ground clauses: seen=160445, kept=160337. Selections=160, assignments=4254, propagations=82837, current_models=0. Rewrite_terms=6103269, rewrite_bools=897167, indexes=623061. Rules_from_neg_clauses=1552, cross_offs=882167. ============================== end of statistics ===================== ============================== DOMAIN SIZE 55 ======================== ============================== STATISTICS ============================ For domain size 55. Current CPU time: 0.00 seconds (total CPU time: 167.62 seconds). Ground clauses: seen=169466, kept=169356. Selections=163, assignments=4418, propagations=88582, current_models=0. Rewrite_terms=6588304, rewrite_bools=951439, indexes=663114. Rules_from_neg_clauses=1721, cross_offs=944836. ============================== end of statistics ===================== ============================== DOMAIN SIZE 56 ======================== ============================== STATISTICS ============================ For domain size 56. Current CPU time: 0.00 seconds (total CPU time: 185.64 seconds). Ground clauses: seen=178819, kept=178707. Selections=163, assignments=4419, propagations=90487, current_models=0. Rewrite_terms=6989521, rewrite_bools=995749, indexes=695601. Rules_from_neg_clauses=1490, cross_offs=1010475. ============================== end of statistics ===================== ============================== DOMAIN SIZE 57 ======================== ============================== STATISTICS ============================ For domain size 57. Current CPU time: 0.00 seconds (total CPU time: 205.94 seconds). Ground clauses: seen=188510, kept=188396. Selections=165, assignments=4533, propagations=96516, current_models=0. Rewrite_terms=7623109, rewrite_bools=1113786, indexes=736243. Rules_from_neg_clauses=1654, cross_offs=1078333. ============================== end of statistics ===================== ============================== DOMAIN SIZE 58 ======================== ============================== STATISTICS ============================ For domain size 58. Current CPU time: 0.00 seconds (total CPU time: 228.14 seconds). Ground clauses: seen=198545, kept=198429. Selections=166, assignments=4591, propagations=98174, current_models=0. Rewrite_terms=8120492, rewrite_bools=1206357, indexes=774193. Rules_from_neg_clauses=1837, cross_offs=1138151. ============================== end of statistics ===================== ============================== DOMAIN SIZE 59 ======================== ============================== STATISTICS ============================ For domain size 59. Current CPU time: 0.00 seconds (total CPU time: 252.38 seconds). Ground clauses: seen=208930, kept=208812. Selections=170, assignments=4825, propagations=103590, current_models=0. Rewrite_terms=8533755, rewrite_bools=1250729, indexes=819863. Rules_from_neg_clauses=2346, cross_offs=1209156. ============================== end of statistics ===================== ============================== DOMAIN SIZE 60 ======================== ============================== STATISTICS ============================ For domain size 60. Current CPU time: 0.00 seconds (total CPU time: 279.59 seconds). Ground clauses: seen=219671, kept=219551. Selections=172, assignments=4944, propagations=104137, current_models=0. Rewrite_terms=9258758, rewrite_bools=1416434, indexes=862898. Rules_from_neg_clauses=1961, cross_offs=1284428. ============================== end of statistics ===================== ============================== DOMAIN SIZE 61 ======================== ============================== STATISTICS ============================ For domain size 61. Current CPU time: 0.00 seconds (total CPU time: 309.55 seconds). Ground clauses: seen=230774, kept=230652. Selections=175, assignments=5126, propagations=111281, current_models=0. Rewrite_terms=9877259, rewrite_bools=1479779, indexes=910093. Rules_from_neg_clauses=2032, cross_offs=1367000. ============================== end of statistics ===================== ============================== DOMAIN SIZE 62 ======================== ============================== STATISTICS ============================ For domain size 62. Current CPU time: 0.00 seconds (total CPU time: 342.89 seconds). Ground clauses: seen=242245, kept=242121. Selections=175, assignments=5127, propagations=113683, current_models=0. Rewrite_terms=10704002, rewrite_bools=1643508, indexes=957664. Rules_from_neg_clauses=1789, cross_offs=1452898. ============================== end of statistics ===================== ============================== DOMAIN SIZE 63 ======================== ============================== STATISTICS ============================ For domain size 63. Current CPU time: 0.00 seconds (total CPU time: 379.31 seconds). Ground clauses: seen=254090, kept=253964. Selections=177, assignments=5253, propagations=120975, current_models=0. Rewrite_terms=11397732, rewrite_bools=1741774, indexes=1007432. Rules_from_neg_clauses=2033, cross_offs=1542784. ============================== end of statistics ===================== ============================== DOMAIN SIZE 64 ======================== ============================== STATISTICS ============================ For domain size 64. Current CPU time: 0.00 seconds (total CPU time: 419.17 seconds). Ground clauses: seen=266315, kept=266187. Selections=178, assignments=5317, propagations=123032, current_models=0. Rewrite_terms=12084256, rewrite_bools=1896612, indexes=1057329. Rules_from_neg_clauses=2123, cross_offs=1622337. ============================== end of statistics ===================== ============================== DOMAIN SIZE 65 ======================== ============================== STATISTICS ============================ For domain size 65. Current CPU time: 0.00 seconds (total CPU time: 467.61 seconds). Ground clauses: seen=278926, kept=278796. Selections=182, assignments=5575, propagations=129844, current_models=0. Rewrite_terms=13315405, rewrite_bools=2174505, indexes=1117983. Rules_from_neg_clauses=2808, cross_offs=1725015. ============================== end of statistics ===================== ============================== DOMAIN SIZE 66 ======================== ============================== STATISTICS ============================ For domain size 66. Current CPU time: 0.00 seconds (total CPU time: 515.76 seconds). Ground clauses: seen=291929, kept=291797. Selections=184, assignments=5706, propagations=130678, current_models=0. Rewrite_terms=13851251, rewrite_bools=2272001, indexes=1176279. Rules_from_neg_clauses=2230, cross_offs=1816389. ============================== end of statistics ===================== ============================== DOMAIN SIZE 67 ======================== ============================== STATISTICS ============================ For domain size 67. Current CPU time: 0.00 seconds (total CPU time: 566.89 seconds). Ground clauses: seen=305330, kept=305196. Selections=187, assignments=5906, propagations=138028, current_models=0. Rewrite_terms=14426361, rewrite_bools=2350403, indexes=1240483. Rules_from_neg_clauses=2317, cross_offs=1924482. ============================== end of statistics ===================== ============================== DOMAIN SIZE 68 ======================== ============================== STATISTICS ============================ For domain size 68. Current CPU time: 0.00 seconds (total CPU time: 621.03 seconds). Ground clauses: seen=319135, kept=318999. Selections=187, assignments=5907, propagations=138646, current_models=0. Rewrite_terms=14953789, rewrite_bools=2426342, indexes=1296944. Rules_from_neg_clauses=2050, cross_offs=2030854. ============================== end of statistics ===================== ============================== DOMAIN SIZE 69 ======================== ============================== STATISTICS ============================ For domain size 69. Current CPU time: 0.00 seconds (total CPU time: 684.09 seconds). Ground clauses: seen=333350, kept=333212. Selections=189, assignments=6045, propagations=148525, current_models=0. Rewrite_terms=16586929, rewrite_bools=2668659, indexes=1375405. Rules_from_neg_clauses=2216, cross_offs=2155624. ============================== end of statistics ===================== ============================== DOMAIN SIZE 70 ======================== ============================== STATISTICS ============================ For domain size 70. Current CPU time: 0.00 seconds (total CPU time: 748.17 seconds). Ground clauses: seen=347981, kept=347841. Selections=189, assignments=6046, propagations=152080, current_models=0. Rewrite_terms=16745942, rewrite_bools=2622987, indexes=1431849. Rules_from_neg_clauses=2297, cross_offs=2263985. ============================== end of statistics ===================== ============================== DOMAIN SIZE 71 ======================== ============================== STATISTICS ============================ For domain size 71. Current CPU time: 0.00 seconds (total CPU time: 816.84 seconds). Ground clauses: seen=363034, kept=362892. Selections=191, assignments=6188, propagations=157371, current_models=0. Rewrite_terms=17599413, rewrite_bools=2859148, indexes=1496942. Rules_from_neg_clauses=2290, cross_offs=2382289. ============================== end of statistics ===================== ============================== DOMAIN SIZE 72 ======================== ============================== STATISTICS ============================ For domain size 72. Current CPU time: 0.00 seconds (total CPU time: 887.25 seconds). Ground clauses: seen=378515, kept=378371. Selections=191, assignments=6189, propagations=159691, current_models=0. Rewrite_terms=17809364, rewrite_bools=2860741, indexes=1551799. Rules_from_neg_clauses=2307, cross_offs=2481737. ============================== end of statistics ===================== ============================== DOMAIN SIZE 73 ======================== ============================== STATISTICS ============================ For domain size 73. Current CPU time: 0.00 seconds (total CPU time: 964.88 seconds). Ground clauses: seen=394430, kept=394284. Selections=192, assignments=6262, propagations=164686, current_models=0. Rewrite_terms=18956494, rewrite_bools=3015010, indexes=1632151. Rules_from_neg_clauses=2187, cross_offs=2613709. ============================== end of statistics ===================== ============================== DOMAIN SIZE 74 ======================== ============================== STATISTICS ============================ For domain size 74. Current CPU time: 0.00 seconds (total CPU time: 1047.03 seconds). Ground clauses: seen=410785, kept=410637. Selections=192, assignments=6262, propagations=165620, current_models=0. Rewrite_terms=19643003, rewrite_bools=3120231, indexes=1701041. Rules_from_neg_clauses=2089, cross_offs=2693892. ============================== end of statistics ===================== ============================== DOMAIN SIZE 75 ======================== ============================== STATISTICS ============================ For domain size 75. Current CPU time: 0.00 seconds (total CPU time: 1135.02 seconds). Ground clauses: seen=427586, kept=427436. Selections=193, assignments=6336, propagations=171837, current_models=0. Rewrite_terms=20470795, rewrite_bools=3224692, indexes=1806511. Rules_from_neg_clauses=2800, cross_offs=2790316. ============================== end of statistics ===================== ============================== DOMAIN SIZE 76 ======================== ============================== STATISTICS ============================ For domain size 76. Current CPU time: 0.00 seconds (total CPU time: 1225.28 seconds). Ground clauses: seen=444839, kept=444687. Selections=194, assignments=6411, propagations=176096, current_models=0. Rewrite_terms=20729829, rewrite_bools=3242430, indexes=1868008. Rules_from_neg_clauses=2780, cross_offs=2850886. ============================== end of statistics ===================== ============================== DOMAIN SIZE 77 ======================== ============================== STATISTICS ============================ For domain size 77. Current CPU time: 0.00 seconds (total CPU time: 1317.80 seconds). Ground clauses: seen=462550, kept=462396. Selections=195, assignments=6487, propagations=180670, current_models=0. Rewrite_terms=20992822, rewrite_bools=3261448, indexes=1929520. Rules_from_neg_clauses=2774, cross_offs=2911568. ============================== end of statistics ===================== ============================== DOMAIN SIZE 78 ======================== ============================== STATISTICS ============================ For domain size 78. Current CPU time: 0.00 seconds (total CPU time: 1425.06 seconds). Ground clauses: seen=480725, kept=480569. Selections=196, assignments=6564, propagations=185525, current_models=0. Rewrite_terms=21262728, rewrite_bools=3282746, indexes=1991068. Rules_from_neg_clauses=2756, cross_offs=2972704. ============================== end of statistics ===================== ============================== DOMAIN SIZE 79 ======================== ============================== STATISTICS ============================ For domain size 79. Current CPU time: 0.00 seconds (total CPU time: 1522.00 seconds). Ground clauses: seen=499370, kept=499212. Selections=197, assignments=6642, propagations=190494, current_models=0. Rewrite_terms=21538866, rewrite_bools=3306331, indexes=2052543. Rules_from_neg_clauses=2726, cross_offs=3033524. ============================== end of statistics ===================== ============================== DOMAIN SIZE 80 ======================== ============================== STATISTICS ============================ For domain size 80. Current CPU time: 0.00 seconds (total CPU time: 1621.11 seconds). Ground clauses: seen=518491, kept=518331. Selections=198, assignments=6721, propagations=195752, current_models=0. Rewrite_terms=21818133, rewrite_bools=3330699, indexes=2114087. Rules_from_neg_clauses=2683, cross_offs=3094382. ============================== end of statistics ===================== ============================== DOMAIN SIZE 81 ======================== ============================== STATISTICS ============================ For domain size 81. Current CPU time: 0.00 seconds (total CPU time: 1722.64 seconds). Ground clauses: seen=538094, kept=537932. Selections=199, assignments=6801, propagations=201161, current_models=0. Rewrite_terms=22104193, rewrite_bools=3357442, indexes=2175558. Rules_from_neg_clauses=2646, cross_offs=3155263. ============================== end of statistics ===================== ============================== DOMAIN SIZE 82 ======================== ============================== STATISTICS ============================ For domain size 82. Current CPU time: 0.00 seconds (total CPU time: 1826.70 seconds). Ground clauses: seen=558185, kept=558021. Selections=200, assignments=6882, propagations=206967, current_models=0. Rewrite_terms=22397687, rewrite_bools=3387139, indexes=2236869. Rules_from_neg_clauses=2603, cross_offs=3216664. ============================== end of statistics ===================== ============================== DOMAIN SIZE 83 ======================== ============================== STATISTICS ============================ For domain size 83. Current CPU time: 0.00 seconds (total CPU time: 1933.17 seconds). Ground clauses: seen=578770, kept=578604. Selections=201, assignments=6964, propagations=213078, current_models=0. Rewrite_terms=22695692, rewrite_bools=3418286, indexes=2298180. Rules_from_neg_clauses=2558, cross_offs=3277483. ============================== end of statistics ===================== ============================== DOMAIN SIZE 84 ======================== ============================== STATISTICS ============================ For domain size 84. Current CPU time: 0.00 seconds (total CPU time: 2042.05 seconds). Ground clauses: seen=599855, kept=599687. Selections=202, assignments=7047, propagations=219081, current_models=0. Rewrite_terms=23000763, rewrite_bools=3452279, indexes=2359271. Rules_from_neg_clauses=2498, cross_offs=3338454. ============================== end of statistics ===================== ============================== DOMAIN SIZE 85 ======================== ============================== STATISTICS ============================ For domain size 85. Current CPU time: 0.00 seconds (total CPU time: 2153.44 seconds). Ground clauses: seen=621446, kept=621276. Selections=203, assignments=7131, propagations=225761, current_models=0. Rewrite_terms=23312969, rewrite_bools=3489031, indexes=2420185. Rules_from_neg_clauses=2443, cross_offs=3399708. ============================== end of statistics ===================== ============================== DOMAIN SIZE 86 ======================== ============================== STATISTICS ============================ For domain size 86. Current CPU time: 0.00 seconds (total CPU time: 2267.78 seconds). Ground clauses: seen=643549, kept=643377. Selections=204, assignments=7216, propagations=232410, current_models=0. Rewrite_terms=23632616, rewrite_bools=3528914, indexes=2480813. Rules_from_neg_clauses=2375, cross_offs=3460810. ============================== end of statistics ===================== ============================== DOMAIN SIZE 87 ======================== ============================== STATISTICS ============================ For domain size 87. Current CPU time: 0.00 seconds (total CPU time: 2385.17 seconds). Ground clauses: seen=666170, kept=665996. Selections=205, assignments=7302, propagations=239326, current_models=0. Rewrite_terms=23956875, rewrite_bools=3570429, indexes=2541392. Rules_from_neg_clauses=2316, cross_offs=3521795. ============================== end of statistics ===================== ============================== DOMAIN SIZE 88 ======================== ============================== STATISTICS ============================ For domain size 88. Current CPU time: 0.00 seconds (total CPU time: 2505.16 seconds). Ground clauses: seen=689315, kept=689139. Selections=206, assignments=7389, propagations=246566, current_models=0. Rewrite_terms=24290869, rewrite_bools=3615950, indexes=2601546. Rules_from_neg_clauses=2239, cross_offs=3582670. ============================== end of statistics ===================== ============================== DOMAIN SIZE 89 ======================== ============================== MODEL ================================= interpretation( 89, [number=1, seconds=2628], [ function(a1, [ 0 ]), function(a10, [ 1 ]), function(a2, [ 5 ]), function(a3, [37 ]), function(a4, [ 3 ]), function(a5, [ 2 ]), function(a6, [14 ]), function(a7, [65 ]), function(a8, [72 ]), function(a9, [17 ]), function(*(_,_), [ 0, 5, 1, 4, 7,13,10,18,11,16,17,22,20,29,25,35,37,43,31,28,40,34,52,46,39,49,47,56,57,58,51,63,62,68,69,70,64,75,73,85,79,83,76,84,88,82,87,78,81,67,72,61,80,66,86,77,74,65,55,60,71,59,53,48,45,54,50,44,41,36,33,42,38,27,32,21,26,23,30,15,19,24, 9,12,14, 3, 8, 2, 6, 4, 1, 0, 7,11,10, 5,20,18,13,16,28,22,25,17,29,35,39,34,31,46,40,56,52,37,47,43,57,62,51,49,68,63,69,76,64,58,73,70,83,82,75,79,88,85,87,86,81,84,72,78,66,77,67,80,74,71,59,60,61,65,53,50,44,54,55,48,41,38,30,42,45,36,32,33,23,24,27,26,14,21,15, 6,19, 9, 8,12, 3, 2, 3, 6, 2, 8,12,14, 9,21,19,15,24,27,23,30,26,36,38,44,33,32,45,42,55,54,41,50,48,60,61,59,53,67,66,72,78,71,65,77,74,86,84,80,81,82,87,88,85,76,79,68,69,62,75,63,83,73,70,58,56,57,64,51,49,43,46,52,47,39,37,29,34,40,35,28,31,20,17,22,25,13,18,16, 5,11,10, 4, 7, 0, 1, 2, 9, 6, 3, 8,15,14,19,12,24,26,23,21,36,30,38,41,48,32,27,42,33,54,45,44,53,50,55,60,65,59,66,61,67,72,74,71,80,77,87,81,86,78,79,82,84,88,69,76,63,68,57,83,62,85,75,73,64,52,56,70,58,51,47,40,46,49,43,39,35,31,34,37,22,28,18,25,20,29,16,11,17,10, 7,13, 0, 4, 1, 5, 1,10, 5, 0, 4,16,13,11, 7,17,25,20,18,35,29,37,39,47,28,22,34,31,46,40,43,51,49,52,56,64,58,62,57,63,68,73,70,83,75,88,76,85,69,81,84,79,82,72,78,66,67,60,86,61,87,80,77,71,54,55,74,65,59,50,42,45,53,48,44,38,32,33,41,23,27,19,30,21,36,24,12,26,14, 8,15, 2, 3, 6, 9, 7, 0, 4,11,18, 5, 1,22,20,10,13,31,28,17,16,25,29,37,40,34,52,46,57,56,35,43,39,62,63,49,47,69,68,76,79,58,51,70,64,75,87,73,82,85,83,86,80,84,88,78,81,67,74,72,77,71,65,53,61,66,59,50,48,41,55,60,44,38,36,26,45,54,30,33,42,27,15,32,24, 9,23,14, 2,21, 6,12,19, 8, 3, 8, 2, 3,12,19, 9, 6,23,21,14,15,32,27,26,24,30,36,41,42,33,54,45,60,55,38,48,44,61,66,53,50,72,67,78,81,65,59,74,71,80,88,77,84,87,86,85,83,79,82,69,76,63,73,68,75,70,64,51,57,62,58,49,47,39,52,56,43,37,35,25,40,46,29,31,34,22,16,28,17,10,20,13, 1,18, 5, 7,11, 4, 0, 5,13,10, 1, 0,17,16, 7, 4,25,29,18,11,37,35,39,43,49,22,20,31,28,40,34,47,58,51,46,52,70,64,57,56,62,63,75,73,85,83,84,69,88,68,78,81,76,79,67,72,61,66,55,87,60,82,86,80,74,45,54,77,71,65,53,33,42,59,50,48,41,27,32,44,21,23,12,36,19,38,26, 8,30,15, 3,24, 6, 2, 9,14, 6,14, 9, 2, 3,24,15,12, 8,26,30,21,19,38,36,41,44,50,27,23,33,32,45,42,48,59,53,54,55,71,65,61,60,66,67,77,74,86,80,82,78,87,72,76,79,81,84,68,69,62,63,56,85,57,88,83,75,70,46,52,73,64,58,49,34,40,51,47,43,37,28,31,39,20,22,11,29,18,35,17, 7,25,13, 4,16, 1, 0, 5,10, 12, 3, 8,19,21, 6, 2,27,23, 9,14,33,32,24,15,26,30,38,45,42,55,54,61,60,36,44,41,66,67,50,48,78,72,81,84,59,53,71,65,77,85,74,88,86,80,83,75,82,87,76,79,68,70,69,73,64,58,49,62,63,51,47,43,37,56,57,39,35,29,17,46,52,25,34,40,28,13,31,16, 5,22,10, 0,20, 1,11,18, 7, 4, 11, 4, 7,18,20, 1, 0,28,22, 5,10,34,31,16,13,17,25,35,46,40,56,52,62,57,29,39,37,63,68,47,43,76,69,79,82,51,49,64,58,73,86,70,87,83,75,80,77,88,85,81,84,72,71,78,74,65,59,50,66,67,53,48,44,38,60,61,41,36,30,24,54,55,26,42,45,32,14,33,15, 6,27, 9, 3,23, 2,19,21,12, 8, 10,16,13, 5, 1,25,17, 4, 0,29,35,11, 7,39,37,43,47,51,20,18,28,22,34,31,49,64,58,40,46,73,70,56,52,57,62,83,75,88,85,81,68,84,63,72,78,69,76,66,67,60,61,54,82,55,79,87,86,77,42,45,80,74,71,59,32,33,65,53,50,44,23,27,48,19,21, 8,38,12,41,30, 3,36,24, 2,26, 9, 6,14,15, 9,15,14, 6, 2,26,24, 8, 3,30,36,19,12,41,38,44,48,53,23,21,32,27,42,33,50,65,59,45,54,74,71,60,55,61,66,80,77,87,86,79,72,82,67,69,76,78,81,63,68,57,62,52,88,56,84,85,83,73,40,46,75,70,64,51,31,34,58,49,47,39,22,28,43,18,20, 7,35,11,37,25, 4,29,16, 0,17, 5, 1,10,13, 18, 7,11,20,22, 0, 4,31,28, 1, 5,40,34,13,10,16,17,29,52,46,57,56,63,62,25,37,35,68,69,43,39,79,76,82,87,49,47,58,51,70,80,64,86,75,73,77,74,85,83,84,88,78,65,81,71,59,53,48,67,72,50,44,41,36,61,66,38,30,26,15,55,60,24,45,54,33, 9,42,14, 2,32, 6, 8,27, 3,21,23,19,12, 19, 8,12,21,23, 2, 3,32,27, 6, 9,42,33,15,14,24,26,36,54,45,60,55,66,61,30,41,38,67,72,48,44,81,78,84,88,53,50,65,59,74,83,71,85,80,77,75,73,87,86,79,82,69,64,76,70,58,51,47,63,68,49,43,39,35,57,62,37,29,25,16,52,56,17,40,46,31,10,34,13, 1,28, 5, 4,22, 0,18,20,11, 7, 21,12,19,23,27, 3, 8,33,32, 2, 6,45,42,14, 9,15,24,30,55,54,61,60,67,66,26,38,36,72,78,44,41,84,81,88,85,50,48,59,53,71,75,65,83,77,74,73,70,86,80,82,87,76,58,79,64,51,49,43,68,69,47,39,37,29,62,63,35,25,17,13,56,57,16,46,52,34, 5,40,10, 0,31, 1, 7,28, 4,20,22,18,11, 20,11,18,22,28, 4, 7,34,31, 0, 1,46,40,10, 5,13,16,25,56,52,62,57,68,63,17,35,29,69,76,39,37,82,79,87,86,47,43,51,49,64,77,58,80,73,70,74,71,83,75,88,85,81,59,84,65,53,50,44,72,78,48,41,38,30,66,67,36,26,24,14,60,61,15,54,55,42, 6,45, 9, 3,33, 2,12,32, 8,23,27,21,19, 22,18,20,28,31, 7,11,40,34, 4, 0,52,46, 5, 1,10,13,17,57,56,63,62,69,68,16,29,25,76,79,37,35,87,82,86,80,43,39,49,47,58,74,51,77,70,64,71,65,75,73,85,83,84,53,88,59,50,48,41,78,81,44,38,36,26,67,72,30,24,15, 9,61,66,14,55,60,45, 2,54, 6, 8,42, 3,19,33,12,27,32,23,21, 13,17,16,10, 5,29,25, 0, 1,35,37, 7, 4,43,39,47,49,58,18,11,22,20,31,28,51,70,64,34,40,75,73,52,46,56,57,85,83,84,88,78,63,81,62,67,72,68,69,61,66,55,60,45,79,54,76,82,87,80,33,42,86,77,74,65,27,32,71,59,53,48,21,23,50,12,19, 3,41, 8,44,36, 2,38,26, 6,30,14, 9,15,24, 14,24,15, 9, 6,30,26, 3, 2,36,38,12, 8,44,41,48,50,59,21,19,27,23,33,32,53,71,65,42,45,77,74,55,54,60,61,86,80,82,87,76,67,79,66,68,69,72,78,62,63,56,57,46,84,52,81,88,85,75,34,40,83,73,70,58,28,31,64,51,49,43,20,22,47,11,18, 4,37, 7,39,29, 0,35,17, 1,25,10, 5,13,16, 16,25,17,13,10,35,29, 1, 5,37,39, 4, 0,47,43,49,51,64,11, 7,20,18,28,22,58,73,70,31,34,83,75,46,40,52,56,88,85,81,84,72,62,78,57,66,67,63,68,60,61,54,55,42,76,45,69,79,82,86,32,33,87,80,77,71,23,27,74,65,59,50,19,21,53, 8,12, 2,44, 3,48,38, 6,41,30, 9,36,15,14,24,26, 15,26,24,14, 9,36,30, 2, 6,38,41, 8, 3,48,44,50,53,65,19,12,23,21,32,27,59,74,71,33,42,80,77,54,45,55,60,87,86,79,82,69,66,76,61,63,68,67,72,57,62,52,56,40,81,46,78,84,88,83,31,34,85,75,73,64,22,28,70,58,51,47,18,20,49, 7,11, 0,39, 4,43,35, 1,37,25, 5,29,13,10,16,17, 17,29,25,16,13,37,35, 5,10,39,43, 0, 1,49,47,51,58,70, 7, 4,18,11,22,20,64,75,73,28,31,85,83,40,34,46,52,84,88,78,81,67,57,72,56,61,66,62,63,55,60,45,54,33,69,42,68,76,79,87,27,32,82,86,80,74,21,23,77,71,65,53,12,19,59, 3, 8, 6,48, 2,50,41, 9,44,36,14,38,24,15,26,30, 24,30,26,15,14,38,36, 6, 9,41,44, 3, 2,50,48,53,59,71,12, 8,21,19,27,23,65,77,74,32,33,86,80,45,42,54,55,82,87,76,79,68,61,69,60,62,63,66,67,56,57,46,52,34,78,40,72,81,84,85,28,31,88,83,75,70,20,22,73,64,58,49,11,18,51, 4, 7, 1,43, 0,47,37, 5,39,29,10,35,16,13,17,25, 23,19,21,27,32, 8,12,42,33, 3, 2,54,45, 9, 6,14,15,26,60,55,66,61,72,67,24,36,30,78,81,41,38,88,84,85,83,48,44,53,50,65,73,59,75,74,71,70,64,80,77,87,86,79,51,82,58,49,47,39,69,76,43,37,35,25,63,68,29,17,16,10,57,62,13,52,56,40, 1,46, 5, 4,34, 0,11,31, 7,22,28,20,18, 28,20,22,31,34,11,18,46,40, 7, 4,56,52, 1, 0, 5,10,16,62,57,68,63,76,69,13,25,17,79,82,35,29,86,87,80,77,39,37,47,43,51,71,49,74,64,58,65,59,73,70,83,75,88,50,85,53,48,44,38,81,84,41,36,30,24,72,78,26,15,14, 6,66,67, 9,60,61,54, 3,55, 2,12,45, 8,21,42,19,32,33,27,23, 27,21,23,32,33,12,19,45,42, 8, 3,55,54, 6, 2, 9,14,24,61,60,67,66,78,72,15,30,26,81,84,38,36,85,88,83,75,44,41,50,48,59,70,53,73,71,65,64,58,77,74,86,80,82,49,87,51,47,43,37,76,79,39,35,29,17,68,69,25,16,13, 5,62,63,10,56,57,46, 0,52, 1, 7,40, 4,18,34,11,28,31,22,20, 26,36,30,24,15,41,38, 9,14,44,48, 2, 6,53,50,59,65,74, 8, 3,19,12,23,21,71,80,77,27,32,87,86,42,33,45,54,79,82,69,76,63,60,68,55,57,62,61,66,52,56,40,46,31,72,34,67,78,81,88,22,28,84,85,83,73,18,20,75,70,64,51, 7,11,58, 0, 4, 5,47, 1,49,39,10,43,35,13,37,17,16,25,29, 25,35,29,17,16,39,37,10,13,43,47, 1, 5,51,49,58,64,73, 4, 0,11, 7,20,18,70,83,75,22,28,88,85,34,31,40,46,81,84,72,78,66,56,67,52,60,61,57,62,54,55,42,45,32,68,33,63,69,76,82,23,27,79,87,86,77,19,21,80,74,71,59, 8,12,65, 2, 3, 9,50, 6,53,44,14,48,38,15,41,26,24,30,36, 31,22,28,34,40,18,20,52,46,11, 7,57,56, 0, 4, 1, 5,13,63,62,69,68,79,76,10,17,16,82,87,29,25,80,86,77,74,37,35,43,39,49,65,47,71,58,51,59,53,70,64,75,73,85,48,83,50,44,41,36,84,88,38,30,26,15,78,81,24,14, 9, 2,67,72, 6,61,66,55, 8,60, 3,19,54,12,23,45,21,33,42,32,27, 32,23,27,33,42,19,21,54,45,12, 8,60,55, 2, 3, 6, 9,15,66,61,72,67,81,78,14,26,24,84,88,36,30,83,85,75,73,41,38,48,44,53,64,50,70,65,59,58,51,74,71,80,77,87,47,86,49,43,39,35,79,82,37,29,25,16,69,76,17,13,10, 1,63,68, 5,57,62,52, 4,56, 0,11,46, 7,20,40,18,31,34,28,22, 29,37,35,25,17,43,39,13,16,47,49, 5,10,58,51,64,70,75, 0, 1, 7, 4,18,11,73,85,83,20,22,84,88,31,28,34,40,78,81,67,72,61,52,66,46,55,60,56,57,45,54,33,42,27,63,32,62,68,69,79,21,23,76,82,87,80,12,19,86,77,74,65, 3, 8,71, 6, 2,14,53, 9,59,48,15,50,41,24,44,30,26,36,38, 30,38,36,26,24,44,41,14,15,48,50, 6, 9,59,53,65,71,77, 3, 2,12, 8,21,19,74,86,80,23,27,82,87,33,32,42,45,76,79,68,69,62,55,63,54,56,57,60,61,46,52,34,40,28,67,31,66,72,78,84,20,22,81,88,85,75,11,18,83,73,70,58, 4, 7,64, 1, 0,10,49, 5,51,43,13,47,37,16,39,25,17,29,35, 36,41,38,30,26,48,44,15,24,50,53, 9,14,65,59,71,74,80, 2, 6, 8, 3,19,12,77,87,86,21,23,79,82,32,27,33,42,69,76,63,68,57,54,62,45,52,56,55,60,40,46,31,34,22,66,28,61,67,72,81,18,20,78,84,88,83, 7,11,85,75,73,64, 0, 4,70, 5, 1,13,51,10,58,47,16,49,39,17,43,29,25,35,37, 35,39,37,29,25,47,43,16,17,49,51,10,13,64,58,70,73,83, 1, 5, 4, 0,11, 7,75,88,85,18,20,81,84,28,22,31,34,72,78,66,67,60,46,61,40,54,55,52,56,42,45,32,33,23,62,27,57,63,68,76,19,21,69,79,82,86, 8,12,87,80,77,71, 2, 3,74, 9, 6,15,59,14,65,50,24,53,44,26,48,36,30,38,41, 34,28,31,40,46,20,22,56,52,18,11,62,57, 4, 7, 0, 1,10,68,63,76,69,82,79, 5,16,13,87,86,25,17,77,80,74,71,35,29,39,37,47,59,43,65,51,49,53,50,64,58,73,70,83,44,75,48,41,38,30,88,85,36,26,24,14,81,84,15, 9, 6, 3,72,78, 2,66,67,60,12,61, 8,21,55,19,27,54,23,42,45,33,32, 33,27,32,42,45,21,23,55,54,19,12,61,60, 3, 8, 2, 6,14,67,66,78,72,84,81, 9,24,15,88,85,30,26,75,83,73,70,38,36,44,41,50,58,48,64,59,53,51,49,71,65,77,74,86,43,80,47,39,37,29,82,87,35,25,17,13,76,79,16,10, 5, 0,68,69, 1,62,63,56, 7,57, 4,18,52,11,22,46,20,34,40,31,28, 40,31,34,46,52,22,28,57,56,20,18,63,62, 7,11, 4, 0, 5,69,68,79,76,87,82, 1,13,10,86,80,17,16,74,77,71,65,29,25,37,35,43,53,39,59,49,47,50,48,58,51,70,64,75,41,73,44,38,36,26,85,83,30,24,15, 9,84,88,14, 6, 2, 8,78,81, 3,67,72,61,19,66,12,23,60,21,32,55,27,45,54,42,33, 42,32,33,45,54,23,27,60,55,21,19,66,61, 8,12, 3, 2, 9,72,67,81,78,88,84, 6,15,14,85,83,26,24,73,75,70,64,36,30,41,38,48,51,44,58,53,50,49,47,65,59,74,71,80,39,77,43,37,35,25,87,86,29,17,16,10,79,82,13, 5, 1, 4,69,76, 0,63,68,57,11,62, 7,20,56,18,28,52,22,40,46,34,31, 46,34,40,52,56,28,31,62,57,22,20,68,63,11,18, 7, 4, 1,76,69,82,79,86,87, 0,10, 5,80,77,16,13,71,74,65,59,25,17,35,29,39,50,37,53,47,43,48,44,51,49,64,58,73,38,70,41,36,30,24,83,75,26,15,14, 6,88,85, 9, 2, 3,12,81,84, 8,72,78,66,21,67,19,27,61,23,33,60,32,54,55,45,42, 37,43,39,35,29,49,47,17,25,51,58,13,16,70,64,73,75,85, 5,10, 0, 1, 7, 4,83,84,88,11,18,78,81,22,20,28,31,67,72,61,66,55,40,60,34,45,54,46,52,33,42,27,32,21,57,23,56,62,63,69,12,19,68,76,79,87, 3, 8,82,86,80,74, 6, 2,77,14, 9,24,65,15,71,53,26,59,48,30,50,38,36,41,44, 45,33,42,54,55,27,32,61,60,23,21,67,66,12,19, 8, 3, 6,78,72,84,81,85,88, 2,14, 9,83,75,24,15,70,73,64,58,30,26,38,36,44,49,41,51,50,48,47,43,59,53,71,65,77,37,74,39,35,29,17,86,80,25,16,13, 5,82,87,10, 1, 0, 7,76,79, 4,68,69,62,18,63,11,22,57,20,31,56,28,46,52,40,34, 38,44,41,36,30,50,48,24,26,53,59,14,15,71,65,74,77,86, 6, 9, 3, 2,12, 8,80,82,87,19,21,76,79,27,23,32,33,68,69,62,63,56,45,57,42,46,52,54,55,34,40,28,31,20,61,22,60,66,67,78,11,18,72,81,84,85, 4, 7,88,83,75,70, 1, 0,73,10, 5,16,58,13,64,49,17,51,43,25,47,35,29,37,39, 52,40,46,56,57,31,34,63,62,28,22,69,68,18,20,11, 7, 0,79,76,87,82,80,86, 4, 5, 1,77,74,13,10,65,71,59,53,17,16,29,25,37,48,35,50,43,39,44,41,49,47,58,51,70,36,64,38,30,26,15,75,73,24,14, 9, 2,85,83, 6, 3, 8,19,84,88,12,78,81,67,23,72,21,32,66,27,42,61,33,55,60,54,45, 54,42,45,55,60,32,33,66,61,27,23,72,67,19,21,12, 8, 2,81,78,88,84,83,85, 3, 9, 6,75,73,15,14,64,70,58,51,26,24,36,30,41,47,38,49,48,44,43,39,53,50,65,59,74,35,71,37,29,25,16,80,77,17,13,10, 1,87,86, 5, 0, 4,11,79,82, 7,69,76,63,20,68,18,28,62,22,34,57,31,52,56,46,40, 41,48,44,38,36,53,50,26,30,59,65,15,24,74,71,77,80,87, 9,14, 2, 6, 8, 3,86,79,82,12,19,69,76,23,21,27,32,63,68,57,62,52,42,56,33,40,46,45,54,31,34,22,28,18,60,20,55,61,66,72, 7,11,67,78,81,88, 0, 4,84,85,83,73, 5, 1,75,13,10,17,64,16,70,51,25,58,47,29,49,37,35,39,43, 39,47,43,37,35,51,49,25,29,58,64,16,17,73,70,75,83,88,10,13, 1, 5, 4, 0,85,81,84, 7,11,72,78,20,18,22,28,66,67,60,61,54,34,55,31,42,45,40,46,32,33,23,27,19,56,21,52,57,62,68, 8,12,63,69,76,82, 2, 3,79,87,86,77, 9, 6,80,15,14,26,71,24,74,59,30,65,50,36,53,41,38,44,48, 56,46,52,57,62,34,40,68,63,31,28,76,69,20,22,18,11, 4,82,79,86,87,77,80, 7, 1, 0,74,71,10, 5,59,65,53,50,16,13,25,17,35,44,29,48,39,37,41,38,47,43,51,49,64,30,58,36,26,24,14,73,70,15, 9, 6, 3,83,75, 2, 8,12,21,88,85,19,81,84,72,27,78,23,33,67,32,45,66,42,60,61,55,54, 55,45,54,60,61,33,42,67,66,32,27,78,72,21,23,19,12, 3,84,81,85,88,75,83, 8, 6, 2,73,70,14, 9,58,64,51,49,24,15,30,26,38,43,36,47,44,41,39,37,50,48,59,53,71,29,65,35,25,17,13,77,74,16,10, 5, 0,86,80, 1, 4, 7,18,82,87,11,76,79,68,22,69,20,31,63,28,40,62,34,56,57,52,46, 57,52,56,62,63,40,46,69,68,34,31,79,76,22,28,20,18, 7,87,82,80,86,74,77,11, 0, 4,71,65, 5, 1,53,59,50,48,13,10,17,16,29,41,25,44,37,35,38,36,43,39,49,47,58,26,51,30,24,15, 9,70,64,14, 6, 2, 8,75,73, 3,12,19,23,85,83,21,84,88,78,32,81,27,42,72,33,54,67,45,61,66,60,55, 60,54,55,61,66,42,45,72,67,33,32,81,78,23,27,21,19, 8,88,84,83,85,73,75,12, 2, 3,70,64, 9, 6,51,58,49,47,15,14,26,24,36,39,30,43,41,38,37,35,48,44,53,50,65,25,59,29,17,16,10,74,71,13, 5, 1, 4,80,77, 0, 7,11,20,87,86,18,79,82,69,28,76,22,34,68,31,46,63,40,57,62,56,52, 62,56,57,63,68,46,52,76,69,40,34,82,79,28,31,22,20,11,86,87,77,80,71,74,18, 4, 7,65,59, 1, 0,50,53,48,44,10, 5,16,13,25,38,17,41,35,29,36,30,39,37,47,43,51,24,49,26,15,14, 6,64,58, 9, 2, 3,12,73,70, 8,19,21,27,83,75,23,88,85,81,33,84,32,45,78,42,55,72,54,66,67,61,60, 43,49,47,39,37,58,51,29,35,64,70,17,25,75,73,83,85,84,13,16, 5,10, 0, 1,88,78,81, 4, 7,67,72,18,11,20,22,61,66,55,60,45,31,54,28,33,42,34,40,27,32,21,23,12,52,19,46,56,57,63, 3, 8,62,68,69,79, 6, 2,76,82,87,80,14, 9,86,24,15,30,74,26,77,65,36,71,53,38,59,44,41,48,50, 61,55,60,66,67,45,54,78,72,42,33,84,81,27,32,23,21,12,85,88,75,83,70,73,19, 3, 8,64,58, 6, 2,49,51,47,43,14, 9,24,15,30,37,26,39,38,36,35,29,44,41,50,48,59,17,53,25,16,13, 5,71,65,10, 1, 0, 7,77,74, 4,11,18,22,86,80,20,82,87,76,31,79,28,40,69,34,52,68,46,62,63,57,56, 44,50,48,41,38,59,53,30,36,65,71,24,26,77,74,80,86,82,14,15, 6, 9, 3, 2,87,76,79, 8,12,68,69,21,19,23,27,62,63,56,57,46,33,52,32,34,40,42,45,28,31,20,22,11,55,18,54,60,61,67, 4, 7,66,72,78,84, 1, 0,81,88,85,75,10, 5,83,16,13,25,70,17,73,58,29,64,49,35,51,39,37,43,47, 48,53,50,44,41,65,59,36,38,71,74,26,30,80,77,86,87,79,15,24, 9,14, 2, 6,82,69,76, 3, 8,63,68,19,12,21,23,57,62,52,56,40,32,46,27,31,34,33,42,22,28,18,20, 7,54,11,45,55,60,66, 0, 4,61,67,72,81, 5, 1,78,84,88,83,13,10,85,17,16,29,73,25,75,64,35,70,51,37,58,43,39,47,49, 47,51,49,43,39,64,58,35,37,70,73,25,29,83,75,85,88,81,16,17,10,13, 1, 5,84,72,78, 0, 4,66,67,11, 7,18,20,60,61,54,55,42,28,45,22,32,33,31,34,23,27,19,21, 8,46,12,40,52,56,62, 2, 3,57,63,68,76, 9, 6,69,79,82,86,15,14,87,26,24,36,77,30,80,71,38,74,59,41,65,48,44,50,53, 49,58,51,47,43,70,64,37,39,73,75,29,35,85,83,88,84,78,17,25,13,16, 5,10,81,67,72, 1, 0,61,66, 7, 4,11,18,55,60,45,54,33,22,42,20,27,32,28,31,21,23,12,19, 3,40, 8,34,46,52,57, 6, 2,56,62,63,69,14, 9,68,76,79,87,24,15,82,30,26,38,80,36,86,74,41,77,65,44,71,50,48,53,59, 63,57,62,68,69,52,56,79,76,46,40,87,82,31,34,28,22,18,80,86,74,77,65,71,20, 7,11,59,53, 0, 4,48,50,44,41, 5, 1,13,10,17,36,16,38,29,25,30,26,37,35,43,39,49,15,47,24,14, 9, 2,58,51, 6, 3, 8,19,70,64,12,21,23,32,75,73,27,85,83,84,42,88,33,54,81,45,60,78,55,67,72,66,61, 66,60,61,67,72,54,55,81,78,45,42,88,84,32,33,27,23,19,83,85,73,75,64,70,21, 8,12,58,51, 2, 3,47,49,43,39, 9, 6,15,14,26,35,24,37,36,30,29,25,41,38,48,44,53,16,50,17,13,10, 1,65,59, 5, 0, 4,11,74,71, 7,18,20,28,80,77,22,87,86,79,34,82,31,46,76,40,56,69,52,63,68,62,57, 50,59,53,48,44,71,65,38,41,74,77,30,36,86,80,87,82,76,24,26,14,15, 6, 9,79,68,69, 2, 3,62,63,12, 8,19,21,56,57,46,52,34,27,40,23,28,31,32,33,20,22,11,18, 4,45, 7,42,54,55,61, 1, 0,60,66,67,78,10, 5,72,81,84,85,16,13,88,25,17,35,75,29,83,70,37,73,58,39,64,47,43,49,51, 53,65,59,50,48,74,71,41,44,77,80,36,38,87,86,82,79,69,26,30,15,24, 9,14,76,63,68, 6, 2,57,62, 8, 3,12,19,52,56,40,46,31,23,34,21,22,28,27,32,18,20, 7,11, 0,42, 4,33,45,54,60, 5, 1,55,61,66,72,13,10,67,78,81,88,17,16,84,29,25,37,83,35,85,73,39,75,64,43,70,49,47,51,58, 51,64,58,49,47,73,70,39,43,75,83,35,37,88,85,84,81,72,25,29,16,17,10,13,78,66,67, 5, 1,60,61, 4, 0, 7,11,54,55,42,45,32,20,33,18,23,27,22,28,19,21, 8,12, 2,34, 3,31,40,46,56, 9, 6,52,57,62,68,15,14,63,69,76,82,26,24,79,36,30,41,86,38,87,77,44,80,71,48,74,53,50,59,65, 58,70,64,51,49,75,73,43,47,83,85,37,39,84,88,81,78,67,29,35,17,25,13,16,72,61,66,10, 5,55,60, 0, 1, 4, 7,45,54,33,42,27,18,32,11,21,23,20,22,12,19, 3, 8, 6,31, 2,28,34,40,52,14, 9,46,56,57,63,24,15,62,68,69,79,30,26,76,38,36,44,87,41,82,80,48,86,74,50,77,59,53,65,71, 68,62,63,69,76,56,57,82,79,52,46,86,87,34,40,31,28,20,77,80,71,74,59,65,22,11,18,53,50, 4, 7,44,48,41,38, 1, 0,10, 5,16,30,13,36,25,17,26,24,35,29,39,37,47,14,43,15, 9, 6, 3,51,49, 2, 8,12,21,64,58,19,23,27,33,73,70,32,83,75,88,45,85,42,55,84,54,61,81,60,72,78,67,66, 67,61,66,72,78,55,60,84,81,54,45,85,88,33,42,32,27,21,75,83,70,73,58,64,23,12,19,51,49, 3, 8,43,47,39,37, 6, 2,14, 9,24,29,15,35,30,26,25,17,38,36,44,41,50,13,48,16,10, 5, 0,59,53, 1, 4, 7,18,71,65,11,20,22,31,77,74,28,86,80,82,40,87,34,52,79,46,57,76,56,68,69,63,62, 59,71,65,53,50,77,74,44,48,80,86,38,41,82,87,79,76,68,30,36,24,26,14,15,69,62,63, 9, 6,56,57, 3, 2, 8,12,46,52,34,40,28,21,31,19,20,22,23,27,11,18, 4, 7, 1,33, 0,32,42,45,55,10, 5,54,60,61,67,16,13,66,72,78,84,25,17,81,35,29,39,85,37,88,75,43,83,70,47,73,51,49,58,64, 65,74,71,59,53,80,77,48,50,86,87,41,44,79,82,76,69,63,36,38,26,30,15,24,68,57,62,14, 9,52,56, 2, 6, 3, 8,40,46,31,34,22,19,28,12,18,20,21,23, 7,11, 0, 4, 5,32, 1,27,33,42,54,13,10,45,55,60,66,17,16,61,67,72,81,29,25,78,37,35,43,88,39,84,83,47,85,73,49,75,58,51,64,70, 64,73,70,58,51,83,75,47,49,85,88,39,43,81,84,78,72,66,35,37,25,29,16,17,67,60,61,13,10,54,55, 1, 5, 0, 4,42,45,32,33,23,11,27, 7,19,21,18,20, 8,12, 2, 3, 9,28, 6,22,31,34,46,15,14,40,52,56,62,26,24,57,63,68,76,36,30,69,41,38,48,82,44,79,86,50,87,77,53,80,65,59,71,74, 70,75,73,64,58,85,83,49,51,88,84,43,47,78,81,72,67,61,37,39,29,35,17,25,66,55,60,16,13,45,54, 5,10, 1, 0,33,42,27,32,21, 7,23, 4,12,19,11,18, 3, 8, 6, 2,14,22, 9,20,28,31,40,24,15,34,46,52,57,30,26,56,62,63,69,38,36,68,44,41,50,79,48,76,87,53,82,80,59,86,71,65,74,77, 69,63,68,76,79,57,62,87,82,56,52,80,86,40,46,34,31,22,74,77,65,71,53,59,28,18,20,50,48, 7,11,41,44,38,36, 0, 4, 5, 1,13,26,10,30,17,16,24,15,29,25,37,35,43, 9,39,14, 6, 2, 8,49,47, 3,12,19,23,58,51,21,27,32,42,70,64,33,75,73,85,54,83,45,60,88,55,66,84,61,78,81,72,67, 72,66,67,78,81,60,61,88,84,55,54,83,85,42,45,33,32,23,73,75,64,70,51,58,27,19,21,49,47, 8,12,39,43,37,35, 2, 3, 9, 6,15,25,14,29,26,24,17,16,36,30,41,38,48,10,44,13, 5, 1, 4,53,50, 0, 7,11,20,65,59,18,22,28,34,74,71,31,80,77,87,46,86,40,56,82,52,62,79,57,69,76,68,63, 71,77,74,65,59,86,80,50,53,87,82,44,48,76,79,69,68,62,38,41,30,36,24,26,63,56,57,15,14,46,52, 6, 9, 2, 3,34,40,28,31,20,12,22, 8,11,18,19,21, 4, 7, 1, 0,10,27, 5,23,32,33,45,16,13,42,54,55,61,25,17,60,66,67,78,35,29,72,39,37,47,84,43,81,85,49,88,75,51,83,64,58,70,73, 76,68,69,79,82,62,63,86,87,57,56,77,80,46,52,40,34,28,71,74,59,65,50,53,31,20,22,48,44,11,18,38,41,36,30, 4, 7, 1, 0,10,24, 5,26,16,13,15,14,25,17,35,29,39, 6,37, 9, 2, 3,12,47,43, 8,19,21,27,51,49,23,32,33,45,64,58,42,73,70,83,55,75,54,61,85,60,67,88,66,81,84,78,72, 78,67,72,81,84,61,66,85,88,60,55,75,83,45,54,42,33,27,70,73,58,64,49,51,32,21,23,47,43,12,19,37,39,35,29, 3, 8, 6, 2,14,17, 9,25,24,15,16,13,30,26,38,36,44, 5,41,10, 1, 0, 7,50,48, 4,11,18,22,59,53,20,28,31,40,71,65,34,77,74,86,52,80,46,57,87,56,63,82,62,76,79,69,68, 79,69,76,82,87,63,68,80,86,62,57,74,77,52,56,46,40,31,65,71,53,59,48,50,34,22,28,44,41,18,20,36,38,30,26, 7,11, 0, 4, 5,15, 1,24,13,10,14, 9,17,16,29,25,37, 2,35, 6, 3, 8,19,43,39,12,21,23,32,49,47,27,33,42,54,58,51,45,70,64,75,60,73,55,66,83,61,72,85,67,84,88,81,78, 73,83,75,70,64,88,85,51,58,84,81,47,49,72,78,67,66,60,39,43,35,37,25,29,61,54,55,17,16,42,45,10,13, 5, 1,32,33,23,27,19, 4,21, 0, 8,12, 7,11, 2, 3, 9, 6,15,20,14,18,22,28,34,26,24,31,40,46,56,36,30,52,57,62,68,41,38,63,48,44,53,76,50,69,82,59,79,86,65,87,74,71,77,80, 81,72,78,84,88,66,67,83,85,61,60,73,75,54,55,45,42,32,64,70,51,58,47,49,33,23,27,43,39,19,21,35,37,29,25, 8,12, 2, 3, 9,16, 6,17,15,14,13,10,26,24,36,30,41, 1,38, 5, 0, 4,11,48,44, 7,18,20,28,53,50,22,31,34,46,65,59,40,74,71,80,56,77,52,62,86,57,68,87,63,79,82,76,69, 74,80,77,71,65,87,86,53,59,82,79,48,50,69,76,68,63,57,41,44,36,38,26,30,62,52,56,24,15,40,46, 9,14, 6, 2,31,34,22,28,18, 8,20, 3, 7,11,12,19, 0, 4, 5, 1,13,23,10,21,27,32,42,17,16,33,45,54,60,29,25,55,61,66,72,37,35,67,43,39,49,81,47,78,88,51,84,83,58,85,70,64,73,75, 75,85,83,73,70,84,88,58,64,81,78,49,51,67,72,66,61,55,43,47,37,39,29,35,60,45,54,25,17,33,42,13,16,10, 5,27,32,21,23,12, 0,19, 1, 3, 8, 4, 7, 6, 2,14, 9,24,18,15,11,20,22,31,30,26,28,34,40,52,38,36,46,56,57,63,44,41,62,50,48,59,69,53,68,79,65,76,87,71,82,77,74,80,86, 84,78,81,88,85,67,72,75,83,66,61,70,73,55,60,54,45,33,58,64,49,51,43,47,42,27,32,39,37,21,23,29,35,25,17,12,19, 3, 8, 6,13, 2,16,14, 9,10, 5,24,15,30,26,38, 0,36, 1, 4, 7,18,44,41,11,20,22,31,50,48,28,34,40,52,59,53,46,71,65,77,57,74,56,63,80,62,69,86,68,82,87,79,76, 77,86,80,74,71,82,87,59,65,79,76,50,53,68,69,63,62,56,44,48,38,41,30,36,57,46,52,26,24,34,40,14,15, 9, 6,28,31,20,22,11, 3,18, 2, 4, 7, 8,12, 1, 0,10, 5,16,21,13,19,23,27,33,25,17,32,42,45,55,35,29,54,60,61,67,39,37,66,47,43,51,78,49,72,84,58,81,85,64,88,73,70,75,83, 83,88,85,75,73,81,84,64,70,78,72,51,58,66,67,61,60,54,47,49,39,43,35,37,55,42,45,29,25,32,33,16,17,13,10,23,27,19,21, 8, 1,12, 5, 2, 3, 0, 4, 9, 6,15,14,26,11,24, 7,18,20,28,36,30,22,31,34,46,41,38,40,52,56,62,48,44,57,53,50,65,68,59,63,76,71,69,82,74,79,80,77,86,87, 82,76,79,87,86,68,69,77,80,63,62,71,74,56,57,52,46,34,59,65,50,53,44,48,40,28,31,41,38,20,22,30,36,26,24,11,18, 4, 7, 1,14, 0,15,10, 5, 9, 6,16,13,25,17,35, 3,29, 2, 8,12,21,39,37,19,23,27,33,47,43,32,42,45,55,51,49,54,64,58,73,61,70,60,67,75,66,78,83,72,88,85,84,81, 80,87,86,77,74,79,82,65,71,76,69,53,59,63,68,62,57,52,48,50,41,44,36,38,56,40,46,30,26,31,34,15,24,14, 9,22,28,18,20, 7, 2,11, 6, 0, 4, 3, 8, 5, 1,13,10,17,19,16,12,21,23,32,29,25,27,33,42,54,37,35,45,55,60,66,43,39,61,49,47,58,72,51,67,81,64,78,88,70,84,75,73,83,85, 87,79,82,86,80,69,76,74,77,68,63,65,71,57,62,56,52,40,53,59,48,50,41,44,46,31,34,38,36,22,28,26,30,24,15,18,20, 7,11, 0, 9, 4,14, 5, 1, 6, 2,13,10,17,16,29, 8,25, 3,12,19,23,37,35,21,27,32,42,43,39,33,45,54,60,49,47,55,58,51,70,66,64,61,72,73,67,81,75,78,85,83,88,84, 88,81,84,85,83,72,78,73,75,67,66,64,70,60,61,55,54,42,51,58,47,49,39,43,45,32,33,37,35,23,27,25,29,17,16,19,21, 8,12, 2,10, 3,13, 9, 6, 5, 1,15,14,26,24,36, 4,30, 0, 7,11,20,41,38,18,22,28,34,48,44,31,40,46,56,53,50,52,65,59,74,62,71,57,68,77,63,76,80,69,87,86,82,79, 85,84,88,83,75,78,81,70,73,72,67,58,64,61,66,60,55,45,49,51,43,47,37,39,54,33,42,35,29,27,32,17,25,16,13,21,23,12,19, 3, 5, 8,10, 6, 2, 1, 0,14, 9,24,15,30, 7,26, 4,11,18,22,38,36,20,28,31,40,44,41,34,46,52,57,50,48,56,59,53,71,63,65,62,69,74,68,79,77,76,86,80,87,82, 86,82,87,80,77,76,79,71,74,69,68,59,65,62,63,57,56,46,50,53,44,48,38,41,52,34,40,36,30,28,31,24,26,15,14,20,22,11,18, 4, 6, 7, 9, 1, 0, 2, 3,10, 5,16,13,25,12,17, 8,19,21,27,35,29,23,32,33,45,39,37,42,54,55,61,47,43,60,51,49,64,67,58,66,78,70,72,84,73,81,83,75,85,88 ]) ]). ============================== end of model ========================== ============================== STATISTICS ============================ For domain size 89. Current CPU time: 0.00 seconds (total CPU time: 2629.41 seconds). Ground clauses: seen=712990, kept=712812. Selections=207, assignments=7477, propagations=254071, current_models=1. Rewrite_terms=24934403, rewrite_bools=3768052, indexes=2661648. Rules_from_neg_clauses=2164, cross_offs=3644049. ============================== end of statistics ===================== User_CPU=2629.41, System_CPU=0.25, Wall_clock=2635. Exiting with 1 model. Process 2336 exit (max_models) Sun Mar 17 17:05:55 2013 The process finished Sun Mar 17 17:05:55 2013