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

Nameweb/www.ps.uni-sb.de/~walser/benchmarks/course-ass/normalized-ws97-5.opb
MD5SUM6049145b9f1adfd7114adf044503d587
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 2642
Optimality of the best value was proved YES
Number of terms in the objective function 748
Biggest coefficient in the objective function 240
Number of bits for the biggest coefficient in the objective function 8
Sum of the numbers in the objective function 33855
Number of bits of the sum of numbers in the objective function 16
Biggest number in a constraint 240
Number of bits of the biggest number in a constraint 8
Biggest sum of numbers in a constraint 33855
Number of bits of the biggest sum of numbers16
Best result obtained on this benchmarkOPTIMUM FOUND
Best CPU time to get the best result obtained on this benchmark965.053
Number of variables907
Total number of constraints1309
Number of constraints which are clauses126
Number of constraints which are cardinality constraints (but not clauses)1183
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint1
Maximum length of a constraint134

Trace number 2344

Launcher Data

LAUNCH ON wulflinc22 THE 2005-09-18 19:05:39 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2728 boxname=wulflinc22 idbench=384 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  6049145b9f1adfd7114adf044503d587  /oldhome/oroussel/tmp/wulflinc22/normalized-ws97-5.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc22/normalized-ws97-5.opb
IDLAUNCH: 2728
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.031
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.031
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:        912452 kB
Buffers:         34668 kB
Cached:          60336 kB
SwapCached:        536 kB
Active:          67080 kB
Inactive:        30508 kB
HighTotal:      131008 kB
HighFree:        68656 kB
LowTotal:       903652 kB
LowFree:        843796 kB
SwapTotal:     2097892 kB
SwapFree:      2096832 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5864 kB
Slab:            19104 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-18 19:25:49 (client local time) WITH STATUS 10 IN 1209.51 SECONDS
stats: 2728 7 1209.51 10

Solver Data

