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-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-vpm2.opb
MD5SUM766b2fe57cb2084b069363491485612e
Bench Categoryoptimization, medium integers (OPTMEDINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 134
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 16000000
Number of bits of the biggest number in a constraint 24
Biggest sum of numbers in a constraint 241094849
Number of bits of the biggest sum of numbers28
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1189.02
Number of variables2754
Total number of constraints444
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints444
Minimum length of a constraint11
Maximum length of a constraint84

Trace number 4552

Launcher Data

LAUNCH ON wulflinc29 THE 2005-09-19 18:16:55 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3014 boxname=wulflinc29 idbench=670 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  766b2fe57cb2084b069363491485612e  /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-20-10-vpm2.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-20-10-vpm2.opb
IDLAUNCH: 3014
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.020
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	: 3
cpu MHz		: 451.020
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:        922584 kB
Buffers:         18852 kB
Cached:          64044 kB
SwapCached:        676 kB
Active:           9620 kB
Inactive:        75752 kB
HighTotal:      131008 kB
HighFree:        63756 kB
LowTotal:       903652 kB
LowFree:        858828 kB
SwapTotal:     2097892 kB
SwapFree:      2096528 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5704 kB
Slab:            21020 kB
Committed_AS:    64132 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-19 18:37:06 (client local time) WITH STATUS 0 IN 1208.64 SECONDS
stats: 3014 7 1208.64 0

Solver Data

c Parsing PB file...
c Converting 486 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: ##############################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 485]---> BDD-cost:   10
c ---[ 484]---> BDD-cost:   10
c ---[ 483]---> BDD-cost:   10
c ---[ 482]---> BDD-cost:   10
c ---[ 481]---> BDD-cost:   10
c ---[ 480]---> BDD-cost:   10
c ---[ 479]---> BDD-cost:   10
c ---[ 478]---> BDD-cost:   10
c ---[ 477]---> BDD-cost:   10
c ---[ 474]---> BDD-cost:   10
c ---[ 473]---> BDD-cost:   10
c ---[ 472]---> BDD-cost:   10
c ---[ 471]---> BDD-cost:   10
c ---[ 468]---> BDD-cost:   10
c ---[ 467]---> BDD-cost:   10
c ---[ 466]---> BDD-cost:   10
c ---[ 465]---> BDD-cost:   10
c ---[ 462]---> BDD-cost:   10
c ---[ 459]---> BDD-cost:   10
c ---[ 458]---> BDD-cost:   10
c ---[ 457]---> BDD-cost:   10
c ---[ 454]---> BDD-cost:   10
c ---[ 453]---> BDD-cost:   10
c ---[ 452]---> BDD-cost:   10
c ---[ 451]---> BDD-cost:   10
c ---[ 450]---> BDD-cost:   10
c ---[ 448]---> BDD-cost:   10
c ---[ 447]---> BDD-cost:   10
c ---[ 446]---> BDD-cost:   10
c ---[ 445]---> BDD-cost:   10
c ---[ 444]---> BDD-cost:   10
c ---[ 441]---> BDD-cost:   10
c ---[ 440]---> BDD-cost:   10
c ---[ 439]---> BDD-cost:   10
c ---[ 433]---> BDD-cost:   10
c ---[ 427]---> BDD-cost:   10
c ---[ 422]---> BDD-cost:   10
c ---[ 421]---> BDD-cost:   10
c ---[ 415]---> BDD-cost:   10
c ---[ 409]---> BDD-cost:   10
c ---[ 408]---> BDD-cost:   10
c ---[ 402]---> BDD-cost:   10
c ---[ 397]---> BDD-cost:   10
c ---[ 396]---> BDD-cost:   10
c ---[ 391]---> BDD-cost:   10
c ---[ 390]---> BDD-cost:   10
c ---[ 386]---> BDD-cost:   10
c ---[ 385]---> BDD-cost:   10
c ---[ 384]---> BDD-cost:   10
c ---[ 380]---> BDD-cost:   10
c ---[ 379]---> BDD-cost:   10
c ---[ 378]---> BDD-cost:   10
c ---[ 374]---> BDD-cost:   10
c ---[ 373]---> BDD-cost:   10
c ---[ 372]---> BDD-cost:   10
c ---[ 368]---> BDD-cost:   10
c ---[ 367]---> BDD-cost:   10
c ---[ 366]---> BDD-cost:   10
c ---[ 365]---> BDD-cost:   10
c ---[ 364]---> BDD-cost:   10
c ---[ 359]---> BDD-cost:   10
c ---[ 353]---> BDD-cost:   10
c ---[ 347]---> BDD-cost:   10
c ---[ 339]---> BDD-cost:   10
c ---[ 333]---> BDD-cost:   10
c ---[ 327]---> BDD-cost:   10
c ---[ 321]---> BDD-cost:   10
c ---[ 317]---> BDD-cost:   17
c ---[ 316]---> BDD-cost:   17
c ---[ 315]---> BDD-cost:   17
c ---[ 314]---> BDD-cost:   17
c ---[ 313]---> BDD-cost:   17
c ---[ 312]---> BDD-cost:   17
c ---[ 310]---> BDD-cost:   17
c ---[ 309]---> BDD-cost:   17
c ---[ 308]---> BDD-cost:   17
c ---[ 307]---> BDD-cost:   17
c ---[ 306]---> BDD-cost:   17
c ---[ 302]---> BDD-cost:   16
c ---[ 301]---> BDD-cost:   16
c ---[ 300]---> BDD-cost:   16
c ---[ 295]---> BDD-cost:   16
c ---[ 294]---> BDD-cost:   16
c ---[ 290]---> BDD-cost:   18
c ---[ 289]---> BDD-cost:   18
c ---[ 288]---> BDD-cost:   18
c ---[ 287]---> BDD-cost:   16
c ---[ 286]---> BDD-cost:   16
c ---[ 285]---> BDD-cost:   16
c ---[ 284]---> BDD-cost:   16
c ---[ 283]---> BDD-cost:   16
c ---[ 282]---> BDD-cost:   16
c ---[ 280]---> BDD-cost:   16
c ---[ 279]---> BDD-cost:   16
c ---[ 278]---> BDD-cost:   16
c ---[ 277]---> BDD-cost:   16
c ---[ 276]---> BDD-cost:   16
c ---[ 274]---> Sorter-cost: 3227     Base: 2 2 2 5 5 2 2 2 2 2 2 2 2 3
c ---[ 264]---> Sorter-cost: 3277     Base: 2 2 2 5 5 2 2 2 2 2 2 3 2 2 2
c ---[ 260]---> Adder-cost: 352   maxlim: 2411343   bits: 22/22
c ---[ 258]---> Adder-cost: 352   maxlim: 2411343   bits: 22/22
c ---[ 256]---> Adder-cost: 330   maxlim: 1694543   bits: 21/21
c ---[ 254]---> Adder-cost: 330   maxlim: 1694543   bits: 21/21
c ---[ 252]---> Adder-cost: 352   maxlim: 2104143   bits: 22/22
c ---[ 250]---> Sorter-cost: 2487     Base: 2 2 2 2 2 2 2 2 5 5 2 2 2 2
c ---[ 248]---> Adder-cost: 304   maxlim: 2309043   bits: 22/22
c ---[ 246]---> Adder-cost: 304   maxlim: 2104243   bits: 22/22
c ---[ 244]---> Adder-cost: 304   maxlim: 2104243   bits: 22/22
c ---[ 242]---> Adder-cost: 288   maxlim: 1694643   bits: 21/21
c ---[ 236]---> Sorter-cost: 2294     Base: 2 2 2 2 5 5 2 2 2 2 2 2 2 2
c ---[ 234]---> Adder-cost: 312   maxlim: 2587171   bits: 22/22
c ---[ 232]---> Adder-cost: 260   maxlim: 897571   bits: 20/20
c ---[ 224]---> Sorter-cost: 2815     Base: 2 2 2 5 5 2 2 2 2 2 2 2 2 3
c ---[ 222]---> Adder-cost: 350   maxlim: 1768271   bits: 22/21
c ---[ 216]---> Adder-cost: 274   maxlim: 1228100   bits: 21/21
c ---[ 214]---> Adder-cost: 312   maxlim: 1957187   bits: 22/21
c ---[ 212]---> Adder-cost: 312   maxlim: 1854787   bits: 22/21
c ---[ 210]---> Adder-cost: 390   maxlim: 2279471   bits: 22/22
c ---[ 208]---> Adder-cost: 332   maxlim: 845871   bits: 20/20
c ---[ 206]---> Adder-cost: 332   maxlim: 845871   bits: 20/20
c ---[ 204]---> Adder-cost: 332   maxlim: 845871   bits: 20/20
c ---[ 202]---> Adder-cost: 332   maxlim: 845871   bits: 20/20
c ---[ 200]---> Sorter-cost: 3241     Base: 2 2 2 2 5 5 2 2 2 2 2 2 5
c ---[ 198]---> Adder-cost: 440   maxlim: 3713071   bits: 23/22
c ---[ 196]---> Adder-cost: 368   maxlim: 999471   bits: 21/20
c ---[ 194]---> Adder-cost: 368   maxlim: 999471   bits: 21/20
c ---[ 192]---> Adder-cost: 368   maxlim: 999471   bits: 21/20
c ---[ 191]---> BDD-cost:  237
c ---[ 190]---> BDD-cost:  601
c ---[ 189]---> BDD-cost:  600
c ---[ 188]---> BDD-cost: 1143
c ---[ 187]---> BDD-cost: 1480
c ---[ 186]---> BDD-cost: 1473
c ---[ 185]---> BDD-cost:  273
c ---[ 184]---> BDD-cost:  768
c ---[ 183]---> BDD-cost:  767
c ---[ 182]---> Sorter-cost: 2073     Base: 5 5 5 2 2 5 5 2 2 2 2 2 2 2
c ---[ 181]---> Sorter-cost: 2696     Base: 5 5 5 2 2 5 5 2 2 2 2 2 2 2
c ---[ 180]---> Sorter-cost: 2700     Base: 5 5 5 2 2 5 5 2 2 2 2 2 2 2
c ---[ 179]---> Sorter-cost:  446     Base: 2 2 2 2 2 2 2 2 2 5
c ---[ 178]---> Sorter-cost: 1242     Base: 2 2 2 2 2 5 2 2 2 2
c ---[ 177]---> Sorter-cost: 1199     Base: 2 2 2 2 2 2 2 2 2 5
c ---[ 176]---> Sorter-cost: 1719     Base: 5 2 2 2 2 2 2 2 2 2
c ---[ 175]---> Sorter-cost: 2067     Base: 5 2 2 2 2 2 2 2 2 2
c ---[ 174]---> Sorter-cost: 2045     Base: 5 2 2 2 2 2 2 2 2 2
c ---[ 173]---> Sorter-cost:  223     Base: 2 2 2 2 2 2 2 2 2
c ---[ 172]---> Sorter-cost:  590     Base: 2 2 2 2 2 2 2 2
c ---[ 171]---> Sorter-cost:  538     Base: 2 2 2 2 2 2 2 2 2
c ---[ 170]---> Sorter-cost: 1025     Base: 2 2 2 2 2 2 2 2
c ---[ 169]---> Sorter-cost: 1211     Base: 2 2 2 2 2 2 2 2 2
c ---[ 168]---> Sorter-cost: 1390     Base: 2 2 2 2 2 2 2 2
c ---[ 167]---> BDD-cost:    3
c ---[ 166]---> BDD-cost:    3
c ---[ 165]---> BDD-cost:    3
c ---[ 164]---> BDD-cost:    3
c ---[ 163]---> BDD-cost:    3
c ---[ 162]---> BDD-cost:    3
c ---[ 161]---> BDD-cost:    3
c ---[ 160]---> BDD-cost:    3
c ---[ 159]---> BDD-cost:    3
c ---[ 158]---> BDD-cost:   10
c ---[ 157]---> BDD-cost:   10
c ---[ 156]---> BDD-cost:    3
c ---[ 155]---> BDD-cost:    3
c ---[ 154]---> BDD-cost:    3
c ---[ 153]---> BDD-cost:    3
c ---[ 152]---> BDD-cost:   10
c ---[ 151]---> BDD-cost:   10
c ---[ 150]---> BDD-cost:    3
c ---[ 149]---> BDD-cost:    3
c ---[ 148]---> BDD-cost:    3
c ---[ 147]---> BDD-cost:    3
c ---[ 146]---> BDD-cost:   10
c ---[ 145]---> BDD-cost:   10
c ---[ 144]---> BDD-cost:    3
c ---[ 142]---> BDD-cost:   10
c ---[ 141]---> BDD-cost:    3
c ---[ 140]---> BDD-cost:    3
c ---[ 139]---> BDD-cost:    3
c ---[ 138]---> BDD-cost:   10
c ---[ 136]---> BDD-cost:    3
c ---[ 135]---> BDD-cost:    3
c ---[ 134]---> BDD-cost:    3
c ---[ 133]---> BDD-cost:    3
c ---[ 132]---> BDD-cost:    3
c ---[ 130]---> BDD-cost:    3
c ---[ 129]---> BDD-cost:    3
c ---[ 128]---> BDD-cost:    3
c ---[ 127]---> BDD-cost:    3
c ---[ 126]---> BDD-cost:    3
c ---[ 124]---> BDD-cost:   10
c ---[ 123]---> BDD-cost:    3
c ---[ 122]---> BDD-cost:    3
c ---[ 121]---> BDD-cost:    3
c ---[ 120]---> BDD-cost:   10
c ---[ 116]---> BDD-cost:   10
c ---[ 115]---> BDD-cost:    3
c ---[ 114]---> BDD-cost:    9
c ---[ 110]---> BDD-cost:   10
c ---[ 109]---> BDD-cost:    3
c ---[ 108]---> BDD-cost:    9
c ---[ 104]---> BDD-cost:    3
c ---[ 103]---> BDD-cost:    3
c ---[ 102]---> BDD-cost:    9
c ---[  98]---> BDD-cost:   10
c ---[  97]---> BDD-cost:    3
c ---[  96]---> BDD-cost:    9
c ---[  91]---> BDD-cost:    3
c ---[  90]---> BDD-cost:    3
c ---[  85]---> BDD-cost:   10
c ---[  84]---> BDD-cost:    3
c ---[  79]---> BDD-cost:    3
c ---[  78]---> BDD-cost:    3
c ---[  73]---> BDD-cost:    3
c ---[  72]---> BDD-cost:    3
c ---[  68]---> BDD-cost:    3
c ---[  67]---> BDD-cost:    3
c ---[  66]---> BDD-cost:    3
c ---[  62]---> BDD-cost:    3
c ---[  61]---> BDD-cost:    3
c ---[  60]---> BDD-cost:    3
c ---[  56]---> BDD-cost:    3
c ---[  55]---> BDD-cost:    3
c ---[  54]---> BDD-cost:    3
c ---[  50]---> BDD-cost:    3
c ---[  49]---> BDD-cost:    3
c ---[  48]---> BDD-cost:    3
c ---[  47]---> BDD-cost:    3
c ---[  46]---> BDD-cost:    3
c ---[  45]---> BDD-cost:    9
c ---[  44]---> BDD-cost:    9
c ---[  43]---> BDD-cost:    9
c ---[  42]---> BDD-cost:    9
c ---[  41]---> BDD-cost:    3
c ---[  40]---> BDD-cost:   10
c ---[  39]---> BDD-cost:    9
c ---[  38]---> BDD-cost:    9
c ---[  37]---> BDD-cost:    9
c ---[  36]---> BDD-cost:    9
c ---[  35]---> BDD-cost:    3
c ---[  34]---> BDD-cost:   10
c ---[  33]---> BDD-cost:    8
c ---[  32]---> BDD-cost:    8
c ---[  31]---> BDD-cost:    8
c ---[  30]---> BDD-cost:    8
c ---[  29]---> BDD-cost:    3
c ---[  28]---> BDD-cost:   10
c ---[  27]---> BDD-cost:    8
c ---[  26]---> BDD-cost:    8
c ---[  25]---> BDD-cost:    8
c ---[  24]---> BDD-cost:    8
c ---[  22]---> BDD-cost:   10
c ---[  21]---> BDD-cost:    3
c ---[  20]---> BDD-cost:    9
c ---[  19]---> BDD-cost:    9
c ---[  18]---> BDD-cost:    9
c ---[  16]---> BDD-cost:   10
c ---[  15]---> BDD-cost:    3
c ---[  14]---> BDD-cost:    9
c ---[  13]---> BDD-cost:    9
c ---[  12]---> BDD-cost:    9
c ---[  10]---> BDD-cost:   10
c ---[   9]---> BDD-cost:    3
c ---[   8]---> BDD-cost:    9
c ---[   7]---> BDD-cost:    9
c ---[   6]---> BDD-cost:    9
c ---[   4]---> BDD-cost:    9
c ---[   3]---> BDD-cost:    3
c ---[   2]---> BDD-cost:    8
c ---[   1]---> BDD-cost:    8
c ---[   0]---> BDD-cost:    8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  167213   465118 |   55737       0        0     nan |  0.000 % |
c |       102 |  167213   465118 |   61310     102      580     5.7 |  5.110 % |
c |       252 |  166973   464554 |   67441     189      999     5.3 |  5.244 % |
c |       477 |  166912   464418 |   74185     411     2337     5.7 |  5.273 % |
c |       814 |  166606   463699 |   81604     735     4347     5.9 |  5.435 % |
c |      1322 |  166527   463521 |   89764    1240    14794    11.9 |  5.476 % |
c |      2081 |  166371   463159 |   98741    1994    21643    10.9 |  5.558 % |
c |      3220 |  166045   462422 |  108615    3112    33915    10.9 |  5.725 % |
c |      4929 |  165826   461801 |  119477    4808    57617    12.0 |  5.799 % |
c |      7493 |  165693   461496 |  131424    7365    86799    11.8 |  5.870 % |
c |     11338 |  165494   460951 |  144567   11190   131163    11.7 |  5.947 % |
c |     17105 |  165168   460173 |  159024   16924   215924    12.8 |  6.097 % |
c |     25754 |  164818   459233 |  174926   25507   353203    13.8 |  6.261 % |
c |     38728 |  164449   458053 |  192419   38460   738323    19.2 |  6.357 % |
c |     58190 |  164278   457631 |  211661   57893  1445394    25.0 |  6.442 % |
c |     87382 |  164096   457212 |  232827   87033  2420180    27.8 |  6.538 % |
c |    131172 |  163430   455605 |  256110  130764  3938028    30.1 |  6.886 % |
c |    196856 |  162754   453807 |  281721  196284  6594143    33.6 |  7.190 % |
c |    295383 |  162364   452716 |  309893   26455   639951    24.2 |  7.366 % |
c |    443172 |  162002   451790 |  340882  174183  5391858    31.0 |  7.551 % |

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/30442/stat): 30442 (minisat+_script) R 30441 30442 19818 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1851977985 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/30442/statm): 174 3 169 147 0 27 0
[pid=30442] 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=30443
New process pid=30444
New process pid=30445
execve syscall for /bin/sed executable
One traced child (pid=30444) 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=30445) exited with status: 0
One traced child (pid=30443) exited with status: 0
New process pid=30446
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-20-10-vpm2.opb

