19 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_19-std.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 6912 | | Number of clauses: 15205 | | Parse time: 0.01 s | | Eliminated clauses: 0.14 Mb | | Simplification time: 0.06 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 100 | 3067 9771 44101 | 100 66 64.0 2803.9 | 8.840 % | | 250 | 3067 9771 44101 | 250 48 44.6 1598.5 | 8.840 % | | 475 | 3067 9771 44101 | 475 39 32.2 975.4 | 8.840 % | | 812 | 3067 9771 44101 | 812 38 28.7 672.5 | 8.840 % | | 1318 | 3067 9771 44101 | 1318 37 27.2 512.2 | 8.840 % | | 1633 | 3067 9771 44101 | 1633 36 26.7 461.1 | 8.840 % | ==================================================================================== restarts : 5 (44.65 /sec) (326.60 confs/res) conflicts : 1633 (14583 /sec) decisions : 12350 (0.00 % random) (110286 /sec) propagations : 145998 (1303763 /sec) conflict literals : 58738 (13.36 % deleted) average of lbd : 26.71 Memory used : 8.00 MB CPU time : 0.111982 s SATISFIABLE 20 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_20-std.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 6912 | | Number of clauses: 15212 | | Parse time: 0.01 s | | Eliminated clauses: 0.14 Mb | | Simplification time: 0.06 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 100 | 3099 9850 44619 | 100 58 55.8 2489.6 | 9.679 % | | 250 | 3099 9850 44619 | 250 38 33.6 1310.9 | 9.679 % | | 475 | 3099 9850 44619 | 475 38 30.6 886.1 | 9.679 % | | 721 | 3099 9850 44619 | 721 35 28.0 670.6 | 9.679 % | ==================================================================================== restarts : 3 (34.89 /sec) (240.33 confs/res) conflicts : 721 (8385 /sec) decisions : 11943 (0.00 % random) (138895 /sec) propagations : 69984 (813900 /sec) conflict literals : 25100 (6.71 % deleted) average of lbd : 28.02 Memory used : 8.00 MB CPU time : 0.085986 s SATISFIABLE 21 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_21-std.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 6912 | | Number of clauses: 15208 | | Parse time: 0.01 s | | Eliminated clauses: 0.14 Mb | | Simplification time: 0.06 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 100 | 3113 9889 44957 | 100 47 44.5 2946.2 | 8.854 % | | 250 | 3113 9889 44957 | 250 38 35.0 1786.3 | 8.854 % | | 475 | 3113 9889 44957 | 475 34 27.6 1125.1 | 8.854 % | | 812 | 3113 9889 44957 | 812 36 27.5 803.3 | 8.854 % | | 1318 | 3113 9889 44957 | 1318 36 26.2 615.3 | 8.854 % | | 1830 | 3113 9889 44957 | 1830 33 24.6 477.3 | 8.854 % | ==================================================================================== restarts : 5 (42.74 /sec) (366.00 confs/res) conflicts : 1830 (15643 /sec) decisions : 19237 (0.00 % random) (164444 /sec) propagations : 184107 (1573806 /sec) conflict literals : 60496 (11.92 % deleted) average of lbd : 24.61 Memory used : 8.00 MB CPU time : 0.116982 s SATISFIABLE 22 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_22-std.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 6912 | | Number of clauses: 15200 | | Parse time: 0.01 s | | Eliminated clauses: 0.14 Mb | | Simplification time: 0.05 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 100 | 3117 9911 45121 | 100 62 59.4 2513.9 | 8.507 % | | 250 | 3117 9911 45121 | 250 39 33.4 1311.9 | 8.507 % | | 388 | 3117 9911 45121 | 388 35 27.6 1018.2 | 8.507 % | ==================================================================================== restarts : 2 (26.67 /sec) (194.00 confs/res) conflicts : 388 (5174 /sec) decisions : 11328 (0.00 % random) (151064 /sec) propagations : 32869 (438323 /sec) conflict literals : 13530 (3.87 % deleted) average of lbd : 27.58 Memory used : 9.00 MB CPU time : 0.074988 s SATISFIABLE 23 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_23-std.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 6912 | | Number of clauses: 15213 | | Parse time: 0.01 s | | Eliminated clauses: 0.14 Mb | | Simplification time: 0.05 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 100 | 3168 10033 45922 | 100 75 72.4 2532.8 | 8.275 % | | 250 | 3168 10033 45922 | 250 43 39.2 1352.1 | 8.275 % | | 475 | 3168 10033 45922 | 475 41 33.5 907.7 | 8.275 % | | 798 | 3168 10033 45922 | 798 40 30.6 665.1 | 8.275 % | ==================================================================================== restarts : 3 (36.15 /sec) (266.00 confs/res) conflicts : 798 (9616 /sec) decisions : 13151 (0.00 % random) (158471 /sec) propagations : 72752 (876667 /sec) conflict literals : 31928 (6.57 % deleted) average of lbd : 30.62 Memory used : 9.00 MB CPU time : 0.082987 s SATISFIABLE 24 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_24-std.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 6912 | | Number of clauses: 15210 | | Parse time: 0.01 s | | Eliminated clauses: 0.14 Mb | | Simplification time: 0.05 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 100 | 3148 9995 45778 | 100 62 57.8 2992.8 | 8.145 % | | 250 | 3148 9995 45778 | 250 64 59.6 2828.2 | 8.145 % | | 384 | 3148 9995 45778 | 384 50 45.1 2070.7 | 8.145 % | ==================================================================================== restarts : 2 (27.03 /sec) (192.00 confs/res) conflicts : 384 (5190 /sec) decisions : 12739 (0.00 % random) (172177 /sec) propagations : 27864 (376602 /sec) conflict literals : 19157 (1.39 % deleted) average of lbd : 45.14 Memory used : 8.00 MB CPU time : 0.073988 s SATISFIABLE 25 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_25-std.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 6912 | | Number of clauses: 15210 | | Parse time: 0.01 s | | Eliminated clauses: 0.14 Mb | | Simplification time: 0.05 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 100 | 3161 10004 45809 | 100 52 47.6 3004.2 | 8.464 % | | 250 | 3161 10004 45809 | 250 42 38.4 2208.0 | 8.464 % | | 475 | 3161 10004 45809 | 475 43 36.0 1444.2 | 8.464 % | | 490 | 3161 10004 45809 | 490 42 35.4 1406.6 | 8.464 % | ==================================================================================== restarts : 3 (40.01 /sec) (163.33 confs/res) conflicts : 490 (6534 /sec) decisions : 14244 (0.00 % random) (189950 /sec) propagations : 47632 (635195 /sec) conflict literals : 20812 (4.03 % deleted) average of lbd : 35.39 Memory used : 8.00 MB CPU time : 0.074988 s SATISFIABLE 26 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_26-std.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 6912 | | Number of clauses: 15209 | | Parse time: 0.01 s | | Eliminated clauses: 0.14 Mb | | Simplification time: 0.05 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 100 | 3152 10027 46108 | 100 56 52.3 2998.3 | 8.435 % | | 250 | 3152 10027 46108 | 250 51 47.4 2475.8 | 8.435 % | | 475 | 3152 10027 46108 | 475 39 33.9 1536.8 | 8.435 % | | 747 | 3152 10027 46108 | 747 38 32.0 1135.8 | 8.435 % | ==================================================================================== restarts : 3 (37.04 /sec) (249.00 confs/res) conflicts : 747 (9224 /sec) decisions : 14148 (0.00 % random) (174695 /sec) propagations : 59921 (739884 /sec) conflict literals : 28171 (3.63 % deleted) average of lbd : 32.02 Memory used : 9.00 MB CPU time : 0.080987 s SATISFIABLE 27 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_27-std.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 6912 | | Number of clauses: 15213 | | Parse time: 0.01 s | | Eliminated clauses: 0.14 Mb | | Simplification time: 0.05 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 100 | 3145 10031 46192 | 100 38 34.2 2030.0 | 8.840 % | | 141 | 3145 10031 46192 | 141 33 28.3 1671.7 | 8.840 % | ==================================================================================== restarts : 2 (28.17 /sec) (70.50 confs/res) conflicts : 141 (1986 /sec) decisions : 15568 (0.00 % random) (219302 /sec) propagations : 22471 (316542 /sec) conflict literals : 4584 (1.44 % deleted) average of lbd : 28.35 Memory used : 9.00 MB CPU time : 0.070989 s SATISFIABLE 28 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_28-std.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 6912 | | Number of clauses: 15223 | | Parse time: 0.01 s | | Eliminated clauses: 0.14 Mb | | Simplification time: 0.05 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 100 | 3152 10037 46255 | 100 35 32.1 2089.4 | 8.174 % | | 250 | 3152 10037 46255 | 250 30 25.4 1223.7 | 8.174 % | | 320 | 3152 10037 46255 | 320 31 25.6 1054.8 | 8.174 % | ==================================================================================== restarts : 3 (44.12 /sec) (106.67 confs/res) conflicts : 320 (4707 /sec) decisions : 15997 (0.00 % random) (235288 /sec) propagations : 36317 (534160 /sec) conflict literals : 9873 (2.71 % deleted) average of lbd : 25.64 Memory used : 9.00 MB CPU time : 0.067989 s SATISFIABLE 29 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_29-std.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 6912 | | Number of clauses: 15228 | | Parse time: 0.01 s | | Eliminated clauses: 0.15 Mb | | Simplification time: 0.05 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 100 | 3152 10034 46271 | 100 33 30.4 2013.2 | 7.957 % | | 250 | 3152 10034 46271 | 250 30 25.0 1163.1 | 7.957 % | | 380 | 3152 10034 46271 | 380 31 25.6 900.0 | 7.957 % | ==================================================================================== restarts : 3 (40.01 /sec) (126.67 confs/res) conflicts : 380 (5067 /sec) decisions : 17581 (0.00 % random) (234451 /sec) propagations : 47634 (635222 /sec) conflict literals : 11905 (2.06 % deleted) average of lbd : 25.57 Memory used : 9.00 MB CPU time : 0.074988 s SATISFIABLE 30 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_30-std.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 6912 | | Number of clauses: 15216 | | Parse time: 0.01 s | | Eliminated clauses: 0.14 Mb | | Simplification time: 0.05 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 100 | 3257 10198 46927 | 100 36 33.5 1699.3 | 9.592 % | | 250 | 3257 10198 46927 | 250 33 28.8 1190.9 | 9.592 % | | 284 | 3257 10198 46927 | 284 31 27.3 1109.1 | 9.592 % | ==================================================================================== restarts : 2 (28.99 /sec) (142.00 confs/res) conflicts : 284 (4117 /sec) decisions : 13433 (0.00 % random) (194712 /sec) propagations : 28948 (419603 /sec) conflict literals : 8940 (1.36 % deleted) average of lbd : 27.31 Memory used : 9.00 MB CPU time : 0.068989 s SATISFIABLE 31 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_31-std.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 6912 | | Number of clauses: 15226 | | Parse time: 0.01 s | | Eliminated clauses: 0.13 Mb | | Simplification time: 0.04 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 100 | 3236 10162 46852 | 100 103 100.0 2983.2 | 10.966 % | | 250 | 3236 10162 46852 | 250 61 55.3 1687.7 | 10.966 % | | 285 | 3236 10162 46852 | 285 57 50.8 1554.0 | 10.966 % | ==================================================================================== restarts : 2 (32.26 /sec) (142.50 confs/res) conflicts : 285 (4598 /sec) decisions : 11023 (0.00 % random) (177819 /sec) propagations : 29975 (483546 /sec) conflict literals : 16125 (0.89 % deleted) average of lbd : 50.80 Memory used : 8.00 MB CPU time : 0.06199 s SATISFIABLE 32 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_32-std.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 6912 | | Number of clauses: 15232 | | Parse time: 0.01 s | | Eliminated clauses: 0.12 Mb | | Simplification time: 0.04 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 100 | 3425 10475 47920 | 100 55 52.9 2208.4 | 11.560 % | | 250 | 3425 10475 47920 | 250 50 43.7 1508.3 | 11.560 % | | 455 | 3425 10475 47920 | 455 46 35.8 1276.7 | 11.560 % | ==================================================================================== restarts : 2 (31.75 /sec) (227.50 confs/res) conflicts : 455 (7223 /sec) decisions : 11953 (0.00 % random) (189760 /sec) propagations : 45562 (723321 /sec) conflict literals : 20704 (2.88 % deleted) average of lbd : 35.78 Memory used : 8.00 MB CPU time : 0.06299 s SATISFIABLE 33 WARNING: for repeatability, setting FPU to use double precision glueminisat2.2.5 Command: ../../sat/glueminisat_static alldiff_32_34_33-std.cnf ===============================[ Problem Statistics ]=============================== | | | Number of variables: 6912 | | Number of clauses: 15264 | | Parse time: 0.01 s | | Eliminated clauses: 0.11 Mb | | Simplification time: 0.03 s | | | ===============================[ Search Statistics ]================================ | Conflicts | ORIGINAL | LEARNT | Progress | | | Vars Clauses Literals | Clauses Lit/Cl LBD/Cl DLV/Cl | | ==================================================================================== | 100 | 4160 11771 52164 | 100 37 32.3 1380.8 | 7.407 % | | 250 | 4160 11771 52164 | 250 37 21.3 897.2 | 7.407 % | | 475 | 4160 11771 52164 | 475 42 19.9 726.6 | 7.407 % | | 771 | 4160 11771 52164 | 771 47 20.2 649.5 | 7.407 % | ==================================================================================== restarts : 2 (28.17 /sec) (385.50 confs/res) conflicts : 771 (10861 /sec) decisions : 11311 (0.00 % random) (159335 /sec) propagations : 83670 (1178633 /sec) conflict literals : 36461 (12.92 % deleted) average of lbd : 20.16 Memory used : 9.00 MB CPU time : 0.070989 s SATISFIABLE