c Parsing PB file...
c Converting 661 PB-constraints to clauses...
c   -- Unit propagations: ppp
c   -- Detecting intervals from adjacent constraints: ##################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): .............................................................................................................................
c ---[ 660]---> Adder-cost: 238   maxlim: 90   bits: 7/7
c ---[ 659]---> Adder-cost: 238   maxlim: 90   bits: 7/7
c ---[ 658]---> Adder-cost: 238   maxlim: 90   bits: 7/7
c ---[ 657]---> Adder-cost: 238   maxlim: 91   bits: 7/7
c ---[ 656]---> Adder-cost: 260   maxlim: 85   bits: 8/7
c ---[ 655]---> Adder-cost: 260   maxlim: 84   bits: 8/7
c ---[ 654]---> Adder-cost: 260   maxlim: 84   bits: 8/7
c ---[ 653]---> Adder-cost: 19   maxlim: 23   bits: 6/5
c ---[ 652]---> Adder-cost: 19   maxlim: 23   bits: 6/5
c ---[ 651]---> Adder-cost: 19   maxlim: 23   bits: 6/5
c ---[ 650]---> Adder-cost: 19   maxlim: 22   bits: 6/5
c ---[ 649]---> Adder-cost: 28   maxlim: 33   bits: 7/6
c ---[ 648]---> Adder-cost: 28   maxlim: 34   bits: 7/6
c ---[ 647]---> Adder-cost: 28   maxlim: 34   bits: 7/6
c ---[ 645]---> BDD-cost:    5
c ---[ 643]---> BDD-cost:    3
c ---[ 641]---> BDD-cost:    5
c ---[ 639]---> BDD-cost:    3
c ---[ 637]---> BDD-cost:    5
c ---[ 635]---> BDD-cost:    3
c ---[ 633]---> BDD-cost:    5
c ---[ 631]---> BDD-cost:    3
c ---[ 629]---> BDD-cost:    5
c ---[ 627]---> BDD-cost:    3
c ---[ 625]---> BDD-cost:    5
c ---[ 623]---> BDD-cost:    3
c ---[ 621]---> BDD-cost:    3
c ---[ 619]---> BDD-cost:    5
c ---[ 617]---> BDD-cost:    3
c ---[ 615]---> BDD-cost:    5
c ---[ 613]---> BDD-cost:    3
c ---[ 611]---> BDD-cost:    5
c ---[ 609]---> BDD-cost:    3
c ---[ 607]---> BDD-cost:    3
c ---[ 605]---> BDD-cost:    5
c ---[ 603]---> BDD-cost:    3
c ---[ 601]---> BDD-cost:    5
c ---[ 599]---> BDD-cost:    3
c ---[ 597]---> BDD-cost:    5
c ---[ 595]---> BDD-cost:    3
c ---[ 593]---> BDD-cost:    5
c ---[ 591]---> BDD-cost:    3
c ---[ 589]---> BDD-cost:    5
c ---[ 587]---> BDD-cost:    3
c ---[ 585]---> BDD-cost:    5
c ---[ 583]---> BDD-cost:    3
c ---[ 581]---> BDD-cost:    5
c ---[ 579]---> BDD-cost:    3
c ---[ 577]---> BDD-cost:    5
c ---[ 575]---> BDD-cost:    3
c ---[ 573]---> BDD-cost:    5
c ---[ 571]---> BDD-cost:    3
c ---[ 569]---> BDD-cost:    5
c ---[ 567]---> BDD-cost:    3
c ---[ 565]---> BDD-cost:    5
c ---[ 563]---> BDD-cost:    3
c ---[ 561]---> BDD-cost:    5
c ---[ 559]---> BDD-cost:    3
c ---[ 557]---> BDD-cost:    5
c ---[ 555]---> BDD-cost:    3
c ---[ 553]---> BDD-cost:    5
c ---[ 551]---> BDD-cost:    3
c ---[ 549]---> BDD-cost:    5
c ---[ 547]---> BDD-cost:    3
c ---[ 545]---> BDD-cost:    5
c ---[ 543]---> BDD-cost:    3
c ---[ 541]---> BDD-cost:    5
c ---[ 539]---> BDD-cost:    3
c ---[ 537]---> BDD-cost:    5
c ---[ 535]---> BDD-cost:    3
c ---[ 533]---> BDD-cost:    5
c ---[ 531]---> BDD-cost:    3
c ---[ 529]---> BDD-cost:    5
c ---[ 527]---> BDD-cost:    3
c ---[ 525]---> BDD-cost:    5
c ---[ 523]---> BDD-cost:    3
c ---[ 521]---> BDD-cost:    5
c ---[ 519]---> BDD-cost:    3
c ---[ 517]---> BDD-cost:    5
c ---[ 515]---> BDD-cost:    3
c ---[ 513]---> BDD-cost:    5
c ---[ 511]---> BDD-cost:    3
c ---[ 509]---> BDD-cost:    5
c ---[ 507]---> BDD-cost:    3
c ---[ 505]---> BDD-cost:    5
c ---[ 503]---> BDD-cost:    3
c ---[ 501]---> BDD-cost:    5
c ---[ 499]---> BDD-cost:    3
c ---[ 497]---> BDD-cost:    5
c ---[ 495]---> BDD-cost:    3
c ---[ 493]---> BDD-cost:    5
c ---[ 491]---> BDD-cost:    3
c ---[ 489]---> BDD-cost:    5
c ---[ 487]---> BDD-cost:    3
c ---[ 485]---> BDD-cost:    5
c ---[ 483]---> BDD-cost:    3
c ---[ 481]---> BDD-cost:    5
c ---[ 479]---> BDD-cost:    3
c ---[ 477]---> BDD-cost:    5
c ---[ 475]---> BDD-cost:    3
c ---[ 473]---> BDD-cost:    5
c ---[ 471]---> BDD-cost:    3
c ---[ 469]---> BDD-cost:    5
c ---[ 467]---> BDD-cost:    3
c ---[ 465]---> BDD-cost:    3
c ---[ 463]---> BDD-cost:    5
c ---[ 461]---> BDD-cost:    3
c ---[ 459]---> BDD-cost:    5
c ---[ 457]---> BDD-cost:    3
c ---[ 455]---> BDD-cost:    5
c ---[ 453]---> BDD-cost:    3
c ---[ 451]---> BDD-cost:    5
c ---[ 449]---> BDD-cost:    3
c ---[ 447]---> BDD-cost:    5
c ---[ 445]---> BDD-cost:    3
c ---[ 443]---> BDD-cost:    5
c ---[ 441]---> BDD-cost:    3
c ---[ 439]---> BDD-cost:    5
c ---[ 437]---> BDD-cost:    3
c ---[ 435]---> BDD-cost:    5
c ---[ 433]---> BDD-cost:    3
c ---[ 431]---> BDD-cost:    5
c ---[ 429]---> BDD-cost:    3
c ---[ 427]---> BDD-cost:    5
c ---[ 425]---> BDD-cost:    3
c ---[ 423]---> BDD-cost:    5
c ---[ 421]---> BDD-cost:    3
c ---[ 419]---> BDD-cost:    5
c ---[ 417]---> BDD-cost:    3
c ---[ 415]---> BDD-cost:    5
c ---[ 413]---> BDD-cost:    3
c ---[ 411]---> BDD-cost:    5
c ---[ 409]---> BDD-cost:    3
c ---[ 407]---> BDD-cost:    3
c ---[ 405]---> BDD-cost:    5
c ---[ 403]---> BDD-cost:    3
c ---[ 401]---> BDD-cost:    3
c ---[ 399]---> BDD-cost:    5
c ---[ 397]---> BDD-cost:    3
c ---[ 395]---> BDD-cost:    5
c ---[ 393]---> BDD-cost:    3
c ---[ 391]---> BDD-cost:    5
c ---[ 389]---> BDD-cost:    3
c ---[ 387]---> BDD-cost:    5
c ---[ 385]---> BDD-cost:    3
c ---[ 383]---> BDD-cost:    5
c ---[ 381]---> BDD-cost:    3
c ---[ 379]---> BDD-cost:    5
c ---[ 377]---> BDD-cost:    3
c ---[ 375]---> BDD-cost:    5
c ---[ 373]---> BDD-cost:    3
c ---[ 371]---> BDD-cost:    5
c ---[ 369]---> BDD-cost:    3
c ---[ 367]---> BDD-cost:    5
c ---[ 365]---> BDD-cost:    3
c ---[ 363]---> BDD-cost:    5
c ---[ 361]---> BDD-cost:    3
c ---[ 359]---> BDD-cost:    5
c ---[ 357]---> BDD-cost:    3
c ---[ 355]---> BDD-cost:    5
c ---[ 353]---> BDD-cost:    3
c ---[ 351]---> BDD-cost:    5
c ---[ 349]---> BDD-cost:    3
c ---[ 347]---> BDD-cost:    5
c ---[ 345]---> BDD-cost:    3
c ---[ 343]---> BDD-cost:    5
c ---[ 341]---> BDD-cost:    3
c ---[ 339]---> BDD-cost:    5
c ---[ 337]---> BDD-cost:    3
c ---[ 335]---> BDD-cost:    5
c ---[ 333]---> BDD-cost:    3
c ---[ 327]---> BDD-cost:    5
c ---[ 325]---> BDD-cost:    3
c ---[ 323]---> BDD-cost:    5
c ---[ 321]---> BDD-cost:    3
c ---[ 319]---> BDD-cost:    5
c ---[ 317]---> BDD-cost:    3
c ---[ 315]---> BDD-cost:    5
c ---[ 313]---> BDD-cost:    3
c ---[ 311]---> BDD-cost:    5
c ---[ 309]---> BDD-cost:    3
c ---[ 307]---> BDD-cost:    5
c ---[ 305]---> BDD-cost:    3
c ---[ 303]---> BDD-cost:    5
c ---[ 301]---> BDD-cost:    3
c ---[ 299]---> BDD-cost:    5
c ---[ 297]---> BDD-cost:    3
c ---[ 295]---> BDD-cost:    5
c ---[ 293]---> BDD-cost:    3
c ---[ 291]---> BDD-cost:    5
c ---[ 289]---> BDD-cost:    3
c ---[ 287]---> BDD-cost:    5
c ---[ 285]---> BDD-cost:    3
c ---[ 283]---> BDD-cost:    5
c ---[ 281]---> BDD-cost:    3
c ---[ 279]---> BDD-cost:    5
c ---[ 277]---> BDD-cost:    3
c ---[ 275]---> BDD-cost:    3
c ---[ 273]---> BDD-cost:    5
c ---[ 271]---> BDD-cost:    3
c ---[ 269]---> BDD-cost:    5
c ---[ 267]---> BDD-cost:    3
c ---[ 265]---> BDD-cost:    5
c ---[ 263]---> BDD-cost:    3
c ---[ 261]---> BDD-cost:    5
c ---[ 259]---> BDD-cost:    3
c ---[ 257]---> BDD-cost:    5
c ---[ 255]---> BDD-cost:    3
c ---[ 253]---> BDD-cost:    5
c ---[ 251]---> BDD-cost:    3
c ---[ 249]---> BDD-cost:    5
c ---[ 247]---> BDD-cost:    3
c ---[ 245]---> BDD-cost:    5
c ---[ 243]---> BDD-cost:    3
c ---[ 241]---> BDD-cost:    5
c ---[ 239]---> BDD-cost:    3
c ---[ 237]---> BDD-cost:    5
c ---[ 235]---> BDD-cost:    3
c ---[ 233]---> BDD-cost:    5
c ---[ 231]---> BDD-cost:    3
c ---[ 229]---> BDD-cost:    5
c ---[ 227]---> BDD-cost:    3
c ---[ 225]---> BDD-cost:    5
c ---[ 223]---> BDD-cost:    3
c ---[ 221]---> BDD-cost:    5
c ---[ 219]---> BDD-cost:    3
c ---[ 217]---> BDD-cost:    5
c ---[ 215]---> BDD-cost:    3
c ---[ 213]---> BDD-cost:    5
c ---[ 211]---> BDD-cost:    3
c ---[ 209]---> BDD-cost:    5
c ---[ 207]---> BDD-cost:    3
c ---[ 205]---> BDD-cost:    5
c ---[ 203]---> BDD-cost:    3
c ---[ 201]---> BDD-cost:    5
c ---[ 199]---> BDD-cost:    3
c ---[ 197]---> BDD-cost:    5
c ---[ 195]---> BDD-cost:    3
c ---[ 193]---> BDD-cost:    5
c ---[ 191]---> BDD-cost:    3
c ---[ 189]---> BDD-cost:    5
c ---[ 187]---> BDD-cost:    3
c ---[ 185]---> BDD-cost:    5
c ---[ 183]---> BDD-cost:    3
c ---[ 181]---> BDD-cost:    5
c ---[ 179]---> BDD-cost:    3
c ---[ 177]---> BDD-cost:    5
c ---[ 175]---> BDD-cost:    3
c ---[ 173]---> BDD-cost:    5
c ---[ 171]---> BDD-cost:    3
c ---[ 169]---> BDD-cost:    3
c ---[ 167]---> BDD-cost:    5
c ---[ 165]---> BDD-cost:    3
c ---[ 163]---> BDD-cost:    3
c ---[ 161]---> BDD-cost:    5
c ---[ 159]---> BDD-cost:    3
c ---[ 157]---> BDD-cost:    5
c ---[ 155]---> BDD-cost:    3
c ---[ 153]---> BDD-cost:    5
c ---[ 151]---> BDD-cost:    3
c ---[ 149]---> BDD-cost:    5
c ---[ 147]---> BDD-cost:    3
c ---[ 145]---> BDD-cost:    5
c ---[ 143]---> BDD-cost:    3
c ---[ 141]---> BDD-cost:    5
c ---[ 139]---> BDD-cost:    3
c ---[ 137]---> BDD-cost:    5
c ---[ 135]---> BDD-cost:    3
c ---[ 133]---> BDD-cost:    5
c ---[ 131]---> BDD-cost:    3
c ---[ 129]---> BDD-cost:    5
c ---[ 127]---> BDD-cost:    3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   15366    52416 |    5122       0        0     nan |  0.000 % |
c |       100 |   15366    52416 |    5634     100     1484    14.8 |  8.161 % |
c |       250 |   15360    52399 |    6197     249     2148     8.6 |  8.187 % |
c |       475 |   15360    52399 |    6817     474     3249     6.9 |  8.187 % |
c |       812 |   15360    52399 |    7499     811     4637     5.7 |  8.187 % |
c |      1318 |   15354    52382 |    8249    1316     6837     5.2 |  8.212 % |
c |      2077 |   15354    52382 |    9073    2075    13992     6.7 |  8.212 % |
c |      3216 |   15354    52382 |    9981    3214    24484     7.6 |  8.212 % |
c |      4924 |   15354    52382 |   10979    4922    46561     9.5 |  8.212 % |
c ==============================================================================
c Found solution: 9314
c ---[   0]---> Sorter-cost:30425     Base: 5 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6384 |   79883   203237 |   26627    6382    77937    12.2 |  8.212 % |
c |      6484 |   79883   203237 |   29289    6482    78687    12.1 |  1.057 % |
c |      6634 |   79774   202991 |   32218    6631    79642    12.0 |  1.147 % |
c |      6859 |   74962   191937 |   35440    6753    80126    11.9 |  6.065 % |
c |      7196 |   66846   173214 |   38984    6963    80887    11.6 | 14.536 % |
c |      7703 |   66771   173045 |   42883    7469    93911    12.6 | 14.602 % |
c |      8463 |   62957   164225 |   47171    8109   100743    12.4 | 18.697 % |
c |      9602 |   60585   158744 |   51888    9196   108448    11.8 | 21.206 % |
c |     11310 |   58525   153954 |   57077   10778   126264    11.7 | 23.479 % |
c |     13872 |   57609   151828 |   62785   13275   244456    18.4 | 24.479 % |
c ==============================================================================
c Found solution: 6496
c ---[   0]---> Sorter-cost:    4     Base: 5 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     16671 |   57583   151800 |   19194   16055   319180    19.9 | 24.479 % |
c |     16771 |   57583   151800 |   21113   16155   319971    19.8 | 24.737 % |
c |     16922 |   57583   151800 |   23224   16306   324485    19.9 | 24.737 % |
c |     17147 |   57569   151772 |   25547   16530   326441    19.7 | 24.760 % |
c |     17484 |   57508   151628 |   28101   16852   328167    19.5 | 24.833 % |
c |     17991 |   57508   151628 |   30912   17359   331875    19.1 | 24.833 % |
c |     18750 |   57346   151253 |   34003   18111   345001    19.0 | 25.005 % |
c |     19889 |   57195   150909 |   37403   19248   363574    18.9 | 25.144 % |
c |     21597 |   57191   150900 |   41144   20954   382129    18.2 | 25.147 % |
c ==============================================================================
c Found solution: 5281
c ---[   0]---> Sorter-cost:    5     Base: 5 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     22888 |   57379   151365 |   19126   22245   421408    18.9 | 25.147 % |
c |     22990 |   57315   151216 |   21038   22338   421848    18.9 | 25.233 % |
c |     23140 |   57315   151216 |   23142   22488   423943    18.9 | 25.233 % |
c |     23365 |   57315   151216 |   25456   22713   426109    18.8 | 25.233 % |
c |     23702 |   57309   151200 |   28002   22627   424917    18.8 | 25.243 % |
c |     24211 |   57309   151200 |   30802   23136   434293    18.8 | 25.243 % |
c ==============================================================================
c Found solution: 4066
c ---[   0]---> Sorter-cost:    3     Base: 5 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     24644 |   57392   151404 |   19130   23569   440664    18.7 | 25.243 % |
c |     24744 |   57392   151404 |   21043   23669   442001    18.7 | 25.209 % |
c |     24894 |   57392   151404 |   23147   23819   443191    18.6 | 25.209 % |
c |     25119 |   57392   151404 |   25462   24044   445188    18.5 | 25.209 % |
c |     25456 |   57392   151404 |   28008   24381   448040    18.4 | 25.209 % |
c |     25963 |   57392   151404 |   30809   24888   452670    18.2 | 25.209 % |
c |     26722 |   57392   151404 |   33889   25647   461903    18.0 | 25.209 % |
c |     27862 |   57382   151380 |   37278   26786   497727    18.6 | 25.222 % |
c |     29570 |   57382   151380 |   41006   28494   558553    19.6 | 25.222 % |
c |     32133 |   57382   151380 |   45107   31057   640845    20.6 | 25.222 % |
c |     35978 |   57382   151380 |   49618   34902   779861    22.3 | 25.222 % |
c |     41744 |   57382   151380 |   54580   40668   931170    22.9 | 25.222 % |
c |     50394 |   57382   151380 |   60038   49318  1673623    33.9 | 25.222 % |
c |     63369 |   57382   151380 |   66041   62293  2223642    35.7 | 25.222 % |
c ==============================================================================
c Found solution: 4060
c ---[   0]---> Sorter-cost:    6     Base: 5 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     66063 |   57591   151908 |   19197   64987  2320754    35.7 | 25.222 % |
c |     66163 |   57591   151908 |   21116   16621   568798    34.2 | 25.354 % |
c |     66313 |   57591   151908 |   23228   16771   569641    34.0 | 25.354 % |
c |     66538 |   57591   151908 |   25551   16996   571278    33.6 | 25.354 % |
c |     66875 |   57591   151908 |   28106   17333   577725    33.3 | 25.354 % |
c |     67381 |   57591   151908 |   30916   17839   585593    32.8 | 25.354 % |
c |     68140 |   57591   151908 |   34008   18598   594970    32.0 | 25.354 % |
c |     69279 |   57591   151908 |   37409   19737   624497    31.6 | 25.354 % |
c |     70987 |   57591   151908 |   41150   21445   664586    31.0 | 25.354 % |
c |     73551 |   57585   151894 |   45265   24007   739924    30.8 | 25.361 % |
c |     77397 |   57585   151894 |   49792   27853   904135    32.5 | 25.361 % |
c |     83163 |   57581   151885 |   54771   33617  1060944    31.6 | 25.364 % |
c |     91812 |   57581   151885 |   60248   42266  1452861    34.4 | 25.364 % |
c |    104786 |   57581   151885 |   66273   55240  1873147    33.9 | 25.364 % |
c |    124250 |   57581   151885 |   72900   74704  3161493    42.3 | 25.364 % |
c ==============================================================================
c Found solution: 3662
c ---[   0]---> Sorter-cost:    5     Base: 5 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    133860 |   57892   152632 |   19297   21901   880710    40.2 | 25.364 % |
c |    133960 |   57892   152632 |   21226   22001   881271    40.1 | 25.539 % |
c |    134110 |   57892   152632 |   23349   22151   882042    39.8 | 25.539 % |
c |    134335 |   57892   152632 |   25684   22376   884694    39.5 | 25.539 % |
c |    134673 |   57892   152632 |   28252   22714   889418    39.2 | 25.539 % |
c |    135179 |   57892   152632 |   31078   23220   894281    38.5 | 25.539 % |
c |    135938 |   57892   152632 |   34185   23979   937228    39.1 | 25.539 % |
c |    137077 |   57892   152632 |   37604   25118   975100    38.8 | 25.539 % |
c |    138786 |   57892   152632 |   41364   26827  1027613    38.3 | 25.539 % |
c |    141349 |   57892   152632 |   45501   29390  1098481    37.4 | 25.539 % |
c |    145193 |   57892   152632 |   50051   33234  1274649    38.4 | 25.539 % |
c |    150959 |   57866   152572 |   55056   38996  1470513    37.7 | 25.574 % |
c |    159608 |   57862   152563 |   60562   47643  1747714    36.7 | 25.577 % |
c |    172582 |   57856   152549 |   66618   60615  2281298    37.6 | 25.584 % |
c ==============================================================================
c Found solution: 3079
c ---[   0]---> Sorter-cost:    6     Base: 5 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    175916 |   57912   152735 |   19304   63949  2346819    36.7 | 25.584 % |
c |    176016 |   57912   152735 |   21234   19705   490210    24.9 | 25.558 % |
c |    176166 |   57906   152721 |   23357   19853   491591    24.8 | 25.565 % |
c |    176392 |   57906   152721 |   25693   20079   494326    24.6 | 25.565 % |
c |    176729 |   57906   152721 |   28262   20416   498418    24.4 | 25.565 % |
c |    177236 |   57906   152721 |   31089   20923   508410    24.3 | 25.565 % |
c |    177995 |   57906   152721 |   34198   21682   539343    24.9 | 25.565 % |
c |    179135 |   57906   152721 |   37618   22822   584468    25.6 | 25.565 % |
c |    180843 |   57906   152721 |   41379   24530   638280    26.0 | 25.565 % |
c |    183406 |   57906   152721 |   45517   27093   692449    25.6 | 25.565 % |
c |    187253 |   57906   152721 |   50069   30940   814744    26.3 | 25.565 % |
c |    193019 |   57906   152721 |   55076   36706  1077438    29.4 | 25.565 % |
c ==============================================================================
c Found solution: 2868
c ---[   0]---> Sorter-cost:    5     Base: 5 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    200371 |   58129   153267 |   19376   44058  1296292    29.4 | 25.565 % |
c |    200472 |   58129   153267 |   21313   18468   445112    24.1 | 25.686 % |
c |    200626 |   58129   153267 |   23444   18622   448472    24.1 | 25.686 % |
c |    200855 |   58129   153267 |   25789   18851   454458    24.1 | 25.686 % |
c |    201194 |   58129   153267 |   28368   19190   461572    24.1 | 25.686 % |
c |    201700 |   58129   153267 |   31205   19696   477387    24.2 | 25.686 % |
c |    202459 |   58129   153267 |   34325   20455   493145    24.1 | 25.686 % |
c |    203599 |   58129   153267 |   37758   21595   528313    24.5 | 25.686 % |
c |    205307 |   58129   153267 |   41534   23303   573470    24.6 | 25.686 % |
c |    207870 |   58129   153267 |   45687   25866   672378    26.0 | 25.686 % |
c |    211714 |   58129   153267 |   50256   29710   831617    28.0 | 25.686 % |
c |    217481 |   58129   153267 |   55281   35477  1092125    30.8 | 25.686 % |
c |    226131 |   58129   153267 |   60810   44127  1425615    32.3 | 25.686 % |
c |    239107 |   58119   153241 |   66891   57100  1781631    31.2 | 25.692 % |
c |    258570 |   58119   153241 |   73580   76563  2735065    35.7 | 25.692 % |
c |    287762 |   58119   153241 |   80938   42153  1541978    36.6 | 25.692 % |
c |    331552 |   58119   153241 |   89032   85943  3287901    38.3 | 25.692 % |
c |    397236 |   58119   153241 |   97935   70548  3636854    51.6 | 25.692 % |
c ==============================================================================
c Found solution: 2861
c ---[   0]---> Sorter-cost:    5     Base: 5 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    415642 |   58128   153266 |   19376   88954  4336669    48.8 | 25.692 % |
c |    415742 |   58128   153266 |   21313   18890   451232    23.9 | 25.692 % |
c |    415893 |   58128   153266 |   23444   19041   452115    23.7 | 25.692 % |
c |    416118 |   58128   153266 |   25789   19266   455736    23.7 | 25.692 % |
c |    416457 |   58128   153266 |   28368   19605   460675    23.5 | 25.692 % |
c |    416963 |   58128   153266 |   31205   20111   466605    23.2 | 25.692 % |
c |    417724 |   58128   153266 |   34325   20872   480064    23.0 | 25.692 % |
c |    418863 |   58128   153266 |   37758   22011   515414    23.4 | 25.692 % |
c |    420571 |   58128   153266 |   41534   23719   554657    23.4 | 25.692 % |
c |    423133 |   58128   153266 |   45687   26281   642001    24.4 | 25.692 % |
c |    426977 |   58128   153266 |   50256   30125   761954    25.3 | 25.692 % |
c ==============================================================================
c Found solution: 2851
c ---[   0]---> Sorter-cost:    5     Base: 5 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    429829 |   58134   153280 |   19378   32977   842818    25.6 | 25.692 % |
c |    429931 |   58134   153280 |   21315   16591   334500    20.2 | 25.692 % |
c |    430081 |   58134   153280 |   23447   16741   336379    20.1 | 25.692 % |
c |    430306 |   58134   153280 |   25792   16966   339018    20.0 | 25.692 % |
c |    430643 |   58134   153280 |   28371   17303   344233    19.9 | 25.692 % |
c |    431149 |   58134   153280 |   31208   17809   352370    19.8 | 25.692 % |
c |    431908 |   58134   153280 |   34329   18568   366241    19.7 | 25.692 % |
c |    433050 |   58134   153280 |   37762   19710   407841    20.7 | 25.692 % |
c |    434759 |   58134   153280 |   41538   21419   467633    21.8 | 25.692 % |
c |    437321 |   58134   153280 |   45692   23981   538765    22.5 | 25.692 % |
c |    441165 |   58134   153280 |   50261   27825   683990    24.6 | 25.692 % |
c |    446932 |   58134   153280 |   55287   33592   881186    26.2 | 25.692 % |
c |    455584 |   58134   153280 |   60816   42244  1186549    28.1 | 25.692 % |
c |    468558 |   58134   153280 |   66898   55218  1666272    30.2 | 25.692 % |
c |    488020 |   58134   153280 |   73587   74680  2696073    36.1 | 25.692 % |
c |    517212 |   58134   153280 |   80946   41235  1451208    35.2 | 25.692 % |
c |    561002 |   58134   153280 |   89041   85025  3444853    40.5 | 25.692 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v v1 -v127 -v505 -v640 v774 -v4 v256 v508 -v5 -v131 -v257 v383 v509 -v6 -v132 v258 v510 v7 -v133 -v512 -v8 v134 v513 v388 v516 -v11 v137 -v517 -v12 v138 v518 -v14 v392 -v520 -v15 -v141 v267 -v521 v16 -v394 -v522 -v17 v143 -v523 -v18 v396 -v524 v19 -v525 v659 v20 -v146 -v526 -v21 v273 -v527 v22 -v528 v662 v23 -v149 -v529 v24 -v150 -v530 -v25 -v151 v403 v531 -v26 v152 v532 v27 -v153 -v533 -v28 v406 -v534 v29 -v407 -v535 -v30 -v156 -v536 v31 -v157 -v537 -v32 v158 v672 -v806 -v33 v159 -v285 -v539 v34 -v160 -v540 v287 -v413 -v36 v162 -v542 -v37 v163 v543 -v38 v164 v544 v39 -v545 -v679 v813 -v40 -v166 v546 -v41 v419 -v547 v42 -v168 -v548 -v43 v421 v549 v44 -v170 -v550 v551 v45 -v171 -v552 v686 -v46 v172 v553 -v47 v173 -v425 v554 -v48 -v174 v426 -v555 v49 -v175 -v556 v428 v51 -v177 -v558 -v52 v178 -v559 v431 -v694 v828 -v54 -v180 v432 v561 -v55 v433 -v562 -v56 v308 -v563 v697 -v831 -v57 v435 v564 v58 -v436 -v565 v566 -v59 v185 -v567 -v568 v60 -v569 -v703 v837 -v61 v187 v570 -v62 v314 -v440 -v571 v705 -v839 -v63 v189 v572 -v64 v316 v573 v65 -v317 -v574 -v66 v318 v575 -v67 v193 -v576 v710 -v68 -v194 v320 -v577 v711 -v845 v69 -v195 -v447 -v578 -v70 v196 v579 v71 -v580 v714 -v72 v198 v581 -v73 v582 v74 -v200 -v583 -v75 v201 v584 -v76 v202 v585 -v78 -v204 -v330 v456 -v587 -v79 v457 -v588 v722 -v589 -v81 -v207 -v333 v459 v590 v82 -v334 -v591 -v83 -v335 v461 -v592 v726 v727 -v861 v85 -v211 -v594 v728 -v862 -v86 -v212 v464 -v595 v87 -v213 -v596 v730 -v864 -v88 v214 v597 -v89 v467 -v598 v732 -v90 -v216 v468 v599 -v600 -v92 v218 v602 -v93 v219 v603 v94 -v220 -v604 v738 -v872 -v96 v222 v606 -v349 v475 v741 -v98 v224 v608 v99 -v351 -v477 -v609 v743 -v877 v226 -v744 v878 v227 -v745 v879 -v102 -v228 v354 -v480 v612 -v103 v229 -v355 -v481 v613 v104 -v614 v748 -v105 -v231 v357 -v483 v615 -v106 v616 -v107 -v233 v485 -v617 -v108 v234 v618 -v109 v235 -v619 v753 -v110 -v236 -v362 v488 -v620 -v754 v888 -v756 v890 -v113 v365 v623 v240 -v115 -v241 v493 -v625 v759 -v116 v242 v626 -v627 v761 -v895 -v117 v495 v628 v118 -v370 -v630 v764 -v898 -v119 -v631 -v765 v899 -v120 v246 -v632 v766 -v900 -v121 v373 v633 -v122 -v374 v500 -v634 v123 -v635 v903 -v124 -v376 v502 -v636 v770 -v904 -v771 v905 v126 -v638 v772 -v2 -v128 -v506 -v3 -v507 -v641 -v130 -v642 -v776 -v643 -v777 -v384 -v644 -v778 -v645 -v779 -v259 -v646 v780 -v260 -v386 -v647 -v781 -v261 -v387 -v136 -v389 -v264 -v390 -v652 -v786 -v654 v788 -v655 v789 -v142 -v656 v790 -v269 v657 -v791 -v270 v658 -v792 -v145 -v271 -v272 -v398 -v660 v794 -v147 -v399 v661 -v795 -v148 -v400 -v275 v663 -v797 -v276 -v402 -v664 v798 -v277 -v665 -v799 -v278 -v404 -v666 -v800 -v279 -v405 -v667 v801 -v154 -v280 -v668 v802 -v155 -v281 v669 -v803 -v283 -v409 v671 -v805 -v411 -v286 -v412 -v674 v808 -v675 -v809 -v289 -v415 -v677 -v811 -v290 -v416 -v678 -v812 -v165 -v291 -v417 -v292 -v680 -v814 -v294 -v420 -v682 v816 -v169 -v683 -v817 -v296 -v422 v684 -v818 -v685 -v819 -v297 -v423 -v820 -v299 -v688 -v822 -v300 v689 -v823 -v301 -v427 v690 -v824 -v50 -v176 -v302 -v557 -v691 v825 -v303 -v429 v692 -v826 -v304 -v430 v693 -v827 -v53 -v179 -v305 -v560 -v306 -v695 -v829 -v181 -v696 v830 -v182 -v434 -v183 -v309 -v698 -v832 -v184 -v310 -v700 -v834 -v311 -v437 v701 -v835 -v702 v836 -v186 -v312 -v438 -v313 -v439 -v704 -v838 -v188 -v315 -v706 -v840 -v190 -v442 -v707 -v841 -v191 -v443 -v192 -v444 -v709 -v843 -v319 -v445 -v844 -v446 -v321 -v846 -v322 -v448 -v713 -v847 -v197 -v323 -v449 -v324 -v450 -v715 -v849 -v325 -v716 -v850 -v326 -v452 v717 -v851 -v327 -v453 -v718 -v852 -v328 -v454 -v719 -v853 -v721 v855 -v205 -v331 -v856 -v206 -v724 -v858 -v208 -v460 -v337 -v463 -v338 -v729 v863 -v339 -v465 -v340 -v466 -v731 -v865 -v215 -v341 -v866 -v342 -v733 -v867 -v217 -v344 -v736 -v870 -v345 -v471 -v737 -v871 -v346 -v472 -v347 -v739 -v873 -v348 -v740 -v874 -v350 -v476 -v742 -v876 -v225 -v352 -v478 -v353 -v479 -v746 -v880 -v747 -v881 -v749 -v883 -v484 -v750 -v884 -v359 -v360 -v486 -v752 -v886 -v361 -v487 -v887 -v755 -v889 -v238 -v490 -v491 -v757 -v891 -v114 -v366 -v492 -v624 -v367 -v893 -v368 -v494 -v760 -v894 -v243 -v

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/336/stat): 336 (minisat+_script) R 335 336 21452 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1843640240 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/336/statm): 174 3 169 147 0 27 0
[pid=336] 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=337
New process pid=338
New process pid=339
execve syscall for /bin/sed executable
One traced child (pid=338) 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=339) exited with status: 0
One traced child (pid=337) exited with status: 0
New process pid=340
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc22/normalized-ws97-5.opb