[startup+10.0029 s]
Raw data (loadavg): 0.93 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 2560 0 0 0 978 8 0 0 24 0 1 0 1851977990 11038720 2411 4294967295 134512640 135094434 3221224432 3221218352 134562504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30446/statm): 2695 2411 145 145 0 2550 0
[pid=30446] vsize: 10780
Current children cumulated CPU time (s) 9.88
Current children cumulated vsize (Kb) 12904

[startup+20.0047 s]
Raw data (loadavg): 0.94 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 4906 0 0 0 1954 20 0 0 25 0 1 0 1851977990 20934656 4742 4294967295 134512640 135094434 3221224432 3221223056 134562057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30446/statm): 5111 4742 145 145 0 4966 0
[pid=30446] vsize: 20444
Current children cumulated CPU time (s) 19.76
Current children cumulated vsize (Kb) 22568

[startup+30.0055 s]
Raw data (loadavg): 0.95 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 5270 0 0 0 2948 22 0 0 25 0 1 0 1851977990 22433792 5106 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30446/statm): 5477 5106 145 145 0 5332 0
[pid=30446] vsize: 21908
Current children cumulated CPU time (s) 29.72
Current children cumulated vsize (Kb) 24032

[startup+40.0072 s]
Raw data (loadavg): 0.96 0.97 0.91 1/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) T 30442 30442 19818 0 -1 0 5668 0 0 0 3942 25 0 0 25 0 1 0 1851977990 24150016 5504 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/30446/statm): 5896 5504 145 145 0 5751 0
[pid=30446] vsize: 23584
Current children cumulated CPU time (s) 39.69
Current children cumulated vsize (Kb) 25708

