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/miplib2003/normalized-mps-v2-20-10-vpm2.opb
MD5SUMc1b4c3ad409db732d2b559e570b6f24c
Bench Categoryoptimization, medium integers (OPTMEDINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 138
Optimality of the best value was proved NO
Number of terms in the objective function 168
Biggest coefficient in the objective function 5
Number of bits for the biggest coefficient in the objective function 3
Sum of the numbers in the objective function 504
Number of bits of the sum of numbers in the objective function 9
Biggest number in a constraint 819200
Number of bits of the biggest number in a constraint 20
Biggest sum of numbers in a constraint 4941871
Number of bits of the biggest sum of numbers23
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1189.01
Number of variables2754
Total number of constraints612
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)168
Number of constraints which are nor clauses,nor cardinality constraints444
Minimum length of a constraint1
Maximum length of a constraint84

Trace number 4490

Launcher Data

LAUNCH ON wulflinc2 THE 2005-09-19 17:42:01 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2951 boxname=wulflinc2 idbench=607 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  c1b4c3ad409db732d2b559e570b6f24c  /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-20-10-vpm2.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-20-10-vpm2.opb
IDLAUNCH: 2951
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.191
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.191
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:        856892 kB
Buffers:         39824 kB
Cached:         110980 kB
SwapCached:       1040 kB
Active:          63888 kB
Inactive:        89552 kB
HighTotal:      131008 kB
HighFree:        27496 kB
LowTotal:       903652 kB
LowFree:        829396 kB
SwapTotal:     2097136 kB
SwapFree:      2095568 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5700 kB
Slab:            18548 kB
Committed_AS:    72360 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-19 18:02:11 (client local time) WITH STATUS 0 IN 1208.5 SECONDS
stats: 2951 7 1208.5 0

Solver Data

