Some explanations

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

General information on the benchmark

Namemps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-vpm2.opb
MD5SUMfae1fae180d772ad3ee6c1acfa1c8b4f
Bench Categoryoptimization, medium integers (OPTMEDINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 130
Optimality of the best value was proved NO
Number of terms in the objective function 168
Biggest coefficient in the objective function 5
Number of bits for the biggest coefficient in the objective function 3
Sum of the numbers in the objective function 504
Number of bits of the sum of numbers in the objective function 9
Biggest number in a constraint 2000000
Number of bits of the biggest number in a constraint 21
Biggest sum of numbers in a constraint 30041153
Number of bits of the biggest sum of numbers25
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1189.02
Number of variables2124
Total number of constraints444
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints444
Minimum length of a constraint8
Maximum length of a constraint64

Trace number 6233

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.215
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        914672 kB
Buffers:         11964 kB
Cached:          79000 kB
SwapCached:        904 kB
Active:          21068 kB
Inactive:        72592 kB
HighTotal:      131008 kB
HighFree:        47824 kB
LowTotal:       903652 kB
LowFree:        866848 kB
SwapTotal:     2097892 kB
SwapFree:      2096536 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5732 kB
Slab:            20696 kB
Committed_AS:    64132 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-20 05:01:27 (client local time) WITH STATUS 0 IN 1208.65 SECONDS
stats: 3397 7 1208.65 0

Solver Data

c Parsing PB file...
c Converting 486 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: ##############################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 485]---> BDD-cost:    7
c ---[ 484]---> BDD-cost:    7
c ---[ 483]---> BDD-cost:    7
c ---[ 482]---> BDD-cost:    7
c ---[ 481]---> BDD-cost:    7
c ---[ 480]---> BDD-cost:    7
c ---[ 479]---> BDD-cost:    7
c ---[ 478]---> BDD-cost:    7
c ---[ 477]---> BDD-cost:    7
c ---[ 474]---> BDD-cost:    7
c ---[ 473]---> BDD-cost:    7
c ---[ 472]---> BDD-cost:    7
c ---[ 471]---> BDD-cost:    7
c ---[ 468]---> BDD-cost:    7
c ---[ 467]---> BDD-cost:    7
c ---[ 466]---> BDD-cost:    7
c ---[ 465]---> BDD-cost:    7
c ---[ 462]---> BDD-cost:    7
c ---[ 459]---> BDD-cost:    7
c ---[ 458]---> BDD-cost:    7
c ---[ 457]---> BDD-cost:    7
c ---[ 454]---> BDD-cost:    7
c ---[ 453]---> BDD-cost:    7
c ---[ 452]---> BDD-cost:    7
c ---[ 451]---> BDD-cost:    7
c ---[ 450]---> BDD-cost:    7
c ---[ 448]---> BDD-cost:    7
c ---[ 447]---> BDD-cost:    7
c ---[ 446]---> BDD-cost:    7
c ---[ 445]---> BDD-cost:    7
c ---[ 444]---> BDD-cost:    7
c ---[ 441]---> BDD-cost:    7
c ---[ 440]---> BDD-cost:    7
c ---[ 439]---> BDD-cost:    7
c ---[ 433]---> BDD-cost:    7
c ---[ 427]---> BDD-cost:    7
c ---[ 422]---> BDD-cost:    7
c ---[ 421]---> BDD-cost:    7
c ---[ 415]---> BDD-cost:    7
c ---[ 409]---> BDD-cost:    7
c ---[ 408]---> BDD-cost:    7
c ---[ 402]---> BDD-cost:    7
c ---[ 397]---> BDD-cost:    7
c ---[ 396]---> BDD-cost:    7
c ---[ 391]---> BDD-cost:    7
c ---[ 390]---> BDD-cost:    7
c ---[ 386]---> BDD-cost:    7
c ---[ 385]---> BDD-cost:    7
c ---[ 384]---> BDD-cost:    7
c ---[ 380]---> BDD-cost:    7
c ---[ 379]---> BDD-cost:    7
c ---[ 378]---> BDD-cost:    7
c ---[ 374]---> BDD-cost:    7
c ---[ 373]---> BDD-cost:    7
c ---[ 372]---> BDD-cost:    7
c ---[ 368]---> BDD-cost:    7
c ---[ 367]---> BDD-cost:    7
c ---[ 366]---> BDD-cost:    7
c ---[ 365]---> BDD-cost:    7
c ---[ 364]---> BDD-cost:    7
c ---[ 359]---> BDD-cost:    7
c ---[ 353]---> BDD-cost:    7
c ---[ 347]---> BDD-cost:    7
c ---[ 339]---> BDD-cost:    7
c ---[ 333]---> BDD-cost:    7
c ---[ 327]---> BDD-cost:    7
c ---[ 321]---> BDD-cost:    7
c ---[ 317]---> BDD-cost:   14
c ---[ 316]---> BDD-cost:   14
c ---[ 315]---> BDD-cost:   14
c ---[ 314]---> BDD-cost:   14
c ---[ 313]---> BDD-cost:   14
c ---[ 312]---> BDD-cost:   14
c ---[ 310]---> BDD-cost:   14
c ---[ 309]---> BDD-cost:   14
c ---[ 308]---> BDD-cost:   14
c ---[ 307]---> BDD-cost:   14
c ---[ 306]---> BDD-cost:   14
c ---[ 302]---> BDD-cost:   13
c ---[ 301]---> BDD-cost:   13
c ---[ 300]---> BDD-cost:   13
c ---[ 295]---> BDD-cost:   13
c ---[ 294]---> BDD-cost:   13
c ---[ 290]---> BDD-cost:   15
c ---[ 289]---> BDD-cost:   15
c ---[ 288]---> BDD-cost:   15
c ---[ 287]---> BDD-cost:   13
c ---[ 286]---> BDD-cost:   13
c ---[ 285]---> BDD-cost:   13
c ---[ 284]---> BDD-cost:   13
c ---[ 283]---> BDD-cost:   13
c ---[ 282]---> BDD-cost:   13
c ---[ 280]---> BDD-cost:   13
c ---[ 279]---> BDD-cost:   13
c ---[ 278]---> BDD-cost:   13
c ---[ 277]---> BDD-cost:   13
c ---[ 276]---> BDD-cost:   13
c ---[ 274]---> Sorter-cost: 1988     Base: 2 2 2 5 5 2 2 2 2 2 3
c ---[ 264]---> Sorter-cost: 1824     Base: 2 2 2 5 5 2 2 2 3 2 2 2
c ---[ 260]---> Adder-cost: 262   maxlim: 300367   bits: 19/19
c ---[ 258]---> Adder-cost: 262   maxlim: 300367   bits: 19/19
c ---[ 256]---> Sorter-cost: 2565     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 254]---> Sorter-cost: 2565     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 252]---> Adder-cost: 262   maxlim: 261967   bits: 19/18
c ---[ 250]---> Sorter-cost: 1411     Base: 2 2 2 2 5 5 2 2 2 2 2
c ---[ 248]---> Sorter-cost: 2230     Base: 2 2 2 2 2 2 2 2 2 2 2 3 2
c ---[ 246]---> Sorter-cost: 2232     Base: 2 2 2 2 2 2 2 2 2 2 2 3 2
c ---[ 244]---> Sorter-cost: 2232     Base: 2 2 2 2 2 2 2 2 2 2 2 3 2
c ---[ 242]---> Sorter-cost: 2159     Base: 2 2 2 2 2 2 2 2 2 2 3 2 2
c ---[ 236]---> Sorter-cost: 1318     Base: 2 2 2 2 5 5 2 2 2 2 2
c ---[ 234]---> Sorter-cost: 2540     Base: 2 2 2 2 5 5 2 2 2 2 2 2
c ---[ 232]---> Sorter-cost: 1903     Base: 2 2 2 2 2 2 2 2 2 2 2 3
c ---[ 224]---> Sorter-cost: 1580     Base: 2 2 2 5 5 2 2 2 2 2 3
c ---[ 222]---> Adder-cost: 260   maxlim: 219983   bits: 19/18
c ---[ 216]---> Sorter-cost: 1742     Base: 2 2 2 5 5 2 2 2 2 2 2
c ---[ 214]---> Sorter-cost: 2471     Base: 2 2 2 2 2 2 2 2 2 2 2 3 2
c ---[ 212]---> Sorter-cost: 2473     Base: 2 2 2 2 2 2 2 2 2 2 2 3 2
c ---[ 210]---> Sorter-cost: 3095     Base: 2 2 2 2 2 3 5 2 2 2 5
c ---[ 208]---> Adder-cost: 222   maxlim: 103983   bits: 17/17
c ---[ 206]---> Adder-cost: 222   maxlim: 103983   bits: 17/17
c ---[ 204]---> Adder-cost: 222   maxlim: 103983   bits: 17/17
c ---[ 202]---> Adder-cost: 222   maxlim: 103983   bits: 17/17
c ---[ 200]---> Sorter-cost: 1882     Base: 2 2 2 2 5 5 2 2 2 5
c ---[ 198]---> Sorter-cost: 3211     Base: 2 2 2 2 5 5 2 2 2 2 5
c ---[ 196]---> Adder-cost: 254   maxlim: 123183   bits: 18/17
c ---[ 194]---> Adder-cost: 254   maxlim: 123183   bits: 18/17
c ---[ 192]---> Adder-cost: 254   maxlim: 123183   bits: 18/17
c ---[ 191]---> BDD-cost:  110
c ---[ 190]---> BDD-cost:  237
c ---[ 189]---> BDD-cost:  236
c ---[ 188]---> BDD-cost:  393
c ---[ 187]---> BDD-cost:  495
c ---[ 186]---> BDD-cost:  488
c ---[ 185]---> BDD-cost:  131
c ---[ 184]---> BDD-cost:  262
c ---[ 183]---> BDD-cost:  261
c ---[ 182]---> BDD-cost:  448
c ---[ 181]---> BDD-cost:  550
c ---[ 180]---> BDD-cost:  549
c ---[ 179]---> Sorter-cost:  335     Base: 2 2 2 2 2 2 5
c ---[ 178]---> Sorter-cost:  867     Base: 2 2 5 2 2 2 2
c ---[ 177]---> Sorter-cost:  830     Base: 2 2 2 2 2 2 5
c ---[ 176]---> Sorter-cost: 1298     Base: 2 2 5 2 2 2 2
c ---[ 175]---> Sorter-cost: 1687     Base: 2 2 5 2 2 2 2
c ---[ 174]---> Sorter-cost: 1665     Base: 2 2 5 2 2 2 2
c ---[ 173]---> Sorter-cost:  196     Base: 2 2 2 2 2 2
c ---[ 172]---> Sorter-cost:  473     Base: 2 2 2 2 2
c ---[ 171]---> Sorter-cost:  421     Base: 2 2 2 2 2 2
c ---[ 170]---> Sorter-cost:  764     Base: 2 2 2 2 2
c ---[ 169]---> Sorter-cost:  884     Base: 2 2 2 2 2 2
c ---[ 168]---> Sorter-cost: 1063     Base: 2 2 2 2 2
c ---[ 167]---> BDD-cost:    3
c ---[ 166]---> BDD-cost:    3
c ---[ 165]---> BDD-cost:    3
c ---[ 164]---> BDD-cost:    3
c ---[ 163]---> BDD-cost:    3
c ---[ 162]---> BDD-cost:    3
c ---[ 161]---> BDD-cost:    3
c ---[ 160]---> BDD-cost:    3
c ---[ 159]---> BDD-cost:    3
c ---[ 158]---> BDD-cost:    7
c ---[ 157]---> BDD-cost:    7
c ---[ 156]---> BDD-cost:    3
c ---[ 155]---> BDD-cost:    3
c ---[ 154]---> BDD-cost:    3
c ---[ 153]---> BDD-cost:    3
c ---[ 152]---> BDD-cost:    7
c ---[ 151]---> BDD-cost:    7
c ---[ 150]---> BDD-cost:    3
c ---[ 149]---> BDD-cost:    3
c ---[ 148]---> BDD-cost:    3
c ---[ 147]---> BDD-cost:    3
c ---[ 146]---> BDD-cost:    7
c ---[ 145]---> BDD-cost:    7
c ---[ 144]---> BDD-cost:    3
c ---[ 142]---> BDD-cost:    7
c ---[ 141]---> BDD-cost:    3
c ---[ 140]---> BDD-cost:    3
c ---[ 139]---> BDD-cost:    3
c ---[ 138]---> BDD-cost:    7
c ---[ 136]---> BDD-cost:    3
c ---[ 135]---> BDD-cost:    3
c ---[ 134]---> BDD-cost:    3
c ---[ 133]---> BDD-cost:    3
c ---[ 132]---> BDD-cost:    3
c ---[ 130]---> BDD-cost:    3
c ---[ 129]---> BDD-cost:    3
c ---[ 128]---> BDD-cost:    3
c ---[ 127]---> BDD-cost:    3
c ---[ 126]---> BDD-cost:    3
c ---[ 124]---> BDD-cost:    7
c ---[ 123]---> BDD-cost:    3
c ---[ 122]---> BDD-cost:    3
c ---[ 121]---> BDD-cost:    3
c ---[ 120]---> BDD-cost:    7
c ---[ 116]---> BDD-cost:    7
c ---[ 115]---> BDD-cost:    3
c ---[ 114]---> BDD-cost:    6
c ---[ 110]---> BDD-cost:    7
c ---[ 109]---> BDD-cost:    3
c ---[ 108]---> BDD-cost:    6
c ---[ 104]---> BDD-cost:    3
c ---[ 103]---> BDD-cost:    3
c ---[ 102]---> BDD-cost:    5
c ---[  98]---> BDD-cost:    7
c ---[  97]---> BDD-cost:    3
c ---[  96]---> BDD-cost:    6
c ---[  91]---> BDD-cost:    3
c ---[  90]---> BDD-cost:    3
c ---[  85]---> BDD-cost:    7
c ---[  84]---> BDD-cost:    3
c ---[  79]---> BDD-cost:    3
c ---[  78]---> BDD-cost:    3
c ---[  73]---> BDD-cost:    3
c ---[  72]---> BDD-cost:    3
c ---[  68]---> BDD-cost:    3
c ---[  67]---> BDD-cost:    3
c ---[  66]---> BDD-cost:    3
c ---[  62]---> BDD-cost:    3
c ---[  61]---> BDD-cost:    3
c ---[  60]---> BDD-cost:    3
c ---[  56]---> BDD-cost:    3
c ---[  55]---> BDD-cost:    3
c ---[  54]---> BDD-cost:    3
c ---[  50]---> BDD-cost:    3
c ---[  49]---> BDD-cost:    3
c ---[  48]---> BDD-cost:    3
c ---[  47]---> BDD-cost:    3
c ---[  46]---> BDD-cost:    3
c ---[  45]---> BDD-cost:    6
c ---[  44]---> BDD-cost:    6
c ---[  43]---> BDD-cost:    6
c ---[  42]---> BDD-cost:    6
c ---[  41]---> BDD-cost:    3
c ---[  40]---> BDD-cost:    7
c ---[  39]---> BDD-cost:    6
c ---[  38]---> BDD-cost:    6
c ---[  37]---> BDD-cost:    6
c ---[  36]---> BDD-cost:    6
c ---[  35]---> BDD-cost:    3
c ---[  34]---> BDD-cost:    7
c ---[  33]---> BDD-cost:    5
c ---[  32]---> BDD-cost:    5
c ---[  31]---> BDD-cost:    5
c ---[  30]---> BDD-cost:    5
c ---[  29]---> BDD-cost:    3
c ---[  28]---> BDD-cost:    7
c ---[  27]---> BDD-cost:    5
c ---[  26]---> BDD-cost:    5
c ---[  25]---> BDD-cost:    5
c ---[  24]---> BDD-cost:    5
c ---[  22]---> BDD-cost:    7
c ---[  21]---> BDD-cost:    3
c ---[  20]---> BDD-cost:    6
c ---[  19]---> BDD-cost:    6
c ---[  18]---> BDD-cost:    6
c ---[  16]---> BDD-cost:    7
c ---[  15]---> BDD-cost:    3
c ---[  14]---> BDD-cost:    6
c ---[  13]---> BDD-cost:    6
c ---[  12]---> BDD-cost:    6
c ---[  10]---> BDD-cost:    7
c ---[   9]---> BDD-cost:    3
c ---[   8]---> BDD-cost:    6
c ---[   7]---> BDD-cost:    6
c ---[   6]---> BDD-cost:    6
c ---[   4]---> BDD-cost:    6
c ---[   3]---> BDD-cost:    3
c ---[   2]---> BDD-cost:    5
c ---[   1]---> BDD-cost:    5
c ---[   0]---> BDD-cost:    5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  157483   397264 |   52494       0        0     nan |  0.000 % |
c |       100 |  157402   397079 |   57743      93      599     6.4 |  5.605 % |
c |       250 |  157402   397079 |   63517     243     1788     7.4 |  5.605 % |
c |       475 |  157263   396762 |   69869     457     3288     7.2 |  5.672 % |
c |       813 |  157208   396638 |   76856     794     6792     8.6 |  5.698 % |
c |      1319 |  156812   395741 |   84542    1267    10886     8.6 |  5.895 % |
c |      2078 |  156456   394924 |   92996    2003    54480    27.2 |  6.075 % |
c |      3217 |  156172   394286 |  102295    3121    68140    21.8 |  6.212 % |
c |      4925 |  155735   393282 |  112525    4761   121732    25.6 |  6.437 % |
c |      7488 |  154910   391386 |  123778    7280   209775    28.8 |  6.883 % |
c |     11333 |  154139   389612 |  136155   11054   291237    26.3 |  7.263 % |
c |     17099 |  153662   388518 |  149771   16795   475385    28.3 |  7.514 % |
c |     25750 |  153495   388117 |  164748   25435   925575    36.4 |  7.603 % |
c |     38724 |  152688   386270 |  181223   38366  1340182    34.9 |  8.010 % |
c |     58185 |  151682   383823 |  199345   57753  2030081    35.2 |  8.470 % |
c |     87377 |  151486   383381 |  219280   86899  3425488    39.4 |  8.574 % |
c |    131166 |  150944   382147 |  241208  130636  5406999    41.4 |  8.860 % |
c |    196850 |  149801   379321 |  265329  196246  7845951    40.0 |  9.425 % |
c |    295377 |  149561   378749 |  291862   48914  1362935    27.9 |  9.555 % |
c |    443166 |  148602   376555 |  321048  196630  7273432    37.0 | 10.086 % |

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/29150/stat): 29150 (minisat+_script) R 29149 29150 2660 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1855735044 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/29150/statm): 174 3 169 147 0 27 0
[pid=29150] 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=29151
New process pid=29152
New process pid=29153
execve syscall for /bin/sed executable
One traced child (pid=29152) 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=29153) exited with status: 0
One traced child (pid=29151) exited with status: 0
New process pid=29154
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-13-7-vpm2.opb