[startup+50.008 s]
Raw data (loadavg): 0.96 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 6124 0 0 0 4934 28 0 0 25 0 1 0 1851977990 25976832 5960 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30446/statm): 6342 5960 145 145 0 6197 0
[pid=30446] vsize: 25368
Current children cumulated CPU time (s) 49.64
Current children cumulated vsize (Kb) 27492

[startup+60.0088 s]
Raw data (loadavg): 0.97 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 6547 0 0 0 5926 31 0 0 25 0 1 0 1851977990 27672576 6383 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30446/statm): 6756 6383 145 145 0 6611 0
[pid=30446] vsize: 27024
Current children cumulated CPU time (s) 59.59
Current children cumulated vsize (Kb) 29148

[startup+70.0096 s]
Raw data (loadavg): 0.97 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 6901 0 0 0 6920 34 0 0 25 0 1 0 1851977990 29097984 6737 4294967295 134512640 135094434 3221224432 3221223088 134557856 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30446/statm): 7104 6737 145 145 0 6959 0
[pid=30446] vsize: 28416
Current children cumulated CPU time (s) 69.56
Current children cumulated vsize (Kb) 30540

[startup+80.0104 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 7232 0 0 0 7913 36 0 0 25 0 1 0 1851977990 30707712 7068 4294967295 134512640 135094434 3221224432 3221223088 134557920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30446/statm): 7497 7068 145 145 0 7352 0
[pid=30446] vsize: 29988
Current children cumulated CPU time (s) 79.51
Current children cumulated vsize (Kb) 32112