c Parsing PB file...
c Converting 486 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: ##############################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 485]---> BDD-cost:   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]---> Adder-cost: 352   maxlim: 2411343   bits: 22/22
c ---[ 272]---> Adder-cost: 288   maxlim: 1694643   bits: 21/21
c ---[ 271]---> BDD-cost:    3
c ---[ 270]---> BDD-cost:    3
c ---[ 269]---> BDD-cost:    3
c ---[ 267]---> BDD-cost:    3
c ---[ 266]---> BDD-cost:    3
c ---[ 265]---> BDD-cost:    3
c ---[ 264]---> BDD-cost:    3
c ---[ 263]---> BDD-cost:    3
c ---[ 259]---> BDD-cost:   10
c ---[ 258]---> BDD-cost:    3
c ---[ 257]---> BDD-cost:    3
c ---[ 256]---> BDD-cost:    3
c ---[ 255]---> BDD-cost:   10
c ---[ 251]---> BDD-cost:   10
c ---[ 250]---> BDD-cost:    3
c ---[ 247]---> BDD-cost:    9
c ---[ 243]---> BDD-cost:   10
c ---[ 242]---> BDD-cost:    3
c ---[ 241]---> BDD-cost:    9
c ---[ 236]---> Sorter-cost: 2294     Base: 2 2 2 2 5 5 2 2 2 2 2 2 2 2
c ---[ 235]---> BDD-cost:    3
c ---[ 234]---> BDD-cost:    3
c ---[ 233]---> BDD-cost:    9
c ---[ 229]---> BDD-cost:   10
c ---[ 228]---> BDD-cost:    3
c ---[ 227]---> BDD-cost:    9
c ---[ 224]---> Adder-cost: 312   maxlim: 2587171   bits: 22/22
c ---[ 220]---> BDD-cost:    3
c ---[ 219]---> BDD-cost:    3
c ---[ 214]---> BDD-cost:   10
c ---[ 212]---> Adder-cost: 260   maxlim: 897571   bits: 20/20
c ---[ 211]---> BDD-cost:    3
c ---[ 206]---> BDD-cost:    3
c ---[ 205]---> BDD-cost:    3
c ---[ 198]---> BDD-cost:    3
c ---[ 197]---> BDD-cost:    3
c ---[ 193]---> BDD-cost:    3
c ---[ 192]---> BDD-cost:    3
c ---[ 191]---> BDD-cost:    3
c ---[ 185]---> BDD-cost:    3
c ---[ 184]---> BDD-cost:    3
c ---[ 183]---> BDD-cost:    3
c ---[ 179]---> BDD-cost:    3
c ---[ 178]---> BDD-cost:    3
c ---[ 175]---> BDD-cost:    3
c ---[ 171]---> BDD-cost:    3
c ---[ 170]---> BDD-cost:    3
c ---[ 169]---> BDD-cost:    3
c ---[ 168]---> BDD-cost:    3
c ---[ 167]---> BDD-cost:    3
c ---[ 166]---> BDD-cost:    9
c ---[ 164]---> Sorter-cost: 2815     Base: 2 2 2 5 5 2 2 2 2 2 2 2 2 3
c ---[ 163]---> BDD-cost:    9
c ---[ 162]---> BDD-cost:    9
c ---[ 161]---> BDD-cost:    9
c ---[ 160]---> BDD-cost:    3
c ---[ 159]---> BDD-cost:   10
c ---[ 158]---> BDD-cost:    9
c ---[ 157]---> BDD-cost:    9
c ---[ 156]---> BDD-cost:    9
c ---[ 155]---> BDD-cost:    9
c ---[ 154]---> BDD-cost:    3
c ---[ 152]---> Adder-cost: 352   maxlim: 2411343   bits: 22/22
c ---[ 150]---> Adder-cost: 350   maxlim: 1768271   bits: 22/21
c ---[ 149]---> BDD-cost:   10
c ---[ 148]---> BDD-cost:    8
c ---[ 147]---> BDD-cost:    8
c ---[ 146]---> BDD-cost:    8
c ---[ 145]---> BDD-cost:    8
c ---[ 144]---> BDD-cost:    3
c ---[ 143]---> BDD-cost:   10
c ---[ 142]---> BDD-cost:    8
c ---[ 141]---> BDD-cost:    8
c ---[ 140]---> BDD-cost:    8
c ---[ 137]---> BDD-cost:    8
c ---[ 135]---> BDD-cost:   10
c ---[ 134]---> BDD-cost:    3
c ---[ 133]---> BDD-cost:    9
c ---[ 132]---> BDD-cost:    9
c ---[ 131]---> BDD-cost:    9
c ---[ 129]---> BDD-cost:   10
c ---[ 128]---> BDD-cost:    3
c ---[ 125]---> BDD-cost:    9
c ---[ 124]---> BDD-cost:    9
c ---[ 123]---> BDD-cost:    9
c ---[ 121]---> BDD-cost:   10
c ---[ 120]---> BDD-cost:    3
c ---[ 119]---> BDD-cost:    9
c ---[ 118]---> BDD-cost:    9
c ---[ 117]---> BDD-cost:    9
c ---[ 114]---> Adder-cost: 274   maxlim: 1228100   bits: 21/21
c ---[ 113]---> BDD-cost:   10
c ---[ 112]---> BDD-cost:    3
c ---[ 111]---> BDD-cost:    8
c ---[ 110]---> BDD-cost:    8
c ---[ 109]---> BDD-cost:    8
c ---[ 107]---> Adder-cost: 312   maxlim: 1957187   bits: 22/21
c ---[ 105]---> Adder-cost: 312   maxlim: 1854787   bits: 22/21
c ---[ 103]---> Adder-cost: 390   maxlim: 2279471   bits: 22/22
c ---[ 101]---> Adder-cost: 332   maxlim: 845871   bits: 20/20
c ---[  99]---> Adder-cost: 332   maxlim: 845871   bits: 20/20
c ---[  97]---> Adder-cost: 332   maxlim: 845871   bits: 20/20
c ---[  95]---> Adder-cost: 330   maxlim: 1694543   bits: 21/21
c ---[  93]---> Adder-cost: 332   maxlim: 845871   bits: 20/20
c ---[  91]---> Sorter-cost: 3240     Base: 2 2 2 2 5 5 2 2 2 2 2 2 5
c ---[  89]---> Adder-cost: 440   maxlim: 3713071   bits: 23/22
c ---[  87]---> Adder-cost: 368   maxlim: 999471   bits: 21/20
c ---[  85]---> Adder-cost: 368   maxlim: 999471   bits: 21/20
c ---[  83]---> Adder-cost: 368   maxlim: 999471   bits: 21/20
c ---[  81]---> Sorter-cost: 3227     Base: 2 2 2 5 5 2 2 2 2 2 2 2 2 3
c ---[  73]---> Adder-cost: 330   maxlim: 1694543   bits: 21/21
c ---[  69]---> Sorter-cost: 3277     Base: 2 2 2 5 5 2 2 2 2 2 2 3 2 2 2
c ---[  66]---> BDD-cost:  230
c ---[  65]---> BDD-cost:  661
c ---[  64]---> BDD-cost:  660
c ---[  63]---> Sorter-cost: 1990     Base: 5 5 5 2 2 2 2 2 2 2 2 2
c ---[  62]---> Sorter-cost: 2375     Base: 5 5 5 2 2 2 2 2 2 2 2 2
c ---[  61]---> Sorter-cost: 2299     Base: 5 5 5 2 2 2 2 2 2 2 2 2
c ---[  60]---> Sorter-cost:  414     Base: 2 2 2 2 2 2 2 2 5 2
c ---[  58]---> Adder-cost: 352   maxlim: 2104143   bits: 22/22
c ---[  57]---> Sorter-cost: 1128     Base: 5 2 2 2 2 2 2 2 2 2
c ---[  56]---> Sorter-cost: 1146     Base: 5 2 2 2 2 2 2 2 2 2
c ---[  55]---> Sorter-cost: 1625     Base: 5 2 2 2 2 2 2 2 2 2
c ---[  54]---> Sorter-cost: 1905     Base: 5 2 2 2 2 2 2 2 2 2
c ---[  53]---> Sorter-cost: 1909     Base: 5 2 2 2 2 2 2 2 2 2
c ---[  52]---> Sorter-cost:  446     Base: 2 2 2 2 2 2 2 2 2 5
c ---[  51]---> Sorter-cost: 1242     Base: 2 2 2 2 2 5 2 2 2 2
c ---[  50]---> Sorter-cost: 1199     Base: 2 2 2 2 2 2 2 2 2 5
c ---[  49]---> Sorter-cost: 1719     Base: 5 2 2 2 2 2 2 2 2 2
c ---[  48]---> Sorter-cost: 2067     Base: 5 2 2 2 2 2 2 2 2 2
c ---[  46]---> Sorter-cost: 2487     Base: 2 2 2 2 2 2 2 2 5 5 2 2 2 2
c ---[  45]---> Sorter-cost: 2045     Base: 5 2 2 2 2 2 2 2 2 2
c ---[  44]---> Sorter-cost:  223     Base: 2 2 2 2 2 2 2 2 2
c ---[  43]---> Sorter-cost:  590     Base: 2 2 2 2 2 2 2 2
c ---[  42]---> Sorter-cost:  538     Base: 2 2 2 2 2 2 2 2 2
c ---[  41]---> Sorter-cost: 1025     Base: 2 2 2 2 2 2 2 2
c ---[  40]---> Sorter-cost: 1211     Base: 2 2 2 2 2 2 2 2 2
c ---[  39]---> Sorter-cost: 1390     Base: 2 2 2 2 2 2 2 2
c ---[  38]---> BDD-cost:    3
c ---[  37]---> BDD-cost:    3
c ---[  36]---> BDD-cost:    3
c ---[  34]---> Adder-cost: 304   maxlim: 2309043   bits: 22/22
c ---[  33]---> BDD-cost:    3
c ---[  32]---> BDD-cost:    3
c ---[  31]---> BDD-cost:    3
c ---[  30]---> BDD-cost:    3
c ---[  29]---> BDD-cost:    3
c ---[  28]---> BDD-cost:    3
c ---[  27]---> BDD-cost:   10
c ---[  26]---> BDD-cost:   10
c ---[  25]---> BDD-cost:    3
c ---[  24]---> BDD-cost:    3
c ---[  22]---> Adder-cost: 304   maxlim: 2104243   bits: 22/22
c ---[  21]---> BDD-cost:    3
c ---[  20]---> BDD-cost:    3
c ---[  19]---> BDD-cost:   10
c ---[  18]---> BDD-cost:   10
c ---[  17]---> BDD-cost:    3
c ---[  16]---> BDD-cost:    3
c ---[  15]---> BDD-cost:    3
c ---[  14]---> BDD-cost:    3
c ---[  13]---> BDD-cost:   10
c ---[  12]---> BDD-cost:   10
c ---[  10]---> Adder-cost: 304   maxlim: 2104243   bits: 22/22
c ---[   9]---> BDD-cost:    3
c ---[   7]---> BDD-cost:   10
c ---[   6]---> BDD-cost:    3
c ---[   5]---> BDD-cost:    3
c ---[   4]---> BDD-cost:    3
c ---[   3]---> BDD-cost:   10
c ---[   1]---> BDD-cost:    3
c ---[   0]---> BDD-cost:    3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  171008   465207 |   57002       0        0     nan |  0.000 % |
c |       100 |  171008   465207 |   62702     100      499     5.0 |  5.013 % |
c |       250 |  170886   464914 |   68972     244     1124     4.6 |  5.070 % |
c |       475 |  170813   464741 |   75869     466     2110     4.5 |  5.105 % |
c |       812 |  170740   464545 |   83456     796     3945     5.0 |  5.135 % |
c |      1318 |  170629   464285 |   91802    1296     7491     5.8 |  5.187 % |
c |      2077 |  170483   463926 |  100982    2041    14010     6.9 |  5.252 % |
c |      3217 |  170393   463696 |  111080    3174    25960     8.2 |  5.288 % |
c |      4925 |  170357   463613 |  122188    4875    45072     9.2 |  5.309 % |
c |      7488 |  170331   463525 |  134407    7437    85705    11.5 |  5.313 % |
c |     11333 |  170217   463181 |  147848   11272   148411    13.2 |  5.346 % |
c |     17099 |  169976   462627 |  162633   16981   268977    15.8 |  5.479 % |
c |     25748 |  169586   461746 |  178896   25600   514983    20.1 |  5.667 % |
c |     38723 |  169146   460673 |  196786   38534   879620    22.8 |  5.892 % |
c |     58186 |  168711   459667 |  216465   57904  1288588    22.3 |  6.129 % |
c |     87379 |  168291   458443 |  238111   87052  2301755    26.4 |  6.272 % |
c |    131168 |  167638   456662 |  261922  130676  3553582    27.2 |  6.548 % |
c |    196853 |  167418   456154 |  288114  196348  5992264    30.5 |  6.660 % |
c |    295383 |  167029   455103 |  316926   25590   607141    23.7 |  6.815 % |
c |    443173 |  166301   453298 |  348619  173304  6043059    34.9 |  7.176 % |

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

[startup+10.0042 s]
Raw data (loadavg): 0.49 0.53 0.40 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 4791 0 2 0 941 22 0 0 25 0 1 0 1793563667 21004288 4594 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28366/statm): 5128 4594 145 145 0 4983 0
[pid=28366] vsize: 20512
Current children cumulated CPU time (s) 9.64
Current children cumulated vsize (Kb) 22636

[startup+20.005 s]
Raw data (loadavg): 0.57 0.54 0.40 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 5229 0 2 0 1934 25 0 0 25 0 1 0 1793563667 22843392 5032 4294967295 134512640 135094434 3221224448 3221223104 134557884 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28366/statm): 5577 5032 145 145 0 5432 0
[pid=28366] vsize: 22308
Current children cumulated CPU time (s) 19.6
Current children cumulated vsize (Kb) 24432