[startup+10.0035 s]
Raw data (loadavg): 0.94 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 2712 0 0 0 974 10 0 0 25 0 1 0 1843640246 12128256 2650 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 2961 2650 145 145 0 2816 0
[pid=340] vsize: 11844
Current children cumulated CPU time (s) 9.85
Current children cumulated vsize (Kb) 13968

[startup+20.0042 s]
Raw data (loadavg): 0.95 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 3017 0 0 0 1969 13 0 0 25 0 1 0 1843640246 13340672 2955 4294967295 134512640 135094434 3221224448 3221223136 134554705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/340/statm): 3257 2955 145 145 0 3112 0
[pid=340] vsize: 13028
Current children cumulated CPU time (s) 19.83
Current children cumulated vsize (Kb) 15152

[startup+30.0059 s]
Raw data (loadavg): 0.95 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 3339 0 0 0 2964 14 0 0 25 0 1 0 1843640246 14364672 3213 4294967295 134512640 135094434 3221224448 3221223104 134558405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 3507 3213 145 145 0 3362 0
[pid=340] vsize: 14028
Current children cumulated CPU time (s) 29.79
Current children cumulated vsize (Kb) 16152

[startup+40.0066 s]
Raw data (loadavg): 0.96 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 3685 0 0 0 3958 18 0 0 25 0 1 0 1843640246 15880192 3559 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 3877 3559 145 145 0 3732 0
[pid=340] vsize: 15508
Current children cumulated CPU time (s) 39.77
Current children cumulated vsize (Kb) 17632

