c ---- [ banner ] ------------------------------------------------------------ c c Kissat SAT Solver c c Copyright (c) 2021-2023 Armin Biere University of Freiburg c Copyright (c) 2019-2021 Armin Biere Johannes Kepler University Linz c c Version 3.1.1 71caafb4d182ced9f76cef45b00f37cc598f2a37 c gcc (GCC) 13.2.1 20230801 -W -Wall -O3 -DNDEBUG c Wed Apr 24 16:38:09 EEST 2024 Linux Christoph-laptop 6.8.2-arch2-1 x86_64 c c ---- [ parsing ] ----------------------------------------------------------- c c opened and reading DIMACS file: c c ../sat-rs/rustsat/data/smtlib-qfbv-aigs-ext_con_032_008_0256-tseitin.cnf c c parsed 'p cnf 27224 68879' header c closing input after reading 1111443 bytes (1 MB) c finished parsing after 0.02 seconds c c ---- [ solving ] ----------------------------------------------------------- c c seconds switched conflicts irredundant variables c MB reductions redundant trail remaining c level restarts binary glue c c * 0.02 7 0 0 0 0 0 0 45918 22959 0% 0 27158 100% c { 0.02 7 0 0 0 0 0 0 45918 22959 0% 0 27158 100% c i 0.03 8 73 0 0 0 210 153 45974 22959 18% 2 27156 100% c i 0.05 8 208 0 0 84 413 292 46032 22959 19% 14 27154 100% c - 0.11 8 266 0 1 132 1023 145 45801 22959 23% 46 27154 100% c } 0.11 8 266 1 1 132 1023 145 45801 22959 23% 46 27154 100% c [ 0.11 8 0 1 1 132 1023 145 45801 22959 0% 0 27154 100% c B 0.11 8 0 1 1 132 1023 145 45801 22959 0% 0 27154 100% c i 0.13 8 100 1 1 132 1239 304 45857 22959 19% 2 27153 100% c - 0.20 8 412 1 2 132 2034 283 45804 22959 26% 76 27153 100% c W 0.20 9 412 1 2 132 2034 283 45804 22925 26% 76 27153 100% c d 0.22 9 378 1 2 133 2340 548 45837 22888 25% 74 27151 100% c b 0.22 9 378 1 2 133 2340 548 45837 22888 25% 74 27148 100% c u 0.23 9 378 1 2 133 2340 505 45880 22888 25% 74 27148 100% c v 0.23 9 378 1 2 133 2340 495 45889 22888 25% 74 27147 100% c w 0.24 9 378 1 2 133 2340 495 45917 22752 25% 74 26735 98% c = 0.26 9 378 1 2 133 2340 495 46806 22222 25% 74 26286 97% c d 0.27 9 378 1 2 133 2340 474 45668 21979 25% 74 26281 97% c i 0.27 9 378 1 2 133 2340 474 45668 21979 25% 74 26281 97% c i 0.28 9 377 1 2 133 2391 524 45668 21979 25% 73 26280 97% c c seconds switched conflicts irredundant variables c MB reductions redundant trail remaining c level restarts binary glue c c i 0.28 9 374 1 2 133 2420 552 45668 21979 24% 73 26278 97% c ] 0.32 10 361 2 2 133 2891 1023 45668 21979 24% 68 26278 97% c { 0.32 10 266 2 2 133 2891 1023 45668 21979 23% 46 26278 97% c i 0.33 10 226 2 2 138 3176 1193 45780 21979 22% 37 26277 97% c - 0.37 10 294 2 3 182 3448 454 44424 21979 24% 35 26277 97% c } 0.46 10 442 3 3 362 3891 870 44437 21979 28% 38 26277 97% c [ 0.46 10 361 3 3 362 3891 870 44437 21979 24% 68 26277 97% c I 0.53 10 476 3 3 362 4293 1272 44437 21979 27% 65 26277 97% c d 0.56 10 429 3 3 362 4673 1529 44176 21940 26% 64 26128 96% c u 0.57 10 429 3 3 362 4673 1444 44261 21940 26% 64 26128 96% c v 0.57 10 429 3 3 362 4673 1443 44262 21940 26% 64 26128 96% c = 0.61 10 429 3 3 362 4673 1443 44330 21940 26% 64 26094 96% c d 0.62 10 429 3 3 362 4673 1443 44188 21940 26% 64 26092 96% c - 0.66 10 414 3 4 363 5181 521 44131 21940 25% 62 26092 96% c ] 0.78 10 381 4 4 364 6762 2054 44131 21940 24% 59 26092 96% c { 0.78 10 442 4 4 364 6762 2054 44131 21940 28% 38 26092 96% c i 0.79 10 425 4 4 369 6890 2116 44187 21940 28% 36 26091 96% c - 0.80 10 400 4 5 382 7196 591 44128 21940 27% 39 26091 96% c } 0.92 10 439 5 5 510 9130 2395 44181 21940 28% 43 26091 96% c [ 0.92 10 381 5 5 510 9130 2395 44181 21940 24% 59 26091 96% c c seconds switched conflicts irredundant variables c MB reductions redundant trail remaining c level restarts binary glue c c B 0.92 10 381 5 5 510 9130 2395 44181 21940 24% 59 26091 96% c - 0.95 10 377 5 6 510 9432 791 44181 21940 24% 58 26091 96% c u 0.97 10 375 5 6 510 9506 813 44233 21938 24% 58 26091 96% c v 0.97 10 375 5 6 510 9506 813 44233 21938 24% 58 26091 96% c = 1.02 10 375 5 6 510 9506 813 44235 21938 24% 58 26090 96% c d 1.02 10 375 5 6 510 9506 813 44231 21938 24% 58 26090 96% c t 1.03 10 375 5 6 510 9506 813 44228 21938 24% 58 26090 96% c ] 1.23 10 323 6 6 512 11535 2770 44228 21938 23% 56 26090 96% c { 1.23 10 439 6 6 512 11535 2770 44228 21938 28% 43 26090 96% c 2 1.23 10 437 6 6 514 11703 2858 44171 21938 28% 41 26090 96% c e 1.31 12 437 6 6 514 11703 2858 20 5 28% 41 1 0% c } 1.31 12 437 6 6 514 11703 2858 20 5 28% 41 1 0% c 0 1.31 12 437 6 6 514 11703 2858 20 5 28% 41 1 0% c c ---- [ result ] ------------------------------------------------------------ c s UNSATISFIABLE c c ---- [ profiling ] --------------------------------------------------------- c c 1.02 78.08 % search c 0.64 49.11 % stable c 0.38 28.97 % focused c 0.27 20.62 % simplify c 0.19 14.56 % probe c 0.08 6.35 % sweep c 0.07 5.72 % eliminate c 0.06 4.70 % vivify c 0.02 1.69 % substitute c 0.02 1.28 % parse c 0.01 0.98 % backbone c 0.01 0.83 % transitive c 0.01 0.56 % reduce c 0.00 0.34 % walking c 0.00 0.25 % subsume c 0.00 0.00 % warmup c ============================================= c 1.31 100.00 % total c c ---- [ statistics ] -------------------------------------------------------- c c chronological: 6826 58 % conflicts c conflicts: 11703 8931.73 per second c decisions: 805237 68.81 per conflict c eliminated: 26038 96 % variables c jumped_reasons: 6564398 36 % propagations c propagations: 18029274 13759937 per second c queue_decisions: 402857 50 % decision c random_decisions: 26955 3 % decision c random_sequences: 8 1463 interval c reductions: 6 1950 interval c rephased: 4 2926 interval c restarts: 514 22.77 interval c score_decisions: 375425 47 % decision c substituted: 635 2 % variables c switched: 6 1950 interval c vivified: 331 1 % checks c vivify_checks: 62713 20904 per vivify c vivify_units: 109 0 % variables c walk_improved: 1 100 % walks c walks: 1 11703 interval c c ---- [ resources ] --------------------------------------------------------- c c maximum-resident-set-size: 12193792 bytes 12 MB c process-time: 1s 1.31 seconds c c ---- [ shutting down ] ----------------------------------------------------- c c exit 20