[startup+30.0057 s]
Raw data (loadavg): 0.64 0.56 0.41 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 5627 0 2 0 2925 29 0 0 25 0 1 0 1793563667 24432640 5430 4294967295 134512640 135094434 3221224448 3221223136 134554723 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28366/statm): 5965 5430 145 145 0 5820 0
[pid=28366] vsize: 23860
Current children cumulated CPU time (s) 29.55
Current children cumulated vsize (Kb) 25984

[startup+40.0073 s]
Raw data (loadavg): 0.69 0.57 0.41 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 5997 0 2 0 3919 31 0 0 25 0 1 0 1793563667 26034176 5800 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 6356 5800 145 145 0 6211 0
[pid=28366] vsize: 25424
Current children cumulated CPU time (s) 39.51
Current children cumulated vsize (Kb) 27548

[startup+50.008 s]
Raw data (loadavg): 0.74 0.59 0.42 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 6349 0 2 0 4912 34 0 0 25 0 1 0 1793563667 27418624 6152 4294967295 134512640 135094434 3221224448 3221223080 134557561 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 6694 6152 145 145 0 6549 0
[pid=28366] vsize: 26776
Current children cumulated CPU time (s) 49.47
Current children cumulated vsize (Kb) 28900

[startup+60.0087 s]
Raw data (loadavg): 0.78 0.60 0.43 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 6805 0 2 0 5906 37 0 0 25 0 1 0 1793563667 29229056 6608 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 7136 6608 145 145 0 6991 0
[pid=28366] vsize: 28544
Current children cumulated CPU time (s) 59.44
Current children cumulated vsize (Kb) 30668

[startup+70.0094 s]
Raw data (loadavg): 0.81 0.61 0.43 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 7136 0 2 0 6900 39 0 0 25 0 1 0 1793563667 30826496 6939 4294967295 134512640 135094434 3221224448 3221223104 134557914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 7526 6939 145 145 0 7381 0
[pid=28366] vsize: 30104
Current children cumulated CPU time (s) 69.4
Current children cumulated vsize (Kb) 32228

[startup+80.0101 s]
Raw data (loadavg): 0.84 0.62 0.44 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 7405 0 2 0 7896 42 0 0 25 0 1 0 1793563667 31899648 7208 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 7788 7208 145 145 0 7643 0
[pid=28366] vsize: 31152
Current children cumulated CPU time (s) 79.39
Current children cumulated vsize (Kb) 33276

[startup+90.0108 s]
Raw data (loadavg): 0.86 0.64 0.44 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 7701 0 2 0 8890 44 0 0 25 0 1 0 1793563667 33099776 7504 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 8081 7504 145 145 0 7936 0
[pid=28366] vsize: 32324
Current children cumulated CPU time (s) 89.35
Current children cumulated vsize (Kb) 34448

[startup+100.012 s]
Raw data (loadavg): 0.89 0.65 0.45 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 7990 0 2 0 9885 46 0 0 25 0 1 0 1793563667 34254848 7793 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28366/statm): 8363 7793 145 145 0 8218 0
[pid=28366] vsize: 33452
Current children cumulated CPU time (s) 99.32
Current children cumulated vsize (Kb) 35576

[startup+110.013 s]
Raw data (loadavg): 0.90 0.66 0.46 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 8264 0 2 0 10880 49 0 0 25 0 1 0 1793563667 35348480 8067 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 8630 8067 145 145 0 8485 0
[pid=28366] vsize: 34520
Current children cumulated CPU time (s) 109.3
Current children cumulated vsize (Kb) 36644

[startup+120.014 s]
Raw data (loadavg): 0.92 0.67 0.46 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 8474 0 2 0 11877 51 0 0 25 0 1 0 1793563667 36196352 8277 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 8837 8277 145 145 0 8692 0
[pid=28366] vsize: 35348
Current children cumulated CPU time (s) 119.29
Current children cumulated vsize (Kb) 37472

[startup+130.015 s]
Raw data (loadavg): 0.93 0.68 0.47 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 8733 0 2 0 12874 52 0 0 25 0 1 0 1793563667 37216256 8536 4294967295 134512640 135094434 3221224448 3221223108 134553487 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 9086 8536 145 145 0 8941 0
[pid=28366] vsize: 36344
Current children cumulated CPU time (s) 129.27
Current children cumulated vsize (Kb) 38468

[startup+140.015 s]
Raw data (loadavg): 0.94 0.69 0.47 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 9067 0 2 0 13868 55 0 0 25 0 1 0 1793563667 38539264 8870 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 9409 8870 145 145 0 9264 0
[pid=28366] vsize: 37636
Current children cumulated CPU time (s) 139.24
Current children cumulated vsize (Kb) 39760

[startup+150.016 s]
Raw data (loadavg): 0.95 0.70 0.48 1/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) T 28362 28362 6872 0 -1 0 9332 0 2 0 14863 56 0 0 25 0 1 0 1793563667 39600128 9135 4294967295 134512640 135094434 3221224448 3221222828 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/28366/statm): 9668 9135 145 145 0 9523 0
[pid=28366] vsize: 38672
Current children cumulated CPU time (s) 149.2
Current children cumulated vsize (Kb) 40796

[startup+160.018 s]
Raw data (loadavg): 0.96 0.71 0.48 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 9563 0 2 0 15858 59 0 0 25 0 1 0 1793563667 40521728 9366 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28366/statm): 9893 9366 145 145 0 9748 0
[pid=28366] vsize: 39572
Current children cumulated CPU time (s) 159.18
Current children cumulated vsize (Kb) 41696

[startup+170.018 s]
Raw data (loadavg): 0.96 0.72 0.49 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 9750 0 2 0 16854 61 0 0 25 0 1 0 1793563667 41816064 9553 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28366/statm): 10209 9553 145 145 0 10064 0
[pid=28366] vsize: 40836
Current children cumulated CPU time (s) 169.16
Current children cumulated vsize (Kb) 42960

[startup+180.018 s]
Raw data (loadavg): 0.97 0.73 0.49 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 9987 0 2 0 17850 63 0 0 25 0 1 0 1793563667 42770432 9790 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28366/statm): 10442 9790 145 145 0 10297 0
[pid=28366] vsize: 41768
Current children cumulated CPU time (s) 179.14
Current children cumulated vsize (Kb) 43892

[startup+190.02 s]
Raw data (loadavg): 0.97 0.74 0.50 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 10131 0 2 0 18847 64 0 0 25 0 1 0 1793563667 43356160 9934 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28366/statm): 10585 9934 145 145 0 10440 0
[pid=28366] vsize: 42340
Current children cumulated CPU time (s) 189.12
Current children cumulated vsize (Kb) 44464

[startup+200.021 s]
Raw data (loadavg): 0.98 0.74 0.50 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 10348 0 2 0 19843 66 0 0 25 0 1 0 1793563667 44228608 10151 4294967295 134512640 135094434 3221224448 3221223104 134558227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28366/statm): 10798 10151 145 145 0 10653 0
[pid=28366] vsize: 43192
Current children cumulated CPU time (s) 199.1
Current children cumulated vsize (Kb) 45316

[startup+210.021 s]
Raw data (loadavg): 0.98 0.75 0.50 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 10636 0 2 0 20837 70 0 0 25 0 1 0 1793563667 45379584 10439 4294967295 134512640 135094434 3221224448 3221223104 134557950 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28366/statm): 11079 10439 145 145 0 10934 0
[pid=28366] vsize: 44316
Current children cumulated CPU time (s) 209.08
Current children cumulated vsize (Kb) 46440