[startup+90.0112 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 7535 0 0 0 8907 39 0 0 25 0 1 0 1851977990 31928320 7371 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30446/statm): 7795 7371 145 145 0 7650 0
[pid=30446] vsize: 31180
Current children cumulated CPU time (s) 89.48
Current children cumulated vsize (Kb) 33304

[startup+100.013 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 7792 0 0 0 9903 41 0 0 25 0 1 0 1851977990 32956416 7628 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30446/statm): 8046 7628 145 145 0 7901 0
[pid=30446] vsize: 32184
Current children cumulated CPU time (s) 99.46
Current children cumulated vsize (Kb) 34308

[startup+110.014 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 8023 0 0 0 10899 42 0 0 25 0 1 0 1851977990 33878016 7859 4294967295 134512640 135094434 3221224432 3221223088 134557920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30446/statm): 8271 7859 145 145 0 8126 0
[pid=30446] vsize: 33084
Current children cumulated CPU time (s) 109.43
Current children cumulated vsize (Kb) 35208

[startup+120.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 8286 0 0 0 11894 45 0 0 25 0 1 0 1851977990 34951168 8122 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30446/statm): 8533 8122 145 145 0 8388 0
[pid=30446] vsize: 34132
Current children cumulated CPU time (s) 119.41
Current children cumulated vsize (Kb) 36256

[startup+130.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 8571 0 0 0 12890 48 0 0 25 0 1 0 1851977990 36085760 8407 4294967295 134512640 135094434 3221224432 3221223088 134557945 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30446/statm): 8810 8407 145 145 0 8665 0
[pid=30446] vsize: 35240
Current children cumulated CPU time (s) 129.4
Current children cumulated vsize (Kb) 37364

[startup+140.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 8849 0 0 0 13885 50 0 0 25 0 1 0 1851977990 37212160 8685 4294967295 134512640 135094434 3221224432 3221223100 134562036 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30446/statm): 9085 8685 145 145 0 8940 0
[pid=30446] vsize: 36340
Current children cumulated CPU time (s) 139.37
Current children cumulated vsize (Kb) 38464

[startup+150.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 9049 0 0 0 14881 52 0 0 25 0 1 0 1851977990 38010880 8885 4294967295 134512640 135094434 3221224432 3221223088 134558024 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30446/statm): 9280 8885 145 145 0 9135 0
[pid=30446] vsize: 37120
Current children cumulated CPU time (s) 149.35
Current children cumulated vsize (Kb) 39244

[startup+160.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 9305 0 0 0 15877 54 0 0 25 0 1 0 1851977990 39026688 9141 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30446/statm): 9528 9141 145 145 0 9383 0
[pid=30446] vsize: 38112
Current children cumulated CPU time (s) 159.33
Current children cumulated vsize (Kb) 40236

[startup+170.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 9523 0 0 0 16874 56 0 0 25 0 1 0 1851977990 39911424 9359 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30446/statm): 9744 9359 145 145 0 9599 0
[pid=30446] vsize: 38976
Current children cumulated CPU time (s) 169.32
Current children cumulated vsize (Kb) 41100

[startup+180.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 9716 0 0 0 17870 57 0 0 25 0 1 0 1851977990 40701952 9552 4294967295 134512640 135094434 3221224432 3221223088 134557893 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30446/statm): 9937 9552 145 145 0 9792 0
[pid=30446] vsize: 39748
Current children cumulated CPU time (s) 179.29
Current children cumulated vsize (Kb) 41872

[startup+190.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 9919 0 0 0 18867 59 0 0 25 0 1 0 1851977990 41525248 9755 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30446/statm): 10138 9755 145 145 0 9993 0
[pid=30446] vsize: 40552
Current children cumulated CPU time (s) 189.28
Current children cumulated vsize (Kb) 42676

[startup+200.023 s]
Raw data (loadavg): 0.99 0.97 0.91 1/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) T 30442 30442 19818 0 -1 0 10152 0 0 0 19863 61 0 0 25 0 1 0 1851977990 42987520 9988 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/30446/statm): 10495 9988 145 145 0 10350 0
[pid=30446] vsize: 41980
Current children cumulated CPU time (s) 199.26
Current children cumulated vsize (Kb) 44104

[startup+210.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 10315 0 0 0 20860 62 0 0 25 0 1 0 1851977990 43679744 10151 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30446/statm): 10664 10151 145 145 0 10519 0
[pid=30446] vsize: 42656
Current children cumulated CPU time (s) 209.24
Current children cumulated vsize (Kb) 44780

[startup+220.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 10489 0 0 0 21858 63 0 0 25 0 1 0 1851977990 44392448 10325 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30446/statm): 10838 10325 145 145 0 10693 0
[pid=30446] vsize: 43352
Current children cumulated CPU time (s) 219.23
Current children cumulated vsize (Kb) 45476

[startup+230.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 10726 0 0 0 22853 65 0 0 25 0 1 0 1851977990 45338624 10562 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30446/statm): 11069 10562 145 145 0 10924 0
[pid=30446] vsize: 44276
Current children cumulated CPU time (s) 229.2
Current children cumulated vsize (Kb) 46400

[startup+240.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 10911 0 0 0 23850 67 0 0 25 0 1 0 1851977990 46104576 10747 4294967295 134512640 135094434 3221224432 3221223056 134557636 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30446/statm): 11256 10747 145 145 0 11111 0
[pid=30446] vsize: 45024
Current children cumulated CPU time (s) 239.19
Current children cumulated vsize (Kb) 47148

[startup+250.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 11209 0 0 0 24846 69 0 0 25 0 1 0 1851977990 47316992 11045 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30446/statm): 11552 11045 145 145 0 11407 0
[pid=30446] vsize: 46208
Current children cumulated CPU time (s) 249.17
Current children cumulated vsize (Kb) 48332

[startup+260.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 11520 0 0 0 25840 71 0 0 25 0 1 0 1851977990 48590848 11356 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30446/statm): 11863 11356 145 145 0 11718 0
[pid=30446] vsize: 47452
Current children cumulated CPU time (s) 259.13
Current children cumulated vsize (Kb) 49576

[startup+270.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 11800 0 0 0 26835 73 0 0 25 0 1 0 1851977990 49717248 11636 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30446/statm): 12138 11636 145 145 0 11993 0
[pid=30446] vsize: 48552
Current children cumulated CPU time (s) 269.1
Current children cumulated vsize (Kb) 50676

[startup+280.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 12057 0 0 0 27831 75 0 0 25 0 1 0 1851977990 50749440 11893 4294967295 134512640 135094434 3221224432 3221223024 134556826 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30446/statm): 12390 11893 145 145 0 12245 0
[pid=30446] vsize: 49560
Current children cumulated CPU time (s) 279.08
Current children cumulated vsize (Kb) 51684

[startup+290.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 12390 0 0 0 28824 78 0 0 25 0 1 0 1851977990 52092928 12226 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30446/statm): 12718 12226 145 145 0 12573 0
[pid=30446] vsize: 50872
Current children cumulated CPU time (s) 289.04
Current children cumulated vsize (Kb) 52996

[startup+300.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 12640 0 0 0 29820 79 0 0 25 0 1 0 1851977990 53100544 12476 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30446/statm): 12964 12476 145 145 0 12819 0
[pid=30446] vsize: 51856
Current children cumulated CPU time (s) 299.01
Current children cumulated vsize (Kb) 53980

[startup+310.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 12820 0 0 0 30816 81 0 0 25 0 1 0 1851977990 53813248 12656 4294967295 134512640 135094434 3221224432 3221223088 134558426 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30446/statm): 13138 12656 145 145 0 12993 0
[pid=30446] vsize: 52552
Current children cumulated CPU time (s) 308.99
Current children cumulated vsize (Kb) 54676

