c #BEGIN: [Thu Mar 17 11:43:05 2022]
c #HOST: mini12.local
c #TIMELIMIT: 18000
c #MEMLIMIT: 0
c #FREQ: 10
c #SOLVER: isr-bug-finder
c #CSP: benchmark/graph-instance/core-challenge-2022/color04/le450_25b.col benchmark/graph-instance/core-challenge-2022/color04/le450_25b_02.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/le450_25b.col benchmark/graph-instance/core-challenge-2022/color04/le450_25b_02.dat cadical /Users/soh/app/IsrForCompetition220315-22h16m/cadical
c (0) step 1 UNSAT 2700 22820
c (0) step 2 UNSAT 4949 36928
c (0) step 3 UNSAT 7198 51036
c (0) step 4 UNSAT 9447 65144
c (0) step 5 UNSAT 11696 79252
c (0) step 6 UNSAT 13945 93360
c (0) step 7 UNSAT 16194 107468
c (2) step 8 UNSAT 18443 121576
c (3) step 9 UNSAT 20692 135684
c (3) step 10 SAT 22941 149792
a YES
a 7 13 14 16 17 19 24 25 28 39 44 47 49 55 58 64 68 79 82 85 91 99 107 117 145 152 153 160 174 179 182 187 192 193 209 211 213 214 217 220 225 232 237 243 256 257 260 263 264 267 268 272 274 275 289 293 306 312 318 320 350 352 357 370 386 387 388 392 406 410 412 414 417 436 437 438 442
a 7 13 14 16 17 19 24 25 28 39 44 47 49 55 58 64 68 79 82 85 91 99 107 117 145 152 153 160 174 179 182 187 192 193 209 211 213 214 217 220 225 232 237 243 256 257 260 264 267 268 272 274 275 289 293 306 312 318 320 350 352 357 370 386 387 388 392 406 410 412 414 417 418 436 437 438 442
a 7 13 14 16 17 19 24 25 28 39 44 47 49 55 58 64 68 79 82 85 91 99 107 117 145 152 153 160 174 179 182 187 192 193 209 211 213 214 217 220 225 232 237 243 256 257 260 264 267 268 272 274 275 289 293 306 312 318 320 350 352 357 370 372 386 387 388 392 406 410 414 417 418 436 437 438 442
a 7 13 14 16 17 19 24 25 28 39 44 47 49 55 58 64 68 79 82 85 91 99 107 117 145 152 153 160 174 179 182 187 192 193 209 211 213 214 217 220 221 225 232 237 243 256 257 260 264 267 268 272 274 275 289 293 306 312 318 320 350 352 357 370 372 386 387 388 392 406 410 417 418 436 437 438 442
a 7 13 14 16 17 19 24 25 28 39 44 47 49 55 58 64 68 79 82 85 91 99 107 117 145 151 152 153 160 174 179 182 192 193 209 211 213 214 217 220 221 225 232 237 243 256 257 260 264 267 268 272 274 275 289 293 306 312 318 320 350 352 357 370 372 386 387 388 392 406 410 417 418 436 437 438 442
a 7 13 14 16 17 19 24 25 28 39 44 47 49 55 58 64 68 79 82 85 91 99 107 117 145 151 152 153 160 174 179 182 189 192 193 209 211 213 214 217 220 221 232 237 243 256 257 260 264 267 268 272 274 275 289 293 306 312 318 320 350 352 357 370 372 386 387 388 392 406 410 417 418 436 437 438 442
a 7 13 14 16 17 19 24 25 28 39 44 47 49 55 58 64 68 79 82 85 91 99 107 117 145 151 153 160 162 174 179 182 189 192 193 209 211 213 214 217 220 221 232 237 243 256 257 260 264 267 268 272 274 275 289 293 306 312 318 320 350 352 357 370 372 386 387 388 392 406 410 417 418 436 437 438 442
a 7 13 14 16 17 19 24 25 28 39 44 47 49 55 58 64 68 79 82 83 85 91 99 107 117 145 151 153 160 162 174 179 182 189 192 193 209 211 213 214 217 220 221 232 237 243 256 257 260 264 267 268 272 275 289 293 306 312 318 320 350 352 357 370 372 386 387 388 392 406 410 417 418 436 437 438 442
a 7 13 14 16 17 19 24 25 28 39 44 47 49 55 58 64 68 79 82 83 85 91 99 107 117 145 151 153 157 160 162 174 179 182 189 192 193 209 211 213 214 217 220 221 232 237 243 256 257 260 264 267 268 272 275 289 293 306 312 318 320 350 352 357 370 372 386 387 388 392 406 410 417 418 436 437 442
a 7 13 14 16 17 19 24 25 28 39 44 47 49 55 58 64 68 79 82 83 85 99 107 117 145 151 153 157 160 162 174 179 182 189 192 193 209 211 213 214 217 220 221 232 237 243 256 257 260 264 267 268 272 275 289 293 306 312 318 320 337 350 352 357 370 372 386 387 388 392 406 410 417 418 436 437 442
a 7 13 14 16 17 19 24 25 28 39 44 47 49 55 58 64 68 79 82 83 85 107 117 145 151 153 157 160 162 174 179 182 189 192 193 209 211 213 214 215 217 220 221 232 237 243 256 257 260 264 267 268 272 275 289 293 306 312 318 320 337 350 352 357 370 372 386 387 388 392 406 410 417 418 436 437 442
	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/le450_25b.col benchmark/graph-instance/core-challenge-2022/color04/le450_25b_02.dat cadical /Users/soh/app/IsrForCompetition220315-22h16m/cadical"
	User time (seconds): 5.76
	System time (seconds): 0.19
	Percent of CPU this job got: 141%
	Elapsed (wall clock) time (h:mm:ss or m:ss): 0:04.20
	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): 1267253248
	Average resident set size (kbytes): 0
	Major (requiring I/O) page faults: 34
	Minor (reclaiming a frame) page faults: 93989
	Voluntary context switches: 41
	Involuntary context switches: 2872
	Swaps: 0
	File system inputs: 0
	File system outputs: 0
	Socket messages sent: 50
	Socket messages received: 0
	Signals delivered: 5
	Page size (bytes): 4096
	Exit status: 0
c FINISHED CPU 5.95 MEM 0 MAXMEM 0 STALE 1
c #RESULT: UNK
c #FIN: FIN
c #CPU: 5.95
c #MAXMEM: 0
c 
c #END: [Thu Mar 17 11:43:10 2022]