[startup+220.023 s]
Raw data (loadavg): 0.98 0.76 0.51 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 10804 0 2 0 21833 72 0 0 25 0 1 0 1793563667 46067712 10607 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28366/statm): 11247 10607 145 145 0 11102 0
[pid=28366] vsize: 44988
Current children cumulated CPU time (s) 219.06
Current children cumulated vsize (Kb) 47112

[startup+230.024 s]
Raw data (loadavg): 0.98 0.77 0.51 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 10960 0 2 0 22830 74 0 0 25 0 1 0 1793563667 46702592 10763 4294967295 134512640 135094434 3221224448 3221223072 134557612 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28366/statm): 11402 10763 145 145 0 11257 0
[pid=28366] vsize: 45608
Current children cumulated CPU time (s) 229.05
Current children cumulated vsize (Kb) 47732

[startup+240.024 s]
Raw data (loadavg): 0.99 0.77 0.52 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 11124 0 2 0 23826 75 0 0 25 0 1 0 1793563667 47374336 10927 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28366/statm): 11566 10927 145 145 0 11421 0
[pid=28366] vsize: 46264
Current children cumulated CPU time (s) 239.02
Current children cumulated vsize (Kb) 48388

[startup+250.025 s]
Raw data (loadavg): 0.99 0.78 0.52 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 11314 0 2 0 24822 76 0 0 25 0 1 0 1793563667 48136192 11117 4294967295 134512640 135094434 3221224448 3221223104 134558426 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28366/statm): 11752 11117 145 145 0 11607 0
[pid=28366] vsize: 47008
Current children cumulated CPU time (s) 248.99
Current children cumulated vsize (Kb) 49132

[startup+260.026 s]
Raw data (loadavg): 0.99 0.79 0.53 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 11543 0 2 0 25818 79 0 0 25 0 1 0 1793563667 49061888 11346 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28366/statm): 11978 11346 145 145 0 11833 0
[pid=28366] vsize: 47912
Current children cumulated CPU time (s) 258.98
Current children cumulated vsize (Kb) 50036

[startup+270.026 s]
Raw data (loadavg): 0.99 0.79 0.53 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 11709 0 2 0 26815 80 0 0 25 0 1 0 1793563667 49717248 11512 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28366/statm): 12138 11512 145 145 0 11993 0
[pid=28366] vsize: 48552
Current children cumulated CPU time (s) 268.96
Current children cumulated vsize (Kb) 50676

[startup+280.027 s]
Raw data (loadavg): 0.99 0.80 0.54 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 12027 0 2 0 27809 83 0 0 25 0 1 0 1793563667 50991104 11830 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 12449 11830 145 145 0 12304 0
[pid=28366] vsize: 49796
Current children cumulated CPU time (s) 278.93
Current children cumulated vsize (Kb) 51920

[startup+290.028 s]
Raw data (loadavg): 0.99 0.81 0.54 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 12288 0 2 0 28805 85 0 0 25 0 1 0 1793563667 52043776 12091 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 12706 12091 145 145 0 12561 0
[pid=28366] vsize: 50824
Current children cumulated CPU time (s) 288.91
Current children cumulated vsize (Kb) 52948

[startup+300.027 s]
Raw data (loadavg): 0.99 0.81 0.55 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 12496 0 2 0 29801 86 0 0 25 0 1 0 1793563667 52899840 12299 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 12915 12299 145 145 0 12770 0
[pid=28366] vsize: 51660
Current children cumulated CPU time (s) 298.88
Current children cumulated vsize (Kb) 53784

[startup+310.028 s]
Raw data (loadavg): 0.99 0.82 0.55 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 12689 0 2 0 30798 88 0 0 25 0 1 0 1793563667 53682176 12492 4294967295 134512640 135094434 3221224448 3221223120 134556252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 13106 12492 145 145 0 12961 0
[pid=28366] vsize: 52424
Current children cumulated CPU time (s) 308.87
Current children cumulated vsize (Kb) 54548

[startup+320.029 s]
Raw data (loadavg): 0.99 0.82 0.56 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 12888 0 2 0 31794 89 0 0 25 0 1 0 1793563667 54489088 12691 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 13303 12691 145 145 0 13158 0
[pid=28366] vsize: 53212
Current children cumulated CPU time (s) 318.84
Current children cumulated vsize (Kb) 55336

[startup+330.029 s]
Raw data (loadavg): 0.99 0.83 0.56 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 13046 0 2 0 32792 91 0 0 25 0 1 0 1793563667 55132160 12849 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 13460 12849 145 145 0 13315 0
[pid=28366] vsize: 53840
Current children cumulated CPU time (s) 328.84
Current children cumulated vsize (Kb) 55964

[startup+340.029 s]
Raw data (loadavg): 0.99 0.83 0.56 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 13227 0 2 0 33789 92 0 0 25 0 1 0 1793563667 55840768 13030 4294967295 134512640 135094434 3221224448 3221223104 134558246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 13633 13030 145 145 0 13488 0
[pid=28366] vsize: 54532
Current children cumulated CPU time (s) 338.82
Current children cumulated vsize (Kb) 56656

[startup+350.03 s]
Raw data (loadavg): 0.99 0.84 0.57 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 13342 0 2 0 34787 93 0 0 25 0 1 0 1793563667 56299520 13145 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 13745 13145 145 145 0 13600 0
[pid=28366] vsize: 54980
Current children cumulated CPU time (s) 348.81
Current children cumulated vsize (Kb) 57104

[startup+360.031 s]
Raw data (loadavg): 0.99 0.84 0.57 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 13499 0 2 0 35785 94 0 0 25 0 1 0 1793563667 56946688 13302 4294967295 134512640 135094434 3221224448 3221223104 134558210 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 13903 13302 145 145 0 13758 0
[pid=28366] vsize: 55612
Current children cumulated CPU time (s) 358.8
Current children cumulated vsize (Kb) 57736

[startup+370.031 s]
Raw data (loadavg): 0.99 0.85 0.58 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 13626 0 2 0 36783 95 0 0 25 0 1 0 1793563667 57462784 13429 4294967295 134512640 135094434 3221224448 3221223072 134557585 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 14029 13429 145 145 0 13884 0
[pid=28366] vsize: 56116
Current children cumulated CPU time (s) 368.79
Current children cumulated vsize (Kb) 58240

[startup+380.031 s]
Raw data (loadavg): 0.99 0.85 0.58 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 13859 0 2 0 37780 96 0 0 25 0 1 0 1793563667 58413056 13662 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 14261 13662 145 145 0 14116 0
[pid=28366] vsize: 57044
Current children cumulated CPU time (s) 378.77
Current children cumulated vsize (Kb) 59168

[startup+390.032 s]
Raw data (loadavg): 0.99 0.86 0.58 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 14098 0 2 0 38777 98 0 0 25 0 1 0 1793563667 59375616 13901 4294967295 134512640 135094434 3221224448 3221223104 134557928 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 14496 13901 145 145 0 14351 0
[pid=28366] vsize: 57984
Current children cumulated CPU time (s) 388.76
Current children cumulated vsize (Kb) 60108

[startup+400.033 s]
Raw data (loadavg): 0.99 0.86 0.59 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 14386 0 2 0 39771 100 0 0 25 0 1 0 1793563667 60538880 14189 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 14780 14189 145 145 0 14635 0
[pid=28366] vsize: 59120
Current children cumulated CPU time (s) 398.72
Current children cumulated vsize (Kb) 61244

[startup+410.033 s]
Raw data (loadavg): 0.99 0.87 0.59 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 14671 0 2 0 40767 102 0 0 25 0 1 0 1793563667 61702144 14474 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 15064 14474 145 145 0 14919 0
[pid=28366] vsize: 60256
Current children cumulated CPU time (s) 408.7
Current children cumulated vsize (Kb) 62380

[startup+420.034 s]
Raw data (loadavg): 0.99 0.87 0.60 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 14872 0 2 0 41764 104 0 0 25 0 1 0 1793563667 62513152 14675 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 15262 14675 145 145 0 15117 0
[pid=28366] vsize: 61048
Current children cumulated CPU time (s) 418.69
Current children cumulated vsize (Kb) 63172