[startup+50.0074 s]
Raw data (loadavg): 0.97 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 4424 0 0 0 4946 23 0 0 25 0 1 0 1843640246 18857984 4298 4294967295 134512640 135094434 3221224448 3221223104 134557964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/340/statm): 4604 4298 145 145 0 4459 0
[pid=340] vsize: 18416
Current children cumulated CPU time (s) 49.7
Current children cumulated vsize (Kb) 20540

[startup+60.0081 s]
Raw data (loadavg): 0.97 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 5131 0 0 0 5934 28 0 0 25 0 1 0 1843640246 21708800 5005 4294967295 134512640 135094434 3221224448 3221223104 134558208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/340/statm): 5300 5005 145 145 0 5155 0
[pid=340] vsize: 21200
Current children cumulated CPU time (s) 59.63
Current children cumulated vsize (Kb) 23324

[startup+70.0088 s]
Raw data (loadavg): 0.97 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 5665 0 0 0 6926 32 0 0 25 0 1 0 1843640246 23760896 5507 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/340/statm): 5801 5507 145 145 0 5656 0
[pid=340] vsize: 23204
Current children cumulated CPU time (s) 69.59
Current children cumulated vsize (Kb) 25328

[startup+80.0105 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 5665 0 0 0 7925 32 0 0 25 0 1 0 1843640246 23760896 5507 4294967295 134512640 135094434 3221224448 3221223104 134557987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/340/statm): 5801 5507 145 145 0 5656 0
[pid=340] vsize: 23204
Current children cumulated CPU time (s) 79.58
Current children cumulated vsize (Kb) 25328