[startup+320.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 12981 0 0 0 31812 84 0 0 25 0 1 0 1851977990 54452224 12817 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30446/statm): 13294 12817 145 145 0 13149 0
[pid=30446] vsize: 53176
Current children cumulated CPU time (s) 318.98
Current children cumulated vsize (Kb) 55300

[startup+330.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 13230 0 0 0 32807 86 0 0 25 0 1 0 1851977990 55468032 13066 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30446/statm): 13542 13066 145 145 0 13397 0
[pid=30446] vsize: 54168
Current children cumulated CPU time (s) 328.95
Current children cumulated vsize (Kb) 56292

[startup+340.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 13440 0 0 0 33803 88 0 0 25 0 1 0 1851977990 56315904 13276 4294967295 134512640 135094434 3221224432 3221223024 134557297 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30446/statm): 13749 13276 145 145 0 13604 0
[pid=30446] vsize: 54996
Current children cumulated CPU time (s) 338.93
Current children cumulated vsize (Kb) 57120

[startup+350.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 13585 0 0 0 34800 89 0 0 25 0 1 0 1851977990 56901632 13421 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30446/statm): 13892 13421 145 145 0 13747 0
[pid=30446] vsize: 55568
Current children cumulated CPU time (s) 348.91
Current children cumulated vsize (Kb) 57692

[startup+360.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 13722 0 0 0 35798 90 0 0 25 0 1 0 1851977990 57483264 13558 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30446/statm): 14034 13558 145 145 0 13889 0
[pid=30446] vsize: 56136
Current children cumulated CPU time (s) 358.9
Current children cumulated vsize (Kb) 58260

[startup+370.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 13844 0 0 0 36796 91 0 0 25 0 1 0 1851977990 57974784 13680 4294967295 134512640 135094434 3221224432 3221223120 134554687 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30446/statm): 14154 13680 145 145 0 14009 0
[pid=30446] vsize: 56616
Current children cumulated CPU time (s) 368.89
Current children cumulated vsize (Kb) 58740

[startup+380.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 14214 0 0 0 37789 94 0 0 25 0 1 0 1851977990 59461632 14050 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30446/statm): 14517 14050 145 145 0 14372 0
[pid=30446] vsize: 58068
Current children cumulated CPU time (s) 378.85
Current children cumulated vsize (Kb) 60192

[startup+390.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 14355 0 0 0 38787 95 0 0 25 0 1 0 1851977990 60039168 14191 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30446/statm): 14658 14191 145 145 0 14513 0
[pid=30446] vsize: 58632
Current children cumulated CPU time (s) 388.84
Current children cumulated vsize (Kb) 60756

[startup+400.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 14500 0 0 0 39784 96 0 0 25 0 1 0 1851977990 60620800 14336 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30446/statm): 14800 14336 145 145 0 14655 0
[pid=30446] vsize: 59200
Current children cumulated CPU time (s) 398.82
Current children cumulated vsize (Kb) 61324

[startup+410.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 14649 0 0 0 40781 98 0 0 25 0 1 0 1851977990 61222912 14485 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30446/statm): 14947 14485 145 145 0 14802 0
[pid=30446] vsize: 59788
Current children cumulated CPU time (s) 408.81
Current children cumulated vsize (Kb) 61912

[startup+420.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 14795 0 0 0 41778 99 0 0 25 0 1 0 1851977990 61820928 14631 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30446/statm): 15093 14631 145 145 0 14948 0
[pid=30446] vsize: 60372
Current children cumulated CPU time (s) 418.79
Current children cumulated vsize (Kb) 62496

[startup+430.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 14959 0 0 0 42775 101 0 0 25 0 1 0 1851977990 62496768 14795 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30446/statm): 15258 14795 145 145 0 15113 0
[pid=30446] vsize: 61032
Current children cumulated CPU time (s) 428.78
Current children cumulated vsize (Kb) 63156

[startup+440.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 15096 0 0 0 43773 102 0 0 25 0 1 0 1851977990 63033344 14932 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30446/statm): 15389 14932 145 145 0 15244 0
[pid=30446] vsize: 61556
Current children cumulated CPU time (s) 438.77
Current children cumulated vsize (Kb) 63680

[startup+450.042 s]
Raw data (loadavg): 0.99 0.97 0.91 1/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) T 30442 30442 19818 0 -1 0 15234 0 0 0 44771 103 0 0 25 0 1 0 1851977990 63590400 15070 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/30446/statm): 15525 15070 145 145 0 15380 0
[pid=30446] vsize: 62100
Current children cumulated CPU time (s) 448.76
Current children cumulated vsize (Kb) 64224

[startup+460.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 15376 0 0 0 45769 104 0 0 25 0 1 0 1851977990 64167936 15212 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30446/statm): 15666 15212 145 145 0 15521 0
[pid=30446] vsize: 62664
Current children cumulated CPU time (s) 458.75
Current children cumulated vsize (Kb) 64788

[startup+470.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 15532 0 0 0 46766 105 0 0 25 0 1 0 1851977990 64794624 15368 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30446/statm): 15819 15368 145 145 0 15674 0
[pid=30446] vsize: 63276
Current children cumulated CPU time (s) 468.73
Current children cumulated vsize (Kb) 65400

[startup+480.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 15677 0 0 0 47764 107 0 0 25 0 1 0 1851977990 65380352 15513 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30446/statm): 15962 15513 145 145 0 15817 0
[pid=30446] vsize: 63848
Current children cumulated CPU time (s) 478.73
Current children cumulated vsize (Kb) 65972

[startup+490.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 15824 0 0 0 48761 108 0 0 25 0 1 0 1851977990 65974272 15660 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30446/statm): 16107 15660 145 145 0 15962 0
[pid=30446] vsize: 64428
Current children cumulated CPU time (s) 488.71
Current children cumulated vsize (Kb) 66552

[startup+500.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 16027 0 0 0 49757 110 0 0 25 0 1 0 1851977990 66801664 15863 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30446/statm): 16309 15863 145 145 0 16164 0
[pid=30446] vsize: 65236
Current children cumulated CPU time (s) 498.69
Current children cumulated vsize (Kb) 67360

[startup+510.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 16177 0 0 0 50755 111 0 0 25 0 1 0 1851977990 67391488 16013 4294967295 134512640 135094434 3221224432 3221223088 134557917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30446/statm): 16453 16013 145 145 0 16308 0
[pid=30446] vsize: 65812
Current children cumulated CPU time (s) 508.68
Current children cumulated vsize (Kb) 67936

[startup+520.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 16326 0 0 0 51753 112 0 0 25 0 1 0 1851977990 67989504 16162 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30446/statm): 16599 16162 145 145 0 16454 0
[pid=30446] vsize: 66396
Current children cumulated CPU time (s) 518.67
Current children cumulated vsize (Kb) 68520

[startup+530.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 16478 0 0 0 52750 113 0 0 25 0 1 0 1851977990 68591616 16314 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30446/statm): 16746 16314 145 145 0 16601 0
[pid=30446] vsize: 66984
Current children cumulated CPU time (s) 528.65
Current children cumulated vsize (Kb) 69108

[startup+540.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 16638 0 0 0 53747 115 0 0 25 0 1 0 1851977990 69238784 16474 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30446/statm): 16904 16474 145 145 0 16759 0
[pid=30446] vsize: 67616
Current children cumulated CPU time (s) 538.64
Current children cumulated vsize (Kb) 69740