[startup+430.035 s]
Raw data (loadavg): 0.99 0.87 0.60 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 14980 0 2 0 42762 105 0 0 25 0 1 0 1793563667 62971904 14783 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 15374 14783 145 145 0 15229 0
[pid=28366] vsize: 61496
Current children cumulated CPU time (s) 428.68
Current children cumulated vsize (Kb) 63620

[startup+440.035 s]
Raw data (loadavg): 0.99 0.88 0.60 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 15115 0 2 0 43761 106 0 0 25 0 1 0 1793563667 63508480 14918 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 15505 14918 145 145 0 15360 0
[pid=28366] vsize: 62020
Current children cumulated CPU time (s) 438.68
Current children cumulated vsize (Kb) 64144

[startup+450.036 s]
Raw data (loadavg): 0.99 0.88 0.61 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 15263 0 2 0 44759 107 0 0 25 0 1 0 1793563667 64139264 15066 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 15659 15066 145 145 0 15514 0
[pid=28366] vsize: 62636
Current children cumulated CPU time (s) 448.67
Current children cumulated vsize (Kb) 64760

[startup+460.038 s]
Raw data (loadavg): 0.99 0.88 0.61 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 15348 0 2 0 45757 108 0 0 25 0 1 0 1793563667 64499712 15151 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 15747 15151 145 145 0 15602 0
[pid=28366] vsize: 62988
Current children cumulated CPU time (s) 458.66
Current children cumulated vsize (Kb) 65112

[startup+470.038 s]
Raw data (loadavg): 0.99 0.89 0.61 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 15437 0 2 0 46756 109 0 0 25 0 1 0 1793563667 64872448 15240 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 15838 15240 145 145 0 15693 0
[pid=28366] vsize: 63352
Current children cumulated CPU time (s) 468.66
Current children cumulated vsize (Kb) 65476

[startup+480.038 s]
Raw data (loadavg): 0.99 0.89 0.62 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 15522 0 2 0 47755 109 0 0 25 0 1 0 1793563667 65224704 15325 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 15924 15325 145 145 0 15779 0
[pid=28366] vsize: 63696
Current children cumulated CPU time (s) 478.65
Current children cumulated vsize (Kb) 65820

[startup+490.04 s]
Raw data (loadavg): 0.99 0.89 0.62 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 15607 0 2 0 48754 110 0 0 25 0 1 0 1793563667 65589248 15410 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 16013 15410 145 145 0 15868 0
[pid=28366] vsize: 64052
Current children cumulated CPU time (s) 488.65
Current children cumulated vsize (Kb) 66176

[startup+500.041 s]
Raw data (loadavg): 0.99 0.90 0.63 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 15746 0 2 0 49752 111 0 0 25 0 1 0 1793563667 66142208 15549 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 16148 15549 145 145 0 16003 0
[pid=28366] vsize: 64592
Current children cumulated CPU time (s) 498.64
Current children cumulated vsize (Kb) 66716

[startup+510.041 s]
Raw data (loadavg): 0.99 0.90 0.63 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 15893 0 2 0 50749 112 0 0 25 0 1 0 1793563667 66736128 15696 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 16293 15696 145 145 0 16148 0
[pid=28366] vsize: 65172
Current children cumulated CPU time (s) 508.62
Current children cumulated vsize (Kb) 67296

[startup+520.043 s]
Raw data (loadavg): 0.99 0.90 0.63 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 16033 0 2 0 51747 114 0 0 25 0 1 0 1793563667 67309568 15836 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 16433 15836 145 145 0 16288 0
[pid=28366] vsize: 65732
Current children cumulated CPU time (s) 518.62
Current children cumulated vsize (Kb) 67856

[startup+530.043 s]
Raw data (loadavg): 0.99 0.90 0.64 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 16179 0 2 0 52745 115 0 0 25 0 1 0 1793563667 67907584 15982 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 16579 15982 145 145 0 16434 0
[pid=28366] vsize: 66316
Current children cumulated CPU time (s) 528.61
Current children cumulated vsize (Kb) 68440

[startup+540.043 s]
Raw data (loadavg): 0.99 0.91 0.64 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 16460 0 2 0 53740 116 0 0 25 0 1 0 1793563667 70078464 16263 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 17109 16263 145 145 0 16964 0
[pid=28366] vsize: 68436
Current children cumulated CPU time (s) 538.57
Current children cumulated vsize (Kb) 70560

[startup+550.044 s]
Raw data (loadavg): 0.99 0.91 0.64 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 16617 0 2 0 54737 117 0 0 25 0 1 0 1793563667 70705152 16420 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 17262 16420 145 145 0 17117 0
[pid=28366] vsize: 69048
Current children cumulated CPU time (s) 548.55
Current children cumulated vsize (Kb) 71172

[startup+560.046 s]
Raw data (loadavg): 0.99 0.91 0.65 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 16719 0 2 0 55735 119 0 0 25 0 1 0 1793563667 71131136 16522 4294967295 134512640 135094434 3221224448 3221223104 134557900 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 17366 16522 145 145 0 17221 0
[pid=28366] vsize: 69464
Current children cumulated CPU time (s) 558.55
Current children cumulated vsize (Kb) 71588

[startup+570.046 s]
Raw data (loadavg): 0.99 0.91 0.65 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 16912 0 2 0 56732 120 0 0 25 0 1 0 1793563667 71913472 16715 4294967295 134512640 135094434 3221224448 3221223104 134558225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 17557 16715 145 145 0 17412 0
[pid=28366] vsize: 70228
Current children cumulated CPU time (s) 568.53
Current children cumulated vsize (Kb) 72352

[startup+580.047 s]
Raw data (loadavg): 0.99 0.92 0.65 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17087 0 2 0 57729 121 0 0 25 0 1 0 1793563667 72613888 16890 4294967295 134512640 135094434 3221224448 3221223040 134556843 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 17728 16890 145 145 0 17583 0
[pid=28366] vsize: 70912
Current children cumulated CPU time (s) 578.51
Current children cumulated vsize (Kb) 73036

[startup+590.048 s]
Raw data (loadavg): 0.99 0.92 0.66 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17260 0 2 0 58725 122 0 0 25 0 1 0 1793563667 73314304 17063 4294967295 134512640 135094434 3221224448 3221223084 134557560 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 17899 17063 145 145 0 17754 0
[pid=28366] vsize: 71596
Current children cumulated CPU time (s) 588.48
Current children cumulated vsize (Kb) 73720

[startup+600.048 s]
Raw data (loadavg): 0.99 0.92 0.66 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17445 0 2 0 59722 123 0 0 25 0 1 0 1793563667 74047488 17248 4294967295 134512640 135094434 3221224448 3221223072 134557714 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 18078 17248 145 145 0 17933 0
[pid=28366] vsize: 72312
Current children cumulated CPU time (s) 598.46
Current children cumulated vsize (Kb) 74436

[startup+610.048 s]
Raw data (loadavg): 0.99 0.92 0.66 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17579 0 2 0 60719 124 0 0 25 0 1 0 1793563667 74588160 17382 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 18210 17382 145 145 0 18065 0
[pid=28366] vsize: 72840
Current children cumulated CPU time (s) 608.44
Current children cumulated vsize (Kb) 74964

[startup+620.049 s]
Raw data (loadavg): 0.99 0.92 0.66 1/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) T 28362 28362 6872 0 -1 0 17707 0 2 0 61717 125 0 0 25 0 1 0 1793563667 75128832 17510 4294967295 134512640 135094434 3221224448 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/28366/statm): 18342 17510 145 145 0 18197 0
[pid=28366] vsize: 73368
Current children cumulated CPU time (s) 618.43
Current children cumulated vsize (Kb) 75492

