Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
  1. LAUNCHER DATA
    These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
    Note that some very long lines in this section may be truncated by your web browser !
  3. WATCHER DATA
    This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
    Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
    When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
  4. VERIFIER DATA
    The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.

General information on the benchmark

Namemps-v2-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-vpm2.opb
MD5SUM8c44064d4224b1d41c28f152218dd39f
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 121
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 numbers20
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1189.02
Number of variables2124
Total number of constraints612
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)168
Number of constraints which are nor clauses,nor cardinality constraints444
Minimum length of a constraint1
Maximum length of a constraint64

Trace number 6170

Launcher Data

LAUNCH ON wulflinc5 THE 2005-09-20 04:04:11 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3335 boxname=wulflinc5 idbench=991 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  8c44064d4224b1d41c28f152218dd39f  /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-13-7-vpm2.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-13-7-vpm2.opb
IDLAUNCH: 3335
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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.007
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:        913072 kB
Buffers:          8176 kB
Cached:          89068 kB
SwapCached:        744 kB
Active:          25080 kB
Inactive:        74852 kB
HighTotal:      131008 kB
HighFree:        37716 kB
LowTotal:       903652 kB
LowFree:        875356 kB
SwapTotal:     2097136 kB
SwapFree:      2095884 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5756 kB
Slab:            16024 kB
Committed_AS:    64264 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-20 04:24:23 (client local time) WITH STATUS 0 IN 1206.25 SECONDS
stats: 3335 7 1206.25 0

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]---> BDD-cost:    7
c ---[ 484]---> BDD-cost:    7
c ---[ 483]---> BDD-cost:    7
c ---[ 482]---> BDD-cost:    7
c ---[ 481]---> BDD-cost:    7
c ---[ 480]---> BDD-cost:    7
c ---[ 479]---> BDD-cost:    7
c ---[ 478]---> BDD-cost:    7
c ---[ 477]---> BDD-cost:    7
c ---[ 474]---> BDD-cost:    7
c ---[ 473]---> BDD-cost:    7
c ---[ 472]---> BDD-cost:    7
c ---[ 471]---> BDD-cost:    7
c ---[ 468]---> BDD-cost:    7
c ---[ 467]---> BDD-cost:    7
c ---[ 466]---> BDD-cost:    7
c ---[ 465]---> BDD-cost:    7
c ---[ 462]---> BDD-cost:    7
c ---[ 459]---> BDD-cost:    7
c ---[ 458]---> BDD-cost:    7
c ---[ 457]---> BDD-cost:    7
c ---[ 454]---> BDD-cost:    7
c ---[ 453]---> BDD-cost:    7
c ---[ 452]---> BDD-cost:    7
c ---[ 451]---> BDD-cost:    7
c ---[ 450]---> BDD-cost:    7
c ---[ 448]---> BDD-cost:    7
c ---[ 447]---> BDD-cost:    7
c ---[ 446]---> BDD-cost:    7
c ---[ 445]---> BDD-cost:    7
c ---[ 444]---> BDD-cost:    7
c ---[ 441]---> BDD-cost:    7
c ---[ 440]---> BDD-cost:    7
c ---[ 439]---> BDD-cost:    7
c ---[ 433]---> BDD-cost:    7
c ---[ 427]---> BDD-cost:    7
c ---[ 422]---> BDD-cost:    7
c ---[ 421]---> BDD-cost:    7
c ---[ 415]---> BDD-cost:    7
c ---[ 409]---> BDD-cost:    7
c ---[ 408]---> BDD-cost:    7
c ---[ 402]---> BDD-cost:    7
c ---[ 397]---> BDD-cost:    7
c ---[ 396]---> BDD-cost:    7
c ---[ 391]---> BDD-cost:    7
c ---[ 390]---> BDD-cost:    7
c ---[ 386]---> BDD-cost:    7
c ---[ 385]---> BDD-cost:    7
c ---[ 384]---> BDD-cost:    7
c ---[ 380]---> BDD-cost:    7
c ---[ 379]---> BDD-cost:    7
c ---[ 378]---> BDD-cost:    7
c ---[ 374]---> BDD-cost:    7
c ---[ 373]---> BDD-cost:    7
c ---[ 372]---> BDD-cost:    7
c ---[ 368]---> BDD-cost:    7
c ---[ 367]---> BDD-cost:    7
c ---[ 366]---> BDD-cost:    7
c ---[ 365]---> BDD-cost:    7
c ---[ 364]---> BDD-cost:    7
c ---[ 359]---> BDD-cost:    7
c ---[ 353]---> BDD-cost:    7
c ---[ 347]---> BDD-cost:    7
c ---[ 339]---> BDD-cost:    7
c ---[ 333]---> BDD-cost:    7
c ---[ 327]---> BDD-cost:    7
c ---[ 321]---> BDD-cost:    7
c ---[ 317]---> BDD-cost:   14
c ---[ 316]---> BDD-cost:   14
c ---[ 315]---> BDD-cost:   14
c ---[ 314]---> BDD-cost:   14
c ---[ 313]---> BDD-cost:   14
c ---[ 312]---> BDD-cost:   14
c ---[ 310]---> BDD-cost:   14
c ---[ 309]---> BDD-cost:   14
c ---[ 308]---> BDD-cost:   14
c ---[ 307]---> BDD-cost:   14
c ---[ 306]---> BDD-cost:   14
c ---[ 302]---> BDD-cost:   13
c ---[ 301]---> BDD-cost:   13
c ---[ 300]---> BDD-cost:   13
c ---[ 295]---> BDD-cost:   13
c ---[ 294]---> BDD-cost:   13
c ---[ 290]---> BDD-cost:   15
c ---[ 289]---> BDD-cost:   15
c ---[ 288]---> BDD-cost:   15
c ---[ 287]---> BDD-cost:   13
c ---[ 286]---> BDD-cost:   13
c ---[ 285]---> BDD-cost:   13
c ---[ 284]---> BDD-cost:   13
c ---[ 283]---> BDD-cost:   13
c ---[ 282]---> BDD-cost:   13
c ---[ 280]---> BDD-cost:   13
c ---[ 279]---> BDD-cost:   13
c ---[ 278]---> BDD-cost:   13
c ---[ 277]---> BDD-cost:   13
c ---[ 276]---> BDD-cost:   13
c ---[ 274]---> Adder-cost: 262   maxlim: 300367   bits: 19/19
c ---[ 272]---> Sorter-cost: 2159     Base: 2 2 2 2 2 2 2 2 2 2 3 2 2
c ---[ 271]---> BDD-cost:    3
c ---[ 270]---> BDD-cost:    3
c ---[ 269]---> BDD-cost:    3
c ---[ 267]---> BDD-cost:    3
c ---[ 266]---> BDD-cost:    3
c ---[ 265]---> BDD-cost:    3
c ---[ 264]---> BDD-cost:    3
c ---[ 263]---> BDD-cost:    3
c ---[ 259]---> BDD-cost:    7
c ---[ 258]---> BDD-cost:    3
c ---[ 257]---> BDD-cost:    3
c ---[ 256]---> BDD-cost:    3
c ---[ 255]---> BDD-cost:    7
c ---[ 251]---> BDD-cost:    7
c ---[ 250]---> BDD-cost:    3
c ---[ 247]---> BDD-cost:    6
c ---[ 243]---> BDD-cost:    7
c ---[ 242]---> BDD-cost:    3
c ---[ 241]---> BDD-cost:    6
c ---[ 236]---> Sorter-cost: 1318     Base: 2 2 2 2 5 5 2 2 2 2 2
c ---[ 235]---> BDD-cost:    3
c ---[ 234]---> BDD-cost:    3
c ---[ 233]---> BDD-cost:    6
c ---[ 229]---> BDD-cost:    7
c ---[ 228]---> BDD-cost:    3
c ---[ 227]---> BDD-cost:    6
c ---[ 224]---> Sorter-cost: 2540     Base: 2 2 2 2 5 5 2 2 2 2 2 2
c ---[ 220]---> BDD-cost:    3
c ---[ 219]---> BDD-cost:    3
c ---[ 214]---> BDD-cost:    7
c ---[ 212]---> Sorter-cost: 1902     Base: 2 2 2 2 2 2 2 2 2 2 2 3
c ---[ 211]---> BDD-cost:    3
c ---[ 206]---> BDD-cost:    3
c ---[ 205]---> BDD-cost:    3
c ---[ 198]---> BDD-cost:    3
c ---[ 197]---> BDD-cost:    3
c ---[ 193]---> BDD-cost:    3
c ---[ 192]---> BDD-cost:    3
c ---[ 191]---> BDD-cost:    3
c ---[ 185]---> BDD-cost:    3
c ---[ 184]---> BDD-cost:    3
c ---[ 183]---> BDD-cost:    3
c ---[ 179]---> BDD-cost:    3
c ---[ 178]---> BDD-cost:    3
c ---[ 175]---> BDD-cost:    3
c ---[ 171]---> BDD-cost:    3
c ---[ 170]---> BDD-cost:    3
c ---[ 169]---> BDD-cost:    3
c ---[ 168]---> BDD-cost:    3
c ---[ 167]---> BDD-cost:    3
c ---[ 166]---> BDD-cost:    6
c ---[ 164]---> Sorter-cost: 1580     Base: 2 2 2 5 5 2 2 2 2 2 3
c ---[ 163]---> BDD-cost:    6
c ---[ 162]---> BDD-cost:    6
c ---[ 161]---> BDD-cost:    6
c ---[ 160]---> BDD-cost:    3
c ---[ 159]---> BDD-cost:    7
c ---[ 158]---> BDD-cost:    6
c ---[ 157]---> BDD-cost:    6
c ---[ 156]---> BDD-cost:    6
c ---[ 155]---> BDD-cost:    6
c ---[ 154]---> BDD-cost:    3
c ---[ 152]---> Adder-cost: 262   maxlim: 300367   bits: 19/19
c ---[ 150]---> Adder-cost: 260   maxlim: 219983   bits: 19/18
c ---[ 149]---> BDD-cost:    7
c ---[ 148]---> BDD-cost:    5
c ---[ 147]---> BDD-cost:    5
c ---[ 146]---> BDD-cost:    5
c ---[ 145]---> BDD-cost:    5
c ---[ 144]---> BDD-cost:    3
c ---[ 143]---> BDD-cost:    7
c ---[ 142]---> BDD-cost:    5
c ---[ 141]---> BDD-cost:    5
c ---[ 140]---> BDD-cost:    5
c ---[ 137]---> BDD-cost:    5
c ---[ 135]---> BDD-cost:    7
c ---[ 134]---> BDD-cost:    3
c ---[ 133]---> BDD-cost:    6
c ---[ 132]---> BDD-cost:    6
c ---[ 131]---> BDD-cost:    6
c ---[ 129]---> BDD-cost:    7
c ---[ 128]---> BDD-cost:    3
c ---[ 125]---> BDD-cost:    6
c ---[ 124]---> BDD-cost:    6
c ---[ 123]---> BDD-cost:    6
c ---[ 121]---> BDD-cost:    7
c ---[ 120]---> BDD-cost:    3
c ---[ 119]---> BDD-cost:    6
c ---[ 118]---> BDD-cost:    6
c ---[ 117]---> BDD-cost:    6
c ---[ 114]---> Sorter-cost: 1742     Base: 2 2 2 5 5 2 2 2 2 2 2
c ---[ 113]---> BDD-cost:    7
c ---[ 112]---> BDD-cost:    3
c ---[ 111]---> BDD-cost:    5
c ---[ 110]---> BDD-cost:    5
c ---[ 109]---> BDD-cost:    5
c ---[ 107]---> Sorter-cost: 2471     Base: 2 2 2 2 2 2 2 2 2 2 2 3 2
c ---[ 105]---> Sorter-cost: 2473     Base: 2 2 2 2 2 2 2 2 2 2 2 3 2
c ---[ 103]---> Sorter-cost: 3095     Base: 2 2 2 2 2 3 5 2 2 2 5
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]---> Sorter-cost: 2565     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  93]---> Adder-cost: 222   maxlim: 103983   bits: 17/17
c ---[  91]---> Sorter-cost: 1881     Base: 2 2 2 2 5 5 2 2 2 5
c ---[  89]---> Sorter-cost: 3211     Base: 2 2 2 2 5 5 2 2 2 2 5
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]---> Sorter-cost: 1988     Base: 2 2 2 5 5 2 2 2 2 2 3
c ---[  73]---> Sorter-cost: 2565     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  69]---> Sorter-cost: 1824     Base: 2 2 2 5 5 2 2 2 3 2 2 2
c ---[  66]---> BDD-cost:  136
c ---[  65]---> BDD-cost:  283
c ---[  64]---> BDD-cost:  282
c ---[  63]---> BDD-cost:  470
c ---[  62]---> BDD-cost:  579
c ---[  61]---> BDD-cost:  572
c ---[  60]---> Sorter-cost:  303     Base: 2 2 2 2 2 5 2
c ---[  58]---> Adder-cost: 262   maxlim: 261967   bits: 19/18
c ---[  57]---> Sorter-cost:  801     Base: 2 2 2 2 2 5 2
c ---[  56]---> Sorter-cost:  819     Base: 2 2 2 2 2 5 2
c ---[  55]---> Sorter-cost: 1035     Base: 5 2 2 2 2 2 2
c ---[  54]---> Sorter-cost: 1285     Base: 5 2 2 2 2 2 2
c ---[  53]---> Sorter-cost: 1289     Base: 5 2 2 2 2 2 2
c ---[  52]---> Sorter-cost:  335     Base: 2 2 2 2 2 2 5
c ---[  51]---> Sorter-cost:  867     Base: 2 2 5 2 2 2 2
c ---[  50]---> Sorter-cost:  830     Base: 2 2 2 2 2 2 5
c ---[  49]---> Sorter-cost: 1298     Base: 2 2 5 2 2 2 2
c ---[  48]---> Sorter-cost: 1687     Base: 2 2 5 2 2 2 2
c ---[  46]---> Sorter-cost: 1411     Base: 2 2 2 2 5 5 2 2 2 2 2
c ---[  45]---> Sorter-cost: 1665     Base: 2 2 5 2 2 2 2
c ---[  44]---> Sorter-cost:  196     Base: 2 2 2 2 2 2
c ---[  43]---> Sorter-cost:  473     Base: 2 2 2 2 2
c ---[  42]---> Sorter-cost:  421     Base: 2 2 2 2 2 2
c ---[  41]---> Sorter-cost:  764     Base: 2 2 2 2 2
c ---[  40]---> Sorter-cost:  884     Base: 2 2 2 2 2 2
c ---[  39]---> Sorter-cost: 1063     Base: 2 2 2 2 2
c ---[  38]---> BDD-cost:    3
c ---[  37]---> BDD-cost:    3
c ---[  36]---> BDD-cost:    3
c ---[  34]---> Sorter-cost: 2230     Base: 2 2 2 2 2 2 2 2 2 2 2 3 2
c ---[  33]---> BDD-cost:    3
c ---[  32]---> BDD-cost:    3
c ---[  31]---> BDD-cost:    3
c ---[  30]---> BDD-cost:    3
c ---[  29]---> BDD-cost:    3
c ---[  28]---> BDD-cost:    3
c ---[  27]---> BDD-cost:    7
c ---[  26]---> BDD-cost:    7
c ---[  25]---> BDD-cost:    3
c ---[  24]---> BDD-cost:    3
c ---[  22]---> Sorter-cost: 2232     Base: 2 2 2 2 2 2 2 2 2 2 2 3 2
c ---[  21]---> BDD-cost:    3
c ---[  20]---> BDD-cost:    3
c ---[  19]---> BDD-cost:    7
c ---[  18]---> BDD-cost:    7
c ---[  17]---> BDD-cost:    3
c ---[  16]---> BDD-cost:    3
c ---[  15]---> BDD-cost:    3
c ---[  14]---> BDD-cost:    3
c ---[  13]---> BDD-cost:    7
c ---[  12]---> BDD-cost:    7
c ---[  10]---> Sorter-cost: 2232     Base: 2 2 2 2 2 2 2 2 2 2 2 3 2
c ---[   9]---> BDD-cost:    3
c ---[   7]---> BDD-cost:    7
c ---[   6]---> BDD-cost:    3
c ---[   5]---> BDD-cost:    3
c ---[   4]---> BDD-cost:    3
c ---[   3]---> BDD-cost:    7
c ---[   1]---> BDD-cost:    3
c ---[   0]---> BDD-cost:    3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  165694   413657 |   55231       0        0     nan |  0.000 % |
c |       102 |  165616   413479 |   60754      99     1459    14.7 |  5.324 % |
c |       252 |  165375   412930 |   66829     245     2721    11.1 |  5.428 % |
c |       477 |  165357   412890 |   73512     469     6101    13.0 |  5.437 % |
c |       814 |  165188   412504 |   80863     802     9398    11.7 |  5.516 % |
c |      1320 |  164865   411746 |   88950    1267    13983    11.0 |  5.666 % |
c |      2079 |  163978   409703 |   97845    1922    20743    10.8 |  6.104 % |
c |      3218 |  163801   409297 |  107629    3060    52624    17.2 |  6.187 % |
c |      4927 |  163739   409157 |  118392    4765   111807    23.5 |  6.219 % |
c |      7493 |  163484   408561 |  130231    7305   169316    23.2 |  6.337 % |
c |     11340 |  163364   408284 |  143254   11146   339381    30.4 |  6.392 % |
c |     17107 |  162493   406293 |  157580   16863   525197    31.1 |  6.813 % |
c |     25759 |  162097   405354 |  173338   25483   778910    30.6 |  7.013 % |
c |     38733 |  161410   403789 |  190672   38387  1212692    31.6 |  7.343 % |
c |     58194 |  160811   402413 |  209739   57805  2041019    35.3 |  7.645 % |
c |     87386 |  159402   399021 |  230713   85832  3126290    36.4 |  8.285 % |
c |    131175 |  158653   397316 |  253784  129543  4806879    37.1 |  8.645 % |
c |    196859 |  157962   395566 |  279163  195169  6798047    34.8 |  8.947 % |
c |    295386 |  157436   394369 |  307079   38965  1023168    26.3 |  9.228 % |