[startup+10.0037 s]
Raw data (loadavg): 0.90 0.95 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 4877 0 0 0 959 18 0 0 25 0 1 0 1855735049 20553728 4672 4294967295 134512640 135094434 3221224432 3221223056 134557650 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 5018 4672 145 145 0 4873 0
[pid=29154] vsize: 20072
Current children cumulated CPU time (s) 9.78
Current children cumulated vsize (Kb) 22196

[startup+20.0054 s]
Raw data (loadavg): 0.92 0.96 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 5154 0 0 0 1954 19 0 0 25 0 1 0 1855735049 21667840 4949 4294967295 134512640 135094434 3221224432 3221223056 134557681 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 5290 4949 145 145 0 5145 0
[pid=29154] vsize: 21160
Current children cumulated CPU time (s) 19.74
Current children cumulated vsize (Kb) 23284

[startup+30.0062 s]
Raw data (loadavg): 0.93 0.96 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 5419 0 0 0 2948 22 0 0 25 0 1 0 1855735049 22794240 5214 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29154/statm): 5565 5214 145 145 0 5420 0
[pid=29154] vsize: 22260
Current children cumulated CPU time (s) 29.71
Current children cumulated vsize (Kb) 24384

[startup+40.0069 s]
Raw data (loadavg): 0.94 0.96 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 5886 0 0 0 3941 25 0 0 25 0 1 0 1855735049 24678400 5681 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29154/statm): 6025 5681 145 145 0 5880 0
[pid=29154] vsize: 24100
Current children cumulated CPU time (s) 39.67
Current children cumulated vsize (Kb) 26224