[startup+630.05 s]
Raw data (loadavg): 0.99 0.93 0.67 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17761 0 2 0 62716 126 0 0 25 0 1 0 1793563667 75337728 17564 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 18393 17564 145 145 0 18248 0
[pid=28366] vsize: 73572
Current children cumulated CPU time (s) 628.43
Current children cumulated vsize (Kb) 75696

[startup+640.05 s]
Raw data (loadavg): 0.99 0.93 0.67 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17761 0 2 0 63716 126 0 0 25 0 1 0 1793563667 75337728 17564 4294967295 134512640 135094434 3221224448 3221223060 134563055 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28366/statm): 18393 17564 145 145 0 18248 0
[pid=28366] vsize: 73572
Current children cumulated CPU time (s) 638.43
Current children cumulated vsize (Kb) 75696

[startup+650.051 s]
Raw data (loadavg): 0.99 0.93 0.67 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17761 0 2 0 64715 126 0 0 25 0 1 0 1793563667 75337728 17564 4294967295 134512640 135094434 3221224448 3221223104 134558395 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28366/statm): 18393 17564 145 145 0 18248 0
[pid=28366] vsize: 73572
Current children cumulated CPU time (s) 648.42
Current children cumulated vsize (Kb) 75696

[startup+660.053 s]
Raw data (loadavg): 0.99 0.93 0.68 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17761 0 2 0 65715 127 0 0 25 0 1 0 1793563667 75337728 17564 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 18393 17564 145 145 0 18248 0
[pid=28366] vsize: 73572
Current children cumulated CPU time (s) 658.43
Current children cumulated vsize (Kb) 75696

[startup+670.053 s]
Raw data (loadavg): 0.99 0.93 0.68 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17761 0 2 0 66715 127 0 0 25 0 1 0 1793563667 75337728 17564 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 18393 17564 145 145 0 18248 0
[pid=28366] vsize: 73572
Current children cumulated CPU time (s) 668.43
Current children cumulated vsize (Kb) 75696

[startup+680.053 s]
Raw data (loadavg): 0.99 0.94 0.68 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17761 0 2 0 67715 127 0 0 25 0 1 0 1793563667 75337728 17564 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 18393 17564 145 145 0 18248 0
[pid=28366] vsize: 73572
Current children cumulated CPU time (s) 678.43
Current children cumulated vsize (Kb) 75696

[startup+690.054 s]
Raw data (loadavg): 0.99 0.94 0.68 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17761 0 2 0 68715 127 0 0 25 0 1 0 1793563667 75337728 17564 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 18393 17564 145 145 0 18248 0
[pid=28366] vsize: 73572
Current children cumulated CPU time (s) 688.43
Current children cumulated vsize (Kb) 75696

[startup+700.054 s]
Raw data (loadavg): 0.99 0.94 0.69 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17761 0 2 0 69715 127 0 0 25 0 1 0 1793563667 75337728 17564 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 18393 17564 145 145 0 18248 0
[pid=28366] vsize: 73572
Current children cumulated CPU time (s) 698.43
Current children cumulated vsize (Kb) 75696

[startup+710.055 s]
Raw data (loadavg): 0.99 0.94 0.69 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17761 0 2 0 70716 127 0 0 25 0 1 0 1793563667 75337728 17564 4294967295 134512640 135094434 3221224448 3221223104 134558426 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 18393 17564 145 145 0 18248 0
[pid=28366] vsize: 73572
Current children cumulated CPU time (s) 708.44
Current children cumulated vsize (Kb) 75696

[startup+720.056 s]
Raw data (loadavg): 0.99 0.94 0.69 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17761 0 2 0 71716 127 0 0 25 0 1 0 1793563667 75337728 17564 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 18393 17564 145 145 0 18248 0
[pid=28366] vsize: 73572
Current children cumulated CPU time (s) 718.44
Current children cumulated vsize (Kb) 75696

[startup+730.057 s]
Raw data (loadavg): 0.99 0.94 0.70 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17761 0 2 0 72716 127 0 0 25 0 1 0 1793563667 75337728 17564 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 18393 17564 145 145 0 18248 0
[pid=28366] vsize: 73572
Current children cumulated CPU time (s) 728.44
Current children cumulated vsize (Kb) 75696

[startup+740.057 s]
Raw data (loadavg): 0.99 0.94 0.70 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17761 0 2 0 73716 127 0 0 25 0 1 0 1793563667 75337728 17564 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 18393 17564 145 145 0 18248 0
[pid=28366] vsize: 73572
Current children cumulated CPU time (s) 738.44
Current children cumulated vsize (Kb) 75696

[startup+750.058 s]
Raw data (loadavg): 0.99 0.95 0.70 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17761 0 2 0 74717 127 0 0 25 0 1 0 1793563667 75337728 17564 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 18393 17564 145 145 0 18248 0
[pid=28366] vsize: 73572
Current children cumulated CPU time (s) 748.45
Current children cumulated vsize (Kb) 75696

[startup+760.06 s]
Raw data (loadavg): 0.99 0.95 0.71 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17761 0 2 0 75717 127 0 0 25 0 1 0 1793563667 75337728 17564 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 18393 17564 145 145 0 18248 0
[pid=28366] vsize: 73572
Current children cumulated CPU time (s) 758.45
Current children cumulated vsize (Kb) 75696

[startup+770.06 s]
Raw data (loadavg): 0.99 0.95 0.71 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17762 0 2 0 76717 127 0 0 25 0 1 0 1793563667 75337728 17565 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 18393 17565 145 145 0 18248 0
[pid=28366] vsize: 73572
Current children cumulated CPU time (s) 768.45
Current children cumulated vsize (Kb) 75696

[startup+780.061 s]
Raw data (loadavg): 0.99 0.95 0.71 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17762 0 2 0 77717 127 0 0 25 0 1 0 1793563667 75337728 17565 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 18393 17565 145 145 0 18248 0
[pid=28366] vsize: 73572
Current children cumulated CPU time (s) 778.45
Current children cumulated vsize (Kb) 75696

[startup+790.062 s]
Raw data (loadavg): 0.99 0.95 0.71 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17762 0 2 0 78718 127 0 0 25 0 1 0 1793563667 75337728 17565 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 18393 17565 145 145 0 18248 0
[pid=28366] vsize: 73572
Current children cumulated CPU time (s) 788.46
Current children cumulated vsize (Kb) 75696

[startup+800.062 s]
Raw data (loadavg): 0.99 0.95 0.72 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17763 0 2 0 79718 127 0 0 25 0 1 0 1793563667 75337728 17566 4294967295 134512640 135094434 3221224448 3221223072 134557653 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 18393 17566 145 145 0 18248 0
[pid=28366] vsize: 73572
Current children cumulated CPU time (s) 798.46
Current children cumulated vsize (Kb) 75696

[startup+810.063 s]
Raw data (loadavg): 0.99 0.95 0.72 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17763 0 2 0 80718 127 0 0 25 0 1 0 1793563667 75337728 17566 4294967295 134512640 135094434 3221224448 3221223072 134557696 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 18393 17566 145 145 0 18248 0
[pid=28366] vsize: 73572
Current children cumulated CPU time (s) 808.46
Current children cumulated vsize (Kb) 75696

[startup+820.064 s]
Raw data (loadavg): 0.99 0.95 0.72 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17763 0 2 0 81718 127 0 0 25 0 1 0 1793563667 75337728 17566 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 18393 17566 145 145 0 18248 0
[pid=28366] vsize: 73572
Current children cumulated CPU time (s) 818.46
Current children cumulated vsize (Kb) 75696

[startup+830.065 s]
Raw data (loadavg): 0.99 0.95 0.73 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17763 0 2 0 82719 127 0 0 25 0 1 0 1793563667 75337728 17566 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 18393 17566 145 145 0 18248 0
[pid=28366] vsize: 73572
Current children cumulated CPU time (s) 828.47
Current children cumulated vsize (Kb) 75696