Watcher Data

Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing Stack size limit: 67108864 bytes
Enforcing memory limit (will send SIGTERM then SIGKILL): 921600 Kb
Enforcing VSIZE limit: 994918400 bytes
Current StackSize limit: 67108864 bytes
Raw data (/proc/25192/stat): 25192 (minisat+_script) R 25191 25192 824 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1797290153 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/25192/statm): 174 3 169 147 0 27 0
[pid=25192] vsize: 696
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libtermcap.so.2
open syscall for file tls/i686/libtermcap.so.2
open syscall for file tls/mmx/libtermcap.so.2
open syscall for file tls/libtermcap.so.2
open syscall for file i686/mmx/libtermcap.so.2
open syscall for file i686/libtermcap.so.2
open syscall for file mmx/libtermcap.so.2
open syscall for file libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/i686/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/i686/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/i686/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/libtermcap.so.2
open syscall for file /etc/ld.so.cache
open syscall for file /lib/libtermcap.so.2
open syscall for file tls/i686/mmx/libdl.so.2
open syscall for file tls/i686/libdl.so.2
open syscall for file tls/mmx/libdl.so.2
open syscall for file tls/libdl.so.2
open syscall for file i686/mmx/libdl.so.2
open syscall for file i686/libdl.so.2
open syscall for file mmx/libdl.so.2
open syscall for file libdl.so.2
open syscall for file /oldhome/oroussel/lib/libdl.so.2
open syscall for file /lib/libdl.so.2
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /lib/tls/libc.so.6
open syscall for file /dev/tty
open syscall for file /etc/mtab
open syscall for file /proc/meminfo
open syscall for file /oldhome/oroussel/solvers/minisat+_script
New process pid=25193
New process pid=25194
New process pid=25195
execve syscall for /bin/sed executable
One traced child (pid=25194) exited with status: 0
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=25195) exited with status: 0
One traced child (pid=25193) exited with status: 0
New process pid=25196
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-13-7-vpm2.opb