[startup+550.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 16777 0 0 0 54745 116 0 0 25 0 1 0 1851977990 69828608 16613 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30446/statm): 17048 16613 145 145 0 16903 0
[pid=30446] vsize: 68192
Current children cumulated CPU time (s) 548.63
Current children cumulated vsize (Kb) 70316

[startup+560.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 16912 0 0 0 55743 117 0 0 25 0 1 0 1851977990 71446528 16748 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30446/statm): 17443 16748 145 145 0 17298 0
[pid=30446] vsize: 69772
Current children cumulated CPU time (s) 558.62
Current children cumulated vsize (Kb) 71896

[startup+570.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 17136 0 0 0 56739 118 0 0 25 0 1 0 1851977990 72343552 16972 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30446/statm): 17662 16972 145 145 0 17517 0
[pid=30446] vsize: 70648
Current children cumulated CPU time (s) 568.59
Current children cumulated vsize (Kb) 72772

[startup+580.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 17271 0 0 0 57737 120 0 0 25 0 1 0 1851977990 72896512 17107 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30446/statm): 17797 17107 145 145 0 17652 0
[pid=30446] vsize: 71188
Current children cumulated CPU time (s) 578.59
Current children cumulated vsize (Kb) 73312

[startup+590.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 17552 0 0 0 58732 122 0 0 25 0 1 0 1851977990 74022912 17388 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30446/statm): 18072 17388 145 145 0 17927 0
[pid=30446] vsize: 72288
Current children cumulated CPU time (s) 588.56
Current children cumulated vsize (Kb) 74412

[startup+600.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 17889 0 0 0 59726 124 0 0 25 0 1 0 1851977990 75370496 17725 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30446/statm): 18401 17725 145 145 0 18256 0
[pid=30446] vsize: 73604
Current children cumulated CPU time (s) 598.52
Current children cumulated vsize (Kb) 75728

[startup+610.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 18049 0 0 0 60723 126 0 0 25 0 1 0 1851977990 76017664 17885 4294967295 134512640 135094434 3221224432 3221223056 134562057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30446/statm): 18559 17885 145 145 0 18414 0
[pid=30446] vsize: 74236
Current children cumulated CPU time (s) 608.51
Current children cumulated vsize (Kb) 76360

[startup+620.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 18049 0 0 0 61723 126 0 0 25 0 1 0 1851977990 76017664 17885 4294967295 134512640 135094434 3221224432 3221223104 134556073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30446/statm): 18559 17885 145 145 0 18414 0
[pid=30446] vsize: 74236
Current children cumulated CPU time (s) 618.51
Current children cumulated vsize (Kb) 76360

[startup+630.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 18049 0 0 0 62723 127 0 0 25 0 1 0 1851977990 76017664 17885 4294967295 134512640 135094434 3221224432 3221223108 134552241 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30446/statm): 18559 17885 145 145 0 18414 0
[pid=30446] vsize: 74236
Current children cumulated CPU time (s) 628.52
Current children cumulated vsize (Kb) 76360

[startup+640.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 18049 0 0 0 63722 127 0 0 25 0 1 0 1851977990 76017664 17885 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30446/statm): 18559 17885 145 145 0 18414 0
[pid=30446] vsize: 74236
Current children cumulated CPU time (s) 638.51
Current children cumulated vsize (Kb) 76360

[startup+650.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 18049 0 0 0 64722 128 0 0 25 0 1 0 1851977990 76017664 17885 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30446/statm): 18559 17885 145 145 0 18414 0
[pid=30446] vsize: 74236
Current children cumulated CPU time (s) 648.52
Current children cumulated vsize (Kb) 76360

[startup+660.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 18049 0 0 0 65721 128 0 0 25 0 1 0 1851977990 76017664 17885 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30446/statm): 18559 17885 145 145 0 18414 0
[pid=30446] vsize: 74236
Current children cumulated CPU time (s) 658.51
Current children cumulated vsize (Kb) 76360

[startup+670.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 18049 0 0 0 66721 129 0 0 25 0 1 0 1851977990 76017664 17885 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30446/statm): 18559 17885 145 145 0 18414 0
[pid=30446] vsize: 74236
Current children cumulated CPU time (s) 668.52
Current children cumulated vsize (Kb) 76360

[startup+680.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 18049 0 0 0 67721 129 0 0 25 0 1 0 1851977990 76017664 17885 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30446/statm): 18559 17885 145 145 0 18414 0
[pid=30446] vsize: 74236
Current children cumulated CPU time (s) 678.52
Current children cumulated vsize (Kb) 76360

[startup+690.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 18049 0 0 0 68721 129 0 0 25 0 1 0 1851977990 76017664 17885 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30446/statm): 18559 17885 145 145 0 18414 0
[pid=30446] vsize: 74236
Current children cumulated CPU time (s) 688.52
Current children cumulated vsize (Kb) 76360

[startup+700.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 18049 0 0 0 69721 129 0 0 25 0 1 0 1851977990 76017664 17885 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30446/statm): 18559 17885 145 145 0 18414 0
[pid=30446] vsize: 74236
Current children cumulated CPU time (s) 698.52
Current children cumulated vsize (Kb) 76360

[startup+710.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 18049 0 0 0 70721 129 0 0 25 0 1 0 1851977990 76017664 17885 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30446/statm): 18559 17885 145 145 0 18414 0
[pid=30446] vsize: 74236
Current children cumulated CPU time (s) 708.52
Current children cumulated vsize (Kb) 76360

[startup+720.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 18049 0 0 0 71721 130 0 0 25 0 1 0 1851977990 76017664 17885 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30446/statm): 18559 17885 145 145 0 18414 0
[pid=30446] vsize: 74236
Current children cumulated CPU time (s) 718.53
Current children cumulated vsize (Kb) 76360

[startup+730.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 18049 0 0 0 72721 130 0 0 25 0 1 0 1851977990 76017664 17885 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30446/statm): 18559 17885 145 145 0 18414 0
[pid=30446] vsize: 74236
Current children cumulated CPU time (s) 728.53
Current children cumulated vsize (Kb) 76360

[startup+740.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 18049 0 0 0 73721 130 0 0 25 0 1 0 1851977990 76017664 17885 4294967295 134512640 135094434 3221224432 3221223024 134556812 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30446/statm): 18559 17885 145 145 0 18414 0
[pid=30446] vsize: 74236
Current children cumulated CPU time (s) 738.53
Current children cumulated vsize (Kb) 76360

[startup+750.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 18049 0 0 0 74722 130 0 0 25 0 1 0 1851977990 76017664 17885 4294967295 134512640 135094434 3221224432 3221223088 134557962 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30446/statm): 18559 17885 145 145 0 18414 0
[pid=30446] vsize: 74236
Current children cumulated CPU time (s) 748.54
Current children cumulated vsize (Kb) 76360

[startup+760.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 18049 0 0 0 75722 130 0 0 25 0 1 0 1851977990 76017664 17885 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30446/statm): 18559 17885 145 145 0 18414 0
[pid=30446] vsize: 74236
Current children cumulated CPU time (s) 758.54
Current children cumulated vsize (Kb) 76360

[startup+770.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 18049 0 0 0 76722 130 0 0 25 0 1 0 1851977990 76017664 17885 4294967295 134512640 135094434 3221224432 3221223088 134557945 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30446/statm): 18559 17885 145 145 0 18414 0
[pid=30446] vsize: 74236
Current children cumulated CPU time (s) 768.54
Current children cumulated vsize (Kb) 76360