[startup+840.065 s]
Raw data (loadavg): 0.99 0.95 0.73 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17763 0 2 0 83719 127 0 0 25 0 1 0 1793563667 75337728 17566 4294967295 134512640 135094434 3221224448 3221223104 134558172 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 18393 17566 145 145 0 18248 0
[pid=28366] vsize: 73572
Current children cumulated CPU time (s) 838.47
Current children cumulated vsize (Kb) 75696

[startup+850.066 s]
Raw data (loadavg): 0.99 0.96 0.73 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17764 0 2 0 84719 127 0 0 25 0 1 0 1793563667 75337728 17567 4294967295 134512640 135094434 3221224448 3221223072 134557669 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 18393 17567 145 145 0 18248 0
[pid=28366] vsize: 73572
Current children cumulated CPU time (s) 848.47
Current children cumulated vsize (Kb) 75696

[startup+860.067 s]
Raw data (loadavg): 0.99 0.96 0.73 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17764 0 2 0 85719 127 0 0 25 0 1 0 1793563667 75337728 17567 4294967295 134512640 135094434 3221224448 3221223060 134563069 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 18393 17567 145 145 0 18248 0
[pid=28366] vsize: 73572
Current children cumulated CPU time (s) 858.47
Current children cumulated vsize (Kb) 75696

[startup+870.067 s]
Raw data (loadavg): 0.99 0.96 0.73 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17765 0 2 0 86720 127 0 0 25 0 1 0 1793563667 75337728 17568 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 18393 17568 145 145 0 18248 0
[pid=28366] vsize: 73572
Current children cumulated CPU time (s) 868.48
Current children cumulated vsize (Kb) 75696

[startup+880.068 s]
Raw data (loadavg): 0.99 0.96 0.74 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17765 0 2 0 87720 127 0 0 25 0 1 0 1793563667 75337728 17568 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 18393 17568 145 145 0 18248 0
[pid=28366] vsize: 73572
Current children cumulated CPU time (s) 878.48
Current children cumulated vsize (Kb) 75696

[startup+890.069 s]
Raw data (loadavg): 0.99 0.96 0.74 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17765 0 2 0 88720 127 0 0 25 0 1 0 1793563667 75337728 17568 4294967295 134512640 135094434 3221224448 3221223104 134557829 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 18393 17568 145 145 0 18248 0
[pid=28366] vsize: 73572
Current children cumulated CPU time (s) 888.48
Current children cumulated vsize (Kb) 75696

[startup+900.07 s]
Raw data (loadavg): 0.99 0.96 0.74 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17765 0 2 0 89720 127 0 0 25 0 1 0 1793563667 75337728 17568 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28366/statm): 18393 17568 145 145 0 18248 0
[pid=28366] vsize: 73572
Current children cumulated CPU time (s) 898.48
Current children cumulated vsize (Kb) 75696

[startup+910.071 s]
Raw data (loadavg): 0.99 0.96 0.74 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17765 0 2 0 90720 127 0 0 25 0 1 0 1793563667 75337728 17568 4294967295 134512640 135094434 3221224448 3221223108 134553491 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 18393 17568 145 145 0 18248 0
[pid=28366] vsize: 73572
Current children cumulated CPU time (s) 908.48
Current children cumulated vsize (Kb) 75696

[startup+920.072 s]
Raw data (loadavg): 0.99 0.96 0.74 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17765 0 2 0 91720 127 0 0 25 0 1 0 1793563667 75337728 17568 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 18393 17568 145 145 0 18248 0
[pid=28366] vsize: 73572
Current children cumulated CPU time (s) 918.48
Current children cumulated vsize (Kb) 75696

[startup+930.073 s]
Raw data (loadavg): 0.99 0.96 0.75 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17766 0 2 0 92720 127 0 0 25 0 1 0 1793563667 75337728 17569 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 18393 17569 145 145 0 18248 0
[pid=28366] vsize: 73572
Current children cumulated CPU time (s) 928.48
Current children cumulated vsize (Kb) 75696

[startup+940.073 s]
Raw data (loadavg): 0.99 0.96 0.75 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17768 0 2 0 93721 127 0 0 25 0 1 0 1793563667 75337728 17571 4294967295 134512640 135094434 3221224448 3221223136 134554739 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 18393 17571 145 145 0 18248 0
[pid=28366] vsize: 73572
Current children cumulated CPU time (s) 938.49
Current children cumulated vsize (Kb) 75696

[startup+950.074 s]
Raw data (loadavg): 0.99 0.97 0.75 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17768 0 2 0 94721 127 0 0 25 0 1 0 1793563667 75337728 17571 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 18393 17571 145 145 0 18248 0
[pid=28366] vsize: 73572
Current children cumulated CPU time (s) 948.49
Current children cumulated vsize (Kb) 75696

[startup+960.075 s]
Raw data (loadavg): 0.99 0.97 0.75 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17768 0 2 0 95721 127 0 0 25 0 1 0 1793563667 75337728 17571 4294967295 134512640 135094434 3221224448 3221223104 134557879 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 18393 17571 145 145 0 18248 0
[pid=28366] vsize: 73572
Current children cumulated CPU time (s) 958.49
Current children cumulated vsize (Kb) 75696

[startup+970.075 s]
Raw data (loadavg): 0.99 0.97 0.75 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17769 0 2 0 96721 127 0 0 25 0 1 0 1793563667 75337728 17572 4294967295 134512640 135094434 3221224448 3221223104 134558218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 18393 17572 145 145 0 18248 0
[pid=28366] vsize: 73572
Current children cumulated CPU time (s) 968.49
Current children cumulated vsize (Kb) 75696

[startup+980.075 s]
Raw data (loadavg): 0.99 0.97 0.76 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17769 0 2 0 97722 127 0 0 25 0 1 0 1793563667 75337728 17572 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 18393 17572 145 145 0 18248 0
[pid=28366] vsize: 73572
Current children cumulated CPU time (s) 978.5
Current children cumulated vsize (Kb) 75696

[startup+990.076 s]
Raw data (loadavg): 0.99 0.97 0.76 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17769 0 2 0 98722 127 0 0 25 0 1 0 1793563667 75337728 17572 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 18393 17572 145 145 0 18248 0
[pid=28366] vsize: 73572
Current children cumulated CPU time (s) 988.5
Current children cumulated vsize (Kb) 75696

[startup+1000.08 s]
Raw data (loadavg): 0.99 0.97 0.76 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17769 0 2 0 99722 127 0 0 25 0 1 0 1793563667 75337728 17572 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 18393 17572 145 145 0 18248 0
[pid=28366] vsize: 73572
Current children cumulated CPU time (s) 998.5
Current children cumulated vsize (Kb) 75696

[startup+1010.08 s]
Raw data (loadavg): 0.99 0.97 0.76 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17769 0 2 0 100722 127 0 0 25 0 1 0 1793563667 75337728 17572 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 18393 17572 145 145 0 18248 0
[pid=28366] vsize: 73572
Current children cumulated CPU time (s) 1008.5
Current children cumulated vsize (Kb) 75696

[startup+1020.08 s]
Raw data (loadavg): 0.99 0.97 0.76 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17769 0 2 0 101723 127 0 0 25 0 1 0 1793563667 75337728 17572 4294967295 134512640 135094434 3221224448 3221223092 134558040 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 18393 17572 145 145 0 18248 0
[pid=28366] vsize: 73572
Current children cumulated CPU time (s) 1018.51
Current children cumulated vsize (Kb) 75696

[startup+1030.08 s]
Raw data (loadavg): 0.99 0.97 0.77 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17769 0 2 0 102723 127 0 0 25 0 1 0 1793563667 75337728 17572 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 18393 17572 145 145 0 18248 0
[pid=28366] vsize: 73572
Current children cumulated CPU time (s) 1028.51
Current children cumulated vsize (Kb) 75696