[startup+10.0037 s]
Raw data (loadavg): 0.93 0.98 0.97 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 5011 0 0 0 958 17 0 0 25 0 1 0 1797290158 22478848 4818 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 5488 4818 145 145 0 5343 0
[pid=25196] vsize: 21952
Current children cumulated CPU time (s) 9.75
Current children cumulated vsize (Kb) 24076

[startup+20.0055 s]
Raw data (loadavg): 0.94 0.98 0.97 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 5240 0 0 0 1953 19 0 0 25 0 1 0 1797290158 23420928 5047 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25196/statm): 5718 5047 145 145 0 5573 0
[pid=25196] vsize: 22872
Current children cumulated CPU time (s) 19.72
Current children cumulated vsize (Kb) 24996

[startup+31.2863 s]
Raw data (loadavg): 1.03 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) T 25192 25192 824 0 -1 0 5408 0 0 0 2710 20 0 0 25 0 1 0 1797290158 24096768 5215 4294967295 134512640 135094434 3221224448 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/25196/statm): 5883 5215 145 145 0 5738 0
[pid=25196] vsize: 23532
Current children cumulated CPU time (s) 27.3
Current children cumulated vsize (Kb) 25656

[startup+41.2876 s]
Raw data (loadavg): 1.03 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 5604 0 0 0 3707 21 0 0 25 0 1 0 1797290158 24936448 5411 4294967295 134512640 135094434 3221224448 3221223120 134555413 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 6088 5411 145 145 0 5943 0
[pid=25196] vsize: 24352
Current children cumulated CPU time (s) 37.28
Current children cumulated vsize (Kb) 26476

[startup+51.2883 s]
Raw data (loadavg): 1.02 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 5802 0 0 0 4703 22 0 0 25 0 1 0 1797290158 25726976 5609 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 6281 5609 145 145 0 6136 0
[pid=25196] vsize: 25124
Current children cumulated CPU time (s) 47.25
Current children cumulated vsize (Kb) 27248

[startup+61.2881 s]
Raw data (loadavg): 1.02 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 5993 0 0 0 5698 24 0 0 25 0 1 0 1797290158 26488832 5800 4294967295 134512640 135094434 3221224448 3221223072 134557642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25196/statm): 6467 5800 145 145 0 6322 0
[pid=25196] vsize: 25868
Current children cumulated CPU time (s) 57.22
Current children cumulated vsize (Kb) 27992

[startup+71.2898 s]
Raw data (loadavg): 1.02 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 6180 0 0 0 6695 26 0 0 25 0 1 0 1797290158 27238400 5987 4294967295 134512640 135094434 3221224448 3221223072 134557655 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 6650 5987 145 145 0 6505 0
[pid=25196] vsize: 26600
Current children cumulated CPU time (s) 67.21
Current children cumulated vsize (Kb) 28724