[startup+780.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 18049 0 0 0 77722 130 0 0 25 0 1 0 1851977990 76017664 17885 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30446/statm): 18559 17885 145 145 0 18414 0
[pid=30446] vsize: 74236
Current children cumulated CPU time (s) 778.54
Current children cumulated vsize (Kb) 76360

[startup+790.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 18049 0 0 0 78722 130 0 0 25 0 1 0 1851977990 76017664 17885 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30446/statm): 18559 17885 145 145 0 18414 0
[pid=30446] vsize: 74236
Current children cumulated CPU time (s) 788.54
Current children cumulated vsize (Kb) 76360

[startup+800.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 18049 0 0 0 79722 130 0 0 25 0 1 0 1851977990 76017664 17885 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30446/statm): 18559 17885 145 145 0 18414 0
[pid=30446] vsize: 74236
Current children cumulated CPU time (s) 798.54
Current children cumulated vsize (Kb) 76360

[startup+810.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 18049 0 0 0 80722 130 0 0 25 0 1 0 1851977990 76017664 17885 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30446/statm): 18559 17885 145 145 0 18414 0
[pid=30446] vsize: 74236
Current children cumulated CPU time (s) 808.54
Current children cumulated vsize (Kb) 76360

[startup+820.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 18049 0 0 0 81723 130 0 0 25 0 1 0 1851977990 76017664 17885 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30446/statm): 18559 17885 145 145 0 18414 0
[pid=30446] vsize: 74236
Current children cumulated CPU time (s) 818.55
Current children cumulated vsize (Kb) 76360

[startup+830.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 18049 0 0 0 82723 130 0 0 25 0 1 0 1851977990 76017664 17885 4294967295 134512640 135094434 3221224432 3221223120 134554748 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30446/statm): 18559 17885 145 145 0 18414 0
[pid=30446] vsize: 74236
Current children cumulated CPU time (s) 828.55
Current children cumulated vsize (Kb) 76360

[startup+840.075 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 18049 0 0 0 83723 130 0 0 25 0 1 0 1851977990 76017664 17885 4294967295 134512640 135094434 3221224432 3221223088 134557879 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30446/statm): 18559 17885 145 145 0 18414 0
[pid=30446] vsize: 74236
Current children cumulated CPU time (s) 838.55
Current children cumulated vsize (Kb) 76360

[startup+850.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 18049 0 0 0 84723 130 0 0 25 0 1 0 1851977990 76017664 17885 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30446/statm): 18559 17885 145 145 0 18414 0
[pid=30446] vsize: 74236
Current children cumulated CPU time (s) 848.55
Current children cumulated vsize (Kb) 76360

[startup+860.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 18049 0 0 0 85723 130 0 0 25 0 1 0 1851977990 76017664 17885 4294967295 134512640 135094434 3221224432 3221223088 134558172 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30446/statm): 18559 17885 145 145 0 18414 0
[pid=30446] vsize: 74236
Current children cumulated CPU time (s) 858.55
Current children cumulated vsize (Kb) 76360

[startup+870.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 18049 0 0 0 86724 130 0 0 25 0 1 0 1851977990 76017664 17885 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30446/statm): 18559 17885 145 145 0 18414 0
[pid=30446] vsize: 74236
Current children cumulated CPU time (s) 868.56
Current children cumulated vsize (Kb) 76360

[startup+880.078 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 18049 0 0 0 87724 130 0 0 25 0 1 0 1851977990 76017664 17885 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30446/statm): 18559 17885 145 145 0 18414 0
[pid=30446] vsize: 74236
Current children cumulated CPU time (s) 878.56
Current children cumulated vsize (Kb) 76360

[startup+890.079 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 18049 0 0 0 88724 131 0 0 25 0 1 0 1851977990 76017664 17885 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30446/statm): 18559 17885 145 145 0 18414 0
[pid=30446] vsize: 74236
Current children cumulated CPU time (s) 888.57
Current children cumulated vsize (Kb) 76360

[startup+900.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 18049 0 0 0 89724 131 0 0 25 0 1 0 1851977990 76017664 17885 4294967295 134512640 135094434 3221224432 3221223044 134563140 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30446/statm): 18559 17885 145 145 0 18414 0
[pid=30446] vsize: 74236
Current children cumulated CPU time (s) 898.57
Current children cumulated vsize (Kb) 76360

[startup+910.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 18049 0 0 0 90724 131 0 0 25 0 1 0 1851977990 76017664 17885 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30446/statm): 18559 17885 145 145 0 18414 0
[pid=30446] vsize: 74236
Current children cumulated CPU time (s) 908.57
Current children cumulated vsize (Kb) 76360

[startup+920.081 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 18049 0 0 0 91722 133 0 0 25 0 1 0 1851977990 76017664 17885 4294967295 134512640 135094434 3221224432 3221223088 134557928 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30446/statm): 18559 17885 145 145 0 18414 0
[pid=30446] vsize: 74236
Current children cumulated CPU time (s) 918.57
Current children cumulated vsize (Kb) 76360

[startup+930.082 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 18049 0 0 0 92722 133 0 0 25 0 1 0 1851977990 76017664 17885 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30446/statm): 18559 17885 145 145 0 18414 0
[pid=30446] vsize: 74236
Current children cumulated CPU time (s) 928.57
Current children cumulated vsize (Kb) 76360

[startup+940.084 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 18049 0 0 0 93722 134 0 0 25 0 1 0 1851977990 76017664 17885 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30446/statm): 18559 17885 145 145 0 18414 0
[pid=30446] vsize: 74236
Current children cumulated CPU time (s) 938.58
Current children cumulated vsize (Kb) 76360

[startup+950.084 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 18049 0 0 0 94722 134 0 0 25 0 1 0 1851977990 76017664 17885 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30446/statm): 18559 17885 145 145 0 18414 0
[pid=30446] vsize: 74236
Current children cumulated CPU time (s) 948.58
Current children cumulated vsize (Kb) 76360

[startup+960.085 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 18049 0 0 0 95722 134 0 0 25 0 1 0 1851977990 76017664 17885 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30446/statm): 18559 17885 145 145 0 18414 0
[pid=30446] vsize: 74236
Current children cumulated CPU time (s) 958.58
Current children cumulated vsize (Kb) 76360

[startup+970.087 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 18049 0 0 0 96723 134 0 0 25 0 1 0 1851977990 76017664 17885 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30446/statm): 18559 17885 145 145 0 18414 0
[pid=30446] vsize: 74236
Current children cumulated CPU time (s) 968.59
Current children cumulated vsize (Kb) 76360

[startup+980.088 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 18049 0 0 0 97723 134 0 0 25 0 1 0 1851977990 76017664 17885 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30446/statm): 18559 17885 145 145 0 18414 0
[pid=30446] vsize: 74236
Current children cumulated CPU time (s) 978.59
Current children cumulated vsize (Kb) 76360

[startup+990.089 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 18049 0 0 0 98723 134 0 0 25 0 1 0 1851977990 76017664 17885 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30446/statm): 18559 17885 145 145 0 18414 0
[pid=30446] vsize: 74236
Current children cumulated CPU time (s) 988.59
Current children cumulated vsize (Kb) 76360

[startup+1000.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 18049 0 0 0 99722 135 0 0 25 0 1 0 1851977990 76017664 17885 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30446/statm): 18559 17885 145 145 0 18414 0
[pid=30446] vsize: 74236
Current children cumulated CPU time (s) 998.59
Current children cumulated vsize (Kb) 76360

[startup+1010.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 18049 0 0 0 100722 135 0 0 25 0 1 0 1851977990 76017664 17885 4294967295 134512640 135094434 3221224432 3221223092 134553480 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30446/statm): 18559 17885 145 145 0 18414 0
[pid=30446] vsize: 74236
Current children cumulated CPU time (s) 1008.59
Current children cumulated vsize (Kb) 76360