[startup+1040.08 s]
Raw data (loadavg): 0.99 0.97 0.77 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17770 0 2 0 103723 127 0 0 25 0 1 0 1793563667 75337728 17573 4294967295 134512640 135094434 3221224448 3221223040 134557232 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 18393 17573 145 145 0 18248 0
[pid=28366] vsize: 73572
Current children cumulated CPU time (s) 1038.51
Current children cumulated vsize (Kb) 75696

[startup+1050.08 s]
Raw data (loadavg): 0.99 0.97 0.77 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17771 0 2 0 104723 127 0 0 25 0 1 0 1793563667 75337728 17574 4294967295 134512640 135094434 3221224448 3221223104 134558004 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 18393 17574 145 145 0 18248 0
[pid=28366] vsize: 73572
Current children cumulated CPU time (s) 1048.51
Current children cumulated vsize (Kb) 75696

[startup+1060.08 s]
Raw data (loadavg): 0.99 0.97 0.77 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17771 0 2 0 105724 127 0 0 25 0 1 0 1793563667 75337728 17574 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 18393 17574 145 145 0 18248 0
[pid=28366] vsize: 73572
Current children cumulated CPU time (s) 1058.52
Current children cumulated vsize (Kb) 75696

[startup+1070.08 s]
Raw data (loadavg): 0.99 0.97 0.77 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17771 0 2 0 106724 127 0 0 25 0 1 0 1793563667 75337728 17574 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 18393 17574 145 145 0 18248 0
[pid=28366] vsize: 73572
Current children cumulated CPU time (s) 1068.52
Current children cumulated vsize (Kb) 75696

[startup+1080.08 s]
Raw data (loadavg): 0.99 0.97 0.78 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17771 0 2 0 107724 127 0 0 25 0 1 0 1793563667 75337728 17574 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 18393 17574 145 145 0 18248 0
[pid=28366] vsize: 73572
Current children cumulated CPU time (s) 1078.52
Current children cumulated vsize (Kb) 75696

[startup+1090.08 s]
Raw data (loadavg): 0.99 0.97 0.78 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17771 0 2 0 108724 127 0 0 25 0 1 0 1793563667 75337728 17574 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 18393 17574 145 145 0 18248 0
[pid=28366] vsize: 73572
Current children cumulated CPU time (s) 1088.52
Current children cumulated vsize (Kb) 75696

[startup+1100.08 s]
Raw data (loadavg): 0.99 0.97 0.78 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17772 0 2 0 109725 127 0 0 25 0 1 0 1793563667 75337728 17575 4294967295 134512640 135094434 3221224448 3221223072 134557734 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 18393 17575 145 145 0 18248 0
[pid=28366] vsize: 73572
Current children cumulated CPU time (s) 1098.53
Current children cumulated vsize (Kb) 75696

[startup+1110.09 s]
Raw data (loadavg): 0.99 0.97 0.78 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17772 0 2 0 110725 127 0 0 25 0 1 0 1793563667 75337728 17575 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 18393 17575 145 145 0 18248 0
[pid=28366] vsize: 73572
Current children cumulated CPU time (s) 1108.53
Current children cumulated vsize (Kb) 75696

[startup+1120.09 s]
Raw data (loadavg): 0.99 0.97 0.78 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17772 0 2 0 111725 127 0 0 25 0 1 0 1793563667 75337728 17575 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 18393 17575 145 145 0 18248 0
[pid=28366] vsize: 73572
Current children cumulated CPU time (s) 1118.53
Current children cumulated vsize (Kb) 75696

[startup+1130.09 s]
Raw data (loadavg): 0.99 0.97 0.79 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17773 0 2 0 112725 127 0 0 25 0 1 0 1793563667 75337728 17576 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 18393 17576 145 145 0 18248 0
[pid=28366] vsize: 73572
Current children cumulated CPU time (s) 1128.53
Current children cumulated vsize (Kb) 75696

[startup+1140.09 s]
Raw data (loadavg): 0.99 0.97 0.79 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17773 0 2 0 113726 127 0 0 25 0 1 0 1793563667 75337728 17576 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 18393 17576 145 145 0 18248 0
[pid=28366] vsize: 73572
Current children cumulated CPU time (s) 1138.54
Current children cumulated vsize (Kb) 75696

[startup+1150.09 s]
Raw data (loadavg): 0.99 0.97 0.79 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17773 0 2 0 114726 127 0 0 25 0 1 0 1793563667 75337728 17576 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 18393 17576 145 145 0 18248 0
[pid=28366] vsize: 73572
Current children cumulated CPU time (s) 1148.54
Current children cumulated vsize (Kb) 75696

[startup+1160.09 s]
Raw data (loadavg): 0.99 0.97 0.79 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17773 0 2 0 115726 127 0 0 25 0 1 0 1793563667 75337728 17576 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 18393 17576 145 145 0 18248 0
[pid=28366] vsize: 73572
Current children cumulated CPU time (s) 1158.54
Current children cumulated vsize (Kb) 75696

[startup+1170.09 s]
Raw data (loadavg): 0.99 0.97 0.79 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17851 0 2 0 116725 127 0 0 25 0 1 0 1793563667 75657216 17654 4294967295 134512640 135094434 3221224448 3221223104 134557950 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 18471 17654 145 145 0 18326 0
[pid=28366] vsize: 73884
Current children cumulated CPU time (s) 1168.53
Current children cumulated vsize (Kb) 76008

[startup+1180.09 s]
Raw data (loadavg): 0.99 0.97 0.79 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 17959 0 2 0 117723 129 0 0 25 0 1 0 1793563667 76111872 17762 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 18582 17762 145 145 0 18437 0
[pid=28366] vsize: 74328
Current children cumulated CPU time (s) 1178.53
Current children cumulated vsize (Kb) 76452

[startup+1190.09 s]
Raw data (loadavg): 0.99 0.97 0.80 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 18059 0 2 0 118722 129 0 0 25 0 1 0 1793563667 76517376 17862 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 18681 17862 145 145 0 18536 0
[pid=28366] vsize: 74724
Current children cumulated CPU time (s) 1188.52
Current children cumulated vsize (Kb) 76848

[startup+1200.09 s]
Raw data (loadavg): 0.99 0.97 0.80 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 18235 0 2 0 119719 130 0 0 25 0 1 0 1793563667 77238272 18038 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 18857 18038 145 145 0 18712 0
[pid=28366] vsize: 75428
Current children cumulated CPU time (s) 1198.5
Current children cumulated vsize (Kb) 77552

[startup+1210.09 s]
Raw data (loadavg): 0.99 0.97 0.80 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 18579 0 2 0 120714 132 0 0 25 0 1 0 1793563667 78647296 18382 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 19201 18382 145 145 0 19056 0
[pid=28366] vsize: 76804
Current children cumulated CPU time (s) 1208.47
Current children cumulated vsize (Kb) 78928



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.09 s]
Raw data (loadavg): 0.99 0.97 0.80 2/57 28366
Raw data (/proc/28362/stat): 28362 (minisat+_script) S 28361 28362 6872 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1793563661 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/28362/statm): 531 226 485 147 0 384 0
[pid=28362] vsize: 2124
Raw data (/proc/28366/stat): 28366 (minisat+_64-bit) R 28362 28362 6872 0 -1 0 18579 0 2 0 120714 132 0 0 25 0 1 0 1793563667 78647296 18382 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28366/statm): 19201 18382 145 145 0 19056 0
[pid=28366] vsize: 76804
Current children cumulated CPU time (s) 1208.47
Current children cumulated vsize (Kb) 78928

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

Child status: 0
Real time (s): 1210.13
CPU time (s): 1208.5
CPU user time (s): 1207.14
CPU system time (s): 1.35579
CPU usage (%): 99.8651
Max. virtual memory (cumulated for all children) (Kb): 78928

Verifier Data

ERROR: no interpretation found !