[startup+81.2905 s]
Raw data (loadavg): 1.01 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 6359 0 0 0 7692 28 0 0 25 0 1 0 1797290158 28090368 6166 4294967295 134512640 135094434 3221224448 3221223104 134557849 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 6858 6166 145 145 0 6713 0
[pid=25196] vsize: 27432
Current children cumulated CPU time (s) 77.2
Current children cumulated vsize (Kb) 29556

[startup+91.2913 s]
Raw data (loadavg): 1.01 1.00 0.98 3/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 6537 0 0 0 8689 30 0 0 25 0 1 0 1797290158 28803072 6344 4294967295 134512640 135094434 3221224448 3221223072 134557717 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 7032 6344 145 145 0 6887 0
[pid=25196] vsize: 28128
Current children cumulated CPU time (s) 87.19
Current children cumulated vsize (Kb) 30252

[startup+101.292 s]
Raw data (loadavg): 1.01 1.00 0.98 3/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 7083 0 0 0 9681 33 0 0 25 0 1 0 1797290158 31002624 6890 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 7569 6890 145 145 0 7424 0
[pid=25196] vsize: 30276
Current children cumulated CPU time (s) 97.14
Current children cumulated vsize (Kb) 32400

[startup+111.293 s]
Raw data (loadavg): 1.01 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 7265 0 0 0 10679 34 0 0 25 0 1 0 1797290158 31719424 7072 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 7744 7072 145 145 0 7599 0
[pid=25196] vsize: 30976
Current children cumulated CPU time (s) 107.13
Current children cumulated vsize (Kb) 33100

[startup+121.293 s]
Raw data (loadavg): 1.01 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 7535 0 0 0 11674 36 0 0 25 0 1 0 1797290158 32796672 7342 4294967295 134512640 135094434 3221224448 3221223060 134563061 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 8007 7342 145 145 0 7862 0
[pid=25196] vsize: 32028
Current children cumulated CPU time (s) 117.1
Current children cumulated vsize (Kb) 34152

