c #BEGIN: [Fri Mar 18 16:53:53 2022] c #HOST: mini14.local c #TIMELIMIT: 18000 c #MEMLIMIT: 0 c #FREQ: 10 c #SOLVER: isr-bug-finder c #CSP: benchmark/graph-instance/core-challenge-2022/color04/wap08a.col benchmark/graph-instance/core-challenge-2022/color04/wap08a_01.dat c #COMMAND: /Users/soh/app/scala-2.12.4/bin/scala -J-Xms16g -J-Xmx16g -cp /Users/soh/app/IsrForCompetition220315-22h16m/scop.jar:/Users/soh/app/IsrForCompetition220315-22h16m/isr4competition_2.12-1.3.5.jar fun.scop.app.isr.IsrSolverTj03 benchmark/graph-instance/core-challenge-2022/color04/wap08a.col benchmark/graph-instance/core-challenge-2022/color04/wap08a_01.dat cadical /Users/soh/app/IsrForCompetition220315-22h16m/cadical c (0) step 1 UNSAT 11220 234526 c (0) step 2 UNSAT 20569 363007 c (0) step 3 UNSAT 29918 491488 c (1) step 4 UNSAT 39267 619969 c (1) step 5 UNSAT 48616 748450 c (2) step 6 UNSAT 57965 876931 c (5) step 7 UNSAT 67314 1005412 c (13) step 8 UNSAT 76663 1133893 c (34) step 9 UNSAT 86012 1262374 c (63) step 10 UNSAT 95361 1390855 c (102) step 11 UNSAT 104710 1519336 c (144) step 12 UNSAT 114059 1647817 c (144) step 13 SAT 123408 1776298 a YES a 33 41 44 66 68 83 84 90 91 109 112 127 129 131 133 134 139 143 145 148 149 154 157 163 165 167 184 185 189 190 197 200 201 215 217 221 223 225 229 230 234 247 251 252 253 255 259 261 262 267 270 273 291 293 299 300 305 307 310 311 318 336 340 341 344 345 350 352 354 355 360 364 366 368 376 382 398 407 414 415 417 443 444 447 449 459 462 468 472 482 486 488 496 504 512 516 518 528 541 543 555 560 586 599 600 606 610 621 626 632 647 653 657 684 693 731 785 811 843 900 1044 1132 1251 1521 1712 1811 1812 1820 1822 1824 1825 1826 1828 1829 1832 1836 1837 1838 1843 1844 1845 1846 1848 1856 1857 1862 1865 1867 1868 1870 a 33 41 44 66 68 83 84 90 91 109 112 127 129 131 133 134 139 143 145 148 149 154 157 163 165 167 184 185 189 190 197 200 201 215 217 221 223 225 229 230 234 247 251 252 253 255 259 261 262 267 270 273 291 293 299 300 305 307 310 311 318 336 340 341 344 345 350 352 354 355 360 364 366 368 376 382 398 407 414 415 417 443 444 447 449 459 462 468 472 482 486 488 496 504 512 516 518 528 541 543 555 560 586 599 600 606 610 621 626 632 647 653 657 684 693 731 785 811 843 900 1044 1132 1251 1521 1712 1811 1812 1820 1822 1824 1825 1826 1828 1829 1832 1835 1836 1837 1838 1843 1844 1845 1846 1848 1856 1857 1862 1865 1867 1870 a 33 41 44 66 68 83 84 90 91 109 112 127 129 131 133 134 139 143 145 148 149 154 157 163 165 167 184 185 189 190 197 200 201 215 217 221 223 225 229 230 234 247 251 252 255 259 261 262 267 270 273 291 293 299 300 305 307 310 311 318 336 340 341 344 345 350 352 354 355 360 364 366 368 376 382 398 407 414 415 417 443 444 447 449 459 462 468 472 482 486 488 496 504 512 516 518 528 541 543 555 560 586 599 600 606 610 621 626 632 647 653 657 684 693 731 739 785 811 843 900 1044 1132 1251 1521 1712 1811 1812 1820 1822 1824 1825 1826 1828 1829 1832 1835 1836 1837 1838 1843 1844 1845 1846 1848 1856 1857 1862 1865 1867 1870 a 33 41 44 66 68 83 84 90 91 109 112 127 129 131 133 134 139 143 145 148 149 154 157 163 165 167 184 185 189 190 197 200 201 215 217 221 223 225 229 230 234 247 251 252 254 259 261 262 267 270 273 291 293 299 300 305 307 310 311 318 336 340 341 344 345 350 352 354 355 360 364 366 368 376 382 398 407 414 415 417 443 444 447 449 459 462 468 472 482 486 488 496 504 512 516 518 528 541 543 555 560 586 599 600 606 610 621 626 632 647 653 657 684 693 731 739 785 811 843 900 1044 1132 1251 1521 1712 1811 1812 1820 1822 1824 1825 1826 1828 1829 1832 1835 1836 1837 1838 1843 1844 1845 1846 1848 1856 1857 1862 1865 1867 1870 a 33 41 44 66 68 83 84 90 91 109 112 127 129 131 133 134 139 143 145 148 149 154 157 163 165 167 184 185 189 190 197 200 201 215 217 221 223 225 229 230 234 247 251 252 254 259 261 262 267 269 273 291 293 299 300 305 307 310 311 318 336 340 341 344 345 350 352 354 355 360 364 366 368 376 382 398 407 414 415 417 443 444 447 449 459 462 468 472 482 486 488 496 504 512 516 518 528 541 543 555 560 586 599 600 606 610 621 626 632 647 653 657 684 693 731 739 785 811 843 900 1044 1132 1251 1521 1712 1811 1812 1820 1822 1824 1825 1826 1828 1829 1832 1835 1836 1837 1838 1843 1844 1845 1846 1848 1856 1857 1862 1865 1867 1870 a 33 41 44 66 68 83 84 90 91 95 112 127 129 131 133 134 139 143 145 148 149 154 157 163 165 167 184 185 189 190 197 200 201 215 217 221 223 225 229 230 234 247 251 252 254 259 261 262 267 269 273 291 293 299 300 305 307 310 311 318 336 340 341 344 345 350 352 354 355 360 364 366 368 376 382 398 407 414 415 417 443 444 447 449 459 462 468 472 482 486 488 496 504 512 516 518 528 541 543 555 560 586 599 600 606 610 621 626 632 647 653 657 684 693 731 739 785 811 843 900 1044 1132 1251 1521 1712 1811 1812 1820 1822 1824 1825 1826 1828 1829 1832 1835 1836 1837 1838 1843 1844 1845 1846 1848 1856 1857 1862 1865 1867 1870 a 33 41 44 66 68 83 84 90 91 95 112 127 129 131 133 134 139 143 145 148 149 154 157 163 165 167 184 185 189 190 197 200 201 215 217 221 223 225 229 230 234 247 251 252 254 259 261 262 267 269 273 291 293 299 300 305 307 310 311 318 336 340 341 344 345 350 352 354 355 360 364 366 368 376 382 398 407 414 415 417 443 444 447 449 459 462 468 472 482 486 488 496 504 512 516 518 528 541 543 555 560 586 599 606 610 621 626 632 647 653 657 684 693 731 739 785 811 817 843 900 1044 1132 1251 1521 1712 1811 1812 1820 1822 1824 1825 1826 1828 1829 1832 1835 1836 1837 1838 1843 1844 1845 1846 1848 1856 1857 1862 1865 1867 1870 a 33 41 44 66 68 83 84 90 91 95 112 127 129 131 133 134 139 143 145 148 149 154 157 163 165 167 184 185 189 190 197 200 201 215 217 221 223 225 229 230 234 247 251 252 254 259 261 262 267 269 273 291 293 295 299 300 305 307 310 311 318 336 340 341 344 345 350 352 354 355 360 364 366 368 376 382 398 407 414 415 417 443 444 447 449 459 462 468 472 482 486 488 496 504 512 516 518 528 541 543 555 560 586 599 606 610 621 626 632 647 653 657 684 693 731 739 785 811 817 843 900 1044 1132 1251 1521 1712 1811 1812 1820 1822 1824 1825 1826 1828 1829 1832 1835 1836 1838 1843 1844 1845 1846 1848 1856 1857 1862 1865 1867 1870 a 33 41 44 66 68 83 84 90 95 112 127 129 131 133 134 139 143 145 148 149 154 157 163 165 167 184 185 189 190 197 200 201 215 217 221 223 225 229 230 234 247 251 252 254 259 261 262 267 269 273 291 293 295 299 300 305 307 310 311 318 336 340 341 344 345 350 352 354 355 360 364 366 368 376 382 398 407 414 415 417 443 444 447 449 459 462 468 472 482 486 488 496 504 512 516 518 528 541 543 555 560 586 599 606 610 621 626 632 647 653 657 684 693 731 739 785 811 817 843 900 1004 1044 1132 1251 1521 1712 1811 1812 1820 1822 1824 1825 1826 1828 1829 1832 1835 1836 1838 1843 1844 1845 1846 1848 1856 1857 1862 1865 1867 1870 a 33 41 44 66 68 83 84 90 95 112 127 129 131 133 134 139 143 145 148 149 154 157 163 165 167 184 185 189 190 197 200 201 215 217 221 223 225 229 230 234 247 251 252 254 259 261 262 267 269 273 291 293 295 299 300 305 307 310 311 318 336 340 341 344 345 350 352 354 355 360 364 366 368 376 382 398 404 407 415 417 443 444 447 449 459 462 468 472 482 486 488 496 504 512 516 518 528 541 543 555 560 586 599 606 610 621 626 632 647 653 657 684 693 731 739 785 811 817 843 900 1004 1044 1132 1251 1521 1712 1811 1812 1820 1822 1824 1825 1826 1828 1829 1832 1835 1836 1838 1843 1844 1845 1846 1848 1856 1857 1862 1865 1867 1870 a 33 41 44 66 68 83 84 90 95 112 127 129 131 133 134 139 143 145 148 149 154 157 163 165 167 184 185 189 190 197 200 201 215 217 221 223 225 229 230 234 247 251 252 254 259 261 262 267 269 273 291 293 295 299 300 305 307 310 311 318 336 340 341 344 345 350 352 354 355 360 364 366 368 376 382 398 404 407 415 417 443 444 447 449 459 462 468 472 482 486 488 496 504 512 516 518 528 541 543 555 560 586 599 606 610 621 626 632 647 653 657 684 693 739 785 811 817 843 845 900 1004 1044 1132 1251 1521 1712 1811 1812 1820 1822 1824 1825 1826 1828 1829 1832 1835 1836 1838 1843 1844 1845 1846 1848 1856 1857 1862 1865 1867 1870 a 33 41 44 66 68 83 84 90 95 112 127 129 131 133 134 139 143 145 148 149 154 157 163 165 167 184 185 189 190 197 200 201 215 217 221 223 225 229 230 234 247 251 252 254 259 261 262 267 269 273 291 293 295 299 300 305 307 310 311 318 336 340 341 344 345 350 352 354 355 360 363 364 366 368 376 382 398 404 407 415 417 443 444 447 449 459 462 468 472 482 486 488 496 504 512 516 518 528 541 543 555 560 586 599 606 610 621 626 632 647 653 657 684 693 739 785 811 817 843 845 900 1004 1044 1132 1251 1521 1712 1811 1812 1820 1822 1824 1825 1826 1828 1829 1832 1835 1836 1838 1843 1844 1845 1846 1848 1856 1857 1862 1865 1867 a 33 41 44 66 68 83 84 90 95 112 127 129 131 133 134 139 143 145 148 149 157 163 165 167 184 185 189 190 197 200 201 215 217 221 223 225 229 230 234 247 251 252 254 259 261 262 267 269 273 291 293 295 299 300 305 307 310 311 318 336 340 341 344 345 350 352 354 355 360 363 364 366 368 376 382 398 404 407 415 417 443 444 447 449 459 462 468 472 482 486 488 496 504 512 516 518 528 541 543 555 560 586 599 606 610 621 626 632 647 653 657 684 693 739 785 811 817 829 843 845 900 1004 1044 1132 1251 1521 1712 1811 1812 1820 1822 1824 1825 1826 1828 1829 1832 1835 1836 1838 1843 1844 1845 1846 1848 1856 1857 1862 1865 1867 a 33 41 44 66 68 83 84 90 95 112 127 129 131 133 134 137 143 145 148 149 157 163 165 167 184 185 189 190 197 200 201 215 217 221 223 225 229 230 234 247 251 252 254 259 261 262 267 269 273 291 293 295 299 300 305 307 310 311 318 336 340 341 344 345 350 352 354 355 360 363 364 366 368 376 382 398 404 407 415 417 443 444 447 449 459 462 468 472 482 486 488 496 504 512 516 518 528 541 543 555 560 586 599 606 610 621 626 632 647 653 657 684 693 739 785 811 817 829 843 845 900 1004 1044 1132 1251 1521 1712 1811 1812 1820 1822 1824 1825 1826 1828 1829 1832 1835 1836 1838 1843 1844 1845 1846 1848 1856 1857 1862 1865 1867 Command being timed: "/Users/soh/app/scala-2.12.4/bin/scala -J-Xms16g -J-Xmx16g -cp /Users/soh/app/IsrForCompetition220315-22h16m/scop.jar:/Users/soh/app/IsrForCompetition220315-22h16m/isr4competition_2.12-1.3.5.jar fun.scop.app.isr.IsrSolverTj03 benchmark/graph-instance/core-challenge-2022/color04/wap08a.col benchmark/graph-instance/core-challenge-2022/color04/wap08a_01.dat cadical /Users/soh/app/IsrForCompetition220315-22h16m/cadical" User time (seconds): 147.88 System time (seconds): 1.51 Percent of CPU this job got: 102% Elapsed (wall clock) time (h:mm:ss or m:ss): 2:26.11 Average shared text size (kbytes): 0 Average unshared data size (kbytes): 0 Average stack size (kbytes): 0 Average total size (kbytes): 0 Maximum resident set size (kbytes): 7556661248 Average resident set size (kbytes): 0 Major (requiring I/O) page faults: 2 Minor (reclaiming a frame) page faults: 768332 Voluntary context switches: 53 Involuntary context switches: 19505 Swaps: 0 File system inputs: 0 File system outputs: 0 Socket messages sent: 64 Socket messages received: 0 Signals delivered: 5 Page size (bytes): 4096 Exit status: 0 c FINISHED CPU 149.39 MEM 0 MAXMEM 0 STALE 1 c #RESULT: UNK c #FIN: FIN c #CPU: 149.39 c #MAXMEM: 0 c c #END: [Fri Mar 18 16:56:19 2022]