[startup+50.0086 s]
Raw data (loadavg): 0.95 0.96 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 6126 0 0 0 4935 28 0 0 25 0 1 0 1855735049 25624576 5921 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 6256 5921 145 145 0 6111 0
[pid=29154] vsize: 25024
Current children cumulated CPU time (s) 49.64
Current children cumulated vsize (Kb) 27148

[startup+60.0083 s]
Raw data (loadavg): 0.95 0.96 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 6354 0 0 0 5931 29 0 0 25 0 1 0 1855735049 26673152 6149 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 6512 6149 145 145 0 6367 0
[pid=29154] vsize: 26048
Current children cumulated CPU time (s) 59.61
Current children cumulated vsize (Kb) 28172

[startup+70.009 s]
Raw data (loadavg): 0.96 0.96 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 6551 0 0 0 6928 31 0 0 25 0 1 0 1855735049 27451392 6346 4294967295 134512640 135094434 3221224432 3221223092 134553530 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 6702 6346 145 145 0 6557 0
[pid=29154] vsize: 26808
Current children cumulated CPU time (s) 69.6
Current children cumulated vsize (Kb) 28932

[startup+80.0097 s]
Raw data (loadavg): 0.97 0.96 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 6867 0 0 0 7921 33 0 0 25 0 1 0 1855735049 28712960 6662 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 7010 6662 145 145 0 6865 0
[pid=29154] vsize: 28040
Current children cumulated CPU time (s) 79.55
Current children cumulated vsize (Kb) 30164