[startup+131.294 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 7656 0 0 0 12672 37 0 0 25 0 1 0 1797290158 33284096 7463 4294967295 134512640 135094434 3221224448 3221223104 134557937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 8126 7463 145 145 0 7981 0
[pid=25196] vsize: 32504
Current children cumulated CPU time (s) 127.09
Current children cumulated vsize (Kb) 34628

[startup+141.296 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 7841 0 0 0 13669 38 0 0 25 0 1 0 1797290158 34021376 7648 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 8306 7648 145 145 0 8161 0
[pid=25196] vsize: 33224
Current children cumulated CPU time (s) 137.07
Current children cumulated vsize (Kb) 35348

[startup+151.297 s]
Raw data (loadavg): 1.00 1.00 0.98 3/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 8169 0 0 0 14661 41 0 0 25 0 1 0 1797290158 35598336 7976 4294967295 134512640 135094434 3221224448 3221223108 134553536 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 8691 7976 145 145 0 8546 0
[pid=25196] vsize: 34764
Current children cumulated CPU time (s) 147.02
Current children cumulated vsize (Kb) 36888

[startup+161.296 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 8371 0 0 0 15658 43 0 0 25 0 1 0 1797290158 36401152 8178 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 8887 8178 145 145 0 8742 0
[pid=25196] vsize: 35548
Current children cumulated CPU time (s) 157.01
Current children cumulated vsize (Kb) 37672

[startup+171.297 s]
Raw data (loadavg): 1.00 1.00 0.98 1/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) T 25192 25192 824 0 -1 0 8560 0 0 0 16653 45 0 0 25 0 1 0 1797290158 37167104 8367 4294967295 134512640 135094434 3221224448 3221222828 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/25196/statm): 9074 8367 145 145 0 8929 0
[pid=25196] vsize: 36296
Current children cumulated CPU time (s) 166.98
Current children cumulated vsize (Kb) 38420

[startup+181.298 s]
Raw data (loadavg): 1.00 1.00 0.98 3/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 8700 0 0 0 17651 46 0 0 25 0 1 0 1797290158 37728256 8507 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 9211 8507 145 145 0 9066 0
[pid=25196] vsize: 36844
Current children cumulated CPU time (s) 176.97
Current children cumulated vsize (Kb) 38968

[startup+191.299 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 8856 0 0 0 18648 47 0 0 25 0 1 0 1797290158 38363136 8663 4294967295 134512640 135094434 3221224448 3221222976 134780540 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 9366 8663 145 145 0 9221 0
[pid=25196] vsize: 37464
Current children cumulated CPU time (s) 186.95
Current children cumulated vsize (Kb) 39588

[startup+201.299 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 9011 0 0 0 19645 49 0 0 25 0 1 0 1797290158 38981632 8818 4294967295 134512640 135094434 3221224448 3221223108 134553497 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 9517 8818 145 145 0 9372 0
[pid=25196] vsize: 38068
Current children cumulated CPU time (s) 196.94
Current children cumulated vsize (Kb) 40192

[startup+211.3 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 9278 0 0 0 20641 50 0 0 25 0 1 0 1797290158 40030208 9085 4294967295 134512640 135094434 3221224448 3221223104 134557984 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 9773 9085 145 145 0 9628 0
[pid=25196] vsize: 39092
Current children cumulated CPU time (s) 206.91
Current children cumulated vsize (Kb) 41216

[startup+221.301 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 9446 0 0 0 21637 52 0 0 25 0 1 0 1797290158 40726528 9253 4294967295 134512640 135094434 3221224448 3221223104 134557964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 9943 9253 145 145 0 9798 0
[pid=25196] vsize: 39772
Current children cumulated CPU time (s) 216.89
Current children cumulated vsize (Kb) 41896

[startup+231.302 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 9629 0 0 0 22634 53 0 0 25 0 1 0 1797290158 41455616 9436 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 10121 9436 145 145 0 9976 0
[pid=25196] vsize: 40484
Current children cumulated CPU time (s) 226.87
Current children cumulated vsize (Kb) 42608

[startup+241.302 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 9905 0 0 0 23630 55 0 0 25 0 1 0 1797290158 42561536 9712 4294967295 134512640 135094434 3221224448 3221223104 134558208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 10391 9712 145 145 0 10246 0
[pid=25196] vsize: 41564
Current children cumulated CPU time (s) 236.85
Current children cumulated vsize (Kb) 43688

[startup+251.303 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 10243 0 0 0 24623 58 0 0 25 0 1 0 1797290158 43921408 10050 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 10723 10050 145 145 0 10578 0
[pid=25196] vsize: 42892
Current children cumulated CPU time (s) 246.81
Current children cumulated vsize (Kb) 45016

[startup+261.304 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 10395 0 0 0 25621 59 0 0 25 0 1 0 1797290158 44531712 10202 4294967295 134512640 135094434 3221224448 3221223120 134555399 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 10872 10202 145 145 0 10727 0
[pid=25196] vsize: 43488
Current children cumulated CPU time (s) 256.8
Current children cumulated vsize (Kb) 45612

[startup+271.305 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 10518 0 0 0 26618 60 0 0 25 0 1 0 1797290158 45023232 10325 4294967295 134512640 135094434 3221224448 3221223136 134554709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 10992 10325 145 145 0 10847 0
[pid=25196] vsize: 43968
Current children cumulated CPU time (s) 266.78
Current children cumulated vsize (Kb) 46092

[startup+281.305 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 10663 0 0 0 27615 61 0 0 25 0 1 0 1797290158 45608960 10470 4294967295 134512640 135094434 3221224448 3221223104 134557872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 11135 10470 145 145 0 10990 0
[pid=25196] vsize: 44540
Current children cumulated CPU time (s) 276.76
Current children cumulated vsize (Kb) 46664

[startup+291.307 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 10820 0 0 0 28613 62 0 0 25 0 1 0 1797290158 46243840 10627 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 11290 10627 145 145 0 11145 0
[pid=25196] vsize: 45160
Current children cumulated CPU time (s) 286.75
Current children cumulated vsize (Kb) 47284

[startup+301.308 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 11017 0 0 0 29609 64 0 0 25 0 1 0 1797290158 47042560 10824 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25196/statm): 11485 10824 145 145 0 11340 0
[pid=25196] vsize: 45940
Current children cumulated CPU time (s) 296.73
Current children cumulated vsize (Kb) 48064

[startup+311.309 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 11132 0 0 0 30607 65 0 0 25 0 1 0 1797290158 48037888 10939 4294967295 134512640 135094434 3221224448 3221223104 134558225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 11728 10939 145 145 0 11583 0
[pid=25196] vsize: 46912
Current children cumulated CPU time (s) 306.72
Current children cumulated vsize (Kb) 49036

[startup+321.309 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 11407 0 0 0 31602 66 0 0 25 0 1 0 1797290158 49139712 11214 4294967295 134512640 135094434 3221224448 3221223108 134553536 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 11997 11214 145 145 0 11852 0
[pid=25196] vsize: 47988
Current children cumulated CPU time (s) 316.68
Current children cumulated vsize (Kb) 50112

[startup+331.31 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 11562 0 0 0 32600 68 0 0 25 0 1 0 1797290158 49758208 11369 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 12148 11369 145 145 0 12003 0
[pid=25196] vsize: 48592
Current children cumulated CPU time (s) 326.68
Current children cumulated vsize (Kb) 50716

[startup+341.311 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 11722 0 0 0 33597 69 0 0 25 0 1 0 1797290158 50405376 11529 4294967295 134512640 135094434 3221224448 3221223072 134557604 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 12306 11529 145 145 0 12161 0
[pid=25196] vsize: 49224
Current children cumulated CPU time (s) 336.66
Current children cumulated vsize (Kb) 51348

[startup+351.312 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 11873 0 0 0 34595 70 0 0 25 0 1 0 1797290158 51023872 11680 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 12457 11680 145 145 0 12312 0
[pid=25196] vsize: 49828
Current children cumulated CPU time (s) 346.65
Current children cumulated vsize (Kb) 51952

[startup+361.312 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 12098 0 0 0 35591 71 0 0 25 0 1 0 1797290158 51924992 11905 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 12677 11905 145 145 0 12532 0
[pid=25196] vsize: 50708
Current children cumulated CPU time (s) 356.62
Current children cumulated vsize (Kb) 52832

[startup+371.313 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 12296 0 0 0 36587 74 0 0 25 0 1 0 1797290158 52723712 12103 4294967295 134512640 135094434 3221224448 3221223040 134556826 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 12872 12103 145 145 0 12727 0
[pid=25196] vsize: 51488
Current children cumulated CPU time (s) 366.61
Current children cumulated vsize (Kb) 53612

[startup+381.314 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 12486 0 0 0 37584 75 0 0 25 0 1 0 1797290158 53481472 12293 4294967295 134512640 135094434 3221224448 3221223088 134562098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 13057 12293 145 145 0 12912 0
[pid=25196] vsize: 52228
Current children cumulated CPU time (s) 376.59
Current children cumulated vsize (Kb) 54352

[startup+391.315 s]
Raw data (loadavg): 1.00 1.00 0.98 3/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 12683 0 0 0 38580 77 0 0 25 0 1 0 1797290158 54267904 12490 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 13249 12490 145 145 0 13104 0
[pid=25196] vsize: 52996
Current children cumulated CPU time (s) 386.57
Current children cumulated vsize (Kb) 55120

[startup+401.316 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 12867 0 0 0 39577 79 0 0 25 0 1 0 1797290158 55025664 12674 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 13434 12674 145 145 0 13289 0
[pid=25196] vsize: 53736
Current children cumulated CPU time (s) 396.56
Current children cumulated vsize (Kb) 55860

[startup+411.317 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 12994 0 0 0 40575 80 0 0 25 0 1 0 1797290158 55549952 12801 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 13562 12801 145 145 0 13417 0
[pid=25196] vsize: 54248
Current children cumulated CPU time (s) 406.55
Current children cumulated vsize (Kb) 56372

[startup+421.318 s]
Raw data (loadavg): 1.00 1.00 0.98 3/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 13136 0 0 0 41573 81 0 0 25 0 1 0 1797290158 56131584 12943 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 13704 12943 145 145 0 13559 0
[pid=25196] vsize: 54816
Current children cumulated CPU time (s) 416.54
Current children cumulated vsize (Kb) 56940

[startup+431.318 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 13258 0 0 0 42572 81 0 0 25 0 1 0 1797290158 56606720 13065 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 13820 13065 145 145 0 13675 0
[pid=25196] vsize: 55280
Current children cumulated CPU time (s) 426.53
Current children cumulated vsize (Kb) 57404

[startup+441.32 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 13404 0 0 0 43571 82 0 0 25 0 1 0 1797290158 57180160 13211 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 13960 13211 145 145 0 13815 0
[pid=25196] vsize: 55840
Current children cumulated CPU time (s) 436.53
Current children cumulated vsize (Kb) 57964

[startup+451.321 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 13580 0 0 0 44568 83 0 0 25 0 1 0 1797290158 57896960 13387 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 14135 13387 145 145 0 13990 0
[pid=25196] vsize: 56540
Current children cumulated CPU time (s) 446.51
Current children cumulated vsize (Kb) 58664

[startup+461.322 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) T 25192 25192 824 0 -1 0 13697 0 0 0 45566 84 0 0 25 0 1 0 1797290158 58388480 13504 4294967295 134512640 135094434 3221224448 3221222828 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/25196/statm): 14255 13504 145 145 0 14110 0
[pid=25196] vsize: 57020
Current children cumulated CPU time (s) 456.5
Current children cumulated vsize (Kb) 59144

[startup+471.322 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 13837 0 0 0 46562 86 0 0 25 0 1 0 1797290158 58953728 13644 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25196/statm): 14393 13644 145 145 0 14248 0
[pid=25196] vsize: 57572
Current children cumulated CPU time (s) 466.48
Current children cumulated vsize (Kb) 59696

[startup+481.323 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 13964 0 0 0 47559 87 0 0 25 0 1 0 1797290158 59465728 13771 4294967295 134512640 135094434 3221224448 3221223104 134558398 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25196/statm): 14518 13771 145 145 0 14373 0
[pid=25196] vsize: 58072
Current children cumulated CPU time (s) 476.46
Current children cumulated vsize (Kb) 60196

[startup+491.325 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 14086 0 0 0 48557 88 0 0 25 0 1 0 1797290158 59961344 13893 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 14639 13893 145 145 0 14494 0
[pid=25196] vsize: 58556
Current children cumulated CPU time (s) 486.45
Current children cumulated vsize (Kb) 60680

[startup+501.326 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 14238 0 0 0 49554 89 0 0 25 0 1 0 1797290158 60575744 14045 4294967295 134512640 135094434 3221224448 3221223072 134557734 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 14789 14045 145 145 0 14644 0
[pid=25196] vsize: 59156
Current children cumulated CPU time (s) 496.43
Current children cumulated vsize (Kb) 61280

[startup+511.326 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 14406 0 0 0 50552 90 0 0 25 0 1 0 1797290158 61247488 14213 4294967295 134512640 135094434 3221224448 3221223104 134558232 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 14953 14213 145 145 0 14808 0
[pid=25196] vsize: 59812
Current children cumulated CPU time (s) 506.42
Current children cumulated vsize (Kb) 61936

[startup+521.327 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 14545 0 0 0 51550 90 0 0 25 0 1 0 1797290158 61857792 14352 4294967295 134512640 135094434 3221224448 3221223104 134557900 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 15102 14352 145 145 0 14957 0
[pid=25196] vsize: 60408
Current children cumulated CPU time (s) 516.4
Current children cumulated vsize (Kb) 62532

[startup+531.328 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 14645 0 0 0 52549 91 0 0 25 0 1 0 1797290158 62267392 14452 4294967295 134512640 135094434 3221224448 3221223072 134557685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 15202 14452 145 145 0 15057 0
[pid=25196] vsize: 60808
Current children cumulated CPU time (s) 526.4
Current children cumulated vsize (Kb) 62932

[startup+541.329 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 14786 0 0 0 53547 92 0 0 25 0 1 0 1797290158 62840832 14593 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 15342 14593 145 145 0 15197 0
[pid=25196] vsize: 61368
Current children cumulated CPU time (s) 536.39
Current children cumulated vsize (Kb) 63492

[startup+551.329 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 14874 0 0 0 54545 93 0 0 25 0 1 0 1797290158 63180800 14681 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 15425 14681 145 145 0 15280 0
[pid=25196] vsize: 61700
Current children cumulated CPU time (s) 546.38
Current children cumulated vsize (Kb) 63824

[startup+561.33 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 14960 0 0 0 55544 93 0 0 25 0 1 0 1797290158 63524864 14767 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25196/statm): 15509 14767 145 145 0 15364 0
[pid=25196] vsize: 62036
Current children cumulated CPU time (s) 556.37
Current children cumulated vsize (Kb) 64160

[startup+571.331 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 15050 0 0 0 56542 95 0 0 25 0 1 0 1797290158 63909888 14857 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 15603 14857 145 145 0 15458 0
[pid=25196] vsize: 62412
Current children cumulated CPU time (s) 566.37
Current children cumulated vsize (Kb) 64536

[startup+581.332 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 15158 0 0 0 57540 95 0 0 25 0 1 0 1797290158 64335872 14965 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 15707 14965 145 145 0 15562 0
[pid=25196] vsize: 62828
Current children cumulated CPU time (s) 576.35
Current children cumulated vsize (Kb) 64952

[startup+591.332 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 15363 0 0 0 58537 97 0 0 25 0 1 0 1797290158 65159168 15170 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 15908 15170 145 145 0 15763 0
[pid=25196] vsize: 63632
Current children cumulated CPU time (s) 586.34
Current children cumulated vsize (Kb) 65756

[startup+601.333 s]
Raw data (loadavg): 1.00 1.00 0.98 1/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) T 25192 25192 824 0 -1 0 15606 0 0 0 59532 99 0 0 25 0 1 0 1797290158 66142208 15413 4294967295 134512640 135094434 3221224448 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/25196/statm): 16148 15413 145 145 0 16003 0
[pid=25196] vsize: 64592
Current children cumulated CPU time (s) 596.31
Current children cumulated vsize (Kb) 66716

[startup+611.334 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 15729 0 0 0 60530 99 0 0 25 0 1 0 1797290158 66650112 15536 4294967295 134512640 135094434 3221224448 3221223104 134557832 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 16272 15536 145 145 0 16127 0
[pid=25196] vsize: 65088
Current children cumulated CPU time (s) 606.29
Current children cumulated vsize (Kb) 67212

[startup+621.335 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 15860 0 0 0 61528 100 0 0 25 0 1 0 1797290158 67182592 15667 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 16402 15667 145 145 0 16257 0
[pid=25196] vsize: 65608
Current children cumulated CPU time (s) 616.28
Current children cumulated vsize (Kb) 67732

[startup+631.335 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 15961 0 0 0 62527 101 0 0 25 0 1 0 1797290158 67633152 15768 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 16512 15768 145 145 0 16367 0
[pid=25196] vsize: 66048
Current children cumulated CPU time (s) 626.28
Current children cumulated vsize (Kb) 68172

[startup+641.336 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 16070 0 0 0 63527 101 0 0 25 0 1 0 1797290158 68042752 15877 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 16612 15877 145 145 0 16467 0
[pid=25196] vsize: 66448
Current children cumulated CPU time (s) 636.28
Current children cumulated vsize (Kb) 68572

[startup+651.337 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 16180 0 0 0 64525 102 0 0 25 0 1 0 1797290158 68501504 15987 4294967295 134512640 135094434 3221224448 3221223040 134556802 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 16724 15987 145 145 0 16579 0
[pid=25196] vsize: 66896
Current children cumulated CPU time (s) 646.27
Current children cumulated vsize (Kb) 69020

[startup+661.336 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 16282 0 0 0 65524 103 0 0 25 0 1 0 1797290158 68902912 16089 4294967295 134512640 135094434 3221224448 3221223072 134557612 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 16822 16089 145 145 0 16677 0
[pid=25196] vsize: 67288
Current children cumulated CPU time (s) 656.27
Current children cumulated vsize (Kb) 69412

[startup+671.338 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 16383 0 0 0 66523 103 0 0 25 0 1 0 1797290158 69320704 16190 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 16924 16190 145 145 0 16779 0
[pid=25196] vsize: 67696
Current children cumulated CPU time (s) 666.26
Current children cumulated vsize (Kb) 69820

[startup+681.339 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 16480 0 0 0 67521 104 0 0 25 0 1 0 1797290158 69718016 16287 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 17021 16287 145 145 0 16876 0
[pid=25196] vsize: 68084
Current children cumulated CPU time (s) 676.25
Current children cumulated vsize (Kb) 70208

[startup+691.34 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 16639 0 0 0 68518 106 0 0 25 0 1 0 1797290158 70365184 16446 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 17179 16446 145 145 0 17034 0
[pid=25196] vsize: 68716
Current children cumulated CPU time (s) 686.24
Current children cumulated vsize (Kb) 70840

[startup+701.34 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 16809 0 0 0 69515 107 0 0 25 0 1 0 1797290158 71065600 16616 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 17350 16616 145 145 0 17205 0
[pid=25196] vsize: 69400
Current children cumulated CPU time (s) 696.22
Current children cumulated vsize (Kb) 71524

[startup+711.341 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 17003 0 0 0 70510 109 0 0 25 0 1 0 1797290158 71852032 16810 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 17542 16810 145 145 0 17397 0
[pid=25196] vsize: 70168
Current children cumulated CPU time (s) 706.19
Current children cumulated vsize (Kb) 72292

[startup+721.342 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 17100 0 0 0 71510 109 0 0 25 0 1 0 1797290158 72237056 16907 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 17636 16907 145 145 0 17491 0
[pid=25196] vsize: 70544
Current children cumulated CPU time (s) 716.19
Current children cumulated vsize (Kb) 72668

[startup+731.343 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 17206 0 0 0 72509 109 0 0 25 0 1 0 1797290158 73711616 17013 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 17996 17013 145 145 0 17851 0
[pid=25196] vsize: 71984
Current children cumulated CPU time (s) 726.18
Current children cumulated vsize (Kb) 74108

[startup+741.344 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 17316 0 0 0 73507 110 0 0 25 0 1 0 1797290158 74137600 17123 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 18100 17123 145 145 0 17955 0
[pid=25196] vsize: 72400
Current children cumulated CPU time (s) 736.17
Current children cumulated vsize (Kb) 74524

[startup+751.345 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 17397 0 0 0 74506 111 0 0 25 0 1 0 1797290158 74481664 17204 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 18184 17204 145 145 0 18039 0
[pid=25196] vsize: 72736
Current children cumulated CPU time (s) 746.17
Current children cumulated vsize (Kb) 74860

[startup+761.346 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 17483 0 0 0 75504 112 0 0 25 0 1 0 1797290158 74825728 17290 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 18268 17290 145 145 0 18123 0
[pid=25196] vsize: 73072
Current children cumulated CPU time (s) 756.16
Current children cumulated vsize (Kb) 75196

[startup+771.348 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 17579 0 0 0 76503 113 0 0 25 0 1 0 1797290158 75218944 17386 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 18364 17386 145 145 0 18219 0
[pid=25196] vsize: 73456
Current children cumulated CPU time (s) 766.16
Current children cumulated vsize (Kb) 75580

[startup+781.348 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 17684 0 0 0 77501 114 0 0 25 0 1 0 1797290158 75677696 17491 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 18476 17491 145 145 0 18331 0
[pid=25196] vsize: 73904
Current children cumulated CPU time (s) 776.15
Current children cumulated vsize (Kb) 76028

[startup+791.35 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 17776 0 0 0 78500 115 0 0 25 0 1 0 1797290158 76042240 17583 4294967295 134512640 135094434 3221224448 3221223060 134563046 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 18565 17583 145 145 0 18420 0
[pid=25196] vsize: 74260
Current children cumulated CPU time (s) 786.15
Current children cumulated vsize (Kb) 76384

[startup+801.351 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 17882 0 0 0 79498 115 0 0 25 0 1 0 1797290158 76464128 17689 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 18668 17689 145 145 0 18523 0
[pid=25196] vsize: 74672
Current children cumulated CPU time (s) 796.13
Current children cumulated vsize (Kb) 76796

[startup+811.352 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 17963 0 0 0 80496 116 0 0 25 0 1 0 1797290158 76779520 17770 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 18745 17770 145 145 0 18600 0
[pid=25196] vsize: 74980
Current children cumulated CPU time (s) 806.12
Current children cumulated vsize (Kb) 77104

[startup+821.352 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 18054 0 0 0 81496 117 0 0 25 0 1 0 1797290158 77172736 17861 4294967295 134512640 135094434 3221224448 3221223040 134557269 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 18841 17861 145 145 0 18696 0
[pid=25196] vsize: 75364
Current children cumulated CPU time (s) 816.13
Current children cumulated vsize (Kb) 77488

[startup+831.353 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 18111 0 0 0 82495 117 0 0 25 0 1 0 1797290158 77459456 17918 4294967295 134512640 135094434 3221224448 3221223104 134557937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 18911 17918 145 145 0 18766 0
[pid=25196] vsize: 75644
Current children cumulated CPU time (s) 826.12
Current children cumulated vsize (Kb) 77768

[startup+841.355 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 18184 0 0 0 83494 118 0 0 25 0 1 0 1797290158 77746176 17991 4294967295 134512640 135094434 3221224448 3221223040 134551434 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 18981 17991 145 145 0 18836 0
[pid=25196] vsize: 75924
Current children cumulated CPU time (s) 836.12
Current children cumulated vsize (Kb) 78048

[startup+851.356 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 18184 0 0 0 84495 118 0 0 25 0 1 0 1797290158 77746176 17991 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 18981 17991 145 145 0 18836 0
[pid=25196] vsize: 75924
Current children cumulated CPU time (s) 846.13
Current children cumulated vsize (Kb) 78048

[startup+861.356 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 18184 0 0 0 85495 118 0 0 25 0 1 0 1797290158 77746176 17991 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 18981 17991 145 145 0 18836 0
[pid=25196] vsize: 75924
Current children cumulated CPU time (s) 856.13
Current children cumulated vsize (Kb) 78048

[startup+871.357 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 18184 0 0 0 86494 118 0 0 25 0 1 0 1797290158 77746176 17991 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/25196/statm): 18981 17991 145 145 0 18836 0
[pid=25196] vsize: 75924
Current children cumulated CPU time (s) 866.12
Current children cumulated vsize (Kb) 78048

[startup+881.358 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 18184 0 0 0 87493 119 0 0 25 0 1 0 1797290158 77746176 17991 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 18981 17991 145 145 0 18836 0
[pid=25196] vsize: 75924
Current children cumulated CPU time (s) 876.12
Current children cumulated vsize (Kb) 78048

[startup+891.359 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 18184 0 0 0 88493 119 0 0 25 0 1 0 1797290158 77746176 17991 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 18981 17991 145 145 0 18836 0
[pid=25196] vsize: 75924
Current children cumulated CPU time (s) 886.12
Current children cumulated vsize (Kb) 78048

[startup+901.359 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 18184 0 0 0 89493 119 0 0 25 0 1 0 1797290158 77746176 17991 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 18981 17991 145 145 0 18836 0
[pid=25196] vsize: 75924
Current children cumulated CPU time (s) 896.12
Current children cumulated vsize (Kb) 78048

[startup+911.36 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 18184 0 0 0 90494 119 0 0 25 0 1 0 1797290158 77746176 17991 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 18981 17991 145 145 0 18836 0
[pid=25196] vsize: 75924
Current children cumulated CPU time (s) 906.13
Current children cumulated vsize (Kb) 78048

[startup+921.361 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 18184 0 0 0 91494 119 0 0 25 0 1 0 1797290158 77746176 17991 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 18981 17991 145 145 0 18836 0
[pid=25196] vsize: 75924
Current children cumulated CPU time (s) 916.13
Current children cumulated vsize (Kb) 78048

[startup+931.361 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 18184 0 0 0 92494 119 0 0 25 0 1 0 1797290158 77746176 17991 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 18981 17991 145 145 0 18836 0
[pid=25196] vsize: 75924
Current children cumulated CPU time (s) 926.13
Current children cumulated vsize (Kb) 78048

[startup+941.362 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 18185 0 0 0 93494 119 0 0 25 0 1 0 1797290158 77746176 17992 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 18981 17992 145 145 0 18836 0
[pid=25196] vsize: 75924
Current children cumulated CPU time (s) 936.13
Current children cumulated vsize (Kb) 78048

[startup+951.363 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 18185 0 0 0 94495 119 0 0 25 0 1 0 1797290158 77746176 17992 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 18981 17992 145 145 0 18836 0
[pid=25196] vsize: 75924
Current children cumulated CPU time (s) 946.14
Current children cumulated vsize (Kb) 78048

[startup+961.363 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 18185 0 0 0 95495 119 0 0 25 0 1 0 1797290158 77746176 17992 4294967295 134512640 135094434 3221224448 3221223060 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 18981 17992 145 145 0 18836 0
[pid=25196] vsize: 75924
Current children cumulated CPU time (s) 956.14
Current children cumulated vsize (Kb) 78048

[startup+971.363 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 18185 0 0 0 96495 119 0 0 25 0 1 0 1797290158 77746176 17992 4294967295 134512640 135094434 3221224448 3221223104 134557900 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 18981 17992 145 145 0 18836 0
[pid=25196] vsize: 75924
Current children cumulated CPU time (s) 966.14
Current children cumulated vsize (Kb) 78048

[startup+981.364 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 18187 0 0 0 97495 119 0 0 25 0 1 0 1797290158 77746176 17994 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 18981 17994 145 145 0 18836 0
[pid=25196] vsize: 75924
Current children cumulated CPU time (s) 976.14
Current children cumulated vsize (Kb) 78048

[startup+991.365 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 18197 0 0 0 98496 119 0 0 25 0 1 0 1797290158 77811712 18004 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 18997 18004 145 145 0 18852 0
[pid=25196] vsize: 75988
Current children cumulated CPU time (s) 986.15
Current children cumulated vsize (Kb) 78112

[startup+1001.37 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 18208 0 0 0 99496 119 0 0 25 0 1 0 1797290158 77877248 18015 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 19013 18015 145 145 0 18868 0
[pid=25196] vsize: 76052
Current children cumulated CPU time (s) 996.15
Current children cumulated vsize (Kb) 78176

[startup+1011.37 s]
Raw data (loadavg): 1.00 1.00 0.98 3/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 18218 0 0 0 100496 119 0 0 25 0 1 0 1797290158 77942784 18025 4294967295 134512640 135094434 3221224448 3221223040 134551757 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 19029 18025 145 145 0 18884 0
[pid=25196] vsize: 76116
Current children cumulated CPU time (s) 1006.15
Current children cumulated vsize (Kb) 78240

[startup+1021.37 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 18221 0 0 0 101496 119 0 0 25 0 1 0 1797290158 77942784 18028 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 19029 18028 145 145 0 18884 0
[pid=25196] vsize: 76116
Current children cumulated CPU time (s) 1016.15
Current children cumulated vsize (Kb) 78240

[startup+1031.37 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 18223 0 0 0 102497 119 0 0 25 0 1 0 1797290158 77942784 18030 4294967295 134512640 135094434 3221224448 3221223060 134563024 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 19029 18030 145 145 0 18884 0
[pid=25196] vsize: 76116
Current children cumulated CPU time (s) 1026.16
Current children cumulated vsize (Kb) 78240

[startup+1041.37 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 18224 0 0 0 103497 119 0 0 25 0 1 0 1797290158 77942784 18031 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 19029 18031 145 145 0 18884 0
[pid=25196] vsize: 76116
Current children cumulated CPU time (s) 1036.16
Current children cumulated vsize (Kb) 78240

[startup+1051.37 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 18224 0 0 0 104497 119 0 0 25 0 1 0 1797290158 77942784 18031 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 19029 18031 145 145 0 18884 0
[pid=25196] vsize: 76116
Current children cumulated CPU time (s) 1046.16
Current children cumulated vsize (Kb) 78240

[startup+1061.37 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 18224 0 0 0 105497 119 0 0 25 0 1 0 1797290158 77942784 18031 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 19029 18031 145 145 0 18884 0
[pid=25196] vsize: 76116
Current children cumulated CPU time (s) 1056.16
Current children cumulated vsize (Kb) 78240

[startup+1071.37 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 18224 0 0 0 106498 119 0 0 25 0 1 0 1797290158 77942784 18031 4294967295 134512640 135094434 3221224448 3221223120 134556517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 19029 18031 145 145 0 18884 0
[pid=25196] vsize: 76116
Current children cumulated CPU time (s) 1066.17
Current children cumulated vsize (Kb) 78240

[startup+1081.37 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 18224 0 0 0 107498 119 0 0 25 0 1 0 1797290158 77942784 18031 4294967295 134512640 135094434 3221224448 3221223104 134557914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 19029 18031 145 145 0 18884 0
[pid=25196] vsize: 76116
Current children cumulated CPU time (s) 1076.17
Current children cumulated vsize (Kb) 78240

[startup+1091.37 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 18224 0 0 0 108498 119 0 0 25 0 1 0 1797290158 77942784 18031 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 19029 18031 145 145 0 18884 0
[pid=25196] vsize: 76116
Current children cumulated CPU time (s) 1086.17
Current children cumulated vsize (Kb) 78240

[startup+1101.38 s]
Raw data (loadavg): 1.00 1.00 0.98 3/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 18224 0 0 0 109499 119 0 0 25 0 1 0 1797290158 77942784 18031 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 19029 18031 145 145 0 18884 0
[pid=25196] vsize: 76116
Current children cumulated CPU time (s) 1096.18
Current children cumulated vsize (Kb) 78240

[startup+1111.38 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 18224 0 0 0 110499 119 0 0 25 0 1 0 1797290158 77942784 18031 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 19029 18031 145 145 0 18884 0
[pid=25196] vsize: 76116
Current children cumulated CPU time (s) 1106.18
Current children cumulated vsize (Kb) 78240

[startup+1121.38 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 18224 0 0 0 111499 119 0 0 25 0 1 0 1797290158 77942784 18031 4294967295 134512640 135094434 3221224448 3221223080 134557561 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 19029 18031 145 145 0 18884 0
[pid=25196] vsize: 76116
Current children cumulated CPU time (s) 1116.18
Current children cumulated vsize (Kb) 78240

[startup+1131.38 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 18224 0 0 0 112499 119 0 0 25 0 1 0 1797290158 77942784 18031 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 19029 18031 145 145 0 18884 0
[pid=25196] vsize: 76116
Current children cumulated CPU time (s) 1126.18
Current children cumulated vsize (Kb) 78240

[startup+1141.38 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 18224 0 0 0 113500 119 0 0 25 0 1 0 1797290158 77942784 18031 4294967295 134512640 135094434 3221224448 3221223120 134555583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 19029 18031 145 145 0 18884 0
[pid=25196] vsize: 76116
Current children cumulated CPU time (s) 1136.19
Current children cumulated vsize (Kb) 78240

[startup+1151.38 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 18226 0 0 0 114500 119 0 0 25 0 1 0 1797290158 77942784 18033 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 19029 18033 145 145 0 18884 0
[pid=25196] vsize: 76116
Current children cumulated CPU time (s) 1146.19
Current children cumulated vsize (Kb) 78240

[startup+1161.38 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 18237 0 0 0 115500 119 0 0 25 0 1 0 1797290158 78008320 18044 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 19045 18044 145 145 0 18900 0
[pid=25196] vsize: 76180
Current children cumulated CPU time (s) 1156.19
Current children cumulated vsize (Kb) 78304

[startup+1171.38 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 18240 0 0 0 116500 119 0 0 25 0 1 0 1797290158 78008320 18047 4294967295 134512640 135094434 3221224448 3221223104 134558024 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 19045 18047 145 145 0 18900 0
[pid=25196] vsize: 76180
Current children cumulated CPU time (s) 1166.19
Current children cumulated vsize (Kb) 78304

[startup+1181.38 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 18252 0 0 0 117500 119 0 0 25 0 1 0 1797290158 78073856 18059 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 19061 18059 145 145 0 18916 0
[pid=25196] vsize: 76244
Current children cumulated CPU time (s) 1176.19
Current children cumulated vsize (Kb) 78368

[startup+1191.39 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 18263 0 0 0 118501 119 0 0 25 0 1 0 1797290158 78139392 18070 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 19077 18070 145 145 0 18932 0
[pid=25196] vsize: 76308
Current children cumulated CPU time (s) 1186.2
Current children cumulated vsize (Kb) 78432

[startup+1201.39 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 18266 0 0 0 119501 119 0 0 25 0 1 0 1797290158 78139392 18073 4294967295 134512640 135094434 3221224448 3221223104 134557860 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 19077 18073 145 145 0 18932 0
[pid=25196] vsize: 76308
Current children cumulated CPU time (s) 1196.2
Current children cumulated vsize (Kb) 78432

[startup+1211.39 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 18266 0 0 0 120501 119 0 0 25 0 1 0 1797290158 78139392 18073 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 19077 18073 145 145 0 18932 0
[pid=25196] vsize: 76308
Current children cumulated CPU time (s) 1206.2
Current children cumulated vsize (Kb) 78432



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1211.39 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 25196
Raw data (/proc/25192/stat): 25192 (minisat+_script) S 25191 25192 824 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797290153 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/25192/statm): 531 226 485 147 0 384 0
[pid=25192] vsize: 2124
Raw data (/proc/25196/stat): 25196 (minisat+_64-bit) R 25192 25192 824 0 -1 0 18266 0 0 0 120501 119 0 0 25 0 1 0 1797290158 78139392 18073 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/25196/statm): 19077 18073 145 145 0 18932 0
[pid=25196] vsize: 76308
Current children cumulated CPU time (s) 1206.2
Current children cumulated vsize (Kb) 78432

Sending SIGTERM to -25192
Sleeping 2 seconds
One traced child (pid=25192) ended because it received signal 15 (SIGTERM)
One traced child (pid=25196) exited with status: 0
All traced children have exited ! Game is over.

Child status: 0
Real time (s): 1211.43
CPU time (s): 1206.25
CPU user time (s): 1205.02
CPU system time (s): 1.23281
CPU usage (%): 99.5726
Max. virtual memory (cumulated for all children) (Kb): 78432

Verifier Data

ERROR: no interpretation found !