[startup+90.0112 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 5665 0 0 0 8925 33 0 0 25 0 1 0 1843640246 23760896 5507 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/340/statm): 5801 5507 145 145 0 5656 0
[pid=340] vsize: 23204
Current children cumulated CPU time (s) 89.59
Current children cumulated vsize (Kb) 25328

[startup+100.012 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 5665 0 0 0 9925 33 0 0 25 0 1 0 1843640246 23760896 5507 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/340/statm): 5801 5507 145 145 0 5656 0
[pid=340] vsize: 23204
Current children cumulated CPU time (s) 99.59
Current children cumulated vsize (Kb) 25328

[startup+110.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 5665 0 0 0 10924 34 0 0 25 0 1 0 1843640246 23760896 5507 4294967295 134512640 135094434 3221224448 3221223120 134555673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/340/statm): 5801 5507 145 145 0 5656 0
[pid=340] vsize: 23204
Current children cumulated CPU time (s) 109.59
Current children cumulated vsize (Kb) 25328

[startup+120.015 s]
Raw data (loadavg): 0.99 0.97 0.91 3/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 5665 0 0 0 11924 34 0 0 25 0 1 0 1843640246 23760896 5507 4294967295 134512640 135094434 3221224448 3221223072 134557724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 5801 5507 145 145 0 5656 0
[pid=340] vsize: 23204
Current children cumulated CPU time (s) 119.59
Current children cumulated vsize (Kb) 25328

[startup+130.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 5666 0 0 0 12924 35 0 0 25 0 1 0 1843640246 23760896 5508 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/340/statm): 5801 5508 145 145 0 5656 0
[pid=340] vsize: 23204
Current children cumulated CPU time (s) 129.6
Current children cumulated vsize (Kb) 25328

[startup+140.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 5784 0 0 0 13922 36 0 0 25 0 1 0 1843640246 24244224 5626 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/340/statm): 5919 5626 145 145 0 5774 0
[pid=340] vsize: 23676
Current children cumulated CPU time (s) 139.59
Current children cumulated vsize (Kb) 25800