[startup+1020.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 18049 0 0 0 101722 135 0 0 25 0 1 0 1851977990 76017664 17885 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30446/statm): 18559 17885 145 145 0 18414 0
[pid=30446] vsize: 74236
Current children cumulated CPU time (s) 1018.59
Current children cumulated vsize (Kb) 76360

[startup+1030.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 18049 0 0 0 102722 136 0 0 25 0 1 0 1851977990 76017664 17885 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30446/statm): 18559 17885 145 145 0 18414 0
[pid=30446] vsize: 74236
Current children cumulated CPU time (s) 1028.6
Current children cumulated vsize (Kb) 76360

[startup+1040.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 18066 0 0 0 103722 136 0 0 25 0 1 0 1851977990 76148736 17902 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30446/statm): 18591 17902 145 145 0 18446 0
[pid=30446] vsize: 74364
Current children cumulated CPU time (s) 1038.6
Current children cumulated vsize (Kb) 76488

[startup+1050.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 18087 0 0 0 104722 136 0 0 25 0 1 0 1851977990 76279808 17923 4294967295 134512640 135094434 3221224432 3221223044 134563110 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30446/statm): 18623 17923 145 145 0 18478 0
[pid=30446] vsize: 74492
Current children cumulated CPU time (s) 1048.6
Current children cumulated vsize (Kb) 76616

[startup+1060.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 18089 0 0 0 105721 136 0 0 25 0 1 0 1851977990 76279808 17925 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30446/statm): 18623 17925 145 145 0 18478 0
[pid=30446] vsize: 74492
Current children cumulated CPU time (s) 1058.59
Current children cumulated vsize (Kb) 76616

[startup+1070.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 18106 0 0 0 106721 137 0 0 25 0 1 0 1851977990 76410880 17942 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30446/statm): 18655 17942 145 145 0 18510 0
[pid=30446] vsize: 74620
Current children cumulated CPU time (s) 1068.6
Current children cumulated vsize (Kb) 76744

[startup+1080.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 18108 0 0 0 107721 137 0 0 25 0 1 0 1851977990 76410880 17944 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30446/statm): 18655 17944 145 145 0 18510 0
[pid=30446] vsize: 74620
Current children cumulated CPU time (s) 1078.6
Current children cumulated vsize (Kb) 76744

[startup+1090.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 18108 0 0 0 108721 138 0 0 25 0 1 0 1851977990 76410880 17944 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30446/statm): 18655 17944 145 145 0 18510 0
[pid=30446] vsize: 74620
Current children cumulated CPU time (s) 1088.61
Current children cumulated vsize (Kb) 76744

[startup+1100.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 18108 0 0 0 109721 138 0 0 25 0 1 0 1851977990 76410880 17944 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30446/statm): 18655 17944 145 145 0 18510 0
[pid=30446] vsize: 74620
Current children cumulated CPU time (s) 1098.61
Current children cumulated vsize (Kb) 76744

[startup+1110.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 18108 0 0 0 110720 138 0 0 25 0 1 0 1851977990 76410880 17944 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30446/statm): 18655 17944 145 145 0 18510 0
[pid=30446] vsize: 74620
Current children cumulated CPU time (s) 1108.6
Current children cumulated vsize (Kb) 76744

[startup+1120.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 18109 0 0 0 111720 138 0 0 25 0 1 0 1851977990 76410880 17945 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30446/statm): 18655 17945 145 145 0 18510 0
[pid=30446] vsize: 74620
Current children cumulated CPU time (s) 1118.6
Current children cumulated vsize (Kb) 76744

[startup+1130.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 18109 0 0 0 112720 139 0 0 25 0 1 0 1851977990 76410880 17945 4294967295 134512640 135094434 3221224432 3221223088 134558176 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30446/statm): 18655 17945 145 145 0 18510 0
[pid=30446] vsize: 74620
Current children cumulated CPU time (s) 1128.61
Current children cumulated vsize (Kb) 76744

[startup+1140.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 18110 0 0 0 113720 139 0 0 25 0 1 0 1851977990 76410880 17946 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30446/statm): 18655 17946 145 145 0 18510 0
[pid=30446] vsize: 74620
Current children cumulated CPU time (s) 1138.61
Current children cumulated vsize (Kb) 76744

[startup+1150.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 18110 0 0 0 114720 139 0 0 25 0 1 0 1851977990 76410880 17946 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30446/statm): 18655 17946 145 145 0 18510 0
[pid=30446] vsize: 74620
Current children cumulated CPU time (s) 1148.61
Current children cumulated vsize (Kb) 76744

[startup+1160.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 18133 0 0 0 115720 140 0 0 25 0 1 0 1851977990 76541952 17969 4294967295 134512640 135094434 3221224432 3221223088 134557890 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30446/statm): 18687 17969 145 145 0 18542 0
[pid=30446] vsize: 74748
Current children cumulated CPU time (s) 1158.62
Current children cumulated vsize (Kb) 76872

[startup+1170.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 18133 0 0 0 116719 140 0 0 25 0 1 0 1851977990 76541952 17969 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30446/statm): 18687 17969 145 145 0 18542 0
[pid=30446] vsize: 74748
Current children cumulated CPU time (s) 1168.61
Current children cumulated vsize (Kb) 76872

[startup+1180.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 18133 0 0 0 117719 140 0 0 25 0 1 0 1851977990 76541952 17969 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30446/statm): 18687 17969 145 145 0 18542 0
[pid=30446] vsize: 74748
Current children cumulated CPU time (s) 1178.61
Current children cumulated vsize (Kb) 76872

[startup+1190.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 18133 0 0 0 118719 140 0 0 25 0 1 0 1851977990 76541952 17969 4294967295 134512640 135094434 3221224432 3221223084 134558255 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30446/statm): 18687 17969 145 145 0 18542 0
[pid=30446] vsize: 74748
Current children cumulated CPU time (s) 1188.61
Current children cumulated vsize (Kb) 76872

[startup+1200.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 18133 0 0 0 119719 141 0 0 25 0 1 0 1851977990 76541952 17969 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30446/statm): 18687 17969 145 145 0 18542 0
[pid=30446] vsize: 74748
Current children cumulated CPU time (s) 1198.62
Current children cumulated vsize (Kb) 76872

[startup+1210.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 18133 0 0 0 120718 141 0 0 25 0 1 0 1851977990 76541952 17969 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30446/statm): 18687 17969 145 145 0 18542 0
[pid=30446] vsize: 74748
Current children cumulated CPU time (s) 1208.61
Current children cumulated vsize (Kb) 76872



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 30446
Raw data (/proc/30442/stat): 30442 (minisat+_script) S 30441 30442 19818 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851977985 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/30442/statm): 531 226 485 147 0 384 0
[pid=30442] vsize: 2124
Raw data (/proc/30446/stat): 30446 (minisat+_64-bit) R 30442 30442 19818 0 -1 0 18133 0 0 0 120718 141 0 0 25 0 1 0 1851977990 76541952 17969 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30446/statm): 18687 17969 145 145 0 18542 0
[pid=30446] vsize: 74748
Current children cumulated CPU time (s) 1208.61
Current children cumulated vsize (Kb) 76872

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

Child status: 0
Real time (s): 1210.15
CPU time (s): 1208.64
CPU user time (s): 1207.19
CPU system time (s): 1.45078
CPU usage (%): 99.8747
Max. virtual memory (cumulated for all children) (Kb): 76872

Verifier Data

ERROR: no interpretation found !