[startup+90.0105 s]
Raw data (loadavg): 0.97 0.96 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 7353 0 0 0 8913 37 0 0 25 0 1 0 1855735049 30670848 7148 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 7488 7148 145 145 0 7343 0
[pid=29154] vsize: 29952
Current children cumulated CPU time (s) 89.51
Current children cumulated vsize (Kb) 32076

[startup+100.011 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 7725 0 0 0 9907 40 0 0 25 0 1 0 1855735049 32169984 7520 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 7854 7520 145 145 0 7709 0
[pid=29154] vsize: 31416
Current children cumulated CPU time (s) 99.48
Current children cumulated vsize (Kb) 33540

[startup+110.012 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 8019 0 0 0 10901 42 0 0 25 0 1 0 1855735049 33619968 7814 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 8208 7814 145 145 0 8063 0
[pid=29154] vsize: 32832
Current children cumulated CPU time (s) 109.44
Current children cumulated vsize (Kb) 34956

[startup+120.013 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 8246 0 0 0 11896 44 0 0 25 0 1 0 1855735049 34541568 8041 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 8433 8041 145 145 0 8288 0
[pid=29154] vsize: 33732
Current children cumulated CPU time (s) 119.41
Current children cumulated vsize (Kb) 35856

[startup+130.013 s]
Raw data (loadavg): 0.98 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 8470 0 0 0 12893 46 0 0 25 0 1 0 1855735049 35454976 8265 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 8656 8265 145 145 0 8511 0
[pid=29154] vsize: 34624
Current children cumulated CPU time (s) 129.4
Current children cumulated vsize (Kb) 36748

[startup+140.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 8654 0 0 0 13890 47 0 0 25 0 1 0 1855735049 36188160 8449 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 8835 8449 145 145 0 8690 0
[pid=29154] vsize: 35340
Current children cumulated CPU time (s) 139.38
Current children cumulated vsize (Kb) 37464

[startup+150.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 8830 0 0 0 14888 48 0 0 25 0 1 0 1855735049 36900864 8625 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 9009 8625 145 145 0 8864 0
[pid=29154] vsize: 36036
Current children cumulated CPU time (s) 149.37
Current children cumulated vsize (Kb) 38160

[startup+160.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 8992 0 0 0 15884 51 0 0 25 0 1 0 1855735049 37556224 8787 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 9169 8787 145 145 0 9024 0
[pid=29154] vsize: 36676
Current children cumulated CPU time (s) 159.36
Current children cumulated vsize (Kb) 38800

[startup+170.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 9168 0 0 0 16881 53 0 0 25 0 1 0 1855735049 38277120 8963 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 9345 8963 145 145 0 9200 0
[pid=29154] vsize: 37380
Current children cumulated CPU time (s) 169.35
Current children cumulated vsize (Kb) 39504

[startup+180.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 9314 0 0 0 17878 54 0 0 25 0 1 0 1855735049 38866944 9109 4294967295 134512640 135094434 3221224432 3221223088 134557984 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 9489 9109 145 145 0 9344 0
[pid=29154] vsize: 37956
Current children cumulated CPU time (s) 179.33
Current children cumulated vsize (Kb) 40080

[startup+190.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 9463 0 0 0 18876 55 0 0 25 0 1 0 1855735049 39477248 9258 4294967295 134512640 135094434 3221224432 3221223072 134558269 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 9638 9258 145 145 0 9493 0
[pid=29154] vsize: 38552
Current children cumulated CPU time (s) 189.32
Current children cumulated vsize (Kb) 40676

[startup+200.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 9624 0 0 0 19873 56 0 0 25 0 1 0 1855735049 40124416 9419 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 9796 9419 145 145 0 9651 0
[pid=29154] vsize: 39184
Current children cumulated CPU time (s) 199.3
Current children cumulated vsize (Kb) 41308

[startup+210.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 9841 0 0 0 20869 58 0 0 25 0 1 0 1855735049 40988672 9636 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 10007 9636 145 145 0 9862 0
[pid=29154] vsize: 40028
Current children cumulated CPU time (s) 209.28
Current children cumulated vsize (Kb) 42152

[startup+220.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 10010 0 0 0 21865 60 0 0 25 0 1 0 1855735049 41668608 9805 4294967295 134512640 135094434 3221224432 3221223088 134558392 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 10173 9805 145 145 0 10028 0
[pid=29154] vsize: 40692
Current children cumulated CPU time (s) 219.26
Current children cumulated vsize (Kb) 42816

[startup+230.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 10275 0 0 0 22859 63 0 0 25 0 1 0 1855735049 42737664 10070 4294967295 134512640 135094434 3221224432 3221223088 134557893 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29154/statm): 10434 10070 145 145 0 10289 0
[pid=29154] vsize: 41736
Current children cumulated CPU time (s) 229.23
Current children cumulated vsize (Kb) 43860

[startup+240.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 10517 0 0 0 23854 65 0 0 25 0 1 0 1855735049 43716608 10312 4294967295 134512640 135094434 3221224432 3221223104 134556073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29154/statm): 10673 10312 145 145 0 10528 0
[pid=29154] vsize: 42692
Current children cumulated CPU time (s) 239.2
Current children cumulated vsize (Kb) 44816

[startup+250.027 s]
Raw data (loadavg): 0.99 0.97 0.91 1/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) T 29150 29150 2660 0 -1 0 10775 0 0 0 24848 67 0 0 25 0 1 0 1855735049 44752896 10570 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/29154/statm): 10926 10570 145 145 0 10781 0
[pid=29154] vsize: 43704
Current children cumulated CPU time (s) 249.16
Current children cumulated vsize (Kb) 45828

[startup+260.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 11088 0 0 0 25842 70 0 0 25 0 1 0 1855735049 46022656 10883 4294967295 134512640 135094434 3221224432 3221223092 134553499 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 11236 10883 145 145 0 11091 0
[pid=29154] vsize: 44944
Current children cumulated CPU time (s) 259.13
Current children cumulated vsize (Kb) 47068

[startup+270.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 11281 0 0 0 26840 71 0 0 25 0 1 0 1855735049 46837760 11076 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 11435 11076 145 145 0 11290 0
[pid=29154] vsize: 45740
Current children cumulated CPU time (s) 269.12
Current children cumulated vsize (Kb) 47864

[startup+280.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 11423 0 0 0 27837 72 0 0 25 0 1 0 1855735049 47398912 11218 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 11572 11218 145 145 0 11427 0
[pid=29154] vsize: 46288
Current children cumulated CPU time (s) 279.1
Current children cumulated vsize (Kb) 48412

[startup+290.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 11622 0 0 0 28832 75 0 0 25 0 1 0 1855735049 48709632 11417 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 11892 11417 145 145 0 11747 0
[pid=29154] vsize: 47568
Current children cumulated CPU time (s) 289.08
Current children cumulated vsize (Kb) 49692

[startup+300.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 11787 0 0 0 29830 76 0 0 25 0 1 0 1855735049 49385472 11582 4294967295 134512640 135094434 3221224432 3221223088 134557972 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 12057 11582 145 145 0 11912 0
[pid=29154] vsize: 48228
Current children cumulated CPU time (s) 299.07
Current children cumulated vsize (Kb) 50352

[startup+310.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 11960 0 0 0 30827 78 0 0 25 0 1 0 1855735049 50094080 11755 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 12230 11755 145 145 0 12085 0
[pid=29154] vsize: 48920
Current children cumulated CPU time (s) 309.06
Current children cumulated vsize (Kb) 51044

[startup+320.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 12199 0 0 0 31822 80 0 0 25 0 1 0 1855735049 51073024 11994 4294967295 134512640 135094434 3221224432 3221223092 134553497 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 12469 11994 145 145 0 12324 0
[pid=29154] vsize: 49876
Current children cumulated CPU time (s) 319.03
Current children cumulated vsize (Kb) 52000

[startup+330.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) T 29150 29150 2660 0 -1 0 12444 0 0 0 32819 82 0 0 25 0 1 0 1855735049 52072448 12239 4294967295 134512640 135094434 3221224432 3221222780 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/29154/statm): 12713 12239 145 145 0 12568 0
[pid=29154] vsize: 50852
Current children cumulated CPU time (s) 329.02
Current children cumulated vsize (Kb) 52976

[startup+340.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 12584 0 0 0 33817 83 0 0 25 0 1 0 1855735049 52625408 12379 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 12848 12379 145 145 0 12703 0
[pid=29154] vsize: 51392
Current children cumulated CPU time (s) 339.01
Current children cumulated vsize (Kb) 53516

[startup+350.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 12786 0 0 0 34814 84 0 0 25 0 1 0 1855735049 53415936 12581 4294967295 134512640 135094434 3221224432 3221223104 134556410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 13041 12581 145 145 0 12896 0
[pid=29154] vsize: 52164
Current children cumulated CPU time (s) 348.99
Current children cumulated vsize (Kb) 54288

[startup+360.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 12971 0 0 0 35810 86 0 0 25 0 1 0 1855735049 54157312 12766 4294967295 134512640 135094434 3221224432 3221223056 134557685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 13222 12766 145 145 0 13077 0
[pid=29154] vsize: 52888
Current children cumulated CPU time (s) 358.97
Current children cumulated vsize (Kb) 55012

[startup+370.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 13132 0 0 0 36809 87 0 0 25 0 1 0 1855735049 54812672 12927 4294967295 134512640 135094434 3221224432 3221223088 134557879 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 13382 12927 145 145 0 13237 0
[pid=29154] vsize: 53528
Current children cumulated CPU time (s) 368.97
Current children cumulated vsize (Kb) 55652

[startup+380.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 13281 0 0 0 37806 88 0 0 25 0 1 0 1855735049 55398400 13076 4294967295 134512640 135094434 3221224432 3221223104 134556297 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 13525 13076 145 145 0 13380 0
[pid=29154] vsize: 54100
Current children cumulated CPU time (s) 378.95
Current children cumulated vsize (Kb) 56224

[startup+390.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 13418 0 0 0 38804 89 0 0 25 0 1 0 1855735049 55971840 13213 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 13665 13213 145 145 0 13520 0
[pid=29154] vsize: 54660
Current children cumulated CPU time (s) 388.94
Current children cumulated vsize (Kb) 56784

[startup+400.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 13586 0 0 0 39802 90 0 0 25 0 1 0 1855735049 56680448 13381 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 13838 13381 145 145 0 13693 0
[pid=29154] vsize: 55352
Current children cumulated CPU time (s) 398.93
Current children cumulated vsize (Kb) 57476

[startup+410.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 13777 0 0 0 40800 91 0 0 25 0 1 0 1855735049 57446400 13572 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29154/statm): 14025 13572 145 145 0 13880 0
[pid=29154] vsize: 56100
Current children cumulated CPU time (s) 408.92
Current children cumulated vsize (Kb) 58224

[startup+420.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 13987 0 0 0 41795 94 0 0 25 0 1 0 1855735049 58294272 13782 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29154/statm): 14232 13782 145 145 0 14087 0
[pid=29154] vsize: 56928
Current children cumulated CPU time (s) 418.9
Current children cumulated vsize (Kb) 59052

[startup+430.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 14256 0 0 0 42788 97 0 0 25 0 1 0 1855735049 59379712 14051 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29154/statm): 14497 14051 145 145 0 14352 0
[pid=29154] vsize: 57988
Current children cumulated CPU time (s) 428.86
Current children cumulated vsize (Kb) 60112

[startup+440.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 14520 0 0 0 43783 99 0 0 25 0 1 0 1855735049 60452864 14315 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29154/statm): 14759 14315 145 145 0 14614 0
[pid=29154] vsize: 59036
Current children cumulated CPU time (s) 438.83
Current children cumulated vsize (Kb) 61160

[startup+450.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 14700 0 0 0 44780 100 0 0 25 0 1 0 1855735049 61181952 14495 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29154/statm): 14937 14495 145 145 0 14792 0
[pid=29154] vsize: 59748
Current children cumulated CPU time (s) 448.81
Current children cumulated vsize (Kb) 61872

[startup+460.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 14857 0 0 0 45777 102 0 0 25 0 1 0 1855735049 61820928 14652 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/29154/statm): 15093 14652 145 145 0 14948 0
[pid=29154] vsize: 60372
Current children cumulated CPU time (s) 458.8
Current children cumulated vsize (Kb) 62496

[startup+470.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 15025 0 0 0 46774 104 0 0 25 0 1 0 1855735049 62500864 14820 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 15259 14820 145 145 0 15114 0
[pid=29154] vsize: 61036
Current children cumulated CPU time (s) 468.79
Current children cumulated vsize (Kb) 63160

[startup+480.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 15232 0 0 0 47771 105 0 0 25 0 1 0 1855735049 63336448 15027 4294967295 134512640 135094434 3221224432 3221223024 134557248 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 15463 15027 145 145 0 15318 0
[pid=29154] vsize: 61852
Current children cumulated CPU time (s) 478.77
Current children cumulated vsize (Kb) 63976

[startup+490.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 15445 0 0 0 48766 107 0 0 25 0 1 0 1855735049 64200704 15240 4294967295 134512640 135094434 3221224432 3221223024 134556961 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 15674 15240 145 145 0 15529 0
[pid=29154] vsize: 62696
Current children cumulated CPU time (s) 488.74
Current children cumulated vsize (Kb) 64820

[startup+500.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 15570 0 0 0 49765 108 0 0 25 0 1 0 1855735049 64724992 15365 4294967295 134512640 135094434 3221224432 3221223088 134558405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 15802 15365 145 145 0 15657 0
[pid=29154] vsize: 63208
Current children cumulated CPU time (s) 498.74
Current children cumulated vsize (Kb) 65332

[startup+510.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 15703 0 0 0 50763 109 0 0 25 0 1 0 1855735049 65241088 15498 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 15928 15498 145 145 0 15783 0
[pid=29154] vsize: 63712
Current children cumulated CPU time (s) 508.73
Current children cumulated vsize (Kb) 65836

[startup+520.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 15843 0 0 0 51761 110 0 0 25 0 1 0 1855735049 65810432 15638 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 16067 15638 145 145 0 15922 0
[pid=29154] vsize: 64268
Current children cumulated CPU time (s) 518.72
Current children cumulated vsize (Kb) 66392

[startup+530.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 15980 0 0 0 52759 110 0 0 25 0 1 0 1855735049 66359296 15775 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 16201 15775 145 145 0 16056 0
[pid=29154] vsize: 64804
Current children cumulated CPU time (s) 528.7
Current children cumulated vsize (Kb) 66928

[startup+540.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 16109 0 0 0 53756 113 0 0 25 0 1 0 1855735049 66883584 15904 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 16329 15904 145 145 0 16184 0
[pid=29154] vsize: 65316
Current children cumulated CPU time (s) 538.7
Current children cumulated vsize (Kb) 67440

[startup+550.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 16252 0 0 0 54753 115 0 0 25 0 1 0 1855735049 67485696 16047 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 16476 16047 145 145 0 16331 0
[pid=29154] vsize: 65904
Current children cumulated CPU time (s) 548.69
Current children cumulated vsize (Kb) 68028

[startup+560.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 16408 0 0 0 55752 116 0 0 25 0 1 0 1855735049 68112384 16203 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 16629 16203 145 145 0 16484 0
[pid=29154] vsize: 66516
Current children cumulated CPU time (s) 558.69
Current children cumulated vsize (Kb) 68640

[startup+570.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 16535 0 0 0 56749 117 0 0 25 0 1 0 1855735049 68620288 16330 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 16753 16330 145 145 0 16608 0
[pid=29154] vsize: 67012
Current children cumulated CPU time (s) 568.67
Current children cumulated vsize (Kb) 69136

[startup+580.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 16672 0 0 0 57747 118 0 0 25 0 1 0 1855735049 69152768 16467 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 16883 16467 145 145 0 16738 0
[pid=29154] vsize: 67532
Current children cumulated CPU time (s) 578.66
Current children cumulated vsize (Kb) 69656

[startup+590.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 16815 0 0 0 58745 119 0 0 25 0 1 0 1855735049 69763072 16610 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 17032 16610 145 145 0 16887 0
[pid=29154] vsize: 68128
Current children cumulated CPU time (s) 588.65
Current children cumulated vsize (Kb) 70252

[startup+600.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 16963 0 0 0 59743 121 0 0 25 0 1 0 1855735049 70352896 16758 4294967295 134512640 135094434 3221224432 3221223104 134556401 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 17176 16758 145 145 0 17031 0
[pid=29154] vsize: 68704
Current children cumulated CPU time (s) 598.65
Current children cumulated vsize (Kb) 70828

[startup+610.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 17104 0 0 0 60740 122 0 0 25 0 1 0 1855735049 70918144 16899 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 17314 16899 145 145 0 17169 0
[pid=29154] vsize: 69256
Current children cumulated CPU time (s) 608.63
Current children cumulated vsize (Kb) 71380

[startup+620.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 17218 0 0 0 61737 123 0 0 25 0 1 0 1855735049 71376896 17013 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 17426 17013 145 145 0 17281 0
[pid=29154] vsize: 69704
Current children cumulated CPU time (s) 618.61
Current children cumulated vsize (Kb) 71828

[startup+630.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 17330 0 0 0 62735 124 0 0 25 0 1 0 1855735049 71827456 17125 4294967295 134512640 135094434 3221224432 3221223024 134557208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 17536 17125 145 145 0 17391 0
[pid=29154] vsize: 70144
Current children cumulated CPU time (s) 628.6
Current children cumulated vsize (Kb) 72268

[startup+640.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 17447 0 0 0 63734 125 0 0 25 0 1 0 1855735049 72310784 17242 4294967295 134512640 135094434 3221224432 3221223088 134557928 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 17654 17242 145 145 0 17509 0
[pid=29154] vsize: 70616
Current children cumulated CPU time (s) 638.6
Current children cumulated vsize (Kb) 72740

[startup+650.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 17561 0 0 0 64732 126 0 0 25 0 1 0 1855735049 72761344 17356 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 17764 17356 145 145 0 17619 0
[pid=29154] vsize: 71056
Current children cumulated CPU time (s) 648.59
Current children cumulated vsize (Kb) 73180

[startup+660.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 17675 0 0 0 65730 126 0 0 25 0 1 0 1855735049 73220096 17470 4294967295 134512640 135094434 3221224432 3221223024 134557238 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 17876 17470 145 145 0 17731 0
[pid=29154] vsize: 71504
Current children cumulated CPU time (s) 658.57
Current children cumulated vsize (Kb) 73628

[startup+670.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 17785 0 0 0 66728 127 0 0 25 0 1 0 1855735049 74731520 17580 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 18245 17580 145 145 0 18100 0
[pid=29154] vsize: 72980
Current children cumulated CPU time (s) 668.56
Current children cumulated vsize (Kb) 75104

[startup+680.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 17880 0 0 0 67726 128 0 0 25 0 1 0 1855735049 75104256 17675 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 18336 17675 145 145 0 18191 0
[pid=29154] vsize: 73344
Current children cumulated CPU time (s) 678.55
Current children cumulated vsize (Kb) 75468

[startup+690.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 17987 0 0 0 68725 128 0 0 25 0 1 0 1855735049 75542528 17782 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 18443 17782 145 145 0 18298 0
[pid=29154] vsize: 73772
Current children cumulated CPU time (s) 688.54
Current children cumulated vsize (Kb) 75896

[startup+700.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18106 0 0 0 69723 129 0 0 25 0 1 0 1855735049 76021760 17901 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 18560 17901 145 145 0 18415 0
[pid=29154] vsize: 74240
Current children cumulated CPU time (s) 698.53
Current children cumulated vsize (Kb) 76364

[startup+710.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18207 0 0 0 70721 129 0 0 25 0 1 0 1855735049 76419072 18002 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 18657 18002 145 145 0 18512 0
[pid=29154] vsize: 74628
Current children cumulated CPU time (s) 708.51
Current children cumulated vsize (Kb) 76752

[startup+720.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18337 0 0 0 71718 131 0 0 25 0 1 0 1855735049 76935168 18132 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 18783 18132 145 145 0 18638 0
[pid=29154] vsize: 75132
Current children cumulated CPU time (s) 718.5
Current children cumulated vsize (Kb) 77256

[startup+730.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18337 0 0 0 72718 131 0 0 25 0 1 0 1855735049 76935168 18132 4294967295 134512640 135094434 3221224432 3221223088 134557956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 18783 18132 145 145 0 18638 0
[pid=29154] vsize: 75132
Current children cumulated CPU time (s) 728.5
Current children cumulated vsize (Kb) 77256

[startup+740.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18337 0 0 0 73719 131 0 0 25 0 1 0 1855735049 76935168 18132 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 18783 18132 145 145 0 18638 0
[pid=29154] vsize: 75132
Current children cumulated CPU time (s) 738.51
Current children cumulated vsize (Kb) 77256

[startup+750.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18337 0 0 0 74719 131 0 0 25 0 1 0 1855735049 76935168 18132 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 18783 18132 145 145 0 18638 0
[pid=29154] vsize: 75132
Current children cumulated CPU time (s) 748.51
Current children cumulated vsize (Kb) 77256

[startup+760.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18337 0 0 0 75719 131 0 0 25 0 1 0 1855735049 76935168 18132 4294967295 134512640 135094434 3221224432 3221223104 134556184 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 18783 18132 145 145 0 18638 0
[pid=29154] vsize: 75132
Current children cumulated CPU time (s) 758.51
Current children cumulated vsize (Kb) 77256

[startup+770.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18337 0 0 0 76719 131 0 0 25 0 1 0 1855735049 76935168 18132 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 18783 18132 145 145 0 18638 0
[pid=29154] vsize: 75132
Current children cumulated CPU time (s) 768.51
Current children cumulated vsize (Kb) 77256

[startup+780.075 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18337 0 0 0 77719 131 0 0 25 0 1 0 1855735049 76935168 18132 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 18783 18132 145 145 0 18638 0
[pid=29154] vsize: 75132
Current children cumulated CPU time (s) 778.51
Current children cumulated vsize (Kb) 77256

[startup+790.075 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18337 0 0 0 78719 131 0 0 25 0 1 0 1855735049 76935168 18132 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 18783 18132 145 145 0 18638 0
[pid=29154] vsize: 75132
Current children cumulated CPU time (s) 788.51
Current children cumulated vsize (Kb) 77256

[startup+800.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18337 0 0 0 79719 131 0 0 25 0 1 0 1855735049 76935168 18132 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 18783 18132 145 145 0 18638 0
[pid=29154] vsize: 75132
Current children cumulated CPU time (s) 798.51
Current children cumulated vsize (Kb) 77256

[startup+810.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18337 0 0 0 80720 131 0 0 25 0 1 0 1855735049 76935168 18132 4294967295 134512640 135094434 3221224432 3221223044 134563080 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 18783 18132 145 145 0 18638 0
[pid=29154] vsize: 75132
Current children cumulated CPU time (s) 808.52
Current children cumulated vsize (Kb) 77256

[startup+820.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18337 0 0 0 81719 132 0 0 25 0 1 0 1855735049 76935168 18132 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 18783 18132 145 145 0 18638 0
[pid=29154] vsize: 75132
Current children cumulated CPU time (s) 818.52
Current children cumulated vsize (Kb) 77256

[startup+830.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18337 0 0 0 82720 132 0 0 25 0 1 0 1855735049 76935168 18132 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 18783 18132 145 145 0 18638 0
[pid=29154] vsize: 75132
Current children cumulated CPU time (s) 828.53
Current children cumulated vsize (Kb) 77256

[startup+840.078 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18337 0 0 0 83720 132 0 0 25 0 1 0 1855735049 76935168 18132 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 18783 18132 145 145 0 18638 0
[pid=29154] vsize: 75132
Current children cumulated CPU time (s) 838.53
Current children cumulated vsize (Kb) 77256

[startup+850.079 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18337 0 0 0 84720 132 0 0 25 0 1 0 1855735049 76935168 18132 4294967295 134512640 135094434 3221224432 3221223056 134557565 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 18783 18132 145 145 0 18638 0
[pid=29154] vsize: 75132
Current children cumulated CPU time (s) 848.53
Current children cumulated vsize (Kb) 77256

[startup+860.079 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18337 0 0 0 85720 132 0 0 25 0 1 0 1855735049 76935168 18132 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 18783 18132 145 145 0 18638 0
[pid=29154] vsize: 75132
Current children cumulated CPU time (s) 858.53
Current children cumulated vsize (Kb) 77256

[startup+870.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18337 0 0 0 86721 132 0 0 25 0 1 0 1855735049 76935168 18132 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 18783 18132 145 145 0 18638 0
[pid=29154] vsize: 75132
Current children cumulated CPU time (s) 868.54
Current children cumulated vsize (Kb) 77256

[startup+880.081 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18339 0 0 0 87720 132 0 0 25 0 1 0 1855735049 76935168 18134 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 18783 18134 145 145 0 18638 0
[pid=29154] vsize: 75132
Current children cumulated CPU time (s) 878.53
Current children cumulated vsize (Kb) 77256

[startup+890.082 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18339 0 0 0 88721 132 0 0 25 0 1 0 1855735049 76935168 18134 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 18783 18134 145 145 0 18638 0
[pid=29154] vsize: 75132
Current children cumulated CPU time (s) 888.54
Current children cumulated vsize (Kb) 77256

[startup+900.082 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18339 0 0 0 89721 132 0 0 25 0 1 0 1855735049 76935168 18134 4294967295 134512640 135094434 3221224432 3221223024 134557334 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 18783 18134 145 145 0 18638 0
[pid=29154] vsize: 75132
Current children cumulated CPU time (s) 898.54
Current children cumulated vsize (Kb) 77256

[startup+910.082 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18339 0 0 0 90721 132 0 0 25 0 1 0 1855735049 76935168 18134 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 18783 18134 145 145 0 18638 0
[pid=29154] vsize: 75132
Current children cumulated CPU time (s) 908.54
Current children cumulated vsize (Kb) 77256

[startup+920.084 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18339 0 0 0 91721 132 0 0 25 0 1 0 1855735049 76935168 18134 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 18783 18134 145 145 0 18638 0
[pid=29154] vsize: 75132
Current children cumulated CPU time (s) 918.54
Current children cumulated vsize (Kb) 77256

[startup+930.085 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18340 0 0 0 92722 132 0 0 25 0 1 0 1855735049 76935168 18135 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 18783 18135 145 145 0 18638 0
[pid=29154] vsize: 75132
Current children cumulated CPU time (s) 928.55
Current children cumulated vsize (Kb) 77256

[startup+940.085 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18340 0 0 0 93722 132 0 0 25 0 1 0 1855735049 76935168 18135 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 18783 18135 145 145 0 18638 0
[pid=29154] vsize: 75132
Current children cumulated CPU time (s) 938.55
Current children cumulated vsize (Kb) 77256

[startup+950.086 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18340 0 0 0 94722 133 0 0 25 0 1 0 1855735049 76935168 18135 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 18783 18135 145 145 0 18638 0
[pid=29154] vsize: 75132
Current children cumulated CPU time (s) 948.56
Current children cumulated vsize (Kb) 77256

[startup+960.086 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18340 0 0 0 95722 133 0 0 25 0 1 0 1855735049 76935168 18135 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 18783 18135 145 145 0 18638 0
[pid=29154] vsize: 75132
Current children cumulated CPU time (s) 958.56
Current children cumulated vsize (Kb) 77256

[startup+970.086 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18340 0 0 0 96722 133 0 0 25 0 1 0 1855735049 76935168 18135 4294967295 134512640 135094434 3221224432 3221223088 134557879 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 18783 18135 145 145 0 18638 0
[pid=29154] vsize: 75132
Current children cumulated CPU time (s) 968.56
Current children cumulated vsize (Kb) 77256

[startup+980.087 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18340 0 0 0 97722 133 0 0 25 0 1 0 1855735049 76935168 18135 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 18783 18135 145 145 0 18638 0
[pid=29154] vsize: 75132
Current children cumulated CPU time (s) 978.56
Current children cumulated vsize (Kb) 77256

[startup+990.088 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18340 0 0 0 98723 133 0 0 25 0 1 0 1855735049 76935168 18135 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 18783 18135 145 145 0 18638 0
[pid=29154] vsize: 75132
Current children cumulated CPU time (s) 988.57
Current children cumulated vsize (Kb) 77256

[startup+1000.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18340 0 0 0 99723 133 0 0 25 0 1 0 1855735049 76935168 18135 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 18783 18135 145 145 0 18638 0
[pid=29154] vsize: 75132
Current children cumulated CPU time (s) 998.57
Current children cumulated vsize (Kb) 77256

[startup+1010.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18340 0 0 0 100723 133 0 0 25 0 1 0 1855735049 76935168 18135 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 18783 18135 145 145 0 18638 0
[pid=29154] vsize: 75132
Current children cumulated CPU time (s) 1008.57
Current children cumulated vsize (Kb) 77256

[startup+1020.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18340 0 0 0 101723 133 0 0 25 0 1 0 1855735049 76935168 18135 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 18783 18135 145 145 0 18638 0
[pid=29154] vsize: 75132
Current children cumulated CPU time (s) 1018.57
Current children cumulated vsize (Kb) 77256

[startup+1030.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18340 0 0 0 102723 133 0 0 25 0 1 0 1855735049 76935168 18135 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 18783 18135 145 145 0 18638 0
[pid=29154] vsize: 75132
Current children cumulated CPU time (s) 1028.57
Current children cumulated vsize (Kb) 77256

[startup+1040.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18340 0 0 0 103724 133 0 0 25 0 1 0 1855735049 76935168 18135 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 18783 18135 145 145 0 18638 0
[pid=29154] vsize: 75132
Current children cumulated CPU time (s) 1038.58
Current children cumulated vsize (Kb) 77256

[startup+1050.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18340 0 0 0 104724 133 0 0 25 0 1 0 1855735049 76935168 18135 4294967295 134512640 135094434 3221224432 3221223056 134557726 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 18783 18135 145 145 0 18638 0
[pid=29154] vsize: 75132
Current children cumulated CPU time (s) 1048.58
Current children cumulated vsize (Kb) 77256

[startup+1060.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18340 0 0 0 105724 133 0 0 25 0 1 0 1855735049 76935168 18135 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 18783 18135 145 145 0 18638 0
[pid=29154] vsize: 75132
Current children cumulated CPU time (s) 1058.58
Current children cumulated vsize (Kb) 77256

[startup+1070.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18340 0 0 0 106724 133 0 0 25 0 1 0 1855735049 76935168 18135 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 18783 18135 145 145 0 18638 0
[pid=29154] vsize: 75132
Current children cumulated CPU time (s) 1068.58
Current children cumulated vsize (Kb) 77256

[startup+1080.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18340 0 0 0 107724 133 0 0 25 0 1 0 1855735049 76935168 18135 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 18783 18135 145 145 0 18638 0
[pid=29154] vsize: 75132
Current children cumulated CPU time (s) 1078.58
Current children cumulated vsize (Kb) 77256

[startup+1090.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18341 0 0 0 108725 133 0 0 25 0 1 0 1855735049 76935168 18136 4294967295 134512640 135094434 3221224432 3221223092 134553487 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 18783 18136 145 145 0 18638 0
[pid=29154] vsize: 75132
Current children cumulated CPU time (s) 1088.59
Current children cumulated vsize (Kb) 77256

[startup+1100.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18341 0 0 0 109725 133 0 0 25 0 1 0 1855735049 76935168 18136 4294967295 134512640 135094434 3221224432 3221223092 134553489 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 18783 18136 145 145 0 18638 0
[pid=29154] vsize: 75132
Current children cumulated CPU time (s) 1098.59
Current children cumulated vsize (Kb) 77256

[startup+1110.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18343 0 0 0 110725 133 0 0 25 0 1 0 1855735049 76935168 18138 4294967295 134512640 135094434 3221224432 3221223088 134557972 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 18783 18138 145 145 0 18638 0
[pid=29154] vsize: 75132
Current children cumulated CPU time (s) 1108.59
Current children cumulated vsize (Kb) 77256

[startup+1120.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18355 0 0 0 111725 133 0 0 25 0 1 0 1855735049 76996608 18150 4294967295 134512640 135094434 3221224432 3221223056 134557577 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 18798 18150 145 145 0 18653 0
[pid=29154] vsize: 75192
Current children cumulated CPU time (s) 1118.59
Current children cumulated vsize (Kb) 77316

[startup+1130.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18355 0 0 0 112725 133 0 0 25 0 1 0 1855735049 76996608 18150 4294967295 134512640 135094434 3221224432 3221223088 134557875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 18798 18150 145 145 0 18653 0
[pid=29154] vsize: 75192
Current children cumulated CPU time (s) 1128.59
Current children cumulated vsize (Kb) 77316

[startup+1140.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18355 0 0 0 113724 135 0 0 25 0 1 0 1855735049 76996608 18150 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 18798 18150 145 145 0 18653 0
[pid=29154] vsize: 75192
Current children cumulated CPU time (s) 1138.6
Current children cumulated vsize (Kb) 77316

[startup+1150.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18355 0 0 0 114723 135 0 0 25 0 1 0 1855735049 76996608 18150 4294967295 134512640 135094434 3221224432 3221223104 134556496 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 18798 18150 145 145 0 18653 0
[pid=29154] vsize: 75192
Current children cumulated CPU time (s) 1148.59
Current children cumulated vsize (Kb) 77316

[startup+1160.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18355 0 0 0 115723 136 0 0 25 0 1 0 1855735049 76996608 18150 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 18798 18150 145 145 0 18653 0
[pid=29154] vsize: 75192
Current children cumulated CPU time (s) 1158.6
Current children cumulated vsize (Kb) 77316

[startup+1170.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18356 0 0 0 116723 136 0 0 25 0 1 0 1855735049 76996608 18151 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 18798 18151 145 145 0 18653 0
[pid=29154] vsize: 75192
Current children cumulated CPU time (s) 1168.6
Current children cumulated vsize (Kb) 77316

[startup+1180.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18356 0 0 0 117723 137 0 0 25 0 1 0 1855735049 76996608 18151 4294967295 134512640 135094434 3221224432 3221223104 134556020 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 18798 18151 145 145 0 18653 0
[pid=29154] vsize: 75192
Current children cumulated CPU time (s) 1178.61
Current children cumulated vsize (Kb) 77316

[startup+1190.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18356 0 0 0 118723 137 0 0 25 0 1 0 1855735049 76996608 18151 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 18798 18151 145 145 0 18653 0
[pid=29154] vsize: 75192
Current children cumulated CPU time (s) 1188.61
Current children cumulated vsize (Kb) 77316

[startup+1200.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18356 0 0 0 119723 137 0 0 25 0 1 0 1855735049 76996608 18151 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 18798 18151 145 145 0 18653 0
[pid=29154] vsize: 75192
Current children cumulated CPU time (s) 1198.61
Current children cumulated vsize (Kb) 77316

[startup+1210.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18356 0 0 0 120723 137 0 0 25 0 1 0 1855735049 76996608 18151 4294967295 134512640 135094434 3221224432 3221223056 134557636 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 18798 18151 145 145 0 18653 0
[pid=29154] vsize: 75192
Current children cumulated CPU time (s) 1208.61
Current children cumulated vsize (Kb) 77316



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 29154
Raw data (/proc/29150/stat): 29150 (minisat+_script) S 29149 29150 2660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1855735044 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/29150/statm): 531 226 485 147 0 384 0
[pid=29150] vsize: 2124
Raw data (/proc/29154/stat): 29154 (minisat+_64-bit) R 29150 29150 2660 0 -1 0 18356 0 0 0 120723 137 0 0 25 0 1 0 1855735049 76996608 18151 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/29154/statm): 18798 18151 145 145 0 18653 0
[pid=29154] vsize: 75192
Current children cumulated CPU time (s) 1208.61
Current children cumulated vsize (Kb) 77316

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

Child status: 0
Real time (s): 1210.14
CPU time (s): 1208.65
CPU user time (s): 1207.24
CPU system time (s): 1.41079
CPU usage (%): 99.8767
Max. virtual memory (cumulated for all children) (Kb): 77316

Verifier Data

ERROR: no interpretation found !