[startup+150.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 6046 0 0 0 14917 38 0 0 25 0 1 0 1843640246 25563136 5888 4294967295 134512640 135094434 3221224448 3221223104 134557996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 6241 5888 145 145 0 6096 0
[pid=340] vsize: 24964
Current children cumulated CPU time (s) 149.56
Current children cumulated vsize (Kb) 27088

[startup+160.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 6341 0 0 0 15912 40 0 0 25 0 1 0 1843640246 26771456 6183 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 6536 6183 145 145 0 6391 0
[pid=340] vsize: 26144
Current children cumulated CPU time (s) 159.53
Current children cumulated vsize (Kb) 28268

[startup+170.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 6634 0 0 0 16907 42 0 0 25 0 1 0 1843640246 27996160 6476 4294967295 134512640 135094434 3221224448 3221223104 134557846 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 6835 6476 145 145 0 6690 0
[pid=340] vsize: 27340
Current children cumulated CPU time (s) 169.5
Current children cumulated vsize (Kb) 29464

[startup+180.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 6869 0 0 0 17903 44 0 0 25 0 1 0 1843640246 28971008 6711 4294967295 134512640 135094434 3221224448 3221223104 134558024 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 7073 6711 145 145 0 6928 0
[pid=340] vsize: 28292
Current children cumulated CPU time (s) 179.48
Current children cumulated vsize (Kb) 30416

[startup+190.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 6999 0 0 0 18901 45 0 0 25 0 1 0 1843640246 29491200 6841 4294967295 134512640 135094434 3221224448 3221223104 134557860 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 7200 6841 145 145 0 7055 0
[pid=340] vsize: 28800
Current children cumulated CPU time (s) 189.47
Current children cumulated vsize (Kb) 30924

[startup+200.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 7106 0 0 0 19899 46 0 0 25 0 1 0 1843640246 29913088 6948 4294967295 134512640 135094434 3221224448 3221223104 134557860 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 7303 6948 145 145 0 7158 0
[pid=340] vsize: 29212
Current children cumulated CPU time (s) 199.46
Current children cumulated vsize (Kb) 31336

[startup+210.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 7123 0 0 0 20899 46 0 0 25 0 1 0 1843640246 29958144 6965 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 7314 6965 145 145 0 7169 0
[pid=340] vsize: 29256
Current children cumulated CPU time (s) 209.46
Current children cumulated vsize (Kb) 31380

[startup+220.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 7123 0 0 0 21899 46 0 0 25 0 1 0 1843640246 29958144 6965 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 7314 6965 145 145 0 7169 0
[pid=340] vsize: 29256
Current children cumulated CPU time (s) 219.46
Current children cumulated vsize (Kb) 31380

[startup+230.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 7123 0 0 0 22899 46 0 0 25 0 1 0 1843640246 29958144 6965 4294967295 134512640 135094434 3221224448 3221223120 134556410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 7314 6965 145 145 0 7169 0
[pid=340] vsize: 29256
Current children cumulated CPU time (s) 229.46
Current children cumulated vsize (Kb) 31380

[startup+240.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 7123 0 0 0 23899 46 0 0 25 0 1 0 1843640246 29958144 6965 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 7314 6965 145 145 0 7169 0
[pid=340] vsize: 29256
Current children cumulated CPU time (s) 239.46
Current children cumulated vsize (Kb) 31380

[startup+250.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 7123 0 0 0 24900 46 0 0 25 0 1 0 1843640246 29958144 6965 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 7314 6965 145 145 0 7169 0
[pid=340] vsize: 29256
Current children cumulated CPU time (s) 249.47
Current children cumulated vsize (Kb) 31380

[startup+260.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 7123 0 0 0 25900 46 0 0 25 0 1 0 1843640246 29958144 6965 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 7314 6965 145 145 0 7169 0
[pid=340] vsize: 29256
Current children cumulated CPU time (s) 259.47
Current children cumulated vsize (Kb) 31380

[startup+270.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 7155 0 0 0 26900 46 0 0 25 0 1 0 1843640246 30208000 6997 4294967295 134512640 135094434 3221224448 3221223040 134557025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 7375 6997 145 145 0 7230 0
[pid=340] vsize: 29500
Current children cumulated CPU time (s) 269.47
Current children cumulated vsize (Kb) 31624

[startup+280.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 7155 0 0 0 27900 46 0 0 25 0 1 0 1843640246 30208000 6997 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 7375 6997 145 145 0 7230 0
[pid=340] vsize: 29500
Current children cumulated CPU time (s) 279.47
Current children cumulated vsize (Kb) 31624

[startup+290.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 7155 0 0 0 28901 46 0 0 25 0 1 0 1843640246 30208000 6997 4294967295 134512640 135094434 3221224448 3221223072 134562068 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 7375 6997 145 145 0 7230 0
[pid=340] vsize: 29500
Current children cumulated CPU time (s) 289.48
Current children cumulated vsize (Kb) 31624

[startup+300.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 7158 0 0 0 29901 46 0 0 25 0 1 0 1843640246 30208000 7000 4294967295 134512640 135094434 3221224448 3221223060 134563089 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 7375 7000 145 145 0 7230 0
[pid=340] vsize: 29500
Current children cumulated CPU time (s) 299.48
Current children cumulated vsize (Kb) 31624

[startup+310.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 7158 0 0 0 30901 46 0 0 25 0 1 0 1843640246 30208000 7000 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 7375 7000 145 145 0 7230 0
[pid=340] vsize: 29500
Current children cumulated CPU time (s) 309.48
Current children cumulated vsize (Kb) 31624

[startup+320.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 7158 0 0 0 31901 46 0 0 25 0 1 0 1843640246 30208000 7000 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 7375 7000 145 145 0 7230 0
[pid=340] vsize: 29500
Current children cumulated CPU time (s) 319.48
Current children cumulated vsize (Kb) 31624

[startup+330.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 7158 0 0 0 32901 46 0 0 25 0 1 0 1843640246 30208000 7000 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 7375 7000 145 145 0 7230 0
[pid=340] vsize: 29500
Current children cumulated CPU time (s) 329.48
Current children cumulated vsize (Kb) 31624

[startup+340.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 7158 0 0 0 33902 46 0 0 25 0 1 0 1843640246 30208000 7000 4294967295 134512640 135094434 3221224448 3221223072 134557685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 7375 7000 145 145 0 7230 0
[pid=340] vsize: 29500
Current children cumulated CPU time (s) 339.49
Current children cumulated vsize (Kb) 31624

[startup+350.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 7158 0 0 0 34902 46 0 0 25 0 1 0 1843640246 30208000 7000 4294967295 134512640 135094434 3221224448 3221223084 134557560 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 7375 7000 145 145 0 7230 0
[pid=340] vsize: 29500
Current children cumulated CPU time (s) 349.49
Current children cumulated vsize (Kb) 31624

[startup+360.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 7158 0 0 0 35902 46 0 0 25 0 1 0 1843640246 30208000 7000 4294967295 134512640 135094434 3221224448 3221223120 134555568 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 7375 7000 145 145 0 7230 0
[pid=340] vsize: 29500
Current children cumulated CPU time (s) 359.49
Current children cumulated vsize (Kb) 31624

[startup+370.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 7158 0 0 0 36902 46 0 0 25 0 1 0 1843640246 30208000 7000 4294967295 134512640 135094434 3221224448 3221223104 134558019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 7375 7000 145 145 0 7230 0
[pid=340] vsize: 29500
Current children cumulated CPU time (s) 369.49
Current children cumulated vsize (Kb) 31624

[startup+380.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 7158 0 0 0 37903 46 0 0 25 0 1 0 1843640246 30208000 7000 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 7375 7000 145 145 0 7230 0
[pid=340] vsize: 29500
Current children cumulated CPU time (s) 379.5
Current children cumulated vsize (Kb) 31624

[startup+390.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 7158 0 0 0 38903 46 0 0 25 0 1 0 1843640246 30208000 7000 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/340/statm): 7375 7000 145 145 0 7230 0
[pid=340] vsize: 29500
Current children cumulated CPU time (s) 389.5
Current children cumulated vsize (Kb) 31624

[startup+400.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 7158 0 0 0 39902 46 0 0 25 0 1 0 1843640246 30208000 7000 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 7375 7000 145 145 0 7230 0
[pid=340] vsize: 29500
Current children cumulated CPU time (s) 399.49
Current children cumulated vsize (Kb) 31624

[startup+410.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 7158 0 0 0 40903 46 0 0 25 0 1 0 1843640246 30208000 7000 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 7375 7000 145 145 0 7230 0
[pid=340] vsize: 29500
Current children cumulated CPU time (s) 409.5
Current children cumulated vsize (Kb) 31624

[startup+420.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 7158 0 0 0 41903 46 0 0 25 0 1 0 1843640246 30208000 7000 4294967295 134512640 135094434 3221224448 3221223072 134557598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 7375 7000 145 145 0 7230 0
[pid=340] vsize: 29500
Current children cumulated CPU time (s) 419.5
Current children cumulated vsize (Kb) 31624

[startup+430.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 7158 0 0 0 42903 46 0 0 25 0 1 0 1843640246 30208000 7000 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 7375 7000 145 145 0 7230 0
[pid=340] vsize: 29500
Current children cumulated CPU time (s) 429.5
Current children cumulated vsize (Kb) 31624

[startup+440.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 7159 0 0 0 43903 46 0 0 25 0 1 0 1843640246 30208000 7001 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 7375 7001 145 145 0 7230 0
[pid=340] vsize: 29500
Current children cumulated CPU time (s) 439.5
Current children cumulated vsize (Kb) 31624

[startup+450.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 7159 0 0 0 44904 46 0 0 25 0 1 0 1843640246 30208000 7001 4294967295 134512640 135094434 3221224448 3221223104 134557804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 7375 7001 145 145 0 7230 0
[pid=340] vsize: 29500
Current children cumulated CPU time (s) 449.51
Current children cumulated vsize (Kb) 31624

[startup+460.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 7174 0 0 0 45904 47 0 0 25 0 1 0 1843640246 30277632 7016 4294967295 134512640 135094434 3221224448 3221223104 134557890 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 7392 7016 145 145 0 7247 0
[pid=340] vsize: 29568
Current children cumulated CPU time (s) 459.52
Current children cumulated vsize (Kb) 31692

[startup+470.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 7190 0 0 0 46904 47 0 0 25 0 1 0 1843640246 30343168 7032 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 7408 7032 145 145 0 7263 0
[pid=340] vsize: 29632
Current children cumulated CPU time (s) 469.52
Current children cumulated vsize (Kb) 31756

[startup+480.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 7203 0 0 0 47904 47 0 0 25 0 1 0 1843640246 30441472 7045 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 7432 7045 145 145 0 7287 0
[pid=340] vsize: 29728
Current children cumulated CPU time (s) 479.52
Current children cumulated vsize (Kb) 31852

[startup+490.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 7222 0 0 0 48904 47 0 0 25 0 1 0 1843640246 30523392 7064 4294967295 134512640 135094434 3221224448 3221223072 134557737 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 7452 7064 145 145 0 7307 0
[pid=340] vsize: 29808
Current children cumulated CPU time (s) 489.52
Current children cumulated vsize (Kb) 31932

[startup+500.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 7223 0 0 0 49904 47 0 0 25 0 1 0 1843640246 30523392 7065 4294967295 134512640 135094434 3221224448 3221223104 134558218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 7452 7065 145 145 0 7307 0
[pid=340] vsize: 29808
Current children cumulated CPU time (s) 499.52
Current children cumulated vsize (Kb) 31932

[startup+510.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 7226 0 0 0 50905 47 0 0 25 0 1 0 1843640246 30539776 7068 4294967295 134512640 135094434 3221224448 3221223104 134558013 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 7456 7068 145 145 0 7311 0
[pid=340] vsize: 29824
Current children cumulated CPU time (s) 509.53
Current children cumulated vsize (Kb) 31948

[startup+520.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 7241 0 0 0 51905 47 0 0 25 0 1 0 1843640246 30605312 7083 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 7472 7083 145 145 0 7327 0
[pid=340] vsize: 29888
Current children cumulated CPU time (s) 519.53
Current children cumulated vsize (Kb) 32012

[startup+530.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 7242 0 0 0 52905 47 0 0 25 0 1 0 1843640246 30605312 7084 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 7472 7084 145 145 0 7327 0
[pid=340] vsize: 29888
Current children cumulated CPU time (s) 529.53
Current children cumulated vsize (Kb) 32012

[startup+540.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 7269 0 0 0 53905 47 0 0 25 0 1 0 1843640246 30769152 7111 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 7512 7111 145 145 0 7367 0
[pid=340] vsize: 30048
Current children cumulated CPU time (s) 539.53
Current children cumulated vsize (Kb) 32172

[startup+550.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 7288 0 0 0 54905 47 0 0 25 0 1 0 1843640246 30867456 7130 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 7536 7130 145 145 0 7391 0
[pid=340] vsize: 30144
Current children cumulated CPU time (s) 549.53
Current children cumulated vsize (Kb) 32268

[startup+560.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 7298 0 0 0 55906 47 0 0 25 0 1 0 1843640246 30916608 7140 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 7548 7140 145 145 0 7403 0
[pid=340] vsize: 30192
Current children cumulated CPU time (s) 559.54
Current children cumulated vsize (Kb) 32316

[startup+570.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 7309 0 0 0 56906 47 0 0 25 0 1 0 1843640246 30982144 7151 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 7564 7151 145 145 0 7419 0
[pid=340] vsize: 30256
Current children cumulated CPU time (s) 569.54
Current children cumulated vsize (Kb) 32380

[startup+580.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 7310 0 0 0 57906 47 0 0 25 0 1 0 1843640246 30982144 7152 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 7564 7152 145 145 0 7419 0
[pid=340] vsize: 30256
Current children cumulated CPU time (s) 579.54
Current children cumulated vsize (Kb) 32380

[startup+590.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 7394 0 0 0 58905 48 0 0 25 0 1 0 1843640246 31326208 7236 4294967295 134512640 135094434 3221224448 3221223104 134557937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 7648 7236 145 145 0 7503 0
[pid=340] vsize: 30592
Current children cumulated CPU time (s) 589.54
Current children cumulated vsize (Kb) 32716

[startup+600.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 7521 0 0 0 59903 49 0 0 25 0 1 0 1843640246 31883264 7363 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 7784 7363 145 145 0 7639 0
[pid=340] vsize: 31136
Current children cumulated CPU time (s) 599.53
Current children cumulated vsize (Kb) 33260

[startup+610.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 7614 0 0 0 60901 50 0 0 25 0 1 0 1843640246 32260096 7456 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 7876 7456 145 145 0 7731 0
[pid=340] vsize: 31504
Current children cumulated CPU time (s) 609.52
Current children cumulated vsize (Kb) 33628

[startup+620.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 7723 0 0 0 61900 50 0 0 25 0 1 0 1843640246 32731136 7565 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 7991 7565 145 145 0 7846 0
[pid=340] vsize: 31964
Current children cumulated CPU time (s) 619.51
Current children cumulated vsize (Kb) 34088

[startup+630.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 7827 0 0 0 62898 51 0 0 25 0 1 0 1843640246 33169408 7669 4294967295 134512640 135094434 3221224448 3221223104 134558162 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 8098 7669 145 145 0 7953 0
[pid=340] vsize: 32392
Current children cumulated CPU time (s) 629.5
Current children cumulated vsize (Kb) 34516

[startup+640.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 7963 0 0 0 63895 52 0 0 25 0 1 0 1843640246 33751040 7805 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 8240 7805 145 145 0 8095 0
[pid=340] vsize: 32960
Current children cumulated CPU time (s) 639.48
Current children cumulated vsize (Kb) 35084

[startup+650.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 8082 0 0 0 64894 53 0 0 25 0 1 0 1843640246 34222080 7924 4294967295 134512640 135094434 3221224448 3221223072 134557574 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 8355 7924 145 145 0 8210 0
[pid=340] vsize: 33420
Current children cumulated CPU time (s) 649.48
Current children cumulated vsize (Kb) 35544

[startup+660.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 8245 0 0 0 65891 53 0 0 25 0 1 0 1843640246 34885632 8087 4294967295 134512640 135094434 3221224448 3221223104 134558232 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 8517 8087 145 145 0 8372 0
[pid=340] vsize: 34068
Current children cumulated CPU time (s) 659.45
Current children cumulated vsize (Kb) 36192

[startup+670.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 8389 0 0 0 66888 54 0 0 25 0 1 0 1843640246 35463168 8231 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/340/statm): 8658 8231 145 145 0 8513 0
[pid=340] vsize: 34632
Current children cumulated CPU time (s) 669.43
Current children cumulated vsize (Kb) 36756

[startup+680.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 8526 0 0 0 67885 56 0 0 25 0 1 0 1843640246 36028416 8368 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 8796 8368 145 145 0 8651 0
[pid=340] vsize: 35184
Current children cumulated CPU time (s) 679.42
Current children cumulated vsize (Kb) 37308

[startup+690.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 8560 0 0 0 68884 56 0 0 25 0 1 0 1843640246 36159488 8402 4294967295 134512640 135094434 3221224448 3221223040 134557421 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 8828 8402 145 145 0 8683 0
[pid=340] vsize: 35312
Current children cumulated CPU time (s) 689.41
Current children cumulated vsize (Kb) 37436

[startup+700.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 8560 0 0 0 69885 56 0 0 25 0 1 0 1843640246 36159488 8402 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 8828 8402 145 145 0 8683 0
[pid=340] vsize: 35312
Current children cumulated CPU time (s) 699.42
Current children cumulated vsize (Kb) 37436

[startup+710.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 8561 0 0 0 70885 56 0 0 25 0 1 0 1843640246 36159488 8403 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 8828 8403 145 145 0 8683 0
[pid=340] vsize: 35312
Current children cumulated CPU time (s) 709.42
Current children cumulated vsize (Kb) 37436

[startup+720.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 8563 0 0 0 71885 56 0 0 25 0 1 0 1843640246 36159488 8405 4294967295 134512640 135094434 3221224448 3221223104 134557860 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 8828 8405 145 145 0 8683 0
[pid=340] vsize: 35312
Current children cumulated CPU time (s) 719.42
Current children cumulated vsize (Kb) 37436

[startup+730.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 8574 0 0 0 72885 56 0 0 25 0 1 0 1843640246 36225024 8416 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 8844 8416 145 145 0 8699 0
[pid=340] vsize: 35376
Current children cumulated CPU time (s) 729.42
Current children cumulated vsize (Kb) 37500

[startup+740.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 8575 0 0 0 73886 56 0 0 25 0 1 0 1843640246 36225024 8417 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 8844 8417 145 145 0 8699 0
[pid=340] vsize: 35376
Current children cumulated CPU time (s) 739.43
Current children cumulated vsize (Kb) 37500

[startup+750.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 8576 0 0 0 74886 56 0 0 25 0 1 0 1843640246 36225024 8418 4294967295 134512640 135094434 3221224448 3221223104 134557860 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 8844 8418 145 145 0 8699 0
[pid=340] vsize: 35376
Current children cumulated CPU time (s) 749.43
Current children cumulated vsize (Kb) 37500

[startup+760.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 8579 0 0 0 75886 56 0 0 25 0 1 0 1843640246 36225024 8421 4294967295 134512640 135094434 3221224448 3221223040 134556851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 8844 8421 145 145 0 8699 0
[pid=340] vsize: 35376
Current children cumulated CPU time (s) 759.43
Current children cumulated vsize (Kb) 37500

[startup+770.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 8588 0 0 0 76886 56 0 0 25 0 1 0 1843640246 36290560 8430 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 8860 8430 145 145 0 8715 0
[pid=340] vsize: 35440
Current children cumulated CPU time (s) 769.43
Current children cumulated vsize (Kb) 37564

[startup+780.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 8599 0 0 0 77887 56 0 0 25 0 1 0 1843640246 36356096 8441 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 8876 8441 145 145 0 8731 0
[pid=340] vsize: 35504
Current children cumulated CPU time (s) 779.44
Current children cumulated vsize (Kb) 37628

[startup+790.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 8599 0 0 0 78887 56 0 0 25 0 1 0 1843640246 36356096 8441 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 8876 8441 145 145 0 8731 0
[pid=340] vsize: 35504
Current children cumulated CPU time (s) 789.44
Current children cumulated vsize (Kb) 37628

[startup+800.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 8599 0 0 0 79887 56 0 0 25 0 1 0 1843640246 36356096 8441 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 8876 8441 145 145 0 8731 0
[pid=340] vsize: 35504
Current children cumulated CPU time (s) 799.44
Current children cumulated vsize (Kb) 37628

[startup+810.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 8629 0 0 0 80887 57 0 0 25 0 1 0 1843640246 36487168 8471 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 8908 8471 145 145 0 8763 0
[pid=340] vsize: 35632
Current children cumulated CPU time (s) 809.45
Current children cumulated vsize (Kb) 37756

[startup+820.075 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 8632 0 0 0 81887 57 0 0 25 0 1 0 1843640246 36618240 8474 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 8940 8474 145 145 0 8795 0
[pid=340] vsize: 35760
Current children cumulated CPU time (s) 819.45
Current children cumulated vsize (Kb) 37884

[startup+830.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 8643 0 0 0 82887 57 0 0 25 0 1 0 1843640246 36618240 8485 4294967295 134512640 135094434 3221224448 3221223072 134557612 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/340/statm): 8940 8485 145 145 0 8795 0
[pid=340] vsize: 35760
Current children cumulated CPU time (s) 829.45
Current children cumulated vsize (Kb) 37884

[startup+840.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 8644 0 0 0 83887 57 0 0 25 0 1 0 1843640246 36618240 8486 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 8940 8486 145 145 0 8795 0
[pid=340] vsize: 35760
Current children cumulated CPU time (s) 839.45
Current children cumulated vsize (Kb) 37884

[startup+850.078 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 8644 0 0 0 84887 57 0 0 25 0 1 0 1843640246 36618240 8486 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 8940 8486 145 145 0 8795 0
[pid=340] vsize: 35760
Current children cumulated CPU time (s) 849.45
Current children cumulated vsize (Kb) 37884

[startup+860.079 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 8737 0 0 0 85886 57 0 0 25 0 1 0 1843640246 37048320 8579 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 9045 8579 145 145 0 8900 0
[pid=340] vsize: 36180
Current children cumulated CPU time (s) 859.44
Current children cumulated vsize (Kb) 38304

[startup+870.079 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 8898 0 0 0 86883 58 0 0 25 0 1 0 1843640246 37711872 8740 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 9207 8740 145 145 0 9062 0
[pid=340] vsize: 36828
Current children cumulated CPU time (s) 869.42
Current children cumulated vsize (Kb) 38952

[startup+880.081 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 9111 0 0 0 87881 59 0 0 25 0 1 0 1843640246 38453248 8921 4294967295 134512640 135094434 3221224448 3221223120 134555579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 9388 8921 145 145 0 9243 0
[pid=340] vsize: 37552
Current children cumulated CPU time (s) 879.41
Current children cumulated vsize (Kb) 39676

[startup+890.082 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 9111 0 0 0 88881 59 0 0 25 0 1 0 1843640246 38453248 8921 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 9388 8921 145 145 0 9243 0
[pid=340] vsize: 37552
Current children cumulated CPU time (s) 889.41
Current children cumulated vsize (Kb) 39676

[startup+900.081 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 9111 0 0 0 89881 59 0 0 25 0 1 0 1843640246 38453248 8921 4294967295 134512640 135094434 3221224448 3221223104 134557849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 9388 8921 145 145 0 9243 0
[pid=340] vsize: 37552
Current children cumulated CPU time (s) 899.41
Current children cumulated vsize (Kb) 39676

[startup+910.083 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 9111 0 0 0 90882 59 0 0 25 0 1 0 1843640246 38453248 8921 4294967295 134512640 135094434 3221224448 3221223040 134556851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 9388 8921 145 145 0 9243 0
[pid=340] vsize: 37552
Current children cumulated CPU time (s) 909.42
Current children cumulated vsize (Kb) 39676

[startup+920.084 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 9111 0 0 0 91882 59 0 0 25 0 1 0 1843640246 38453248 8921 4294967295 134512640 135094434 3221224448 3221223104 134558002 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 9388 8921 145 145 0 9243 0
[pid=340] vsize: 37552
Current children cumulated CPU time (s) 919.42
Current children cumulated vsize (Kb) 39676

[startup+930.085 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 9111 0 0 0 92882 59 0 0 25 0 1 0 1843640246 38453248 8921 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 9388 8921 145 145 0 9243 0
[pid=340] vsize: 37552
Current children cumulated CPU time (s) 929.42
Current children cumulated vsize (Kb) 39676

[startup+940.086 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 9111 0 0 0 93882 59 0 0 25 0 1 0 1843640246 38453248 8921 4294967295 134512640 135094434 3221224448 3221222928 134780630 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 9388 8921 145 145 0 9243 0
[pid=340] vsize: 37552
Current children cumulated CPU time (s) 939.42
Current children cumulated vsize (Kb) 39676

[startup+950.087 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 9111 0 0 0 94882 59 0 0 25 0 1 0 1843640246 38453248 8921 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 9388 8921 145 145 0 9243 0
[pid=340] vsize: 37552
Current children cumulated CPU time (s) 949.42
Current children cumulated vsize (Kb) 39676

[startup+960.088 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 9111 0 0 0 95883 59 0 0 25 0 1 0 1843640246 38453248 8921 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 9388 8921 145 145 0 9243 0
[pid=340] vsize: 37552
Current children cumulated CPU time (s) 959.43
Current children cumulated vsize (Kb) 39676

[startup+970.089 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 9111 0 0 0 96883 59 0 0 25 0 1 0 1843640246 38453248 8921 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 9388 8921 145 145 0 9243 0
[pid=340] vsize: 37552
Current children cumulated CPU time (s) 969.43
Current children cumulated vsize (Kb) 39676

[startup+980.091 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 9111 0 0 0 97883 59 0 0 25 0 1 0 1843640246 38453248 8921 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 9388 8921 145 145 0 9243 0
[pid=340] vsize: 37552
Current children cumulated CPU time (s) 979.43
Current children cumulated vsize (Kb) 39676

[startup+990.092 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 9111 0 0 0 98884 59 0 0 25 0 1 0 1843640246 38453248 8921 4294967295 134512640 135094434 3221224448 3221223104 134557872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 9388 8921 145 145 0 9243 0
[pid=340] vsize: 37552
Current children cumulated CPU time (s) 989.44
Current children cumulated vsize (Kb) 39676

[startup+1000.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 9111 0 0 0 99884 59 0 0 25 0 1 0 1843640246 38453248 8921 4294967295 134512640 135094434 3221224448 3221223072 134557565 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 9388 8921 145 145 0 9243 0
[pid=340] vsize: 37552
Current children cumulated CPU time (s) 999.44
Current children cumulated vsize (Kb) 39676

[startup+1010.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 9111 0 0 0 100884 59 0 0 25 0 1 0 1843640246 38453248 8921 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 9388 8921 145 145 0 9243 0
[pid=340] vsize: 37552
Current children cumulated CPU time (s) 1009.44
Current children cumulated vsize (Kb) 39676

[startup+1020.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 9111 0 0 0 101884 59 0 0 25 0 1 0 1843640246 38453248 8921 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 9388 8921 145 145 0 9243 0
[pid=340] vsize: 37552
Current children cumulated CPU time (s) 1019.44
Current children cumulated vsize (Kb) 39676

[startup+1030.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 9111 0 0 0 102885 59 0 0 25 0 1 0 1843640246 38453248 8921 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 9388 8921 145 145 0 9243 0
[pid=340] vsize: 37552
Current children cumulated CPU time (s) 1029.45
Current children cumulated vsize (Kb) 39676

[startup+1040.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 9111 0 0 0 103885 59 0 0 25 0 1 0 1843640246 38453248 8921 4294967295 134512640 135094434 3221224448 3221223104 134558022 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 9388 8921 145 145 0 9243 0
[pid=340] vsize: 37552
Current children cumulated CPU time (s) 1039.45
Current children cumulated vsize (Kb) 39676

[startup+1050.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 9111 0 0 0 104885 59 0 0 25 0 1 0 1843640246 38453248 8921 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 9388 8921 145 145 0 9243 0
[pid=340] vsize: 37552
Current children cumulated CPU time (s) 1049.45
Current children cumulated vsize (Kb) 39676

[startup+1060.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 9111 0 0 0 105885 59 0 0 25 0 1 0 1843640246 38453248 8921 4294967295 134512640 135094434 3221224448 3221223116 134555968 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 9388 8921 145 145 0 9243 0
[pid=340] vsize: 37552
Current children cumulated CPU time (s) 1059.45
Current children cumulated vsize (Kb) 39676

[startup+1070.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 9111 0 0 0 106886 59 0 0 25 0 1 0 1843640246 38453248 8921 4294967295 134512640 135094434 3221224448 3221223120 134556543 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 9388 8921 145 145 0 9243 0
[pid=340] vsize: 37552
Current children cumulated CPU time (s) 1069.46
Current children cumulated vsize (Kb) 39676

[startup+1080.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 9111 0 0 0 107886 59 0 0 25 0 1 0 1843640246 38453248 8921 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 9388 8921 145 145 0 9243 0
[pid=340] vsize: 37552
Current children cumulated CPU time (s) 1079.46
Current children cumulated vsize (Kb) 39676

[startup+1090.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 9111 0 0 0 108886 59 0 0 25 0 1 0 1843640246 38453248 8921 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 9388 8921 145 145 0 9243 0
[pid=340] vsize: 37552
Current children cumulated CPU time (s) 1089.46
Current children cumulated vsize (Kb) 39676

[startup+1100.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 9111 0 0 0 109886 59 0 0 25 0 1 0 1843640246 38453248 8921 4294967295 134512640 135094434 3221224448 3221223040 134557230 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 9388 8921 145 145 0 9243 0
[pid=340] vsize: 37552
Current children cumulated CPU time (s) 1099.46
Current children cumulated vsize (Kb) 39676

[startup+1110.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 9111 0 0 0 110887 59 0 0 25 0 1 0 1843640246 38453248 8921 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 9388 8921 145 145 0 9243 0
[pid=340] vsize: 37552
Current children cumulated CPU time (s) 1109.47
Current children cumulated vsize (Kb) 39676

[startup+1120.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 9114 0 0 0 111887 59 0 0 25 0 1 0 1843640246 38453248 8924 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 9388 8924 145 145 0 9243 0
[pid=340] vsize: 37552
Current children cumulated CPU time (s) 1119.47
Current children cumulated vsize (Kb) 39676

[startup+1130.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 9115 0 0 0 112887 59 0 0 25 0 1 0 1843640246 38453248 8925 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 9388 8925 145 145 0 9243 0
[pid=340] vsize: 37552
Current children cumulated CPU time (s) 1129.47
Current children cumulated vsize (Kb) 39676

[startup+1140.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 9115 0 0 0 113887 59 0 0 25 0 1 0 1843640246 38453248 8925 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 9388 8925 145 145 0 9243 0
[pid=340] vsize: 37552
Current children cumulated CPU time (s) 1139.47
Current children cumulated vsize (Kb) 39676

[startup+1150.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 9115 0 0 0 114888 59 0 0 25 0 1 0 1843640246 38453248 8925 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 9388 8925 145 145 0 9243 0
[pid=340] vsize: 37552
Current children cumulated CPU time (s) 1149.48
Current children cumulated vsize (Kb) 39676

[startup+1160.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 9117 0 0 0 115888 59 0 0 25 0 1 0 1843640246 38453248 8927 4294967295 134512640 135094434 3221224448 3221223120 134556317 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 9388 8927 145 145 0 9243 0
[pid=340] vsize: 37552
Current children cumulated CPU time (s) 1159.48
Current children cumulated vsize (Kb) 39676

[startup+1170.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 9118 0 0 0 116888 59 0 0 25 0 1 0 1843640246 38453248 8928 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 9388 8928 145 145 0 9243 0
[pid=340] vsize: 37552
Current children cumulated CPU time (s) 1169.48
Current children cumulated vsize (Kb) 39676

[startup+1180.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 9118 0 0 0 117888 59 0 0 25 0 1 0 1843640246 38453248 8928 4294967295 134512640 135094434 3221224448 3221223120 134555566 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 9388 8928 145 145 0 9243 0
[pid=340] vsize: 37552
Current children cumulated CPU time (s) 1179.48
Current children cumulated vsize (Kb) 39676

[startup+1190.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 9118 0 0 0 118889 59 0 0 25 0 1 0 1843640246 38453248 8928 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 9388 8928 145 145 0 9243 0
[pid=340] vsize: 37552
Current children cumulated CPU time (s) 1189.49
Current children cumulated vsize (Kb) 39676

[startup+1200.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 9118 0 0 0 119889 59 0 0 25 0 1 0 1843640246 38453248 8928 4294967295 134512640 135094434 3221224448 3221223104 134557900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 9388 8928 145 145 0 9243 0
[pid=340] vsize: 37552
Current children cumulated CPU time (s) 1199.49
Current children cumulated vsize (Kb) 39676

[startup+1210.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 9118 0 0 0 120889 59 0 0 25 0 1 0 1843640246 38453248 8928 4294967295 134512640 135094434 3221224448 3221223104 134557884 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 9388 8928 145 145 0 9243 0
[pid=340] vsize: 37552
Current children cumulated CPU time (s) 1209.49
Current children cumulated vsize (Kb) 39676



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 340
Raw data (/proc/336/stat): 336 (minisat+_script) S 335 336 21452 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843640240 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/336/statm): 531 226 485 147 0 384 0
[pid=336] vsize: 2124
Raw data (/proc/340/stat): 340 (minisat+_64-bit) R 336 336 21452 0 -1 0 9118 0 0 0 120889 59 0 0 25 0 1 0 1843640246 38453248 8928 4294967295 134512640 135094434 3221224448 3221223104 134557884 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/340/statm): 9388 8928 145 145 0 9243 0
[pid=340] vsize: 37552
Current children cumulated CPU time (s) 1209.49
Current children cumulated vsize (Kb) 39676

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

Child status: 10
Real time (s): 1210.13
CPU time (s): 1209.51
CPU user time (s): 1208.9
CPU system time (s): 0.615906
CPU usage (%): 99.9489
Max. virtual memory (cumulated for all children) (Kb): 39676

Verifier Data

ERROR: no interpretation found !