16 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_16-bij.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 3706 | | Number of clauses: 29171 | | Parse time: 0.01 s | | Eliminated clauses: 0.28 Mb | | Simplification time: 0.30 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 100 | 637 17308 108788 | 100 5 4.2 18.2 | 16.055 % | | 250 | 607 17308 108788 | 247 5 3.6 16.1 | 16.865 % | | 475 | 584 17308 108788 | 461 5 3.6 19.9 | 17.485 % | | 812 | 530 17308 108788 | 787 5 4.2 38.3 | 18.942 % | | 1318 | 512 17308 108788 | 1288 6 5.2 64.9 | 19.428 % | | 2077 | 496 17308 108788 | 2041 7 5.9 81.1 | 19.860 % | | 3216 | 482 17308 108788 | 3178 8 6.3 90.9 | 20.237 % | | 4924 | 477 12569 78026 | 4396 8 7.1 97.3 | 20.372 % | | 5001 | 477 12569 78026 | 4473 8 7.1 97.5 | 20.372 % | < ReduceDB 1 ( 91 restarts, 55 cnfs/res, 50.1% reduced, 27b 124g 318g3) > | 5001 | 477 12569 78026 | 2243 7 6.1 97.5 | 20.372 % | | 7486 | 465 12569 78026 | 4723 8 6.6 97.3 | 20.696 % | | 11120 | 459 12183 75564 | 8312 8 7.0 97.0 | 20.858 % | ==================================================================================== restarts : 175 (350.75 /sec) (63.54 confs/res) conflicts : 11120 (22288 /sec) decisions : 62277 (0.00 % random) (124823 /sec) propagations : 209481 (419866 /sec) conflict literals : 93154 (2.86 % deleted) average of lbd : 7.05 Memory used : 11.00 MB CPU time : 0.498924 s SATISFIABLE 17 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_17-bij.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 3706 | | Number of clauses: 29166 | | Parse time: 0.02 s | | Eliminated clauses: 0.31 Mb | | Simplification time: 0.33 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 100 | 604 16572 102564 | 100 5 4.0 17.3 | 15.920 % | | 250 | 574 16572 102564 | 242 5 4.2 18.4 | 16.730 % | | 475 | 555 16572 102564 | 461 5 3.6 16.7 | 17.242 % | | 812 | 320 16572 102564 | 788 6 4.7 46.8 | 23.583 % | | 1318 | 320 16572 102564 | 1294 7 5.9 69.9 | 23.583 % | | 2077 | 320 16572 102564 | 2053 7 6.5 82.6 | 23.583 % | | 3216 | 320 16572 102564 | 3192 7 6.6 90.7 | 23.583 % | | 4924 | 320 16572 102564 | 4900 8 6.8 97.0 | 23.583 % | | 5001 | 320 16572 102564 | 4977 8 6.8 97.2 | 23.583 % | < ReduceDB 1 ( 90 restarts, 56 cnfs/res, 50.0% reduced, 68b 256g 476g3) > | 5001 | 320 16572 102564 | 2489 7 5.5 97.2 | 23.583 % | | 7486 | 319 10997 66932 | 4651 8 6.6 100.0 | 23.610 % | | 11330 | 319 10885 66260 | 8457 8 7.3 101.0 | 23.610 % | | 15001 | 319 10885 66260 | 12128 9 7.6 99.8 | 23.610 % | < ReduceDB 2 ( 235 restarts, 64 cnfs/res, 50.0% reduced, 30b 386g 1123g3) > | 15001 | 319 10885 66260 | 6064 8 6.4 99.8 | 23.610 % | | 17096 | 319 10885 66260 | 8159 8 7.0 99.6 | 23.610 % | | 25745 | 318 10773 65588 | 16759 10 8.3 98.0 | 23.637 % | | 30001 | 318 10773 65588 | 21015 11 8.8 97.4 | 23.637 % | < ReduceDB 3 ( 465 restarts, 65 cnfs/res, 50.1% reduced, 55b 875g 2130g3) > | 30001 | 318 10773 65588 | 10519 9 7.1 97.4 | 23.637 % | | 38719 | 317 10661 64916 | 19193 12 8.9 96.3 | 23.664 % | | 50001 | 317 10661 64916 | 30475 14 10.4 94.3 | 23.664 % | < ReduceDB 4 ( 783 restarts, 64 cnfs/res, 50.0% reduced, 75b 1446g 3335g3) > | 50001 | 317 10661 64916 | 15243 11 7.9 94.3 | 23.664 % | | 58180 | 317 10661 64916 | 23422 14 9.9 93.6 | 23.664 % | | 75001 | 317 10661 64916 | 40243 18 12.4 92.2 | 23.664 % | < ReduceDB 5 (1216 restarts, 62 cnfs/res, 50.0% reduced, 81b 2147g 4510g3) > | 75001 | 317 10661 64916 | 20130 13 8.6 92.2 | 23.664 % | | 87372 | 317 10661 64916 | 32501 17 11.4 91.4 | 23.664 % | | 105001 | 317 10661 64916 | 50130 21 13.5 90.4 | 23.664 % | < ReduceDB 6 (1734 restarts, 61 cnfs/res, 50.0% reduced, 90b 2885g 5660g3) > | 105001 | 317 10661 64916 | 25072 14 9.0 90.4 | 23.664 % | | 131161 | 317 10661 64916 | 51232 21 13.4 89.2 | 23.664 % | | 140001 | 317 10661 64916 | 60072 22 14.2 88.8 | 23.664 % | < ReduceDB 7 (2300 restarts, 61 cnfs/res, 50.0% reduced, 95b 3681g 6744g3) > | 140001 | 317 10661 64916 | 30044 15 9.2 88.8 | 23.664 % | | 180002 | 317 10661 64916 | 70045 23 14.5 87.3 | 23.664 % | < ReduceDB 8 (2899 restarts, 62 cnfs/res, 49.8% reduced, 103b 4440g 7820g3) > | 180002 | 317 10661 64916 | 34858 15 9.4 87.3 | 23.664 % | | 196845 | 317 10661 64916 | 51701 20 12.4 86.7 | 23.664 % | | 225002 | 317 10661 64916 | 79858 25 15.0 86.1 | 23.664 % | < ReduceDB 9 (3545 restarts, 63 cnfs/res, 46.8% reduced, 108b 5211g 8849g3) > | 225002 | 317 10661 64916 | 37353 15 9.2 86.1 | 23.664 % | | 275001 | 317 10661 64916 | 87352 25 15.0 84.9 | 23.664 % | < ReduceDB 10 (4175 restarts, 66 cnfs/res, 44.6% reduced, 110b 5999g 9968g3) > | 275001 | 317 10661 64916 | 38962 16 8.9 84.9 | 23.664 % | | 295371 | 317 10661 64916 | 59332 21 12.6 84.7 | 23.664 % | | 330001 | 317 10661 64916 | 93962 26 15.5 84.2 | 23.664 % | < ReduceDB 11 (4890 restarts, 67 cnfs/res, 43.4% reduced, 110b 6792g 10841g3) > | 330001 | 317 10661 64916 | 40747 15 8.8 84.2 | 23.664 % | | 390002 | 317 10661 64916 | 100748 27 15.4 83.2 | 23.664 % | < ReduceDB 12 (5537 restarts, 70 cnfs/res, 41.1% reduced, 112b 7606g 11679g3) > | 390002 | 317 10661 64916 | 41408 15 8.5 83.2 | 23.664 % | | 443160 | 317 10661 64916 | 94566 27 14.4 82.5 | 23.664 % | | 455002 | 317 10661 64916 | 106408 27 15.0 82.3 | 23.664 % | < ReduceDB 13 (6069 restarts, 75 cnfs/res, 40.4% reduced, 113b 8316g 12424g3) > | 455002 | 317 10661 64916 | 43003 15 8.2 82.3 | 23.664 % | | 525001 | 317 10661 64916 | 113002 27 15.3 81.7 | 23.664 % | < ReduceDB 14 (6717 restarts, 78 cnfs/res, 39.4% reduced, 115b 9075g 13206g3) > | 525001 | 317 10661 64916 | 44542 15 8.2 81.7 | 23.664 % | | 600002 | 317 10661 64916 | 119543 28 15.2 80.9 | 23.664 % | < ReduceDB 15 (7330 restarts, 82 cnfs/res, 38.2% reduced, 115b 9729g 13910g3) > | 600002 | 317 10661 64916 | 45679 14 8.1 80.9 | 23.664 % | | 664843 | 317 10661 64916 | 110520 26 14.5 80.5 | 23.664 % | | 680001 | 317 10661 64916 | 125678 27 15.1 80.4 | 23.664 % | < ReduceDB 16 (7946 restarts, 86 cnfs/res, 35.6% reduced, 115b 10415g 14713g3) > | 680001 | 317 10661 64916 | 44744 16 7.8 80.4 | 23.664 % | | 765001 | 317 10661 64916 | 129744 28 15.1 79.7 | 23.664 % | < ReduceDB 17 (8523 restarts, 90 cnfs/res, 34.0% reduced, 116b 11051g 15289g3) > | 765001 | 317 10661 64916 | 44069 14 7.4 79.7 | 23.664 % | | 855003 | 317 10661 64916 | 134071 27 14.9 79.2 | 23.664 % | < ReduceDB 18 (9179 restarts, 93 cnfs/res, 34.8% reduced, 117b 11857g 15640g3) > | 855003 | 317 10661 64916 | 46645 14 7.3 79.2 | 23.664 % | | 950001 | 317 10661 64916 | 141643 28 15.2 78.8 | 23.664 % | < ReduceDB 19 (9976 restarts, 95 cnfs/res, 35.4% reduced, 118b 12585g 16360g3) > | 950001 | 317 10661 64916 | 50111 14 7.4 78.8 | 23.664 % | | 997368 | 317 10661 64916 | 97478 24 12.9 78.6 | 23.664 % | | 1050001 | 317 10661 64916 | 150111 28 14.9 78.3 | 23.664 % | < ReduceDB 20 (10712 restarts, 98 cnfs/res, 33.7% reduced, 118b 13313g 17161g3) > | 1050001 | 317 10661 64916 | 50533 14 7.2 78.3 | 23.664 % | | 1155001 | 317 10661 64916 | 155533 28 15.1 78.0 | 23.664 % | < ReduceDB 21 (11524 restarts, 100 cnfs/res, 33.8% reduced, 118b 14064g 17798g3) > | 1155001 | 317 10661 64916 | 52574 14 7.1 78.0 | 23.664 % | | 1265002 | 317 10661 64916 | 162575 28 15.1 77.6 | 23.664 % | < ReduceDB 22 (12294 restarts, 103 cnfs/res, 33.2% reduced, 119b 14693g 18563g3) > | 1265002 | 317 10661 64916 | 54015 14 7.0 77.6 | 23.664 % | | 1380001 | 317 10661 64916 | 169014 28 14.7 77.0 | 23.664 % | < ReduceDB 23 (12976 restarts, 106 cnfs/res, 31.7% reduced, 119b 15333g 19193g3) > | 1380001 | 317 10661 64916 | 53638 14 6.8 77.0 | 23.664 % | | 1496156 | 317 10661 64916 | 169793 27 14.3 76.5 | 23.664 % | | 1500001 | 317 10661 64916 | 173638 28 14.3 76.5 | 23.664 % | < ReduceDB 24 (13684 restarts, 110 cnfs/res, 32.3% reduced, 119b 15976g 19760g3) > | 1500001 | 317 10661 64916 | 56124 13 6.7 76.5 | 23.664 % | | 1625002 | 317 10661 64916 | 181125 28 14.6 76.1 | 23.664 % | < ReduceDB 25 (14436 restarts, 113 cnfs/res, 30.1% reduced, 120b 16770g 20538g3) > | 1625002 | 317 10661 64916 | 54460 15 6.6 76.1 | 23.664 % | | 1755001 | 317 10661 64916 | 184459 28 14.7 75.7 | 23.664 % | < ReduceDB 26 (15328 restarts, 114 cnfs/res, 31.7% reduced, 120b 17433g 20960g3) > | 1755001 | 317 10661 64916 | 58548 13 6.8 75.7 | 23.664 % | | 1890001 | 317 10661 64916 | 193548 28 14.6 75.3 | 23.664 % | < ReduceDB 27 (16105 restarts, 117 cnfs/res, 30.0% reduced, 120b 18169g 21497g3) > | 1890001 | 317 10661 64916 | 58055 13 6.4 75.3 | 23.664 % | | 2030002 | 317 10661 64916 | 198056 27 14.6 75.1 | 23.664 % | < ReduceDB 28 (17225 restarts, 118 cnfs/res, 30.5% reduced, 122b 18830g 22230g3) > | 2030002 | 317 10661 64916 | 60448 13 6.1 75.1 | 23.664 % | | 2175001 | 317 10661 64916 | 205447 28 15.1 75.0 | 23.664 % | < ReduceDB 29 (18582 restarts, 117 cnfs/res, 31.4% reduced, 122b 19591g 22847g3) > | 2175001 | 317 10661 64916 | 64543 13 6.5 75.0 | 23.664 % | | 2244338 | 317 10661 64916 | 133880 24 12.4 74.8 | 23.664 % | | 2325002 | 317 10661 64916 | 214544 28 14.6 74.6 | 23.664 % | < ReduceDB 30 (19397 restarts, 120 cnfs/res, 29.1% reduced, 122b 20235g 23636g3) > | 2325002 | 317 10661 64916 | 62434 12 6.0 74.6 | 23.664 % | | 2480002 | 317 10661 64916 | 217434 28 14.5 74.3 | 23.664 % | < ReduceDB 31 (20412 restarts, 121 cnfs/res, 30.1% reduced, 124b 20964g 24224g3) > | 2480002 | 317 10661 64916 | 65407 12 6.1 74.3 | 23.664 % | | 2640001 | 317 10661 64916 | 225406 28 14.8 74.1 | 23.664 % | < ReduceDB 32 (21646 restarts, 122 cnfs/res, 29.0% reduced, 124b 21724g 25033g3) > | 2640001 | 317 10661 64916 | 65431 12 5.8 74.1 | 23.664 % | | 2805002 | 317 10661 64916 | 230432 28 14.5 73.8 | 23.664 % | < ReduceDB 33 (22728 restarts, 123 cnfs/res, 28.1% reduced, 125b 22424g 25673g3) > | 2805002 | 317 10661 64916 | 64806 13 5.5 73.8 | 23.664 % | | 2975003 | 317 10661 64916 | 234807 29 14.5 73.6 | 23.664 % | < ReduceDB 34 (23677 restarts, 126 cnfs/res, 29.2% reduced, 125b 23107g 26117g3) > | 2975003 | 317 10661 64916 | 68528 12 5.8 73.6 | 23.664 % | | 3150001 | 317 10661 64916 | 243526 28 14.5 73.3 | 23.664 % | < ReduceDB 35 (24887 restarts, 127 cnfs/res, 27.2% reduced, 125b 23751g 26995g3) > | 3150001 | 317 10661 64916 | 66181 13 4.7 73.3 | 23.664 % | | 3330003 | 317 10661 64916 | 246183 29 14.5 73.1 | 23.664 % | < ReduceDB 36 (26130 restarts, 127 cnfs/res, 28.9% reduced, 126b 24618g 27590g3) > | 3330003 | 317 10661 64916 | 71119 12 5.9 73.1 | 23.664 % | | 3366612 | 317 10661 64916 | 107728 19 10.0 73.1 | 23.664 % | | 3515002 | 317 10661 64916 | 256118 28 14.6 72.9 | 23.664 % | < ReduceDB 37 (27262 restarts, 129 cnfs/res, 28.3% reduced, 128b 25321g 28210g3) > | 3515002 | 317 10661 64916 | 72379 12 5.6 72.9 | 23.664 % | | 3705003 | 317 10661 64916 | 262380 28 14.6 72.8 | 23.664 % | < ReduceDB 38 (28591 restarts, 130 cnfs/res, 28.1% reduced, 128b 26046g 28840g3) > | 3705003 | 317 10661 64916 | 73819 12 5.7 72.8 | 23.664 % | | 3900005 | 317 10661 64916 | 268821 28 14.5 72.5 | 23.664 % | < ReduceDB 39 (29637 restarts, 132 cnfs/res, 28.6% reduced, 129b 26810g 29373g3) > | 3900005 | 317 10661 64916 | 76957 12 5.7 72.5 | 23.664 % | | 4100002 | 317 10661 64916 | 276954 28 14.1 72.2 | 23.664 % | < ReduceDB 40 (30641 restarts, 134 cnfs/res, 27.8% reduced, 130b 27514g 30029g3) > | 4100002 | 317 10661 64916 | 76913 12 5.4 72.2 | 23.664 % | | 4305002 | 317 10661 64916 | 281913 28 14.6 72.0 | 23.664 % | < ReduceDB 41 (32176 restarts, 134 cnfs/res, 28.3% reduced, 131b 28187g 30677g3) > | 4305002 | 317 10661 64916 | 79853 12 5.7 72.0 | 23.664 % | | 4515001 | 317 10661 64916 | 289852 28 14.7 71.8 | 23.664 % | < ReduceDB 42 (33483 restarts, 135 cnfs/res, 28.0% reduced, 131b 28992g 31160g3) > | 4515001 | 317 10661 64916 | 81155 12 5.6 71.8 | 23.664 % | | 4730001 | 317 10661 64916 | 296155 28 14.5 71.5 | 23.664 % | < ReduceDB 43 (34510 restarts, 137 cnfs/res, 26.4% reduced, 131b 29703g 31865g3) > | 4730001 | 317 10661 64916 | 78307 11 5.0 71.5 | 23.664 % | | 4950001 | 317 10661 64916 | 298307 27 14.0 71.3 | 23.664 % | < ReduceDB 44 (35883 restarts, 138 cnfs/res, 28.2% reduced, 131b 30474g 32400g3) > | 4950001 | 317 10661 64916 | 84041 12 5.5 71.3 | 23.664 % | | 5050023 | 317 10661 64916 | 184063 23 12.0 71.1 | 23.664 % | | 5175001 | 317 10661 64916 | 309041 27 14.0 70.9 | 23.664 % | < ReduceDB 45 (36815 restarts, 141 cnfs/res, 26.3% reduced, 131b 31217g 32963g3) > | 5175001 | 317 10661 64916 | 81291 12 5.1 70.9 | 23.664 % | | 5405001 | 317 10661 64916 | 311291 28 14.4 70.8 | 23.664 % | < ReduceDB 46 (38463 restarts, 141 cnfs/res, 27.5% reduced, 131b 31998g 33472g3) > | 5405001 | 317 10661 64916 | 85690 11 5.3 70.8 | 23.664 % | | 5529376 | 317 10661 64916 | 210065 24 13.0 70.7 | 23.664 % | ==================================================================================== restarts : 39426 (50.28 /sec) (140.25 confs/res) conflicts : 5529376 (7052 /sec) decisions : 12095232 (0.00 % random) (15425 /sec) propagations : 135976017 (173414 /sec) conflict literals : 186790358 (6.38 % deleted) average of lbd : 12.97 Memory used : 136.00 MB CPU time : 784.111 s INDETERMINATE 18 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_18-bij.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 3706 | | Number of clauses: 29166 | | Parse time: 0.02 s | | Eliminated clauses: 0.25 Mb | | Simplification time: 0.25 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 0 | 662 18121 113558 | 0 nan nan nan | 15.623 % | ==================================================================================== restarts : 1 (3.68 /sec) (0.00 confs/res) conflicts : 0 (0 /sec) decisions : 0 ( nan % random) (0 /sec) propagations : 579 (2129 /sec) conflict literals : 0 ( nan % deleted) average of lbd : nan Memory used : 11.00 MB CPU time : 0.271958 s INDETERMINATE 19 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_19-bij.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 3706 | | Number of clauses: 29178 | | Parse time: 0.02 s | | Eliminated clauses: 0.23 Mb | | Simplification time: 0.18 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 0 | 714 19367 121202 | 0 nan nan nan | 15.111 % | ==================================================================================== restarts : 1 (5.18 /sec) (0.00 confs/res) conflicts : 0 (0 /sec) decisions : 0 ( nan % random) (0 /sec) propagations : 560 (2902 /sec) conflict literals : 0 ( nan % deleted) average of lbd : nan Memory used : 11.00 MB CPU time : 0.19297 s INDETERMINATE 20 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_20-bij.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 3706 | | Number of clauses: 29185 | | Parse time: 0.02 s | | Eliminated clauses: 0.19 Mb | | Simplification time: 0.15 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 0 | 738 20358 128059 | 0 nan nan nan | 14.922 % | ==================================================================================== restarts : 1 (5.92 /sec) (0.00 confs/res) conflicts : 0 (0 /sec) decisions : 0 ( nan % random) (0 /sec) propagations : 553 (3273 /sec) conflict literals : 0 ( nan % deleted) average of lbd : nan Memory used : 11.00 MB CPU time : 0.168974 s INDETERMINATE 21 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_21-bij.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 3706 | | Number of clauses: 29181 | | Parse time: 0.01 s | | Eliminated clauses: 0.24 Mb | | Simplification time: 0.22 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 0 | 695 18013 111623 | 0 nan nan nan | 15.326 % | ==================================================================================== restarts : 1 (4.33 /sec) (0.00 confs/res) conflicts : 0 (0 /sec) decisions : 0 ( nan % random) (0 /sec) propagations : 568 (2459 /sec) conflict literals : 0 ( nan % deleted) average of lbd : nan Memory used : 10.00 MB CPU time : 0.230964 s INDETERMINATE 22 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_22-bij.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 3706 | | Number of clauses: 29173 | | Parse time: 0.01 s | | Simplification time: 0.01 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 0 | 3161 28349 81847 | 0 nan nan nan | 14.706 % | ==================================================================================== restarts : 1 (38.47 /sec) (0.00 confs/res) conflicts : 0 (0 /sec) decisions : 0 ( nan % random) (0 /sec) propagations : 545 (20965 /sec) conflict literals : 0 ( nan % deleted) average of lbd : nan Memory used : 8.00 MB CPU time : 0.025996 s INDETERMINATE 23 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_23-bij.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 3706 | | Number of clauses: 29186 | | Parse time: 0.01 s | | Simplification time: 0.01 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 0 | 3181 28482 82745 | 0 nan nan nan | 14.166 % | ==================================================================================== restarts : 1 (45.46 /sec) (0.00 confs/res) conflicts : 0 (0 /sec) decisions : 0 ( nan % random) (0 /sec) propagations : 525 (23868 /sec) conflict literals : 0 ( nan % deleted) average of lbd : nan Memory used : 8.00 MB CPU time : 0.021996 s INDETERMINATE 24 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_24-bij.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 3706 | | Number of clauses: 29183 | | Parse time: 0.02 s | | Simplification time: 0.01 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 0 | 3181 28479 82739 | 0 nan nan nan | 14.166 % | ==================================================================================== restarts : 1 (35.72 /sec) (0.00 confs/res) conflicts : 0 (0 /sec) decisions : 0 ( nan % random) (0 /sec) propagations : 525 (18753 /sec) conflict literals : 0 ( nan % deleted) average of lbd : nan Memory used : 8.00 MB CPU time : 0.027995 s INDETERMINATE 25 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_25-bij.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 3706 | | Number of clauses: 29183 | | Parse time: 0.02 s | | Simplification time: 0.01 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 0 | 3163 28479 82737 | 0 nan nan nan | 14.652 % | ==================================================================================== restarts : 1 (34.49 /sec) (0.00 confs/res) conflicts : 0 (0 /sec) decisions : 0 ( nan % random) (0 /sec) propagations : 543 (18727 /sec) conflict literals : 0 ( nan % deleted) average of lbd : nan Memory used : 8.00 MB CPU time : 0.028995 s INDETERMINATE 26 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_26-bij.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 3706 | | Number of clauses: 29182 | | Parse time: 0.02 s | | Simplification time: 0.01 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 0 | 3169 28478 82737 | 0 nan nan nan | 14.490 % | ==================================================================================== restarts : 1 (35.72 /sec) (0.00 confs/res) conflicts : 0 (0 /sec) decisions : 0 ( nan % random) (0 /sec) propagations : 537 (19182 /sec) conflict literals : 0 ( nan % deleted) average of lbd : nan Memory used : 8.00 MB CPU time : 0.027995 s INDETERMINATE 27 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_27-bij.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 3706 | | Number of clauses: 29186 | | Parse time: 0.02 s | | Simplification time: 0.01 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 0 | 3163 28482 82751 | 0 nan nan nan | 14.652 % | ==================================================================================== restarts : 1 (38.47 /sec) (0.00 confs/res) conflicts : 0 (0 /sec) decisions : 0 ( nan % random) (0 /sec) propagations : 543 (20888 /sec) conflict literals : 0 ( nan % deleted) average of lbd : nan Memory used : 8.00 MB CPU time : 0.025996 s INDETERMINATE 28 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_28-bij.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 3706 | | Number of clauses: 29196 | | Parse time: 0.02 s | | Simplification time: 0.01 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 0 | 3184 28492 82784 | 0 nan nan nan | 14.085 % | ==================================================================================== restarts : 1 (37.04 /sec) (0.00 confs/res) conflicts : 0 (0 /sec) decisions : 0 ( nan % random) (0 /sec) propagations : 522 (19337 /sec) conflict literals : 0 ( nan % deleted) average of lbd : nan Memory used : 8.00 MB CPU time : 0.026995 s INDETERMINATE 29 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_29-bij.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 3706 | | Number of clauses: 29201 | | Parse time: 0.02 s | | Simplification time: 0.01 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 0 | 3199 28497 82809 | 0 nan nan nan | 13.681 % | ==================================================================================== restarts : 1 (35.72 /sec) (0.00 confs/res) conflicts : 0 (0 /sec) decisions : 0 ( nan % random) (0 /sec) propagations : 507 (18110 /sec) conflict literals : 0 ( nan % deleted) average of lbd : nan Memory used : 8.00 MB CPU time : 0.027995 s INDETERMINATE 30 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_30-bij.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 3706 | | Number of clauses: 29189 | | Parse time: 0.02 s | | Simplification time: 0.01 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 0 | 3144 28485 82750 | 0 nan nan nan | 15.165 % | ==================================================================================== restarts : 1 (34.49 /sec) (0.00 confs/res) conflicts : 0 (0 /sec) decisions : 0 ( nan % random) (0 /sec) propagations : 562 (19383 /sec) conflict literals : 0 ( nan % deleted) average of lbd : nan Memory used : 8.00 MB CPU time : 0.028995 s INDETERMINATE 31 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_31-bij.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 3706 | | Number of clauses: 29199 | | Parse time: 0.02 s | | Simplification time: 0.01 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 0 | 3138 28495 82780 | 0 nan nan nan | 15.326 % | ==================================================================================== restarts : 1 (34.49 /sec) (0.00 confs/res) conflicts : 0 (0 /sec) decisions : 0 ( nan % random) (0 /sec) propagations : 568 (19590 /sec) conflict literals : 0 ( nan % deleted) average of lbd : nan Memory used : 8.00 MB CPU time : 0.028995 s INDETERMINATE 32 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_32-bij.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 3706 | | Number of clauses: 29205 | | Parse time: 0.02 s | | Simplification time: 0.01 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 0 | 3117 28501 82775 | 0 nan nan nan | 15.893 % | ==================================================================================== restarts : 1 (40.01 /sec) (0.00 confs/res) conflicts : 0 (0 /sec) decisions : 0 ( nan % random) (0 /sec) propagations : 589 (23564 /sec) conflict literals : 0 ( nan % deleted) average of lbd : nan Memory used : 8.00 MB CPU time : 0.024996 s INDETERMINATE 33 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_33-bij.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 3706 | | Number of clauses: 29237 | | Parse time: 0.02 s | | Simplification time: 0.01 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 0 | 3194 28533 82856 | 0 nan nan nan | 13.815 % | ==================================================================================== restarts : 1 (37.04 /sec) (0.00 confs/res) conflicts : 0 (0 /sec) decisions : 0 ( nan % random) (0 /sec) propagations : 512 (18966 /sec) conflict literals : 0 ( nan % deleted) average of lbd : nan Memory used : 8.00 MB CPU time : 0.026995 s INDETERMINATE