Name | normalized-opb/mps-v2-20-10/MIPLIB/miplib2003/normalized-mps-v2-20-10-vpm2.opb |
MD5SUM | c1b4c3ad409db732d2b559e570b6f24c |
Bench Category | optimization, medium integers (OPTMEDINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 138 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 168 |
Biggest coefficient in the objective function | 5 |
Number of bits for the biggest coefficient in the objective function | 3 |
Sum of the numbers in the objective function | 504 |
Number of bits of the sum of numbers in the objective function | 9 |
Biggest number in a constraint | 819200 |
Number of bits of the biggest number in a constraint | 20 |
Biggest sum of numbers in a constraint | 4941871 |
Number of bits of the biggest sum of numbers | 23 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1189.01 |
Number of variables | 2754 |
Total number of constraints | 612 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 168 |
Number of constraints which are nor clauses,nor cardinality constraints | 444 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 84 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc6 THE 2005-04-21 07:45:01 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=13140 boxname=wulflinc6 idbench=1011 idsolver=10 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: c1b4c3ad409db732d2b559e570b6f24c /oldhome/oroussel/tmp/wulflinc6/normalized-mps-v2-20-10-vpm2.opb REAL COMMAND: minisat+ -ca /oldhome/oroussel/tmp/wulflinc6/normalized-mps-v2-20-10-vpm2.opb /oldhome/oroussel/tmp/wulflinc6/normalized-mps-v2-20-10-vpm2.opb IDLAUNCH: 13140 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.042 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.042 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 614324 kB Buffers: 29656 kB Cached: 368708 kB SwapCached: 320 kB Active: 113428 kB Inactive: 287496 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 614072 kB SwapTotal: 2097136 kB SwapFree: 2096448 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5752 kB Slab: 13704 kB Committed_AS: 63584 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-04-21 08:05:04 (client local time) WITH STATUS 0 IN 1200.58 SECONDS stats: 13140 7 1200.58 0 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 486 PB-constraints to clauses... c -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp c -- Detecting intervals from adjacent constraints: ############################## c -- Clauses(.)/Splits(s): (none) c ---[ 485]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 484]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 483]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 482]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 481]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 480]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 479]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 478]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 477]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 474]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 473]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 472]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 471]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 468]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 467]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 466]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 465]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 462]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 459]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 458]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 457]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 454]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 453]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 452]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 451]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 450]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 448]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 447]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 446]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 445]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 444]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 441]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 440]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 439]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 433]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 427]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 422]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 421]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 415]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 409]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 408]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 402]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 397]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 396]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 391]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 390]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 386]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 385]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 384]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 380]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 379]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 378]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 374]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 373]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 372]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 368]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 367]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 366]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 365]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 364]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 359]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 353]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 347]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 339]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 333]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 327]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 321]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 317]---> Adder-cost: 61 maxlim: 57342 bits: 17/16 c ---[ 316]---> Adder-cost: 61 maxlim: 57342 bits: 17/16 c ---[ 315]---> Adder-cost: 61 maxlim: 57342 bits: 17/16 c ---[ 314]---> Adder-cost: 61 maxlim: 57342 bits: 17/16 c ---[ 313]---> Adder-cost: 61 maxlim: 57342 bits: 17/16 c ---[ 312]---> Adder-cost: 61 maxlim: 57342 bits: 17/16 c ---[ 310]---> Adder-cost: 61 maxlim: 57342 bits: 17/16 c ---[ 309]---> Adder-cost: 61 maxlim: 57342 bits: 17/16 c ---[ 308]---> Adder-cost: 61 maxlim: 57342 bits: 17/16 c ---[ 307]---> Adder-cost: 61 maxlim: 57342 bits: 17/16 c ---[ 306]---> Adder-cost: 61 maxlim: 57342 bits: 17/16 c ---[ 302]---> Adder-cost: 57 maxlim: 28670 bits: 16/15 c ---[ 301]---> Adder-cost: 57 maxlim: 28670 bits: 16/15 c ---[ 300]---> Adder-cost: 57 maxlim: 28670 bits: 16/15 c ---[ 295]---> Adder-cost: 57 maxlim: 28670 bits: 16/15 c ---[ 294]---> Adder-cost: 57 maxlim: 28670 bits: 16/15 c ---[ 290]---> Adder-cost: 36 maxlim: 217086 bits: 19/18 c ---[ 289]---> Adder-cost: 36 maxlim: 217086 bits: 19/18 c ---[ 288]---> Adder-cost: 36 maxlim: 217086 bits: 19/18 c ---[ 287]---> Adder-cost: 57 maxlim: 28670 bits: 16/15 c ---[ 286]---> Adder-cost: 57 maxlim: 28670 bits: 16/15 c ---[ 285]---> Adder-cost: 57 maxlim: 28670 bits: 16/15 c ---[ 284]---> Adder-cost: 57 maxlim: 28670 bits: 16/15 c ---[ 283]---> Adder-cost: 57 maxlim: 28670 bits: 16/15 c ---[ 282]---> Adder-cost: 57 maxlim: 28670 bits: 16/15 c ---[ 280]---> Adder-cost: 57 maxlim: 28670 bits: 16/15 c ---[ 279]---> Adder-cost: 57 maxlim: 28670 bits: 16/15 c ---[ 278]---> Adder-cost: 57 maxlim: 28670 bits: 16/15 c ---[ 277]---> Adder-cost: 57 maxlim: 28670 bits: 16/15 c ---[ 276]---> Adder-cost: 57 maxlim: 28670 bits: 16/15 c ---[ 274]---> Adder-cost: 352 maxlim: 2411343 bits: 22/22 c ---[ 272]---> Adder-cost: 288 maxlim: 1694643 bits: 21/21 c ---[ 271]---> Adder-cost: 2 maxlim: 2046 bits: 12/11 c ---[ 270]---> Adder-cost: 2 maxlim: 2046 bits: 12/11 c ---[ 269]---> Adder-cost: 2 maxlim: 2046 bits: 12/11 c ---[ 267]---> Adder-cost: 2 maxlim: 2046 bits: 12/11 c ---[ 266]---> Adder-cost: 2 maxlim: 2046 bits: 12/11 c ---[ 265]---> Adder-cost: 2 maxlim: 2046 bits: 12/11 c ---[ 264]---> Adder-cost: 2 maxlim: 2046 bits: 12/11 c ---[ 263]---> Adder-cost: 2 maxlim: 2046 bits: 12/11 c ---[ 259]---> Adder-cost: 0 maxlim: 1022 bits: 11/10 c ---[ 258]---> Adder-cost: 2 maxlim: 2046 bits: 12/11 c ---[ 257]---> Adder-cost: 2 maxlim: 2046 bits: 12/11 c ---[ 256]---> Adder-cost: 2 maxlim: 2046 bits: 12/11 c ---[ 255]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 251]---> Adder-cost: 0 maxlim: 1022 bits: 11/10 c ---[ 250]---> Adder-cost: 2 maxlim: 2046 bits: 12/11 c ---[ 247]---> Adder-cost: 0 maxlim: 510 bits: 10/9 c ---[ 243]---> Adder-cost: 0 maxlim: 1022 bits: 11/10 c ---[ 242]---> Adder-cost: 2 maxlim: 2046 bits: 12/11 c ---[ 241]---> Adder-cost: 0 maxlim: 510 bits: 10/9 c ---[ 236]---> Adder-cost: 282 maxlim: 1636900 bits: 21/21 c ---[ 235]---> Adder-cost: 2 maxlim: 2046 bits: 12/11 c ---[ 234]---> Adder-cost: 2 maxlim: 2046 bits: 12/11 c ---[ 233]---> Adder-cost: 0 maxlim: 510 bits: 10/9 c ---[ 229]---> Adder-cost: 0 maxlim: 1022 bits: 11/10 c ---[ 228]---> Adder-cost: 2 maxlim: 2046 bits: 12/11 c ---[ 227]---> Adder-cost: 0 maxlim: 510 bits: 10/9 c ---[ 224]---> Adder-cost: 312 maxlim: 2587171 bits: 22/22 c ---[ 220]---> Adder-cost: 2 maxlim: 2046 bits: 12/11 c ---[ 219]---> Adder-cost: 2 maxlim: 2046 bits: 12/11 c ---[ 214]---> Adder-cost: 0 maxlim: 1022 bits: 11/10 c ---[ 212]---> Adder-cost: 260 maxlim: 897571 bits: 20/20 c ---[ 211]---> Adder-cost: 2 maxlim: 2046 bits: 12/11 c ---[ 206]---> Adder-cost: 2 maxlim: 2046 bits: 12/11 c ---[ 205]---> Adder-cost: 2 maxlim: 2046 bits: 12/11 c ---[ 198]---> Adder-cost: 2 maxlim: 2046 bits: 12/11 c ---[ 197]---> Adder-cost: 2 maxlim: 2046 bits: 12/11 c ---[ 193]---> Adder-cost: 2 maxlim: 2046 bits: 12/11 c ---[ 192]---> Adder-cost: 2 maxlim: 2046 bits: 12/11 c ---[ 191]---> Adder-cost: 2 maxlim: 2046 bits: 12/11 c ---[ 185]---> Adder-cost: 2 maxlim: 2046 bits: 12/11 c ---[ 184]---> Adder-cost: 2 maxlim: 2046 bits: 12/11 c ---[ 183]---> Adder-cost: 2 maxlim: 2046 bits: 12/11 c ---[ 179]---> Adder-cost: 2 maxlim: 2046 bits: 12/11 c ---[ 178]---> Adder-cost: 2 maxlim: 2046 bits: 12/11 c ---[ 175]---> Adder-cost: 2 maxlim: 2046 bits: 12/11 c ---[ 171]---> Adder-cost: 2 maxlim: 2046 bits: 12/11 c ---[ 170]---> Adder-cost: 2 maxlim: 2046 bits: 12/11 c ---[ 169]---> Adder-cost: 2 maxlim: 2046 bits: 12/11 c ---[ 168]---> Adder-cost: 2 maxlim: 2046 bits: 12/11 c ---[ 167]---> Adder-cost: 2 maxlim: 2046 bits: 12/11 c ---[ 166]---> Adder-cost: 0 maxlim: 510 bits: 10/9 c ---[ 164]---> Adder-cost: 312 maxlim: 1842000 bits: 22/21 c ---[ 163]---> Adder-cost: 0 maxlim: 510 bits: 10/9 c ---[ 162]---> Adder-cost: 0 maxlim: 510 bits: 10/9 c ---[ 161]---> Adder-cost: 0 maxlim: 510 bits: 10/9 c ---[ 160]---> Adder-cost: 2 maxlim: 2046 bits: 12/11 c ---[ 159]---> Adder-cost: 0 maxlim: 1022 bits: 11/10 c ---[ 158]---> Adder-cost: 0 maxlim: 510 bits: 10/9 c ---[ 157]---> Adder-cost: 0 maxlim: 510 bits: 10/9 c ---[ 156]---> Adder-cost: 0 maxlim: 510 bits: 10/9 c ---[ 155]---> Adder-cost: 0 maxlim: 510 bits: 10/9 c ---[ 154]---> Adder-cost: 2 maxlim: 2046 bits: 12/11 c ---[ 152]---> Adder-cost: 352 maxlim: 2411343 bits: 22/22 c ---[ 150]---> Adder-cost: 350 maxlim: 1768271 bits: 22/21 c ---[ 149]---> Adder-cost: 0 maxlim: 1022 bits: 11/10 c ---[ 148]---> Adder-cost: 0 maxlim: 254 bits: 9/8 c ---[ 147]---> Adder-cost: 0 maxlim: 254 bits: 9/8 c ---[ 146]---> Adder-cost: 0 maxlim: 254 bits: 9/8 c ---[ 145]---> Adder-cost: 0 maxlim: 254 bits: 9/8 c ---[ 144]---> Adder-cost: 2 maxlim: 2046 bits: 12/11 c ---[ 143]---> Adder-cost: 0 maxlim: 1022 bits: 11/10 c ---[ 142]---> Adder-cost: 0 maxlim: 254 bits: 9/8 c ---[ 141]---> Adder-cost: 0 maxlim: 254 bits: 9/8 c ---[ 140]---> Adder-cost: 0 maxlim: 254 bits: 9/8 c ---[ 137]---> Adder-cost: 0 maxlim: 254 bits: 9/8 c ---[ 135]---> Adder-cost: 0 maxlim: 1022 bits: 11/10 c ---[ 134]---> Adder-cost: 2 maxlim: 2046 bits: 12/11 c ---[ 133]---> Adder-cost: 0 maxlim: 510 bits: 10/9 c ---[ 132]---> Adder-cost: 0 maxlim: 510 bits: 10/9 c ---[ 131]---> Adder-cost: 0 maxlim: 510 bits: 10/9 c ---[ 129]---> Adder-cost: 0 maxlim: 1022 bits: 11/10 c ---[ 128]---> Adder-cost: 2 maxlim: 2046 bits: 12/11 c ---[ 125]---> Adder-cost: 0 maxlim: 510 bits: 10/9 c ---[ 124]---> Adder-cost: 0 maxlim: 510 bits: 10/9 c ---[ 123]---> Adder-cost: 0 maxlim: 510 bits: 10/9 c ---[ 121]---> Adder-cost: 0 maxlim: 1022 bits: 11/10 c ---[ 120]---> Adder-cost: 2 maxlim: 2046 bits: 12/11 c ---[ 119]---> Adder-cost: 0 maxlim: 510 bits: 10/9 c ---[ 118]---> Adder-cost: 0 maxlim: 510 bits: 10/9 c ---[ 117]---> Adder-cost: 0 maxlim: 510 bits: 10/9 c ---[ 114]---> Adder-cost: 274 maxlim: 1228100 bits: 21/21 c ---[ 113]---> Adder-cost: 0 maxlim: 1022 bits: 11/10 c ---[ 112]---> Adder-cost: 2 maxlim: 2046 bits: 12/11 c ---[ 111]---> Adder-cost: 0 maxlim: 254 bits: 9/8 c ---[ 110]---> Adder-cost: 0 maxlim: 254 bits: 9/8 c ---[ 109]---> Adder-cost: 0 maxlim: 254 bits: 9/8 c ---[ 107]---> Adder-cost: 312 maxlim: 1957187 bits: 22/21 c ---[ 105]---> Adder-cost: 312 maxlim: 1854787 bits: 22/21 c ---[ 103]---> Adder-cost: 390 maxlim: 2279471 bits: 22/22 c ---[ 101]---> Adder-cost: 332 maxlim: 845871 bits: 20/20 c ---[ 99]---> Adder-cost: 332 maxlim: 845871 bits: 20/20 c ---[ 97]---> Adder-cost: 332 maxlim: 845871 bits: 20/20 c ---[ 95]---> Adder-cost: 330 maxlim: 1694543 bits: 21/21 c ---[ 93]---> Adder-cost: 332 maxlim: 845871 bits: 20/20 c ---[ 91]---> Adder-cost: 394 maxlim: 1841200 bits: 22/21 c ---[ 89]---> Adder-cost: 440 maxlim: 3713071 bits: 23/22 c ---[ 87]---> Adder-cost: 368 maxlim: 999471 bits: 21/20 c ---[ 85]---> Adder-cost: 368 maxlim: 999471 bits: 21/20 c ---[ 83]---> Adder-cost: 368 maxlim: 999471 bits: 21/20 c ---[ 81]---> Adder-cost: 316 maxlim: 2149200 bits: 22/22 c ---[ 73]---> Adder-cost: 330 maxlim: 1694543 bits: 21/21 c ---[ 69]---> Adder-cost: 384 maxlim: 3377200 bits: 23/22 c ---[ 66]---> Adder-cost: 272 maxlim: 402565 bits: 20/19 c ---[ 65]---> Adder-cost: 444 maxlim: 658315 bits: 20/20 c ---[ 64]---> Adder-cost: 454 maxlim: 722315 bits: 20/20 c ---[ 63]---> Adder-cost: 534 maxlim: 914065 bits: 20/20 c ---[ 62]---> Adder-cost: 754 maxlim: 1297940 bits: 21/21 c ---[ 61]---> Adder-cost: 730 maxlim: 977940 bits: 21/20 c ---[ 60]---> Adder-cost: 82 maxlim: 17141 bits: 15/15 c ---[ 58]---> Adder-cost: 352 maxlim: 2104143 bits: 22/22 c ---[ 57]---> Adder-cost: 156 maxlim: 27371 bits: 15/15 c ---[ 56]---> Adder-cost: 164 maxlim: 29931 bits: 16/15 c ---[ 55]---> Adder-cost: 210 maxlim: 32481 bits: 16/15 c ---[ 54]---> Adder-cost: 266 maxlim: 42716 bits: 16/16 c ---[ 53]---> Adder-cost: 270 maxlim: 45276 bits: 16/16 c ---[ 52]---> Adder-cost: 80 maxlim: 18933 bits: 15/15 c ---[ 51]---> Adder-cost: 162 maxlim: 29163 bits: 16/15 c ---[ 50]---> Adder-cost: 156 maxlim: 30443 bits: 16/15 c ---[ 49]---> Adder-cost: 210 maxlim: 38113 bits: 16/16 c ---[ 48]---> Adder-cost: 268 maxlim: 48348 bits: 16/16 c ---[ 46]---> Adder-cost: 258 maxlim: 1330100 bits: 21/21 c ---[ 45]---> Adder-cost: 262 maxlim: 45788 bits: 16/16 c ---[ 44]---> Adder-cost: 40 maxlim: 3965 bits: 13/12 c ---[ 43]---> Adder-cost: 78 maxlim: 4987 bits: 13/13 c ---[ 42]---> Adder-cost: 80 maxlim: 6267 bits: 13/13 c ---[ 41]---> Adder-cost: 112 maxlim: 6521 bits: 13/13 c ---[ 40]---> Adder-cost: 138 maxlim: 9592 bits: 14/14 c ---[ 39]---> Adder-cost: 134 maxlim: 8056 bits: 14/13 c ---[ 38]---> Adder-cost: 2 maxlim: 2046 bits: 12/11 c ---[ 37]---> Adder-cost: 2 maxlim: 2046 bits: 12/11 c ---[ 36]---> Adder-cost: 2 maxlim: 2046 bits: 12/11 c ---[ 34]---> Adder-cost: 304 maxlim: 2309043 bits: 22/22 c ---[ 33]---> Adder-cost: 2 maxlim: 2046 bits: 12/11 c ---[ 32]---> Adder-cost: 2 maxlim: 2046 bits: 12/11 c ---[ 31]---> Adder-cost: 2 maxlim: 2046 bits: 12/11 c ---[ 30]---> Adder-cost: 2 maxlim: 2046 bits: 12/11 c ---[ 29]---> Adder-cost: 2 maxlim: 2046 bits: 12/11 c ---[ 28]---> Adder-cost: 2 maxlim: 2046 bits: 12/11 c ---[ 27]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 26]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 25]---> Adder-cost: 2 maxlim: 2046 bits: 12/11 c ---[ 24]---> Adder-cost: 2 maxlim: 2046 bits: 12/11 c ---[ 22]---> Adder-cost: 304 maxlim: 2104243 bits: 22/22 c ---[ 21]---> Adder-cost: 2 maxlim: 2046 bits: 12/11 c ---[ 20]---> Adder-cost: 2 maxlim: 2046 bits: 12/11 c ---[ 19]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 18]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 17]---> Adder-cost: 2 maxlim: 2046 bits: 12/11 c ---[ 16]---> Adder-cost: 2 maxlim: 2046 bits: 12/11 c ---[ 15]---> Adder-cost: 2 maxlim: 2046 bits: 12/11 c ---[ 14]---> Adder-cost: 2 maxlim: 2046 bits: 12/11 c ---[ 13]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 12]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 10]---> Adder-cost: 304 maxlim: 2104243 bits: 22/22 c ---[ 9]---> Adder-cost: 2 maxlim: 2046 bits: 12/11 c ---[ 7]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 6]---> Adder-cost: 2 maxlim: 2046 bits: 12/11 c ---[ 5]---> Adder-cost: 2 maxlim: 2046 bits: 12/11 c ---[ 4]---> Adder-cost: 2 maxlim: 2046 bits: 12/11 c ---[ 3]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 1]---> Adder-cost: 2 maxlim: 2046 bits: 12/11 c ---[ 0]---> Adder-cost: 2 maxlim: 2046 bits: 12/11 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 128691 468095 | 42897 0 0 nan | 0.000 % | c | 100 | 128691 468095 | 47186 100 357 3.6 | 19.006 % | c | 251 | 128683 468069 | 51905 250 976 3.9 | 19.010 % | c | 476 | 128675 468043 | 57095 474 3069 6.5 | 19.014 % | c | 813 | 128668 468020 | 62805 810 6251 7.7 | 19.018 % | c | 1319 | 128668 468020 | 69086 1316 15715 11.9 | 19.018 % | c | 2078 | 128661 467997 | 75994 2073 29520 14.2 | 19.022 % | c | 3217 | 128603 467805 | 83594 3206 39935 12.5 | 19.058 % | c | 4925 | 128588 467758 | 91953 4913 69817 14.2 | 19.070 % | c | 7487 | 128581 467734 | 101148 7474 149479 20.0 | 19.074 % | c | 11332 | 128581 467734 | 111263 11319 245675 21.7 | 19.074 % | c | 17099 | 128565 467680 | 122390 17081 382307 22.4 | 19.082 % | c | 25749 | 128534 467577 | 134629 25724 630436 24.5 | 19.101 % | c | 38723 | 128534 467577 | 148092 38698 1131256 29.2 | 19.101 % | c | 58185 | 128534 467577 | 162901 58160 1701459 29.3 | 19.101 % | c | 87378 | 128518 467525 | 179191 87351 2524227 28.9 | 19.113 % | c | 131167 | 128400 467103 | 197110 131096 4443419 33.9 | 19.149 % | c | 196853 | 128385 467058 | 216821 196779 6643770 33.8 | 19.161 % | c | 295379 | 128359 466980 | 238503 92114 2776643 30.1 | 19.181 % | c | 443168 | 128304 466795 | 262354 239893 7191120 30.0 | 19.212 % | #### END SOLVER DATA #### #### BEGIN WATCHER DATA #### Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing VSIZE limit: 943718400 bytes Raw data (loadavg): 0.92 0.95 0.90 2/54 10292 Raw data (stat): 10292 (runsolver) R 10291 29653 29652 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 485158340 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 0 7 90112 0 0 0 17 0 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0014 s] Raw data (loadavg): 0.93 0.96 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 4188 0 0 0 990 9 0 0 25 0 1 0 485158340 19378176 4025 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4731 4025 603 41 0 4690 0 vsize: 18924 [startup+20.0019 s] Raw data (loadavg): 0.94 0.96 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 4821 0 0 0 1988 11 0 0 25 0 1 0 485158340 22052864 4658 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5384 4658 603 41 0 5343 0 vsize: 21536 [startup+30.0021 s] Raw data (loadavg): 0.95 0.96 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 5335 0 0 0 2987 12 0 0 25 0 1 0 485158340 24186880 5172 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5905 5172 603 41 0 5864 0 vsize: 23620 [startup+40.0022 s] Raw data (loadavg): 0.96 0.96 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 5715 0 0 0 3985 14 0 0 25 0 1 0 485158340 25661440 5552 4294967295 134512640 134672761 3221224544 3221223648 134560418 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6265 5552 603 41 0 6224 0 vsize: 25060 [startup+50.0024 s] Raw data (loadavg): 0.96 0.96 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 5967 0 0 0 4985 14 0 0 25 0 1 0 485158340 26996736 5804 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6591 5804 603 41 0 6550 0 vsize: 26364 [startup+60.0025 s] Raw data (loadavg): 0.97 0.96 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 6194 0 0 0 5985 15 0 0 25 0 1 0 485158340 27963392 6031 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6827 6031 603 41 0 6786 0 vsize: 27308 [startup+70.003 s] Raw data (loadavg): 0.97 0.96 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 6377 0 0 0 6984 16 0 0 25 0 1 0 485158340 28647424 6214 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6994 6214 603 41 0 6953 0 vsize: 27976 [startup+80.0038 s] Raw data (loadavg): 0.98 0.96 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 6542 0 0 0 7984 16 0 0 25 0 1 0 485158340 29339648 6379 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7163 6379 603 41 0 7122 0 vsize: 28652 [startup+90.004 s] Raw data (loadavg): 0.98 0.96 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 7042 0 0 0 8983 18 0 0 25 0 1 0 485158340 31354880 6879 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7655 6879 603 41 0 7614 0 vsize: 30620 [startup+100.004 s] Raw data (loadavg): 0.98 0.96 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 7501 0 0 0 9982 19 0 0 25 0 1 0 485158340 33239040 7338 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8115 7338 603 41 0 8074 0 vsize: 32460 [startup+110.004 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 7853 0 0 0 10982 20 0 0 25 0 1 0 485158340 34713600 7690 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8475 7690 603 41 0 8434 0 vsize: 33900 [startup+120.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 8153 0 0 0 11982 21 0 0 25 0 1 0 485158340 35934208 7990 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8773 7990 603 41 0 8732 0 vsize: 35092 [startup+130.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 8459 0 0 0 12983 21 0 0 25 0 1 0 485158340 37175296 8296 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9076 8296 603 41 0 9035 0 vsize: 36304 [startup+140.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 8666 0 0 0 13982 22 0 0 25 0 1 0 485158340 37994496 8503 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9276 8503 603 41 0 9235 0 vsize: 37104 [startup+150.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 8927 0 0 0 14982 23 0 0 25 0 1 0 485158340 39096320 8764 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9545 8764 603 41 0 9504 0 vsize: 38180 [startup+160.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 9230 0 0 0 15981 24 0 0 25 0 1 0 485158340 40964096 9067 4294967295 134512640 134672761 3221224544 3221223744 134557916 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10001 9067 603 41 0 9960 0 vsize: 40004 [startup+170.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 9572 0 0 0 16981 25 0 0 25 0 1 0 485158340 42295296 9409 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10326 9409 603 41 0 10285 0 vsize: 41304 [startup+180.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 9871 0 0 0 17980 26 0 0 25 0 1 0 485158340 43507712 9708 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10622 9708 603 41 0 10581 0 vsize: 42488 [startup+190.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 10133 0 0 0 18980 27 0 0 25 0 1 0 485158340 44617728 9970 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10893 9970 603 41 0 10852 0 vsize: 43572 [startup+200.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 10387 0 0 0 19979 28 0 0 25 0 1 0 485158340 45633536 10224 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11141 10224 603 41 0 11100 0 vsize: 44564 [startup+210.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 10568 0 0 0 20979 28 0 0 25 0 1 0 485158340 46305280 10405 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11305 10405 603 41 0 11264 0 vsize: 45220 [startup+220.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 10718 0 0 0 21979 29 0 0 25 0 1 0 485158340 46977024 10555 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11469 10555 603 41 0 11428 0 vsize: 45876 [startup+230.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 10871 0 0 0 22979 29 0 0 25 0 1 0 485158340 47517696 10708 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11601 10708 603 41 0 11560 0 vsize: 46404 [startup+240.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 11024 0 0 0 23979 30 0 0 25 0 1 0 485158340 48214016 10861 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11771 10861 603 41 0 11730 0 vsize: 47084 [startup+250.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 11156 0 0 0 24980 30 0 0 25 0 1 0 485158340 48750592 10993 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11902 10993 603 41 0 11861 0 vsize: 47608 [startup+260.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 11283 0 0 0 25980 31 0 0 25 0 1 0 485158340 49147904 11120 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11999 11120 603 41 0 11958 0 vsize: 47996 [startup+270.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 11409 0 0 0 26980 31 0 0 25 0 1 0 485158340 49680384 11246 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12129 11246 603 41 0 12088 0 vsize: 48516 [startup+280.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 11524 0 0 0 27980 31 0 0 25 0 1 0 485158340 50216960 11361 4294967295 134512640 134672761 3221224544 3221223728 134559559 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12260 11361 603 41 0 12219 0 vsize: 49040 [startup+290.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 11635 0 0 0 28981 32 0 0 25 0 1 0 485158340 50618368 11472 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12358 11472 603 41 0 12317 0 vsize: 49432 [startup+300.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 11745 0 0 0 29981 32 0 0 25 0 1 0 485158340 51048448 11582 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12463 11582 603 41 0 12422 0 vsize: 49852 [startup+310.078 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 11967 0 0 0 30980 33 0 0 25 0 1 0 485158340 52031488 11804 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12703 11804 603 41 0 12662 0 vsize: 50812 [startup+320.078 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 12221 0 0 0 31980 34 0 0 25 0 1 0 485158340 52977664 12058 4294967295 134512640 134672761 3221224544 3221223712 134561133 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12934 12058 603 41 0 12893 0 vsize: 51736 [startup+330.078 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 12481 0 0 0 32980 34 0 0 25 0 1 0 485158340 54054912 12318 4294967295 134512640 134672761 3221224544 3221223712 134560874 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13197 12318 603 41 0 13156 0 vsize: 52788 [startup+340.086 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 12709 0 0 0 33980 34 0 0 25 0 1 0 485158340 55005184 12546 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13429 12546 603 41 0 13388 0 vsize: 53716 [startup+350.085 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 12880 0 0 0 34980 35 0 0 25 0 1 0 485158340 55693312 12717 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13597 12717 603 41 0 13556 0 vsize: 54388 [startup+360.099 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 12996 0 0 0 35981 36 0 0 25 0 1 0 485158340 56238080 12833 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13730 12833 603 41 0 13689 0 vsize: 54920 [startup+370.099 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13088 0 0 0 36981 36 0 0 25 0 1 0 485158340 56643584 12925 4294967295 134512640 134672761 3221224544 3221223648 134554642 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13829 12925 603 41 0 13788 0 vsize: 55316 [startup+380.099 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13088 0 0 0 37982 36 0 0 25 0 1 0 485158340 56643584 12925 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13829 12925 603 41 0 13788 0 vsize: 55316 [startup+390.099 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13089 0 0 0 38982 36 0 0 25 0 1 0 485158340 56643584 12926 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13829 12926 603 41 0 13788 0 vsize: 55316 [startup+400.099 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13090 0 0 0 39982 36 0 0 25 0 1 0 485158340 56643584 12927 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13829 12927 603 41 0 13788 0 vsize: 55316 [startup+410.099 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13093 0 0 0 40983 36 0 0 25 0 1 0 485158340 56643584 12930 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13829 12930 603 41 0 13788 0 vsize: 55316 [startup+420.099 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13093 0 0 0 41983 36 0 0 25 0 1 0 485158340 56643584 12930 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13829 12930 603 41 0 13788 0 vsize: 55316 [startup+430.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13093 0 0 0 42983 36 0 0 25 0 1 0 485158340 56643584 12930 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13829 12930 603 41 0 13788 0 vsize: 55316 [startup+440.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13093 0 0 0 43984 36 0 0 25 0 1 0 485158340 56643584 12930 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13829 12930 603 41 0 13788 0 vsize: 55316 [startup+450.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13093 0 0 0 44984 36 0 0 25 0 1 0 485158340 56643584 12930 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13829 12930 603 41 0 13788 0 vsize: 55316 [startup+460.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13093 0 0 0 45984 36 0 0 25 0 1 0 485158340 56643584 12930 4294967295 134512640 134672761 3221224544 3221223712 134560874 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13829 12930 603 41 0 13788 0 vsize: 55316 [startup+470.103 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13093 0 0 0 46985 36 0 0 25 0 1 0 485158340 56643584 12930 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13829 12930 603 41 0 13788 0 vsize: 55316 [startup+480.103 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13095 0 0 0 47985 36 0 0 25 0 1 0 485158340 56643584 12932 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13829 12932 603 41 0 13788 0 vsize: 55316 [startup+490.109 s] Raw data (loadavg): 1.07 0.99 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13095 0 0 0 48986 36 0 0 25 0 1 0 485158340 56643584 12932 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13829 12932 603 41 0 13788 0 vsize: 55316 [startup+500.116 s] Raw data (loadavg): 1.06 0.99 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13095 0 0 0 49987 36 0 0 25 0 1 0 485158340 56643584 12932 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13829 12932 603 41 0 13788 0 vsize: 55316 [startup+510.127 s] Raw data (loadavg): 1.05 0.99 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13097 0 0 0 50988 36 0 0 25 0 1 0 485158340 56643584 12934 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13829 12934 603 41 0 13788 0 vsize: 55316 [startup+520.127 s] Raw data (loadavg): 1.04 0.99 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13097 0 0 0 51989 36 0 0 25 0 1 0 485158340 56643584 12934 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13829 12934 603 41 0 13788 0 vsize: 55316 [startup+530.127 s] Raw data (loadavg): 1.04 0.99 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13098 0 0 0 52989 36 0 0 25 0 1 0 485158340 56643584 12935 4294967295 134512640 134672761 3221224544 3221223712 134560906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13829 12935 603 41 0 13788 0 vsize: 55316 [startup+540.127 s] Raw data (loadavg): 1.03 0.99 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13098 0 0 0 53989 36 0 0 25 0 1 0 485158340 56643584 12935 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13829 12935 603 41 0 13788 0 vsize: 55316 [startup+550.134 s] Raw data (loadavg): 1.03 0.99 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13116 0 0 0 54990 36 0 0 25 0 1 0 485158340 56844288 12953 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13878 12953 603 41 0 13837 0 vsize: 55512 [startup+560.134 s] Raw data (loadavg): 1.02 0.99 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13116 0 0 0 55991 36 0 0 25 0 1 0 485158340 56844288 12953 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13878 12953 603 41 0 13837 0 vsize: 55512 [startup+570.134 s] Raw data (loadavg): 1.02 0.99 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13136 0 0 0 56991 36 0 0 25 0 1 0 485158340 56844288 12973 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13878 12973 603 41 0 13837 0 vsize: 55512 [startup+580.134 s] Raw data (loadavg): 1.01 0.99 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13139 0 0 0 57991 36 0 0 25 0 1 0 485158340 56844288 12976 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13878 12976 603 41 0 13837 0 vsize: 55512 [startup+590.134 s] Raw data (loadavg): 1.01 0.99 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13139 0 0 0 58992 36 0 0 25 0 1 0 485158340 56844288 12976 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13878 12976 603 41 0 13837 0 vsize: 55512 [startup+600.134 s] Raw data (loadavg): 1.01 0.99 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13139 0 0 0 59992 36 0 0 25 0 1 0 485158340 56844288 12976 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13878 12976 603 41 0 13837 0 vsize: 55512 [startup+610.135 s] Raw data (loadavg): 1.01 0.99 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13139 0 0 0 60992 36 0 0 25 0 1 0 485158340 56844288 12976 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13878 12976 603 41 0 13837 0 vsize: 55512 [startup+620.134 s] Raw data (loadavg): 1.01 0.99 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13157 0 0 0 61993 36 0 0 25 0 1 0 485158340 57106432 12994 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13942 12994 603 41 0 13901 0 vsize: 55768 [startup+630.135 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13158 0 0 0 62993 36 0 0 25 0 1 0 485158340 57106432 12995 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13942 12995 603 41 0 13901 0 vsize: 55768 [startup+640.135 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13159 0 0 0 63993 36 0 0 25 0 1 0 485158340 57106432 12996 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13942 12996 603 41 0 13901 0 vsize: 55768 [startup+650.135 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13165 0 0 0 64994 36 0 0 25 0 1 0 485158340 57106432 13002 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13942 13002 603 41 0 13901 0 vsize: 55768 [startup+660.135 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13182 0 0 0 65994 36 0 0 25 0 1 0 485158340 57106432 13019 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13942 13019 603 41 0 13901 0 vsize: 55768 [startup+670.141 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13185 0 0 0 66995 36 0 0 25 0 1 0 485158340 57106432 13022 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13942 13022 603 41 0 13901 0 vsize: 55768 [startup+680.141 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13186 0 0 0 67995 36 0 0 25 0 1 0 485158340 57106432 13023 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13942 13023 603 41 0 13901 0 vsize: 55768 [startup+690.146 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13187 0 0 0 68996 36 0 0 25 0 1 0 485158340 57106432 13024 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13942 13024 603 41 0 13901 0 vsize: 55768 [startup+700.146 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13188 0 0 0 69996 36 0 0 25 0 1 0 485158340 57106432 13025 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13942 13025 603 41 0 13901 0 vsize: 55768 [startup+710.146 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13235 0 0 0 70997 36 0 0 25 0 1 0 485158340 57368576 13072 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14006 13072 603 41 0 13965 0 vsize: 56024 [startup+720.153 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13242 0 0 0 71998 36 0 0 25 0 1 0 485158340 57368576 13079 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14006 13079 603 41 0 13965 0 vsize: 56024 [startup+730.16 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13243 0 0 0 72999 36 0 0 25 0 1 0 485158340 57368576 13080 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14006 13080 603 41 0 13965 0 vsize: 56024 [startup+740.16 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13264 0 0 0 73999 36 0 0 25 0 1 0 485158340 57630720 13101 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14070 13101 603 41 0 14029 0 vsize: 56280 [startup+750.16 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13272 0 0 0 74999 36 0 0 25 0 1 0 485158340 57630720 13109 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14070 13109 603 41 0 14029 0 vsize: 56280 [startup+760.161 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13307 0 0 0 76000 36 0 0 25 0 1 0 485158340 57892864 13144 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14134 13144 603 41 0 14093 0 vsize: 56536 [startup+770.162 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13308 0 0 0 77000 36 0 0 25 0 1 0 485158340 57892864 13145 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14134 13145 603 41 0 14093 0 vsize: 56536 [startup+780.162 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13309 0 0 0 78000 36 0 0 25 0 1 0 485158340 57892864 13146 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14134 13146 603 41 0 14093 0 vsize: 56536 [startup+790.168 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13373 0 0 0 79001 37 0 0 25 0 1 0 485158340 58089472 13210 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14182 13210 603 41 0 14141 0 vsize: 56728 [startup+800.176 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13379 0 0 0 80002 37 0 0 25 0 1 0 485158340 58089472 13216 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14182 13216 603 41 0 14141 0 vsize: 56728 [startup+810.176 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13381 0 0 0 81003 37 0 0 25 0 1 0 485158340 58089472 13218 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14182 13218 603 41 0 14141 0 vsize: 56728 [startup+820.176 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13382 0 0 0 82003 37 0 0 25 0 1 0 485158340 58089472 13219 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14182 13219 603 41 0 14141 0 vsize: 56728 [startup+830.176 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13382 0 0 0 83003 37 0 0 25 0 1 0 485158340 58089472 13219 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14182 13219 603 41 0 14141 0 vsize: 56728 [startup+840.183 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13385 0 0 0 84004 37 0 0 25 0 1 0 485158340 58089472 13222 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14182 13222 603 41 0 14141 0 vsize: 56728 [startup+850.183 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13386 0 0 0 85005 37 0 0 25 0 1 0 485158340 58089472 13223 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14182 13223 603 41 0 14141 0 vsize: 56728 [startup+860.183 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13386 0 0 0 86005 37 0 0 25 0 1 0 485158340 58089472 13223 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14182 13223 603 41 0 14141 0 vsize: 56728 [startup+870.185 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13386 0 0 0 87005 37 0 0 25 0 1 0 485158340 58089472 13223 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14182 13223 603 41 0 14141 0 vsize: 56728 [startup+880.186 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13386 0 0 0 88006 37 0 0 25 0 1 0 485158340 58089472 13223 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14182 13223 603 41 0 14141 0 vsize: 56728 [startup+890.185 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13386 0 0 0 89006 37 0 0 25 0 1 0 485158340 58089472 13223 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14182 13223 603 41 0 14141 0 vsize: 56728 [startup+900.185 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 10292 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13395 0 0 0 90007 37 0 0 25 0 1 0 485158340 58286080 13232 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14230 13232 603 41 0 14189 0 vsize: 56920 [startup+910.187 s] Raw data (loadavg): 1.15 1.02 0.93 3/57 10328 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13395 0 0 0 91006 37 0 0 25 0 1 0 485158340 58286080 13232 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14230 13232 603 41 0 14189 0 vsize: 56920 [startup+920.187 s] Raw data (loadavg): 1.13 1.02 0.93 2/54 10345 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13395 0 0 0 92006 37 0 0 25 0 1 0 485158340 58286080 13232 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14230 13232 603 41 0 14189 0 vsize: 56920 [startup+930.187 s] Raw data (loadavg): 1.11 1.02 0.93 2/54 10345 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13409 0 0 0 93007 37 0 0 25 0 1 0 485158340 58286080 13246 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14230 13246 603 41 0 14189 0 vsize: 56920 [startup+940.188 s] Raw data (loadavg): 1.09 1.02 0.93 2/54 10345 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13411 0 0 0 94007 37 0 0 25 0 1 0 485158340 58286080 13248 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14230 13248 603 41 0 14189 0 vsize: 56920 [startup+950.188 s] Raw data (loadavg): 1.08 1.02 0.93 2/54 10345 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13411 0 0 0 95007 38 0 0 25 0 1 0 485158340 58286080 13248 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14230 13248 603 41 0 14189 0 vsize: 56920 [startup+960.189 s] Raw data (loadavg): 1.06 1.02 0.93 2/54 10345 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13411 0 0 0 96007 38 0 0 25 0 1 0 485158340 58286080 13248 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14230 13248 603 41 0 14189 0 vsize: 56920 [startup+970.196 s] Raw data (loadavg): 1.05 1.01 0.93 2/54 10345 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13413 0 0 0 97008 38 0 0 25 0 1 0 485158340 58286080 13250 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14230 13250 603 41 0 14189 0 vsize: 56920 [startup+980.203 s] Raw data (loadavg): 1.05 1.01 0.93 2/54 10345 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13415 0 0 0 98009 38 0 0 25 0 1 0 485158340 58286080 13252 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14230 13252 603 41 0 14189 0 vsize: 56920 [startup+990.207 s] Raw data (loadavg): 1.04 1.01 0.93 2/54 10347 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13415 0 0 0 99010 38 0 0 25 0 1 0 485158340 58286080 13252 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14230 13252 603 41 0 14189 0 vsize: 56920 [startup+1000.21 s] Raw data (loadavg): 1.03 1.01 0.93 2/54 10347 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13457 0 0 0 100010 38 0 0 25 0 1 0 485158340 58482688 13294 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14278 13294 603 41 0 14237 0 vsize: 57112 [startup+1010.21 s] Raw data (loadavg): 1.03 1.01 0.93 2/54 10347 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13459 0 0 0 101010 38 0 0 25 0 1 0 485158340 58482688 13296 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14278 13296 603 41 0 14237 0 vsize: 57112 [startup+1020.21 s] Raw data (loadavg): 1.02 1.01 0.93 2/54 10347 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13461 0 0 0 102011 38 0 0 25 0 1 0 485158340 58482688 13298 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14278 13298 603 41 0 14237 0 vsize: 57112 [startup+1030.21 s] Raw data (loadavg): 1.02 1.01 0.93 2/54 10347 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13463 0 0 0 103011 38 0 0 25 0 1 0 485158340 58482688 13300 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14278 13300 603 41 0 14237 0 vsize: 57112 [startup+1040.21 s] Raw data (loadavg): 1.02 1.01 0.93 2/54 10347 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13464 0 0 0 104011 38 0 0 25 0 1 0 485158340 58482688 13301 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14278 13301 603 41 0 14237 0 vsize: 57112 [startup+1050.21 s] Raw data (loadavg): 1.01 1.01 0.93 2/54 10347 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13487 0 0 0 105012 38 0 0 25 0 1 0 485158340 58744832 13324 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14342 13324 603 41 0 14301 0 vsize: 57368 [startup+1060.21 s] Raw data (loadavg): 1.01 1.01 0.93 2/54 10347 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13489 0 0 0 106012 38 0 0 25 0 1 0 485158340 58744832 13326 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14342 13326 603 41 0 14301 0 vsize: 57368 [startup+1070.21 s] Raw data (loadavg): 1.01 1.00 0.93 2/54 10347 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13491 0 0 0 107012 38 0 0 25 0 1 0 485158340 58744832 13328 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14342 13328 603 41 0 14301 0 vsize: 57368 [startup+1080.21 s] Raw data (loadavg): 1.01 1.00 0.93 2/54 10347 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13492 0 0 0 108013 38 0 0 25 0 1 0 485158340 58744832 13329 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14342 13329 603 41 0 14301 0 vsize: 57368 [startup+1090.21 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 10347 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13495 0 0 0 109013 38 0 0 25 0 1 0 485158340 58744832 13332 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14342 13332 603 41 0 14301 0 vsize: 57368 [startup+1100.21 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 10347 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13497 0 0 0 110013 38 0 0 25 0 1 0 485158340 58744832 13334 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14342 13334 603 41 0 14301 0 vsize: 57368 [startup+1110.21 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 10347 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13532 0 0 0 111014 38 0 0 25 0 1 0 485158340 59006976 13369 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14406 13369 603 41 0 14365 0 vsize: 57624 [startup+1120.21 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 10347 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13534 0 0 0 112014 38 0 0 25 0 1 0 485158340 59006976 13371 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14406 13371 603 41 0 14365 0 vsize: 57624 [startup+1130.21 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 10347 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13630 0 0 0 113014 38 0 0 25 0 1 0 485158340 59498496 13467 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14526 13467 603 41 0 14485 0 vsize: 58104 [startup+1140.21 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 10347 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13664 0 0 0 114014 38 0 0 25 0 1 0 485158340 59691008 13501 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14573 13501 603 41 0 14532 0 vsize: 58292 [startup+1150.21 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 10347 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13724 0 0 0 115014 39 0 0 25 0 1 0 485158340 59977728 13561 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14643 13561 603 41 0 14602 0 vsize: 58572 [startup+1160.21 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 10347 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13779 0 0 0 116014 39 0 0 25 0 1 0 485158340 60112896 13616 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14676 13616 603 41 0 14635 0 vsize: 58704 [startup+1170.21 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 10347 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13837 0 0 0 117014 39 0 0 25 0 1 0 485158340 60375040 13674 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14740 13674 603 41 0 14699 0 vsize: 58960 [startup+1180.21 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 10347 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13907 0 0 0 118014 39 0 0 25 0 1 0 485158340 60641280 13744 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14805 13744 603 41 0 14764 0 vsize: 59220 [startup+1190.21 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 10347 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 13961 0 0 0 119015 39 0 0 25 0 1 0 485158340 60903424 13798 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14869 13798 603 41 0 14828 0 vsize: 59476 [startup+1200.21 s] Raw data (loadavg): 1.00 1.00 0.93 2/54 10347 Raw data (stat): 10292 (minisat+) R 10291 29653 29652 0 -1 0 14014 0 0 0 120014 40 0 0 25 0 1 0 485158340 61034496 13851 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14901 13851 603 41 0 14860 0 vsize: 59604 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.24 s] Raw data (loadavg): 1.00 1.00 0.93 1/54 10347 Raw data (stat): 10292 (minisat+) Z 10291 29653 29652 0 -1 12 14016 0 0 0 120014 42 0 0 25 0 1 0 485158340 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0 Raw data (statm): 0 0 0 0 0 0 0 vsize: 0 Maximum CPU time exceeded: sending SIGTERM and SIGKILL Child status: 0 Real time (s): 1200.24 CPU time (s): 1200.58 CPU user time (s): 1200.15 CPU system time (s): 0.429934 CPU usage (%): 100.028 Max. virtual memory (Kb): 59604 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####