Name | normalized-opb/mps-v2-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-vpm2.opb |
MD5SUM | 8c44064d4224b1d41c28f152218dd39f |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 98 |
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 | 102400 |
Number of bits of the biggest number in a constraint | 17 |
Biggest sum of numbers in a constraint | 615983 |
Number of bits of the biggest sum of numbers | 20 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1.05084 |
Number of variables | 2124 |
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 | 64 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc4 THE 2005-04-21 14:42:19 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=18132 boxname=wulflinc4 idbench=1395 idsolver=10 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 8c44064d4224b1d41c28f152218dd39f /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-13-7-vpm2.opb REAL COMMAND: minisat+ -ca /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-13-7-vpm2.opb /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-13-7-vpm2.opb IDLAUNCH: 18132 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.169 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 : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.169 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: 838596 kB Buffers: 21600 kB Cached: 153204 kB SwapCached: 364 kB Active: 13536 kB Inactive: 163716 kB HighTotal: 131008 kB HighFree: 113848 kB LowTotal: 903652 kB LowFree: 724748 kB SwapTotal: 2097136 kB SwapFree: 2096356 kB Dirty: 40 kB Writeback: 0 kB Mapped: 6388 kB Slab: 13160 kB Committed_AS: 71676 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1388 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-04-21 15:02:22 (client local time) WITH STATUS 0 IN 1200.42 SECONDS stats: 18132 7 1200.42 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: 14 maxlim: 126 bits: 8/7 c ---[ 484]---> Adder-cost: 14 maxlim: 126 bits: 8/7 c ---[ 483]---> Adder-cost: 14 maxlim: 126 bits: 8/7 c ---[ 482]---> Adder-cost: 14 maxlim: 126 bits: 8/7 c ---[ 481]---> Adder-cost: 14 maxlim: 126 bits: 8/7 c ---[ 480]---> Adder-cost: 14 maxlim: 126 bits: 8/7 c ---[ 479]---> Adder-cost: 14 maxlim: 126 bits: 8/7 c ---[ 478]---> Adder-cost: 14 maxlim: 126 bits: 8/7 c ---[ 477]---> Adder-cost: 14 maxlim: 126 bits: 8/7 c ---[ 474]---> Adder-cost: 14 maxlim: 126 bits: 8/7 c ---[ 473]---> Adder-cost: 14 maxlim: 126 bits: 8/7 c ---[ 472]---> Adder-cost: 14 maxlim: 126 bits: 8/7 c ---[ 471]---> Adder-cost: 14 maxlim: 126 bits: 8/7 c ---[ 468]---> Adder-cost: 14 maxlim: 126 bits: 8/7 c ---[ 467]---> Adder-cost: 14 maxlim: 126 bits: 8/7 c ---[ 466]---> Adder-cost: 14 maxlim: 126 bits: 8/7 c ---[ 465]---> Adder-cost: 14 maxlim: 126 bits: 8/7 c ---[ 462]---> Adder-cost: 14 maxlim: 126 bits: 8/7 c ---[ 459]---> Adder-cost: 14 maxlim: 126 bits: 8/7 c ---[ 458]---> Adder-cost: 14 maxlim: 126 bits: 8/7 c ---[ 457]---> Adder-cost: 14 maxlim: 126 bits: 8/7 c ---[ 454]---> Adder-cost: 14 maxlim: 126 bits: 8/7 c ---[ 453]---> Adder-cost: 14 maxlim: 126 bits: 8/7 c ---[ 452]---> Adder-cost: 14 maxlim: 126 bits: 8/7 c ---[ 451]---> Adder-cost: 14 maxlim: 126 bits: 8/7 c ---[ 450]---> Adder-cost: 14 maxlim: 126 bits: 8/7 c ---[ 448]---> Adder-cost: 14 maxlim: 126 bits: 8/7 c ---[ 447]---> Adder-cost: 14 maxlim: 126 bits: 8/7 c ---[ 446]---> Adder-cost: 14 maxlim: 126 bits: 8/7 c ---[ 445]---> Adder-cost: 14 maxlim: 126 bits: 8/7 c ---[ 444]---> Adder-cost: 14 maxlim: 126 bits: 8/7 c ---[ 441]---> Adder-cost: 14 maxlim: 126 bits: 8/7 c ---[ 440]---> Adder-cost: 14 maxlim: 126 bits: 8/7 c ---[ 439]---> Adder-cost: 14 maxlim: 126 bits: 8/7 c ---[ 433]---> Adder-cost: 14 maxlim: 126 bits: 8/7 c ---[ 427]---> Adder-cost: 14 maxlim: 126 bits: 8/7 c ---[ 422]---> Adder-cost: 14 maxlim: 126 bits: 8/7 c ---[ 421]---> Adder-cost: 14 maxlim: 126 bits: 8/7 c ---[ 415]---> Adder-cost: 14 maxlim: 126 bits: 8/7 c ---[ 409]---> Adder-cost: 14 maxlim: 126 bits: 8/7 c ---[ 408]---> Adder-cost: 14 maxlim: 126 bits: 8/7 c ---[ 402]---> Adder-cost: 14 maxlim: 126 bits: 8/7 c ---[ 397]---> Adder-cost: 14 maxlim: 126 bits: 8/7 c ---[ 396]---> Adder-cost: 14 maxlim: 126 bits: 8/7 c ---[ 391]---> Adder-cost: 14 maxlim: 126 bits: 8/7 c ---[ 390]---> Adder-cost: 14 maxlim: 126 bits: 8/7 c ---[ 386]---> Adder-cost: 14 maxlim: 126 bits: 8/7 c ---[ 385]---> Adder-cost: 14 maxlim: 126 bits: 8/7 c ---[ 384]---> Adder-cost: 14 maxlim: 126 bits: 8/7 c ---[ 380]---> Adder-cost: 14 maxlim: 126 bits: 8/7 c ---[ 379]---> Adder-cost: 14 maxlim: 126 bits: 8/7 c ---[ 378]---> Adder-cost: 14 maxlim: 126 bits: 8/7 c ---[ 374]---> Adder-cost: 14 maxlim: 126 bits: 8/7 c ---[ 373]---> Adder-cost: 14 maxlim: 126 bits: 8/7 c ---[ 372]---> Adder-cost: 14 maxlim: 126 bits: 8/7 c ---[ 368]---> Adder-cost: 14 maxlim: 126 bits: 8/7 c ---[ 367]---> Adder-cost: 14 maxlim: 126 bits: 8/7 c ---[ 366]---> Adder-cost: 14 maxlim: 126 bits: 8/7 c ---[ 365]---> Adder-cost: 14 maxlim: 126 bits: 8/7 c ---[ 364]---> Adder-cost: 14 maxlim: 126 bits: 8/7 c ---[ 359]---> Adder-cost: 14 maxlim: 126 bits: 8/7 c ---[ 353]---> Adder-cost: 14 maxlim: 126 bits: 8/7 c ---[ 347]---> Adder-cost: 14 maxlim: 126 bits: 8/7 c ---[ 339]---> Adder-cost: 14 maxlim: 126 bits: 8/7 c ---[ 333]---> Adder-cost: 14 maxlim: 126 bits: 8/7 c ---[ 327]---> Adder-cost: 14 maxlim: 126 bits: 8/7 c ---[ 321]---> Adder-cost: 14 maxlim: 126 bits: 8/7 c ---[ 317]---> Adder-cost: 49 maxlim: 7166 bits: 14/13 c ---[ 316]---> Adder-cost: 49 maxlim: 7166 bits: 14/13 c ---[ 315]---> Adder-cost: 49 maxlim: 7166 bits: 14/13 c ---[ 314]---> Adder-cost: 49 maxlim: 7166 bits: 14/13 c ---[ 313]---> Adder-cost: 49 maxlim: 7166 bits: 14/13 c ---[ 312]---> Adder-cost: 49 maxlim: 7166 bits: 14/13 c ---[ 310]---> Adder-cost: 49 maxlim: 7166 bits: 14/13 c ---[ 309]---> Adder-cost: 49 maxlim: 7166 bits: 14/13 c ---[ 308]---> Adder-cost: 49 maxlim: 7166 bits: 14/13 c ---[ 307]---> Adder-cost: 49 maxlim: 7166 bits: 14/13 c ---[ 306]---> Adder-cost: 49 maxlim: 7166 bits: 14/13 c ---[ 302]---> Adder-cost: 45 maxlim: 3582 bits: 13/12 c ---[ 301]---> Adder-cost: 45 maxlim: 3582 bits: 13/12 c ---[ 300]---> Adder-cost: 45 maxlim: 3582 bits: 13/12 c ---[ 295]---> Adder-cost: 45 maxlim: 3582 bits: 13/12 c ---[ 294]---> Adder-cost: 45 maxlim: 3582 bits: 13/12 c ---[ 290]---> Adder-cost: 30 maxlim: 27134 bits: 16/15 c ---[ 289]---> Adder-cost: 30 maxlim: 27134 bits: 16/15 c ---[ 288]---> Adder-cost: 30 maxlim: 27134 bits: 16/15 c ---[ 287]---> Adder-cost: 45 maxlim: 3582 bits: 13/12 c ---[ 286]---> Adder-cost: 45 maxlim: 3582 bits: 13/12 c ---[ 285]---> Adder-cost: 45 maxlim: 3582 bits: 13/12 c ---[ 284]---> Adder-cost: 45 maxlim: 3582 bits: 13/12 c ---[ 283]---> Adder-cost: 45 maxlim: 3582 bits: 13/12 c ---[ 282]---> Adder-cost: 45 maxlim: 3582 bits: 13/12 c ---[ 280]---> Adder-cost: 45 maxlim: 3582 bits: 13/12 c ---[ 279]---> Adder-cost: 45 maxlim: 3582 bits: 13/12 c ---[ 278]---> Adder-cost: 45 maxlim: 3582 bits: 13/12 c ---[ 277]---> Adder-cost: 45 maxlim: 3582 bits: 13/12 c ---[ 276]---> Adder-cost: 45 maxlim: 3582 bits: 13/12 c ---[ 274]---> Adder-cost: 262 maxlim: 300367 bits: 19/19 c ---[ 272]---> Adder-cost: 208 maxlim: 210867 bits: 18/18 c ---[ 271]---> Adder-cost: 2 maxlim: 254 bits: 9/8 c ---[ 270]---> Adder-cost: 2 maxlim: 254 bits: 9/8 c ---[ 269]---> Adder-cost: 2 maxlim: 254 bits: 9/8 c ---[ 267]---> Adder-cost: 2 maxlim: 254 bits: 9/8 c ---[ 266]---> Adder-cost: 2 maxlim: 254 bits: 9/8 c ---[ 265]---> Adder-cost: 2 maxlim: 254 bits: 9/8 c ---[ 264]---> Adder-cost: 2 maxlim: 254 bits: 9/8 c ---[ 263]---> Adder-cost: 2 maxlim: 254 bits: 9/8 c ---[ 259]---> Adder-cost: 0 maxlim: 126 bits: 8/7 c ---[ 258]---> Adder-cost: 2 maxlim: 254 bits: 9/8 c ---[ 257]---> Adder-cost: 2 maxlim: 254 bits: 9/8 c ---[ 256]---> Adder-cost: 2 maxlim: 254 bits: 9/8 c ---[ 255]---> Adder-cost: 14 maxlim: 126 bits: 8/7 c ---[ 251]---> Adder-cost: 0 maxlim: 126 bits: 8/7 c ---[ 250]---> Adder-cost: 2 maxlim: 254 bits: 9/8 c ---[ 247]---> Adder-cost: 0 maxlim: 62 bits: 7/6 c ---[ 243]---> Adder-cost: 0 maxlim: 126 bits: 8/7 c ---[ 242]---> Adder-cost: 2 maxlim: 254 bits: 9/8 c ---[ 241]---> Adder-cost: 0 maxlim: 62 bits: 7/6 c ---[ 236]---> Adder-cost: 196 maxlim: 203300 bits: 18/18 c ---[ 235]---> Adder-cost: 2 maxlim: 254 bits: 9/8 c ---[ 234]---> Adder-cost: 2 maxlim: 254 bits: 9/8 c ---[ 233]---> Adder-cost: 0 maxlim: 62 bits: 7/6 c ---[ 229]---> Adder-cost: 0 maxlim: 126 bits: 8/7 c ---[ 228]---> Adder-cost: 2 maxlim: 254 bits: 9/8 c ---[ 227]---> Adder-cost: 0 maxlim: 62 bits: 7/6 c ---[ 224]---> Adder-cost: 232 maxlim: 322083 bits: 19/19 c ---[ 220]---> Adder-cost: 2 maxlim: 254 bits: 9/8 c ---[ 219]---> Adder-cost: 2 maxlim: 254 bits: 9/8 c ---[ 214]---> Adder-cost: 0 maxlim: 126 bits: 8/7 c ---[ 212]---> Adder-cost: 180 maxlim: 110883 bits: 17/17 c ---[ 211]---> Adder-cost: 2 maxlim: 254 bits: 9/8 c ---[ 206]---> Adder-cost: 2 maxlim: 254 bits: 9/8 c ---[ 205]---> Adder-cost: 2 maxlim: 254 bits: 9/8 c ---[ 198]---> Adder-cost: 2 maxlim: 254 bits: 9/8 c ---[ 197]---> Adder-cost: 2 maxlim: 254 bits: 9/8 c ---[ 193]---> Adder-cost: 2 maxlim: 254 bits: 9/8 c ---[ 192]---> Adder-cost: 2 maxlim: 254 bits: 9/8 c ---[ 191]---> Adder-cost: 2 maxlim: 254 bits: 9/8 c ---[ 185]---> Adder-cost: 2 maxlim: 254 bits: 9/8 c ---[ 184]---> Adder-cost: 2 maxlim: 254 bits: 9/8 c ---[ 183]---> Adder-cost: 2 maxlim: 254 bits: 9/8 c ---[ 179]---> Adder-cost: 2 maxlim: 254 bits: 9/8 c ---[ 178]---> Adder-cost: 2 maxlim: 254 bits: 9/8 c ---[ 175]---> Adder-cost: 2 maxlim: 254 bits: 9/8 c ---[ 171]---> Adder-cost: 2 maxlim: 254 bits: 9/8 c ---[ 170]---> Adder-cost: 2 maxlim: 254 bits: 9/8 c ---[ 169]---> Adder-cost: 2 maxlim: 254 bits: 9/8 c ---[ 168]---> Adder-cost: 2 maxlim: 254 bits: 9/8 c ---[ 167]---> Adder-cost: 2 maxlim: 254 bits: 9/8 c ---[ 166]---> Adder-cost: 0 maxlim: 62 bits: 7/6 c ---[ 164]---> Adder-cost: 228 maxlim: 229200 bits: 19/18 c ---[ 163]---> Adder-cost: 0 maxlim: 62 bits: 7/6 c ---[ 162]---> Adder-cost: 0 maxlim: 62 bits: 7/6 c ---[ 161]---> Adder-cost: 0 maxlim: 62 bits: 7/6 c ---[ 160]---> Adder-cost: 2 maxlim: 254 bits: 9/8 c ---[ 159]---> Adder-cost: 0 maxlim: 126 bits: 8/7 c ---[ 158]---> Adder-cost: 0 maxlim: 62 bits: 7/6 c ---[ 157]---> Adder-cost: 0 maxlim: 62 bits: 7/6 c ---[ 156]---> Adder-cost: 0 maxlim: 62 bits: 7/6 c ---[ 155]---> Adder-cost: 0 maxlim: 62 bits: 7/6 c ---[ 154]---> Adder-cost: 2 maxlim: 254 bits: 9/8 c ---[ 152]---> Adder-cost: 262 maxlim: 300367 bits: 19/19 c ---[ 150]---> Adder-cost: 260 maxlim: 219983 bits: 19/18 c ---[ 149]---> Adder-cost: 0 maxlim: 126 bits: 8/7 c ---[ 148]---> Adder-cost: 0 maxlim: 30 bits: 6/5 c ---[ 147]---> Adder-cost: 0 maxlim: 30 bits: 6/5 c ---[ 146]---> Adder-cost: 0 maxlim: 30 bits: 6/5 c ---[ 145]---> Adder-cost: 0 maxlim: 30 bits: 6/5 c ---[ 144]---> Adder-cost: 2 maxlim: 254 bits: 9/8 c ---[ 143]---> Adder-cost: 0 maxlim: 126 bits: 8/7 c ---[ 142]---> Adder-cost: 0 maxlim: 30 bits: 6/5 c ---[ 141]---> Adder-cost: 0 maxlim: 30 bits: 6/5 c ---[ 140]---> Adder-cost: 0 maxlim: 30 bits: 6/5 c ---[ 137]---> Adder-cost: 0 maxlim: 30 bits: 6/5 c ---[ 135]---> Adder-cost: 0 maxlim: 126 bits: 8/7 c ---[ 134]---> Adder-cost: 2 maxlim: 254 bits: 9/8 c ---[ 133]---> Adder-cost: 0 maxlim: 62 bits: 7/6 c ---[ 132]---> Adder-cost: 0 maxlim: 62 bits: 7/6 c ---[ 131]---> Adder-cost: 0 maxlim: 62 bits: 7/6 c ---[ 129]---> Adder-cost: 0 maxlim: 126 bits: 8/7 c ---[ 128]---> Adder-cost: 2 maxlim: 254 bits: 9/8 c ---[ 125]---> Adder-cost: 0 maxlim: 62 bits: 7/6 c ---[ 124]---> Adder-cost: 0 maxlim: 62 bits: 7/6 c ---[ 123]---> Adder-cost: 0 maxlim: 62 bits: 7/6 c ---[ 121]---> Adder-cost: 0 maxlim: 126 bits: 8/7 c ---[ 120]---> Adder-cost: 2 maxlim: 254 bits: 9/8 c ---[ 119]---> Adder-cost: 0 maxlim: 62 bits: 7/6 c ---[ 118]---> Adder-cost: 0 maxlim: 62 bits: 7/6 c ---[ 117]---> Adder-cost: 0 maxlim: 62 bits: 7/6 c ---[ 114]---> Adder-cost: 202 maxlim: 152900 bits: 18/18 c ---[ 113]---> Adder-cost: 0 maxlim: 126 bits: 8/7 c ---[ 112]---> Adder-cost: 2 maxlim: 254 bits: 9/8 c ---[ 111]---> Adder-cost: 0 maxlim: 30 bits: 6/5 c ---[ 110]---> Adder-cost: 0 maxlim: 30 bits: 6/5 c ---[ 109]---> Adder-cost: 0 maxlim: 30 bits: 6/5 c ---[ 107]---> Adder-cost: 234 maxlim: 244035 bits: 19/18 c ---[ 105]---> Adder-cost: 234 maxlim: 231235 bits: 19/18 c ---[ 103]---> Adder-cost: 278 maxlim: 283183 bits: 19/19 c ---[ 101]---> Adder-cost: 222 maxlim: 103983 bits: 17/17 c ---[ 99]---> Adder-cost: 222 maxlim: 103983 bits: 17/17 c ---[ 97]---> Adder-cost: 222 maxlim: 103983 bits: 17/17 c ---[ 95]---> Adder-cost: 238 maxlim: 210767 bits: 18/18 c ---[ 93]---> Adder-cost: 222 maxlim: 103983 bits: 17/17 c ---[ 91]---> Adder-cost: 280 maxlim: 228400 bits: 19/18 c ---[ 89]---> Adder-cost: 332 maxlim: 462383 bits: 20/19 c ---[ 87]---> Adder-cost: 254 maxlim: 123183 bits: 18/17 c ---[ 85]---> Adder-cost: 254 maxlim: 123183 bits: 18/17 c ---[ 83]---> Adder-cost: 254 maxlim: 123183 bits: 18/17 c ---[ 81]---> Adder-cost: 232 maxlim: 267600 bits: 19/19 c ---[ 73]---> Adder-cost: 238 maxlim: 210767 bits: 18/18 c ---[ 69]---> Adder-cost: 288 maxlim: 420400 bits: 20/19 c ---[ 66]---> Adder-cost: 200 maxlim: 50101 bits: 17/16 c ---[ 65]---> Adder-cost: 328 maxlim: 81851 bits: 17/17 c ---[ 64]---> Adder-cost: 326 maxlim: 89851 bits: 17/17 c ---[ 63]---> Adder-cost: 396 maxlim: 113601 bits: 17/17 c ---[ 62]---> Adder-cost: 530 maxlim: 161476 bits: 18/18 c ---[ 61]---> Adder-cost: 508 maxlim: 121476 bits: 18/17 c ---[ 60]---> Adder-cost: 64 maxlim: 2133 bits: 12/12 c ---[ 58]---> Adder-cost: 262 maxlim: 261967 bits: 19/18 c ---[ 57]---> Adder-cost: 114 maxlim: 3403 bits: 12/12 c ---[ 56]---> Adder-cost: 122 maxlim: 3723 bits: 13/12 c ---[ 55]---> Adder-cost: 156 maxlim: 4033 bits: 13/12 c ---[ 54]---> Adder-cost: 186 maxlim: 5308 bits: 13/13 c ---[ 53]---> Adder-cost: 188 maxlim: 5628 bits: 13/13 c ---[ 52]---> Adder-cost: 62 maxlim: 2357 bits: 12/12 c ---[ 51]---> Adder-cost: 120 maxlim: 3627 bits: 13/12 c ---[ 50]---> Adder-cost: 114 maxlim: 3787 bits: 13/12 c ---[ 49]---> Adder-cost: 156 maxlim: 4737 bits: 13/13 c ---[ 48]---> Adder-cost: 182 maxlim: 6012 bits: 13/13 c ---[ 46]---> Adder-cost: 184 maxlim: 165300 bits: 18/18 c ---[ 45]---> Adder-cost: 182 maxlim: 5692 bits: 13/13 c ---[ 44]---> Adder-cost: 34 maxlim: 493 bits: 10/9 c ---[ 43]---> Adder-cost: 60 maxlim: 619 bits: 10/10 c ---[ 42]---> Adder-cost: 62 maxlim: 779 bits: 10/10 c ---[ 41]---> Adder-cost: 82 maxlim: 809 bits: 10/10 c ---[ 40]---> Adder-cost: 102 maxlim: 1192 bits: 11/11 c ---[ 39]---> Adder-cost: 98 maxlim: 1000 bits: 11/10 c ---[ 38]---> Adder-cost: 2 maxlim: 254 bits: 9/8 c ---[ 37]---> Adder-cost: 2 maxlim: 254 bits: 9/8 c ---[ 36]---> Adder-cost: 2 maxlim: 254 bits: 9/8 c ---[ 34]---> Adder-cost: 224 maxlim: 287667 bits: 19/19 c ---[ 33]---> Adder-cost: 2 maxlim: 254 bits: 9/8 c ---[ 32]---> Adder-cost: 2 maxlim: 254 bits: 9/8 c ---[ 31]---> Adder-cost: 2 maxlim: 254 bits: 9/8 c ---[ 30]---> Adder-cost: 2 maxlim: 254 bits: 9/8 c ---[ 29]---> Adder-cost: 2 maxlim: 254 bits: 9/8 c ---[ 28]---> Adder-cost: 2 maxlim: 254 bits: 9/8 c ---[ 27]---> Adder-cost: 14 maxlim: 126 bits: 8/7 c ---[ 26]---> Adder-cost: 14 maxlim: 126 bits: 8/7 c ---[ 25]---> Adder-cost: 2 maxlim: 254 bits: 9/8 c ---[ 24]---> Adder-cost: 2 maxlim: 254 bits: 9/8 c ---[ 22]---> Adder-cost: 224 maxlim: 262067 bits: 19/18 c ---[ 21]---> Adder-cost: 2 maxlim: 254 bits: 9/8 c ---[ 20]---> Adder-cost: 2 maxlim: 254 bits: 9/8 c ---[ 19]---> Adder-cost: 14 maxlim: 126 bits: 8/7 c ---[ 18]---> Adder-cost: 14 maxlim: 126 bits: 8/7 c ---[ 17]---> Adder-cost: 2 maxlim: 254 bits: 9/8 c ---[ 16]---> Adder-cost: 2 maxlim: 254 bits: 9/8 c ---[ 15]---> Adder-cost: 2 maxlim: 254 bits: 9/8 c ---[ 14]---> Adder-cost: 2 maxlim: 254 bits: 9/8 c ---[ 13]---> Adder-cost: 14 maxlim: 126 bits: 8/7 c ---[ 12]---> Adder-cost: 14 maxlim: 126 bits: 8/7 c ---[ 10]---> Adder-cost: 224 maxlim: 262067 bits: 19/18 c ---[ 9]---> Adder-cost: 2 maxlim: 254 bits: 9/8 c ---[ 7]---> Adder-cost: 14 maxlim: 126 bits: 8/7 c ---[ 6]---> Adder-cost: 2 maxlim: 254 bits: 9/8 c ---[ 5]---> Adder-cost: 2 maxlim: 254 bits: 9/8 c ---[ 4]---> Adder-cost: 2 maxlim: 254 bits: 9/8 c ---[ 3]---> Adder-cost: 14 maxlim: 126 bits: 8/7 c ---[ 1]---> Adder-cost: 2 maxlim: 254 bits: 9/8 c ---[ 0]---> Adder-cost: 2 maxlim: 254 bits: 9/8 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 91851 330985 | 30617 0 0 nan | 0.000 % | c | 100 | 91814 330866 | 33678 95 696 7.3 | 20.180 % | c | 252 | 91806 330840 | 37046 246 1649 6.7 | 20.186 % | c | 477 | 91790 330788 | 40751 469 3404 7.3 | 20.196 % | c | 815 | 91775 330743 | 44826 804 6665 8.3 | 20.213 % | c | 1321 | 91775 330743 | 49308 1310 12548 9.6 | 20.213 % | c | 2080 | 91751 330663 | 54239 2064 21294 10.3 | 20.229 % | c | 3219 | 91735 330609 | 59663 3199 35655 11.1 | 20.240 % | c | 4928 | 91703 330511 | 65630 4904 63152 12.9 | 20.277 % | c | 7490 | 91665 330387 | 72193 7461 104474 14.0 | 20.310 % | c | 11334 | 91581 330111 | 79412 11289 181161 16.0 | 20.380 % | c | 17100 | 91492 329800 | 87353 16987 300639 17.7 | 20.412 % | c | 25752 | 91492 329800 | 96089 25639 478462 18.7 | 20.412 % | c | 38727 | 91483 329769 | 105698 38609 829071 21.5 | 20.418 % | c | 58193 | 91460 329693 | 116268 58072 1381741 23.8 | 20.439 % | c | 87386 | 91460 329693 | 127894 87265 2217399 25.4 | 20.439 % | c | 131175 | 91273 329062 | 140684 130990 3217346 24.6 | 20.542 % | c | 196859 | 91265 329040 | 154752 68276 2335690 34.2 | 20.553 % | c | 295386 | 91073 328397 | 170227 27883 593770 21.3 | 20.677 % | c | 443175 | 91032 328266 | 187250 20108 431274 21.4 | 20.709 % | c | 664858 | 90944 327974 | 205975 68023 2395882 35.2 | 20.785 % | #### 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.85 0.97 0.93 2/54 9652 Raw data (stat): 9652 (runsolver) R 9651 5897 5896 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 487658640 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0015 s] Raw data (loadavg): 0.87 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 3112 0 0 0 990 8 0 0 25 0 1 0 487658640 14962688 3030 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3653 3030 603 41 0 3612 0 vsize: 14612 [startup+20.0019 s] Raw data (loadavg): 0.89 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 3636 0 0 0 1988 10 0 0 25 0 1 0 487658640 17104896 3554 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4176 3554 603 41 0 4135 0 vsize: 16704 [startup+30.0022 s] Raw data (loadavg): 0.91 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 4119 0 0 0 2986 13 0 0 25 0 1 0 487658640 19128320 4037 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4670 4037 603 41 0 4629 0 vsize: 18680 [startup+40.0031 s] Raw data (loadavg): 0.92 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 4438 0 0 0 3984 14 0 0 25 0 1 0 487658640 20332544 4356 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4964 4356 603 41 0 4923 0 vsize: 19856 [startup+50.0035 s] Raw data (loadavg): 0.93 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 4834 0 0 0 4983 16 0 0 25 0 1 0 487658640 22196224 4752 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5419 4752 603 41 0 5378 0 vsize: 21676 [startup+60.0049 s] Raw data (loadavg): 0.94 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 5106 0 0 0 5982 17 0 0 25 0 1 0 487658640 23298048 5024 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5688 5024 603 41 0 5647 0 vsize: 22752 [startup+70.0056 s] Raw data (loadavg): 0.95 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 5611 0 0 0 6980 19 0 0 25 0 1 0 487658640 25337856 5529 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6186 5529 603 41 0 6145 0 vsize: 24744 [startup+80.006 s] Raw data (loadavg): 0.96 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 5809 0 0 0 7978 20 0 0 25 0 1 0 487658640 26169344 5727 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6389 5727 603 41 0 6348 0 vsize: 25556 [startup+90.0099 s] Raw data (loadavg): 0.96 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 5985 0 0 0 8978 21 0 0 25 0 1 0 487658640 26845184 5903 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6554 5903 603 41 0 6513 0 vsize: 26216 [startup+100.02 s] Raw data (loadavg): 0.97 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 6164 0 0 0 9979 21 0 0 25 0 1 0 487658640 27693056 6082 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6761 6082 603 41 0 6720 0 vsize: 27044 [startup+110.038 s] Raw data (loadavg): 0.97 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 6308 0 0 0 10980 22 0 0 25 0 1 0 487658640 28295168 6226 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6908 6226 603 41 0 6867 0 vsize: 27632 [startup+120.06 s] Raw data (loadavg): 0.98 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 6496 0 0 0 11981 23 0 0 25 0 1 0 487658640 28962816 6414 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7071 6414 603 41 0 7030 0 vsize: 28284 [startup+130.075 s] Raw data (loadavg): 0.98 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 6663 0 0 0 12982 24 0 0 25 0 1 0 487658640 29642752 6581 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7237 6581 603 41 0 7196 0 vsize: 28948 [startup+140.075 s] Raw data (loadavg): 0.98 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 6799 0 0 0 13981 24 0 0 25 0 1 0 487658640 30318592 6717 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7402 6717 603 41 0 7361 0 vsize: 29608 [startup+150.088 s] Raw data (loadavg): 0.98 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 6951 0 0 0 14981 26 0 0 25 0 1 0 487658640 31379456 6869 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7661 6869 603 41 0 7620 0 vsize: 30644 [startup+160.088 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 7173 0 0 0 15979 27 0 0 25 0 1 0 487658640 32305152 7091 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7887 7091 603 41 0 7846 0 vsize: 31548 [startup+170.088 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 7355 0 0 0 16979 28 0 0 25 0 1 0 487658640 33112064 7273 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8084 7273 603 41 0 8043 0 vsize: 32336 [startup+180.088 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 7418 0 0 0 17978 29 0 0 25 0 1 0 487658640 33247232 7336 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8117 7336 603 41 0 8076 0 vsize: 32468 [startup+190.09 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 7419 0 0 0 18978 29 0 0 25 0 1 0 487658640 33247232 7337 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8117 7337 603 41 0 8076 0 vsize: 32468 [startup+200.089 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 7422 0 0 0 19978 29 0 0 25 0 1 0 487658640 33247232 7340 4294967295 134512640 134672761 3221224544 3221223724 134559056 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8117 7340 603 41 0 8076 0 vsize: 32468 [startup+210.091 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 7437 0 0 0 20978 29 0 0 25 0 1 0 487658640 33423360 7355 4294967295 134512640 134672761 3221224544 3221223712 134560882 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8160 7355 603 41 0 8119 0 vsize: 32640 [startup+220.091 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 7454 0 0 0 21978 29 0 0 25 0 1 0 487658640 33423360 7372 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8160 7372 603 41 0 8119 0 vsize: 32640 [startup+230.091 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 7469 0 0 0 22978 30 0 0 25 0 1 0 487658640 33619968 7387 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8208 7387 603 41 0 8167 0 vsize: 32832 [startup+240.092 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 7493 0 0 0 23978 30 0 0 25 0 1 0 487658640 33619968 7411 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8208 7411 603 41 0 8167 0 vsize: 32832 [startup+250.092 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 7501 0 0 0 24978 30 0 0 25 0 1 0 487658640 33619968 7419 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8208 7419 603 41 0 8167 0 vsize: 32832 [startup+260.093 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 7545 0 0 0 25978 30 0 0 25 0 1 0 487658640 33816576 7463 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8256 7463 603 41 0 8215 0 vsize: 33024 [startup+270.093 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 7545 0 0 0 26977 31 0 0 25 0 1 0 487658640 33816576 7463 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8256 7463 603 41 0 8215 0 vsize: 33024 [startup+280.092 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 7571 0 0 0 27977 31 0 0 25 0 1 0 487658640 34013184 7489 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8304 7489 603 41 0 8263 0 vsize: 33216 [startup+290.093 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 7574 0 0 0 28977 32 0 0 25 0 1 0 487658640 34013184 7492 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8304 7492 603 41 0 8263 0 vsize: 33216 [startup+300.094 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 7574 0 0 0 29977 32 0 0 25 0 1 0 487658640 34013184 7492 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8304 7492 603 41 0 8263 0 vsize: 33216 [startup+310.094 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 7574 0 0 0 30976 32 0 0 25 0 1 0 487658640 34013184 7492 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8304 7492 603 41 0 8263 0 vsize: 33216 [startup+320.094 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 7575 0 0 0 31976 33 0 0 25 0 1 0 487658640 34013184 7493 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8304 7493 603 41 0 8263 0 vsize: 33216 [startup+330.094 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 7602 0 0 0 32976 33 0 0 25 0 1 0 487658640 34209792 7520 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8352 7520 603 41 0 8311 0 vsize: 33408 [startup+340.094 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 7603 0 0 0 33976 33 0 0 25 0 1 0 487658640 34209792 7521 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8352 7521 603 41 0 8311 0 vsize: 33408 [startup+350.094 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 7614 0 0 0 34976 33 0 0 25 0 1 0 487658640 34209792 7532 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8352 7532 603 41 0 8311 0 vsize: 33408 [startup+360.096 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 7625 0 0 0 35976 33 0 0 25 0 1 0 487658640 34209792 7543 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8352 7543 603 41 0 8311 0 vsize: 33408 [startup+370.096 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 7638 0 0 0 36976 34 0 0 25 0 1 0 487658640 34406400 7556 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8400 7556 603 41 0 8359 0 vsize: 33600 [startup+380.096 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 7670 0 0 0 37976 34 0 0 25 0 1 0 487658640 34541568 7588 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8433 7588 603 41 0 8392 0 vsize: 33732 [startup+390.096 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 7740 0 0 0 38976 34 0 0 25 0 1 0 487658640 34811904 7658 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8499 7658 603 41 0 8458 0 vsize: 33996 [startup+400.096 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 7824 0 0 0 39976 34 0 0 25 0 1 0 487658640 35082240 7742 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8565 7742 603 41 0 8524 0 vsize: 34260 [startup+410.096 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 7899 0 0 0 40976 34 0 0 25 0 1 0 487658640 35487744 7817 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8664 7817 603 41 0 8623 0 vsize: 34656 [startup+420.097 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 7978 0 0 0 41976 35 0 0 25 0 1 0 487658640 35758080 7896 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8730 7896 603 41 0 8689 0 vsize: 34920 [startup+430.097 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 8325 0 0 0 42975 36 0 0 25 0 1 0 487658640 37228544 8243 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9089 8243 603 41 0 9048 0 vsize: 36356 [startup+440.097 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 8478 0 0 0 43974 37 0 0 25 0 1 0 487658640 37888000 8396 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9250 8396 603 41 0 9209 0 vsize: 37000 [startup+450.097 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 8555 0 0 0 44974 37 0 0 25 0 1 0 487658640 38158336 8473 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9316 8473 603 41 0 9275 0 vsize: 37264 [startup+460.098 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 8639 0 0 0 45974 37 0 0 25 0 1 0 487658640 38428672 8557 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9382 8557 603 41 0 9341 0 vsize: 37528 [startup+470.098 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 8718 0 0 0 46974 37 0 0 25 0 1 0 487658640 38879232 8636 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9492 8636 603 41 0 9451 0 vsize: 37968 [startup+480.115 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 8793 0 0 0 47976 38 0 0 25 0 1 0 487658640 39186432 8711 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9567 8711 603 41 0 9526 0 vsize: 38268 [startup+490.115 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 8865 0 0 0 48976 38 0 0 25 0 1 0 487658640 39456768 8783 4294967295 134512640 134672761 3221224544 3221223360 134565852 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9633 8783 603 41 0 9592 0 vsize: 38532 [startup+500.116 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 8865 0 0 0 49976 38 0 0 25 0 1 0 487658640 39456768 8783 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9633 8783 603 41 0 9592 0 vsize: 38532 [startup+510.122 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 8867 0 0 0 50977 38 0 0 25 0 1 0 487658640 39456768 8785 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9633 8785 603 41 0 9592 0 vsize: 38532 [startup+520.122 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 8883 0 0 0 51977 38 0 0 25 0 1 0 487658640 39456768 8801 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9633 8801 603 41 0 9592 0 vsize: 38532 [startup+530.122 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 8909 0 0 0 52977 38 0 0 25 0 1 0 487658640 39604224 8827 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9669 8827 603 41 0 9628 0 vsize: 38676 [startup+540.133 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 8924 0 0 0 53978 38 0 0 25 0 1 0 487658640 39604224 8842 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9669 8842 603 41 0 9628 0 vsize: 38676 [startup+550.235 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 8956 0 0 0 54988 38 0 0 25 0 1 0 487658640 39784448 8874 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9713 8874 603 41 0 9672 0 vsize: 38852 [startup+560.235 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 8978 0 0 0 55988 38 0 0 25 0 1 0 487658640 39931904 8896 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9749 8896 603 41 0 9708 0 vsize: 38996 [startup+570.252 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 8978 0 0 0 56990 38 0 0 25 0 1 0 487658640 39931904 8896 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9749 8896 603 41 0 9708 0 vsize: 38996 [startup+580.252 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 8981 0 0 0 57990 38 0 0 25 0 1 0 487658640 39931904 8899 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9749 8899 603 41 0 9708 0 vsize: 38996 [startup+590.253 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 8984 0 0 0 58991 38 0 0 25 0 1 0 487658640 39931904 8902 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9749 8902 603 41 0 9708 0 vsize: 38996 [startup+600.254 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 8984 0 0 0 59991 38 0 0 25 0 1 0 487658640 39931904 8902 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9749 8902 603 41 0 9708 0 vsize: 38996 [startup+610.255 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 8985 0 0 0 60991 38 0 0 25 0 1 0 487658640 39931904 8903 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9749 8903 603 41 0 9708 0 vsize: 38996 [startup+620.254 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 8993 0 0 0 61991 38 0 0 25 0 1 0 487658640 39931904 8911 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9749 8911 603 41 0 9708 0 vsize: 38996 [startup+630.254 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 9025 0 0 0 62991 38 0 0 25 0 1 0 487658640 40259584 8943 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9829 8943 603 41 0 9788 0 vsize: 39316 [startup+640.255 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 9027 0 0 0 63992 38 0 0 25 0 1 0 487658640 40259584 8945 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9829 8945 603 41 0 9788 0 vsize: 39316 [startup+650.255 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 9028 0 0 0 64992 38 0 0 25 0 1 0 487658640 40259584 8946 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9829 8946 603 41 0 9788 0 vsize: 39316 [startup+660.258 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 9029 0 0 0 65992 38 0 0 25 0 1 0 487658640 40259584 8947 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9829 8947 603 41 0 9788 0 vsize: 39316 [startup+670.26 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 9031 0 0 0 66993 38 0 0 25 0 1 0 487658640 40259584 8949 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9829 8949 603 41 0 9788 0 vsize: 39316 [startup+680.26 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 9032 0 0 0 67993 38 0 0 25 0 1 0 487658640 40259584 8950 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9829 8950 603 41 0 9788 0 vsize: 39316 [startup+690.26 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 9035 0 0 0 68993 38 0 0 25 0 1 0 487658640 40259584 8953 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9829 8953 603 41 0 9788 0 vsize: 39316 [startup+700.26 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 9153 0 0 0 69993 38 0 0 25 0 1 0 487658640 40660992 9071 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9927 9071 603 41 0 9886 0 vsize: 39708 [startup+710.26 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 9259 0 0 0 70993 39 0 0 25 0 1 0 487658640 41066496 9177 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10026 9177 603 41 0 9985 0 vsize: 40104 [startup+720.26 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 9355 0 0 0 71993 39 0 0 25 0 1 0 487658640 41467904 9273 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10124 9273 603 41 0 10083 0 vsize: 40496 [startup+730.26 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 9441 0 0 0 72993 39 0 0 25 0 1 0 487658640 41873408 9359 4294967295 134512640 134672761 3221224544 3221223648 134554665 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10223 9359 603 41 0 10182 0 vsize: 40892 [startup+740.261 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 9441 0 0 0 73993 39 0 0 25 0 1 0 487658640 41873408 9359 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10223 9359 603 41 0 10182 0 vsize: 40892 [startup+750.261 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 9441 0 0 0 74993 39 0 0 25 0 1 0 487658640 41873408 9359 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10223 9359 603 41 0 10182 0 vsize: 40892 [startup+760.261 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 9452 0 0 0 75993 39 0 0 25 0 1 0 487658640 41873408 9370 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10223 9370 603 41 0 10182 0 vsize: 40892 [startup+770.26 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 9455 0 0 0 76993 39 0 0 25 0 1 0 487658640 41873408 9373 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10223 9373 603 41 0 10182 0 vsize: 40892 [startup+780.26 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 9464 0 0 0 77993 39 0 0 25 0 1 0 487658640 41873408 9382 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10223 9382 603 41 0 10182 0 vsize: 40892 [startup+790.261 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 9497 0 0 0 78993 39 0 0 25 0 1 0 487658640 42012672 9415 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10257 9415 603 41 0 10216 0 vsize: 41028 [startup+800.261 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 9499 0 0 0 79993 39 0 0 25 0 1 0 487658640 42012672 9417 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10257 9417 603 41 0 10216 0 vsize: 41028 [startup+810.262 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 9506 0 0 0 80994 39 0 0 25 0 1 0 487658640 42176512 9424 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10297 9424 603 41 0 10256 0 vsize: 41188 [startup+820.262 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 9508 0 0 0 81994 39 0 0 25 0 1 0 487658640 42176512 9426 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10297 9426 603 41 0 10256 0 vsize: 41188 [startup+830.261 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 9517 0 0 0 82994 39 0 0 25 0 1 0 487658640 42176512 9435 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10297 9435 603 41 0 10256 0 vsize: 41188 [startup+840.262 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 9571 0 0 0 83994 39 0 0 25 0 1 0 487658640 42569728 9489 4294967295 134512640 134672761 3221224544 3221223712 134561145 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10393 9489 603 41 0 10352 0 vsize: 41572 [startup+850.263 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 9573 0 0 0 84994 39 0 0 25 0 1 0 487658640 42569728 9491 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10393 9491 603 41 0 10352 0 vsize: 41572 [startup+860.263 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 9603 0 0 0 85995 39 0 0 25 0 1 0 487658640 42733568 9521 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10433 9521 603 41 0 10392 0 vsize: 41732 [startup+870.263 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 9636 0 0 0 86995 39 0 0 25 0 1 0 487658640 42897408 9554 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10473 9554 603 41 0 10432 0 vsize: 41892 [startup+880.263 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 9664 0 0 0 87995 39 0 0 25 0 1 0 487658640 43061248 9582 4294967295 134512640 134672761 3221224544 3221223560 1075353072 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10513 9582 603 41 0 10472 0 vsize: 42052 [startup+890.264 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 9669 0 0 0 88995 39 0 0 25 0 1 0 487658640 43061248 9587 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10513 9587 603 41 0 10472 0 vsize: 42052 [startup+900.264 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 9692 0 0 0 89995 39 0 0 25 0 1 0 487658640 43225088 9610 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10553 9610 603 41 0 10512 0 vsize: 42212 [startup+910.265 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 9702 0 0 0 90995 39 0 0 25 0 1 0 487658640 43225088 9620 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10553 9620 603 41 0 10512 0 vsize: 42212 [startup+920.264 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 9702 0 0 0 91996 39 0 0 25 0 1 0 487658640 43225088 9620 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10553 9620 603 41 0 10512 0 vsize: 42212 [startup+930.264 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 9702 0 0 0 92996 39 0 0 25 0 1 0 487658640 43225088 9620 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10553 9620 603 41 0 10512 0 vsize: 42212 [startup+940.265 s] Raw data (loadavg): 0.99 0.97 0.93 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 9707 0 0 0 93996 39 0 0 25 0 1 0 487658640 43225088 9625 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10553 9625 603 41 0 10512 0 vsize: 42212 [startup+950.265 s] Raw data (loadavg): 1.15 1.00 0.94 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 9746 0 0 0 94996 39 0 0 25 0 1 0 487658640 43360256 9664 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10586 9664 603 41 0 10545 0 vsize: 42344 [startup+960.265 s] Raw data (loadavg): 1.20 1.02 0.95 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 9900 0 0 0 95996 40 0 0 25 0 1 0 487658640 44036096 9818 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10751 9818 603 41 0 10710 0 vsize: 43004 [startup+970.266 s] Raw data (loadavg): 1.17 1.02 0.95 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 10063 0 0 0 96996 40 0 0 25 0 1 0 487658640 44707840 9981 4294967295 134512640 134672761 3221224544 3221223712 134560882 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10915 9981 603 41 0 10874 0 vsize: 43660 [startup+980.265 s] Raw data (loadavg): 1.14 1.02 0.95 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 10219 0 0 0 97996 40 0 0 25 0 1 0 487658640 45375488 10137 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11078 10137 603 41 0 11037 0 vsize: 44312 [startup+990.265 s] Raw data (loadavg): 1.12 1.02 0.95 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 10351 0 0 0 98996 40 0 0 25 0 1 0 487658640 45821952 10269 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11187 10269 603 41 0 11146 0 vsize: 44748 [startup+1000.27 s] Raw data (loadavg): 1.10 1.02 0.95 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 10486 0 0 0 99995 41 0 0 25 0 1 0 487658640 46358528 10404 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11318 10404 603 41 0 11277 0 vsize: 45272 [startup+1010.27 s] Raw data (loadavg): 1.09 1.01 0.95 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 10623 0 0 0 100995 41 0 0 25 0 1 0 487658640 46899200 10541 4294967295 134512640 134672761 3221224544 3221223712 134560906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11450 10541 603 41 0 11409 0 vsize: 45800 [startup+1020.27 s] Raw data (loadavg): 1.07 1.01 0.95 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 10751 0 0 0 101995 42 0 0 25 0 1 0 487658640 47480832 10669 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11592 10669 603 41 0 11551 0 vsize: 46368 [startup+1030.27 s] Raw data (loadavg): 1.06 1.01 0.95 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 10848 0 0 0 102994 42 0 0 25 0 1 0 487658640 47886336 10766 4294967295 134512640 134672761 3221224544 3221223648 134554662 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11691 10766 603 41 0 11650 0 vsize: 46764 [startup+1040.27 s] Raw data (loadavg): 1.05 1.01 0.95 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 10848 0 0 0 103995 42 0 0 25 0 1 0 487658640 47886336 10766 4294967295 134512640 134672761 3221224544 3221223728 134559492 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11691 10766 603 41 0 11650 0 vsize: 46764 [startup+1050.27 s] Raw data (loadavg): 1.04 1.01 0.95 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 10848 0 0 0 104995 42 0 0 25 0 1 0 487658640 47886336 10766 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11691 10766 603 41 0 11650 0 vsize: 46764 [startup+1060.27 s] Raw data (loadavg): 1.04 1.01 0.95 2/54 9652 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 10855 0 0 0 105995 42 0 0 25 0 1 0 487658640 47886336 10773 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11691 10773 603 41 0 11650 0 vsize: 46764 [startup+1070.27 s] Raw data (loadavg): 1.11 1.03 0.95 2/54 9705 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 10873 0 0 0 106994 43 0 0 25 0 1 0 487658640 48033792 10791 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11727 10791 603 41 0 11686 0 vsize: 46908 [startup+1080.27 s] Raw data (loadavg): 1.09 1.02 0.95 2/54 9705 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 10889 0 0 0 107994 43 0 0 25 0 1 0 487658640 48033792 10807 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11727 10807 603 41 0 11686 0 vsize: 46908 [startup+1090.27 s] Raw data (loadavg): 1.08 1.02 0.95 2/54 9705 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 10905 0 0 0 108994 43 0 0 25 0 1 0 487658640 48197632 10823 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11767 10823 603 41 0 11726 0 vsize: 47068 [startup+1100.27 s] Raw data (loadavg): 1.07 1.02 0.95 2/54 9705 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 10928 0 0 0 109994 43 0 0 25 0 1 0 487658640 48361472 10846 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11807 10846 603 41 0 11766 0 vsize: 47228 [startup+1110.27 s] Raw data (loadavg): 1.06 1.02 0.95 2/54 9705 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 10928 0 0 0 110993 44 0 0 25 0 1 0 487658640 48361472 10846 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11807 10846 603 41 0 11766 0 vsize: 47228 [startup+1120.27 s] Raw data (loadavg): 1.05 1.02 0.95 2/54 9705 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 10928 0 0 0 111994 44 0 0 25 0 1 0 487658640 48361472 10846 4294967295 134512640 134672761 3221224544 3221223680 134560608 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11807 10846 603 41 0 11766 0 vsize: 47228 [startup+1130.27 s] Raw data (loadavg): 1.04 1.02 0.95 2/54 9705 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 10928 0 0 0 112994 44 0 0 25 0 1 0 487658640 48361472 10846 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11807 10846 603 41 0 11766 0 vsize: 47228 [startup+1140.27 s] Raw data (loadavg): 1.03 1.02 0.95 2/54 9707 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 10938 0 0 0 113994 44 0 0 25 0 1 0 487658640 48361472 10856 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11807 10856 603 41 0 11766 0 vsize: 47228 [startup+1150.27 s] Raw data (loadavg): 1.03 1.02 0.95 2/54 9707 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 10951 0 0 0 114994 44 0 0 25 0 1 0 487658640 48508928 10869 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11843 10869 603 41 0 11802 0 vsize: 47372 [startup+1160.27 s] Raw data (loadavg): 1.02 1.02 0.95 2/54 9707 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 10961 0 0 0 115994 44 0 0 25 0 1 0 487658640 48508928 10879 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11843 10879 603 41 0 11802 0 vsize: 47372 [startup+1170.27 s] Raw data (loadavg): 1.02 1.02 0.95 2/54 9707 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 10962 0 0 0 116994 44 0 0 25 0 1 0 487658640 48508928 10880 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11843 10880 603 41 0 11802 0 vsize: 47372 [startup+1180.27 s] Raw data (loadavg): 1.02 1.01 0.95 2/54 9707 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 10962 0 0 0 117995 44 0 0 25 0 1 0 487658640 48508928 10880 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11843 10880 603 41 0 11802 0 vsize: 47372 [startup+1190.27 s] Raw data (loadavg): 1.01 1.01 0.95 2/54 9707 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 10972 0 0 0 118995 44 0 0 25 0 1 0 487658640 48508928 10890 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11843 10890 603 41 0 11802 0 vsize: 47372 [startup+1200.27 s] Raw data (loadavg): 1.01 1.01 0.95 2/54 9707 Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 10972 0 0 0 119995 44 0 0 25 0 1 0 487658640 48508928 10890 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11843 10890 603 41 0 11802 0 vsize: 47372 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.3 s] Raw data (loadavg): 1.01 1.01 0.95 1/54 9707 Raw data (stat): 9652 (minisat+) Z 9651 5897 5896 0 -1 12 10974 0 0 0 119995 46 0 0 25 0 1 0 487658640 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 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.3 CPU time (s): 1200.42 CPU user time (s): 1199.96 CPU system time (s): 0.465929 CPU usage (%): 100.01 Max. virtual memory (Kb): 47372 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####