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/plato.asu.edu/pub/milp/normalized-mps-v2-13-7-markshare1_1.opb
MD5SUMf88781e3d6e9a5487d13eaa213c27b55
Bench Categoryoptimization, medium integers (OPTMEDINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 5237
Optimality of the best value was proved NO
Number of terms in the objective function 120
Biggest coefficient in the objective function 524288
Number of bits for the biggest coefficient in the objective function 20
Sum of the numbers in the objective function 6291450
Number of bits of the sum of numbers in the objective function 23
Biggest number in a constraint 524288
Number of bits of the biggest number in a constraint 20
Biggest sum of numbers in a constraint 6291450
Number of bits of the biggest sum of numbers23
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1195.45
Number of variables205
Total number of constraints56
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)45
Number of constraints which are nor clauses,nor cardinality constraints11
Minimum length of a constraint1
Maximum length of a constraint105

Trace number 6287

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.020
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        837120 kB
Buffers:         38612 kB
Cached:         127288 kB
SwapCached:        768 kB
Active:          36532 kB
Inactive:       131880 kB
HighTotal:      131008 kB
HighFree:        35364 kB
LowTotal:       903652 kB
LowFree:        801756 kB
SwapTotal:     2097892 kB
SwapFree:      2096528 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5680 kB
Slab:            23444 kB
Committed_AS:    64132 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-20 05:31:31 (client local time) WITH STATUS 10 IN 1209.51 SECONDS
stats: 3443 7 1209.51 10

Solver Data

c Parsing PB file...
c Converting 17 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ######
c   -- Clauses(.)/Splits(s): (none)
c ---[  16]---> BDD-cost:    7
c ---[  15]---> BDD-cost:    7
c ---[  14]---> BDD-cost:    7
c ---[  13]---> BDD-cost:    7
c ---[  12]---> BDD-cost:    7
c ---[  10]---> Adder-cost: 554   maxlim: 438520   bits: 20/19
c ---[   8]---> Adder-cost: 562   maxlim: 469716   bits: 20/19
c ---[   6]---> Adder-cost: 644   maxlim: 485238   bits: 20/19
c ---[   4]---> Adder-cost: 446   maxlim: 425237   bits: 20/19
c ---[   2]---> Adder-cost: 494   maxlim: 433357   bits: 20/19
c ---[   0]---> Adder-cost: 474   maxlim: 432725   bits: 20/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   21500    76369 |    7166       0        0     nan |  0.000 % |
c |       101 |   21500    76369 |    7882     101      468     4.6 |  7.165 % |
c |       251 |   21500    76369 |    8670     251     3196    12.7 |  7.165 % |
c |       480 |   21492    76343 |    9537     479     7965    16.6 |  7.194 % |
c ==============================================================================
c Found solution: 552006
c ---[   0]---> Sorter-cost: 1464     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       620 |   25213    85029 |    8404     619     9130    14.7 |  7.194 % |
c |       721 |   25213    85029 |    9244     720    18323    25.4 |  5.272 % |
c |       873 |   25213    85029 |   10168     872    38194    43.8 |  5.272 % |
c |      1099 |   25205    85003 |   11185    1097    44770    40.8 |  5.293 % |
c |      1436 |   25205    85003 |   12304    1434    50426    35.2 |  5.293 % |
c ==============================================================================
c Found solution: 326866
c ---[   0]---> Sorter-cost:   17     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1527 |   25232    85100 |    8410    1525    51894    34.0 |  5.293 % |
c |      1628 |   25224    85074 |    9251    1625    53036    32.6 |  5.315 % |
c |      1779 |   25216    85048 |   10176    1775    55394    31.2 |  5.335 % |
c |      2004 |   25208    85022 |   11193    1999    58767    29.4 |  5.356 % |
c |      2341 |   25192    84970 |   12313    2334    62861    26.9 |  5.398 % |
c |      2847 |   25184    84944 |   13544    2839    69965    24.6 |  5.418 % |
c |      3608 |   25184    84944 |   14898    3600    95435    26.5 |  5.418 % |
c |      4747 |   25184    84944 |   16388    4739   144758    30.5 |  5.418 % |
c ==============================================================================
c Found solution: 90720
c ---[   0]---> Sorter-cost:   17     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4797 |   25161    84848 |    8387    4722   138574    29.3 |  5.418 % |
c |      4897 |   25161    84848 |    9225    4822   142605    29.6 |  5.550 % |
c |      5047 |   25161    84848 |   10148    4972   144103    29.0 |  5.550 % |
c |      5272 |   25161    84848 |   11163    5197   147996    28.5 |  5.550 % |
c |      5609 |   25161    84848 |   12279    5534   162224    29.3 |  5.550 % |
c |      6115 |   25161    84848 |   13507    6040   167189    27.7 |  5.550 % |
c |      6874 |   25161    84848 |   14858    6799   192943    28.4 |  5.550 % |
c |      8013 |   25161    84848 |   16343    7938   219858    27.7 |  5.550 % |
c |      9722 |   25161    84848 |   17978    9647   293177    30.4 |  5.550 % |
c |     12285 |   25161    84848 |   19776   12210   421505    34.5 |  5.550 % |
c ==============================================================================
c Found solution: 71680
c ---[   0]---> Sorter-cost:   13     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     13517 |   25175    84879 |    8391   13442   503492    37.5 |  5.550 % |
c |     13617 |   25175    84879 |    9230    6821   271301    39.8 |  5.566 % |
c |     13767 |   25175    84879 |   10153    6971   274301    39.3 |  5.566 % |
c |     13993 |   25175    84879 |   11168    7197   278686    38.7 |  5.566 % |
c |     14330 |   25175    84879 |   12285    7534   287188    38.1 |  5.566 % |
c |     14837 |   25167    84861 |   13513    8040   298611    37.1 |  5.607 % |
c |     15596 |   25167    84861 |   14865    8799   324504    36.9 |  5.607 % |
c |     16737 |   25167    84861 |   16351    9940   380508    38.3 |  5.607 % |
c |     18445 |   25159    84835 |   17986   11647   441573    37.9 |  5.628 % |
c |     21010 |   25159    84835 |   19785   14212   538347    37.9 |  5.628 % |
c |     24854 |   25159    84835 |   21764   18056   694983    38.5 |  5.628 % |
c |     30620 |   25151    84809 |   23940   12175   440850    36.2 |  5.649 % |
c |     39270 |   25151    84809 |   26334   20825   861201    41.4 |  5.649 % |
c |     52244 |   25143    84787 |   28968   19364  1066264    55.1 |  5.690 % |
c |     71706 |   25143    84787 |   31864   21785   832604    38.2 |  5.690 % |
c |    100898 |   25143    84787 |   35051   30864  1585633    51.4 |  5.690 % |
c |    144688 |   25127    84735 |   38556   30209  1934568    64.0 |  5.731 % |
c ==============================================================================
c Found solution: 57194
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    156428 |   24849    84050 |    8283   16798   793938    47.3 |  5.731 % |
c |    156528 |   24849    84050 |    9111    8499   353305    41.6 |  7.456 % |
c |    156678 |   24849    84050 |   10022    8649   356887    41.3 |  7.456 % |
c |    156906 |   24849    84050 |   11024    8877   362140    40.8 |  7.456 % |
c |    157244 |   24841    84024 |   12127    9213   367653    39.9 |  7.786 % |
c |    157750 |   24791    83912 |   13339    9716   380059    39.1 |  7.786 % |
c |    158510 |   24791    83912 |   14673   10476   402291    38.4 |  7.786 % |
c |    159650 |   24791    83912 |   16141   11616   445572    38.4 |  7.786 % |
c |    161358 |   24791    83912 |   17755   13324   500491    37.6 |  7.786 % |
c |    163922 |   24633    83548 |   19530   15878   584275    36.8 |  8.963 % |
c |    167767 |   24633    83548 |   21483   19723   717286    36.4 |  8.963 % |
c |    173533 |   24633    83548 |   23632   14127   524723    37.1 |  8.963 % |
c |    182182 |   24615    83508 |   25995   22775   900769    39.6 |  9.067 % |
c |    195157 |   24615    83508 |   28595   22368   947167    42.3 |  9.067 % |
c |    214618 |   24609    83494 |   31454   25616  1241598    48.5 |  9.108 % |
c |    243810 |   24609    83494 |   34600   15970  1161777    72.7 |  9.108 % |
c |    287599 |   24609    83494 |   38060   17320   924662    53.4 |  9.108 % |
c |    353284 |   24609    83494 |   41866   33078  2000413    60.5 |  9.108 % |
c ==============================================================================
c Found solution: 50892
c ---[   0]---> Sorter-cost:   15     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    357437 |   24626    83535 |    8208   37231  2195337    59.0 |  9.108 % |
c |    357538 |   24626    83535 |    9028    7749   343658    44.3 |  9.110 % |
c |    357688 |   24626    83535 |    9931    7899   346693    43.9 |  9.110 % |
c |    357913 |   24626    83535 |   10924    8124   351062    43.2 |  9.110 % |
c |    358250 |   24626    83535 |   12017    8461   353734    41.8 |  9.110 % |
c |    358756 |   24626    83535 |   13219    8967   373042    41.6 |  9.110 % |
c |    359516 |   24626    83535 |   14540    9727   389280    40.0 |  9.110 % |
c |    360655 |   24626    83535 |   15995   10866   432959    39.8 |  9.110 % |
c |    362365 |   24626    83535 |   17594   12576   498251    39.6 |  9.110 % |
c |    364927 |   24626    83535 |   19354   15138   598074    39.5 |  9.110 % |
c |    368772 |   24626    83535 |   21289   18983   932407    49.1 |  9.110 % |
c |    374538 |   24626    83535 |   23418   13599   607840    44.7 |  9.110 % |
c |    383187 |   24626    83535 |   25760   22248  1058848    47.6 |  9.110 % |
c |    396162 |   24626    83535 |   28336   20986  1245980    59.4 |  9.110 % |
c |    415623 |   24619    83519 |   31169   22739  1211865    53.3 |  9.171 % |
c |    444817 |   24619    83519 |   34286   33541  1608075    47.9 |  9.171 % |
c |    488606 |   24602    83481 |   37715   16382   727364    44.4 |  9.275 % |
c |    554292 |   24602    83481 |   41487   31383  2050371    65.3 |  9.275 % |
c ==============================================================================
c Found solution: 48690
c ---[   0]---> Sorter-cost:   12     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    558165 |   24611    83506 |    8203   35256  2301853    65.3 |  9.275 % |
c |    558266 |   24611    83506 |    9023    7352   361671    49.2 |  9.286 % |
c |    558416 |   24611    83506 |    9925    7502   363308    48.4 |  9.286 % |
c |    558641 |   24611    83506 |   10918    7727   367204    47.5 |  9.286 % |
c |    558978 |   24611    83506 |   12010    8064   374027    46.4 |  9.286 % |
c |    559485 |   24611    83506 |   13211    8571   390397    45.5 |  9.286 % |
c |    560245 |   24611    83506 |   14532    9331   411224    44.1 |  9.286 % |
c |    561384 |   24611    83506 |   15985   10470   451355    43.1 |  9.286 % |
c |    563093 |   24611    83506 |   17583   12179   555621    45.6 |  9.286 % |
c |    565655 |   24611    83506 |   19342   14741   639049    43.4 |  9.286 % |
c |    569500 |   24611    83506 |   21276   18586   781212    42.0 |  9.286 % |
c |    575266 |   24611    83506 |   23404   13076   496567    38.0 |  9.286 % |
c |    583917 |   24611    83506 |   25744   21727   836747    38.5 |  9.286 % |
c |    596891 |   24611    83506 |   28318   21220   824464    38.9 |  9.286 % |
c |    616352 |   24611    83506 |   31150   24464  1080641    44.2 |  9.286 % |
c |    645545 |   24611    83506 |   34265   15444   790113    51.2 |  9.286 % |
c |    689337 |   24611    83506 |   37692   15693   616696    39.3 |  9.286 % |
c |    755022 |   24611    83506 |   41461   30159  3542491   117.5 |  9.286 % |
c |    853548 |   24611    83506 |   45608   18346   925859    50.5 |  9.286 % |

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/5665/stat): 5665 (minisat+_script) R 5664 5665 19818 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1855904970 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/5665/statm): 174 3 169 147 0 27 0
[pid=5665] 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=5666
New process pid=5667
New process pid=5668
execve syscall for /bin/sed executable
One traced child (pid=5667) 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=5668) exited with status: 0
One traced child (pid=5666) exited with status: 0
New process pid=5669
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-13-7-markshare1_1.opb

[startup+10.0034 s]
Raw data (loadavg): 0.93 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 1335 0 0 0 978 7 0 0 25 0 1 0 1855904975 5943296 1322 4294967295 134512640 135094434 3221224432 3221222896 134780607 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 1451 1322 145 145 0 1306 0
[pid=5669] vsize: 5804
Current children cumulated CPU time (s) 9.85
Current children cumulated vsize (Kb) 7928

[startup+20.0052 s]
Raw data (loadavg): 0.94 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 1758 0 0 0 1969 10 0 0 25 0 1 0 1855904975 7708672 1745 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 1882 1745 145 145 0 1737 0
[pid=5669] vsize: 7528
Current children cumulated CPU time (s) 19.79
Current children cumulated vsize (Kb) 9652

[startup+30.006 s]
Raw data (loadavg): 0.95 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 1901 0 0 0 2965 12 0 0 25 0 1 0 1855904975 8286208 1888 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5669/statm): 2023 1888 145 145 0 1878 0
[pid=5669] vsize: 8092
Current children cumulated CPU time (s) 29.77
Current children cumulated vsize (Kb) 10216

[startup+40.0067 s]
Raw data (loadavg): 0.95 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 2290 0 0 0 3958 16 0 0 25 0 1 0 1855904975 9863168 2277 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 2408 2277 145 145 0 2263 0
[pid=5669] vsize: 9632
Current children cumulated CPU time (s) 39.74
Current children cumulated vsize (Kb) 11756

[startup+50.0075 s]
Raw data (loadavg): 0.96 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 2408 0 0 0 4956 16 0 0 25 0 1 0 1855904975 10346496 2395 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 2526 2395 145 145 0 2381 0
[pid=5669] vsize: 10104
Current children cumulated CPU time (s) 49.72
Current children cumulated vsize (Kb) 12228

[startup+60.0073 s]
Raw data (loadavg): 0.97 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 2597 0 0 0 5953 17 0 0 25 0 1 0 1855904975 11145216 2584 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 2721 2584 145 145 0 2576 0
[pid=5669] vsize: 10884
Current children cumulated CPU time (s) 59.7
Current children cumulated vsize (Kb) 13008

[startup+70.0081 s]
Raw data (loadavg): 0.97 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 2601 0 0 0 6954 18 0 0 25 0 1 0 1855904975 11145216 2588 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 2721 2588 145 145 0 2576 0
[pid=5669] vsize: 10884
Current children cumulated CPU time (s) 69.72
Current children cumulated vsize (Kb) 13008

[startup+80.0089 s]
Raw data (loadavg): 0.98 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 2634 0 0 0 7954 18 0 0 25 0 1 0 1855904975 11407360 2621 4294967295 134512640 135094434 3221224432 3221223024 134557416 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 2785 2621 145 145 0 2640 0
[pid=5669] vsize: 11140
Current children cumulated CPU time (s) 79.72
Current children cumulated vsize (Kb) 13264

[startup+90.0086 s]
Raw data (loadavg): 0.98 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 2917 0 0 0 8948 20 0 0 25 0 1 0 1855904975 12554240 2904 4294967295 134512640 135094434 3221224432 3221223088 134558029 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 3065 2904 145 145 0 2920 0
[pid=5669] vsize: 12260
Current children cumulated CPU time (s) 89.68
Current children cumulated vsize (Kb) 14384

[startup+100.009 s]
Raw data (loadavg): 0.98 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 3203 0 0 0 9944 22 0 0 25 0 1 0 1855904975 13713408 3190 4294967295 134512640 135094434 3221224432 3221223088 134557978 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 3348 3190 145 145 0 3203 0
[pid=5669] vsize: 13392
Current children cumulated CPU time (s) 99.66
Current children cumulated vsize (Kb) 15516

[startup+110.01 s]
Raw data (loadavg): 0.98 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 3203 0 0 0 10944 22 0 0 25 0 1 0 1855904975 13713408 3190 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 3348 3190 145 145 0 3203 0
[pid=5669] vsize: 13392
Current children cumulated CPU time (s) 109.66
Current children cumulated vsize (Kb) 15516

[startup+120.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 3467 0 0 0 11940 24 0 0 25 0 1 0 1855904975 14794752 3454 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 3612 3454 145 145 0 3467 0
[pid=5669] vsize: 14448
Current children cumulated CPU time (s) 119.64
Current children cumulated vsize (Kb) 16572

[startup+130.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 3842 0 0 0 12935 26 0 0 25 0 1 0 1855904975 16334848 3829 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 3988 3829 145 145 0 3843 0
[pid=5669] vsize: 15952
Current children cumulated CPU time (s) 129.61
Current children cumulated vsize (Kb) 18076

[startup+140.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 3842 0 0 0 13935 26 0 0 25 0 1 0 1855904975 16334848 3829 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 3988 3829 145 145 0 3843 0
[pid=5669] vsize: 15952
Current children cumulated CPU time (s) 139.61
Current children cumulated vsize (Kb) 18076

[startup+150.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 3842 0 0 0 14935 26 0 0 25 0 1 0 1855904975 16334848 3829 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 3988 3829 145 145 0 3843 0
[pid=5669] vsize: 15952
Current children cumulated CPU time (s) 149.61
Current children cumulated vsize (Kb) 18076

[startup+160.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 3874 0 0 0 15935 26 0 0 25 0 1 0 1855904975 16453632 3861 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 4017 3861 145 145 0 3872 0
[pid=5669] vsize: 16068
Current children cumulated CPU time (s) 159.61
Current children cumulated vsize (Kb) 18192

[startup+170.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 3882 0 0 0 16934 27 0 0 25 0 1 0 1855904975 16486400 3869 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5669/statm): 4025 3869 145 145 0 3880 0
[pid=5669] vsize: 16100
Current children cumulated CPU time (s) 169.61
Current children cumulated vsize (Kb) 18224

[startup+180.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 3882 0 0 0 17933 28 0 0 25 0 1 0 1855904975 16486400 3869 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5669/statm): 4025 3869 145 145 0 3880 0
[pid=5669] vsize: 16100
Current children cumulated CPU time (s) 179.61
Current children cumulated vsize (Kb) 18224

[startup+190.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 3882 0 0 0 18933 28 0 0 25 0 1 0 1855904975 16486400 3869 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 4025 3869 145 145 0 3880 0
[pid=5669] vsize: 16100
Current children cumulated CPU time (s) 189.61
Current children cumulated vsize (Kb) 18224

[startup+200.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 3882 0 0 0 19933 28 0 0 25 0 1 0 1855904975 16486400 3869 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 4025 3869 145 145 0 3880 0
[pid=5669] vsize: 16100
Current children cumulated CPU time (s) 199.61
Current children cumulated vsize (Kb) 18224

[startup+210.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 3882 0 0 0 20933 28 0 0 25 0 1 0 1855904975 16486400 3869 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 4025 3869 145 145 0 3880 0
[pid=5669] vsize: 16100
Current children cumulated CPU time (s) 209.61
Current children cumulated vsize (Kb) 18224

[startup+220.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 3882 0 0 0 21933 28 0 0 25 0 1 0 1855904975 16486400 3869 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 4025 3869 145 145 0 3880 0
[pid=5669] vsize: 16100
Current children cumulated CPU time (s) 219.61
Current children cumulated vsize (Kb) 18224

[startup+230.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 3882 0 0 0 22933 28 0 0 25 0 1 0 1855904975 16486400 3869 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 4025 3869 145 145 0 3880 0
[pid=5669] vsize: 16100
Current children cumulated CPU time (s) 229.61
Current children cumulated vsize (Kb) 18224

[startup+240.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 3882 0 0 0 23933 28 0 0 25 0 1 0 1855904975 16486400 3869 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 4025 3869 145 145 0 3880 0
[pid=5669] vsize: 16100
Current children cumulated CPU time (s) 239.61
Current children cumulated vsize (Kb) 18224

[startup+250.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 3882 0 0 0 24934 28 0 0 25 0 1 0 1855904975 16486400 3869 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 4025 3869 145 145 0 3880 0
[pid=5669] vsize: 16100
Current children cumulated CPU time (s) 249.62
Current children cumulated vsize (Kb) 18224

[startup+260.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 3946 0 0 0 25933 28 0 0 25 0 1 0 1855904975 16748544 3933 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 4089 3933 145 145 0 3944 0
[pid=5669] vsize: 16356
Current children cumulated CPU time (s) 259.61
Current children cumulated vsize (Kb) 18480

[startup+270.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4210 0 0 0 26928 29 0 0 25 0 1 0 1855904975 17829888 4197 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 4353 4197 145 145 0 4208 0
[pid=5669] vsize: 17412
Current children cumulated CPU time (s) 269.57
Current children cumulated vsize (Kb) 19536

[startup+280.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4210 0 0 0 27929 29 0 0 25 0 1 0 1855904975 17829888 4197 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 4353 4197 145 145 0 4208 0
[pid=5669] vsize: 17412
Current children cumulated CPU time (s) 279.58
Current children cumulated vsize (Kb) 19536

[startup+290.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4210 0 0 0 28929 29 0 0 25 0 1 0 1855904975 17829888 4197 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 4353 4197 145 145 0 4208 0
[pid=5669] vsize: 17412
Current children cumulated CPU time (s) 289.58
Current children cumulated vsize (Kb) 19536

[startup+300.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4210 0 0 0 29929 29 0 0 25 0 1 0 1855904975 17829888 4197 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 4353 4197 145 145 0 4208 0
[pid=5669] vsize: 17412
Current children cumulated CPU time (s) 299.58
Current children cumulated vsize (Kb) 19536

[startup+310.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4210 0 0 0 30929 29 0 0 25 0 1 0 1855904975 17829888 4197 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 4353 4197 145 145 0 4208 0
[pid=5669] vsize: 17412
Current children cumulated CPU time (s) 309.58
Current children cumulated vsize (Kb) 19536

[startup+320.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4210 0 0 0 31930 29 0 0 25 0 1 0 1855904975 17829888 4197 4294967295 134512640 135094434 3221224432 3221223104 134556257 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 4353 4197 145 145 0 4208 0
[pid=5669] vsize: 17412
Current children cumulated CPU time (s) 319.59
Current children cumulated vsize (Kb) 19536

[startup+330.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4210 0 0 0 32930 29 0 0 25 0 1 0 1855904975 17829888 4197 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 4353 4197 145 145 0 4208 0
[pid=5669] vsize: 17412
Current children cumulated CPU time (s) 329.59
Current children cumulated vsize (Kb) 19536

[startup+340.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4210 0 0 0 33930 29 0 0 25 0 1 0 1855904975 17829888 4197 4294967295 134512640 135094434 3221224432 3221223120 134554676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 4353 4197 145 145 0 4208 0
[pid=5669] vsize: 17412
Current children cumulated CPU time (s) 339.59
Current children cumulated vsize (Kb) 19536

[startup+350.026 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4210 0 0 0 34930 29 0 0 25 0 1 0 1855904975 17829888 4197 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 4353 4197 145 145 0 4208 0
[pid=5669] vsize: 17412
Current children cumulated CPU time (s) 349.59
Current children cumulated vsize (Kb) 19536

[startup+360.027 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4210 0 0 0 35930 29 0 0 25 0 1 0 1855904975 17829888 4197 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 4353 4197 145 145 0 4208 0
[pid=5669] vsize: 17412
Current children cumulated CPU time (s) 359.59
Current children cumulated vsize (Kb) 19536

[startup+370.028 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4210 0 0 0 36931 29 0 0 25 0 1 0 1855904975 17829888 4197 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 4353 4197 145 145 0 4208 0
[pid=5669] vsize: 17412
Current children cumulated CPU time (s) 369.6
Current children cumulated vsize (Kb) 19536

[startup+380.028 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4210 0 0 0 37931 29 0 0 25 0 1 0 1855904975 17829888 4197 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 4353 4197 145 145 0 4208 0
[pid=5669] vsize: 17412
Current children cumulated CPU time (s) 379.6
Current children cumulated vsize (Kb) 19536

[startup+390.028 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4210 0 0 0 38931 29 0 0 25 0 1 0 1855904975 17829888 4197 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 4353 4197 145 145 0 4208 0
[pid=5669] vsize: 17412
Current children cumulated CPU time (s) 389.6
Current children cumulated vsize (Kb) 19536

[startup+400.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4211 0 0 0 39931 29 0 0 25 0 1 0 1855904975 17829888 4198 4294967295 134512640 135094434 3221224432 3221223024 134556776 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 4353 4198 145 145 0 4208 0
[pid=5669] vsize: 17412
Current children cumulated CPU time (s) 399.6
Current children cumulated vsize (Kb) 19536

[startup+410.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4211 0 0 0 40931 30 0 0 25 0 1 0 1855904975 17829888 4198 4294967295 134512640 135094434 3221224432 3221223088 134557956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 4353 4198 145 145 0 4208 0
[pid=5669] vsize: 17412
Current children cumulated CPU time (s) 409.61
Current children cumulated vsize (Kb) 19536

[startup+420.031 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4211 0 0 0 41932 30 0 0 25 0 1 0 1855904975 17829888 4198 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 4353 4198 145 145 0 4208 0
[pid=5669] vsize: 17412
Current children cumulated CPU time (s) 419.62
Current children cumulated vsize (Kb) 19536

[startup+430.031 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4211 0 0 0 42932 30 0 0 25 0 1 0 1855904975 17829888 4198 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 4353 4198 145 145 0 4208 0
[pid=5669] vsize: 17412
Current children cumulated CPU time (s) 429.62
Current children cumulated vsize (Kb) 19536

[startup+440.032 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4211 0 0 0 43932 30 0 0 25 0 1 0 1855904975 17829888 4198 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 4353 4198 145 145 0 4208 0
[pid=5669] vsize: 17412
Current children cumulated CPU time (s) 439.62
Current children cumulated vsize (Kb) 19536

[startup+450.033 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4211 0 0 0 44932 30 0 0 25 0 1 0 1855904975 17829888 4198 4294967295 134512640 135094434 3221224432 3221223088 134557987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 4353 4198 145 145 0 4208 0
[pid=5669] vsize: 17412
Current children cumulated CPU time (s) 449.62
Current children cumulated vsize (Kb) 19536

[startup+460.034 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4211 0 0 0 45933 30 0 0 25 0 1 0 1855904975 17829888 4198 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 4353 4198 145 145 0 4208 0
[pid=5669] vsize: 17412
Current children cumulated CPU time (s) 459.63
Current children cumulated vsize (Kb) 19536

[startup+470.034 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4211 0 0 0 46933 30 0 0 25 0 1 0 1855904975 17829888 4198 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 4353 4198 145 145 0 4208 0
[pid=5669] vsize: 17412
Current children cumulated CPU time (s) 469.63
Current children cumulated vsize (Kb) 19536

[startup+480.035 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4211 0 0 0 47933 30 0 0 25 0 1 0 1855904975 17829888 4198 4294967295 134512640 135094434 3221224432 3221223024 134557531 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 4353 4198 145 145 0 4208 0
[pid=5669] vsize: 17412
Current children cumulated CPU time (s) 479.63
Current children cumulated vsize (Kb) 19536

[startup+490.035 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4211 0 0 0 48933 30 0 0 25 0 1 0 1855904975 17829888 4198 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 4353 4198 145 145 0 4208 0
[pid=5669] vsize: 17412
Current children cumulated CPU time (s) 489.63
Current children cumulated vsize (Kb) 19536

[startup+500.037 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4211 0 0 0 49934 30 0 0 25 0 1 0 1855904975 17829888 4198 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 4353 4198 145 145 0 4208 0
[pid=5669] vsize: 17412
Current children cumulated CPU time (s) 499.64
Current children cumulated vsize (Kb) 19536

[startup+510.038 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4211 0 0 0 50934 30 0 0 25 0 1 0 1855904975 17829888 4198 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 4353 4198 145 145 0 4208 0
[pid=5669] vsize: 17412
Current children cumulated CPU time (s) 509.64
Current children cumulated vsize (Kb) 19536

[startup+520.038 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4211 0 0 0 51934 30 0 0 25 0 1 0 1855904975 17829888 4198 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 4353 4198 145 145 0 4208 0
[pid=5669] vsize: 17412
Current children cumulated CPU time (s) 519.64
Current children cumulated vsize (Kb) 19536

[startup+530.039 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4211 0 0 0 52934 30 0 0 25 0 1 0 1855904975 17829888 4198 4294967295 134512640 135094434 3221224432 3221223024 134551702 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 4353 4198 145 145 0 4208 0
[pid=5669] vsize: 17412
Current children cumulated CPU time (s) 529.64
Current children cumulated vsize (Kb) 19536

[startup+540.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4211 0 0 0 53934 30 0 0 25 0 1 0 1855904975 17829888 4198 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 4353 4198 145 145 0 4208 0
[pid=5669] vsize: 17412
Current children cumulated CPU time (s) 539.64
Current children cumulated vsize (Kb) 19536

[startup+550.041 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4211 0 0 0 54935 30 0 0 25 0 1 0 1855904975 17829888 4198 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 4353 4198 145 145 0 4208 0
[pid=5669] vsize: 17412
Current children cumulated CPU time (s) 549.65
Current children cumulated vsize (Kb) 19536

[startup+560.042 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4211 0 0 0 55935 30 0 0 25 0 1 0 1855904975 17829888 4198 4294967295 134512640 135094434 3221224432 3221223088 134557879 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 4353 4198 145 145 0 4208 0
[pid=5669] vsize: 17412
Current children cumulated CPU time (s) 559.65
Current children cumulated vsize (Kb) 19536

[startup+570.043 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4211 0 0 0 56935 30 0 0 25 0 1 0 1855904975 17829888 4198 4294967295 134512640 135094434 3221224432 3221223056 134557612 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 4353 4198 145 145 0 4208 0
[pid=5669] vsize: 17412
Current children cumulated CPU time (s) 569.65
Current children cumulated vsize (Kb) 19536

[startup+580.044 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4211 0 0 0 57936 30 0 0 25 0 1 0 1855904975 17829888 4198 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 4353 4198 145 145 0 4208 0
[pid=5669] vsize: 17412
Current children cumulated CPU time (s) 579.66
Current children cumulated vsize (Kb) 19536

[startup+590.045 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4211 0 0 0 58936 30 0 0 25 0 1 0 1855904975 17829888 4198 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 4353 4198 145 145 0 4208 0
[pid=5669] vsize: 17412
Current children cumulated CPU time (s) 589.66
Current children cumulated vsize (Kb) 19536

[startup+600.047 s]
Raw data (loadavg): 0.99 0.97 0.92 1/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) T 5665 5665 19818 0 -1 0 4714 0 0 0 59927 33 0 0 25 0 1 0 1855904975 19914752 4701 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/5669/statm): 4862 4701 145 145 0 4717 0
[pid=5669] vsize: 19448
Current children cumulated CPU time (s) 599.6
Current children cumulated vsize (Kb) 21572

[startup+610.048 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4884 0 0 0 60924 34 0 0 25 0 1 0 1855904975 20611072 4871 4294967295 134512640 135094434 3221224432 3221223104 134556288 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 5032 4871 145 145 0 4887 0
[pid=5669] vsize: 20128
Current children cumulated CPU time (s) 609.58
Current children cumulated vsize (Kb) 22252

[startup+620.049 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4884 0 0 0 61924 34 0 0 25 0 1 0 1855904975 20611072 4871 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 5032 4871 145 145 0 4887 0
[pid=5669] vsize: 20128
Current children cumulated CPU time (s) 619.58
Current children cumulated vsize (Kb) 22252

[startup+630.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4884 0 0 0 62924 34 0 0 25 0 1 0 1855904975 20611072 4871 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 5032 4871 145 145 0 4887 0
[pid=5669] vsize: 20128
Current children cumulated CPU time (s) 629.58
Current children cumulated vsize (Kb) 22252

[startup+640.051 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4884 0 0 0 63925 34 0 0 25 0 1 0 1855904975 20611072 4871 4294967295 134512640 135094434 3221224432 3221223088 134558238 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 5032 4871 145 145 0 4887 0
[pid=5669] vsize: 20128
Current children cumulated CPU time (s) 639.59
Current children cumulated vsize (Kb) 22252

[startup+650.052 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4884 0 0 0 64925 34 0 0 25 0 1 0 1855904975 20611072 4871 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 5032 4871 145 145 0 4887 0
[pid=5669] vsize: 20128
Current children cumulated CPU time (s) 649.59
Current children cumulated vsize (Kb) 22252

[startup+660.052 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4884 0 0 0 65924 35 0 0 25 0 1 0 1855904975 20611072 4871 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5669/statm): 5032 4871 145 145 0 4887 0
[pid=5669] vsize: 20128
Current children cumulated CPU time (s) 659.59
Current children cumulated vsize (Kb) 22252

[startup+670.054 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4884 0 0 0 66924 35 0 0 25 0 1 0 1855904975 20611072 4871 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 5032 4871 145 145 0 4887 0
[pid=5669] vsize: 20128
Current children cumulated CPU time (s) 669.59
Current children cumulated vsize (Kb) 22252

[startup+680.055 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4884 0 0 0 67924 35 0 0 25 0 1 0 1855904975 20611072 4871 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 5032 4871 145 145 0 4887 0
[pid=5669] vsize: 20128
Current children cumulated CPU time (s) 679.59
Current children cumulated vsize (Kb) 22252

[startup+690.055 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4884 0 0 0 68924 35 0 0 25 0 1 0 1855904975 20611072 4871 4294967295 134512640 135094434 3221224432 3221223088 134557920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 5032 4871 145 145 0 4887 0
[pid=5669] vsize: 20128
Current children cumulated CPU time (s) 689.59
Current children cumulated vsize (Kb) 22252

[startup+700.056 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4884 0 0 0 69924 35 0 0 25 0 1 0 1855904975 20611072 4871 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 5032 4871 145 145 0 4887 0
[pid=5669] vsize: 20128
Current children cumulated CPU time (s) 699.59
Current children cumulated vsize (Kb) 22252

[startup+710.056 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4884 0 0 0 70925 35 0 0 25 0 1 0 1855904975 20611072 4871 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 5032 4871 145 145 0 4887 0
[pid=5669] vsize: 20128
Current children cumulated CPU time (s) 709.6
Current children cumulated vsize (Kb) 22252

[startup+720.057 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4884 0 0 0 71925 35 0 0 25 0 1 0 1855904975 20611072 4871 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 5032 4871 145 145 0 4887 0
[pid=5669] vsize: 20128
Current children cumulated CPU time (s) 719.6
Current children cumulated vsize (Kb) 22252

[startup+730.058 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4884 0 0 0 72925 35 0 0 25 0 1 0 1855904975 20611072 4871 4294967295 134512640 135094434 3221224432 3221223120 134554687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 5032 4871 145 145 0 4887 0
[pid=5669] vsize: 20128
Current children cumulated CPU time (s) 729.6
Current children cumulated vsize (Kb) 22252

[startup+740.059 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4884 0 0 0 73925 35 0 0 25 0 1 0 1855904975 20611072 4871 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 5032 4871 145 145 0 4887 0
[pid=5669] vsize: 20128
Current children cumulated CPU time (s) 739.6
Current children cumulated vsize (Kb) 22252

[startup+750.059 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4884 0 0 0 74926 35 0 0 25 0 1 0 1855904975 20611072 4871 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 5032 4871 145 145 0 4887 0
[pid=5669] vsize: 20128
Current children cumulated CPU time (s) 749.61
Current children cumulated vsize (Kb) 22252

[startup+760.06 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4884 0 0 0 75926 35 0 0 25 0 1 0 1855904975 20611072 4871 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 5032 4871 145 145 0 4887 0
[pid=5669] vsize: 20128
Current children cumulated CPU time (s) 759.61
Current children cumulated vsize (Kb) 22252

[startup+770.062 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4884 0 0 0 76926 35 0 0 25 0 1 0 1855904975 20611072 4871 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 5032 4871 145 145 0 4887 0
[pid=5669] vsize: 20128
Current children cumulated CPU time (s) 769.61
Current children cumulated vsize (Kb) 22252

[startup+780.063 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4884 0 0 0 77926 35 0 0 25 0 1 0 1855904975 20611072 4871 4294967295 134512640 135094434 3221224432 3221223024 134557208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 5032 4871 145 145 0 4887 0
[pid=5669] vsize: 20128
Current children cumulated CPU time (s) 779.61
Current children cumulated vsize (Kb) 22252

[startup+790.063 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4884 0 0 0 78927 35 0 0 25 0 1 0 1855904975 20611072 4871 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 5032 4871 145 145 0 4887 0
[pid=5669] vsize: 20128
Current children cumulated CPU time (s) 789.62
Current children cumulated vsize (Kb) 22252

[startup+800.064 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4884 0 0 0 79927 35 0 0 25 0 1 0 1855904975 20611072 4871 4294967295 134512640 135094434 3221224432 3221223120 134554715 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 5032 4871 145 145 0 4887 0
[pid=5669] vsize: 20128
Current children cumulated CPU time (s) 799.62
Current children cumulated vsize (Kb) 22252

[startup+810.065 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4884 0 0 0 80927 35 0 0 25 0 1 0 1855904975 20611072 4871 4294967295 134512640 135094434 3221224432 3221223104 134556073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 5032 4871 145 145 0 4887 0
[pid=5669] vsize: 20128
Current children cumulated CPU time (s) 809.62
Current children cumulated vsize (Kb) 22252

[startup+820.066 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4884 0 0 0 81928 35 0 0 25 0 1 0 1855904975 20611072 4871 4294967295 134512640 135094434 3221224432 3221223072 134558264 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 5032 4871 145 145 0 4887 0
[pid=5669] vsize: 20128
Current children cumulated CPU time (s) 819.63
Current children cumulated vsize (Kb) 22252

[startup+830.067 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4884 0 0 0 82928 35 0 0 25 0 1 0 1855904975 20611072 4871 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 5032 4871 145 145 0 4887 0
[pid=5669] vsize: 20128
Current children cumulated CPU time (s) 829.63
Current children cumulated vsize (Kb) 22252

[startup+840.067 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 4884 0 0 0 83928 35 0 0 25 0 1 0 1855904975 20611072 4871 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 5032 4871 145 145 0 4887 0
[pid=5669] vsize: 20128
Current children cumulated CPU time (s) 839.63
Current children cumulated vsize (Kb) 22252

[startup+850.068 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 5255 0 0 0 84922 37 0 0 25 0 1 0 1855904975 22130688 5242 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 5403 5242 145 145 0 5258 0
[pid=5669] vsize: 21612
Current children cumulated CPU time (s) 849.59
Current children cumulated vsize (Kb) 23736

[startup+860.069 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 5674 0 0 0 85915 40 0 0 25 0 1 0 1855904975 23871488 5661 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 5828 5661 145 145 0 5683 0
[pid=5669] vsize: 23312
Current children cumulated CPU time (s) 859.55
Current children cumulated vsize (Kb) 25436

[startup+870.071 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 5874 0 0 0 86911 41 0 0 25 0 1 0 1855904975 24690688 5861 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 6028 5861 145 145 0 5883 0
[pid=5669] vsize: 24112
Current children cumulated CPU time (s) 869.52
Current children cumulated vsize (Kb) 26236

[startup+880.072 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 5874 0 0 0 87912 41 0 0 25 0 1 0 1855904975 24690688 5861 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 6028 5861 145 145 0 5883 0
[pid=5669] vsize: 24112
Current children cumulated CPU time (s) 879.53
Current children cumulated vsize (Kb) 26236

[startup+890.072 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 5874 0 0 0 88912 41 0 0 25 0 1 0 1855904975 24690688 5861 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 6028 5861 145 145 0 5883 0
[pid=5669] vsize: 24112
Current children cumulated CPU time (s) 889.53
Current children cumulated vsize (Kb) 26236

[startup+900.073 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 5874 0 0 0 89912 41 0 0 25 0 1 0 1855904975 24690688 5861 4294967295 134512640 135094434 3221224432 3221223024 134557037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 6028 5861 145 145 0 5883 0
[pid=5669] vsize: 24112
Current children cumulated CPU time (s) 899.53
Current children cumulated vsize (Kb) 26236

[startup+910.074 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 6087 0 0 0 90908 43 0 0 25 0 1 0 1855904975 25567232 6074 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5669/statm): 6242 6074 145 145 0 6097 0
[pid=5669] vsize: 24968
Current children cumulated CPU time (s) 909.51
Current children cumulated vsize (Kb) 27092

[startup+920.076 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 6429 0 0 0 91900 46 0 0 25 0 1 0 1855904975 26968064 6416 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 6584 6416 145 145 0 6439 0
[pid=5669] vsize: 26336
Current children cumulated CPU time (s) 919.46
Current children cumulated vsize (Kb) 28460

[startup+930.077 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 6778 0 0 0 92893 49 0 0 25 0 1 0 1855904975 28393472 6765 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 6932 6765 145 145 0 6787 0
[pid=5669] vsize: 27728
Current children cumulated CPU time (s) 929.42
Current children cumulated vsize (Kb) 29852

[startup+940.077 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 6826 0 0 0 93893 50 0 0 25 0 1 0 1855904975 28585984 6813 4294967295 134512640 135094434 3221224432 3221223088 134550369 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 6979 6813 145 145 0 6834 0
[pid=5669] vsize: 27916
Current children cumulated CPU time (s) 939.43
Current children cumulated vsize (Kb) 30040

[startup+950.078 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 6826 0 0 0 94893 50 0 0 25 0 1 0 1855904975 28585984 6813 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 6979 6813 145 145 0 6834 0
[pid=5669] vsize: 27916
Current children cumulated CPU time (s) 949.43
Current children cumulated vsize (Kb) 30040

[startup+960.079 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 6826 0 0 0 95893 50 0 0 25 0 1 0 1855904975 28585984 6813 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 6979 6813 145 145 0 6834 0
[pid=5669] vsize: 27916
Current children cumulated CPU time (s) 959.43
Current children cumulated vsize (Kb) 30040

[startup+970.08 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 6826 0 0 0 96893 50 0 0 25 0 1 0 1855904975 28585984 6813 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 6979 6813 145 145 0 6834 0
[pid=5669] vsize: 27916
Current children cumulated CPU time (s) 969.43
Current children cumulated vsize (Kb) 30040

[startup+980.082 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 6826 0 0 0 97894 50 0 0 25 0 1 0 1855904975 28585984 6813 4294967295 134512640 135094434 3221224432 3221223104 134556252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 6979 6813 145 145 0 6834 0
[pid=5669] vsize: 27916
Current children cumulated CPU time (s) 979.44
Current children cumulated vsize (Kb) 30040

[startup+990.081 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 6826 0 0 0 98894 50 0 0 25 0 1 0 1855904975 28585984 6813 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 6979 6813 145 145 0 6834 0
[pid=5669] vsize: 27916
Current children cumulated CPU time (s) 989.44
Current children cumulated vsize (Kb) 30040

[startup+1000.08 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 6826 0 0 0 99894 50 0 0 25 0 1 0 1855904975 28585984 6813 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 6979 6813 145 145 0 6834 0
[pid=5669] vsize: 27916
Current children cumulated CPU time (s) 999.44
Current children cumulated vsize (Kb) 30040

[startup+1010.08 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 6826 0 0 0 100894 50 0 0 25 0 1 0 1855904975 28585984 6813 4294967295 134512640 135094434 3221224432 3221223088 134558181 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 6979 6813 145 145 0 6834 0
[pid=5669] vsize: 27916
Current children cumulated CPU time (s) 1009.44
Current children cumulated vsize (Kb) 30040

[startup+1020.08 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 6826 0 0 0 101895 50 0 0 25 0 1 0 1855904975 28585984 6813 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 6979 6813 145 145 0 6834 0
[pid=5669] vsize: 27916
Current children cumulated CPU time (s) 1019.45
Current children cumulated vsize (Kb) 30040

[startup+1030.08 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 6826 0 0 0 102895 50 0 0 25 0 1 0 1855904975 28585984 6813 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 6979 6813 145 145 0 6834 0
[pid=5669] vsize: 27916
Current children cumulated CPU time (s) 1029.45
Current children cumulated vsize (Kb) 30040

[startup+1040.09 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 6826 0 0 0 103894 50 0 0 25 0 1 0 1855904975 28585984 6813 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 6979 6813 145 145 0 6834 0
[pid=5669] vsize: 27916
Current children cumulated CPU time (s) 1039.44
Current children cumulated vsize (Kb) 30040

[startup+1050.09 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 6826 0 0 0 104895 50 0 0 25 0 1 0 1855904975 28585984 6813 4294967295 134512640 135094434 3221224432 3221223104 134555579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 6979 6813 145 145 0 6834 0
[pid=5669] vsize: 27916
Current children cumulated CPU time (s) 1049.45
Current children cumulated vsize (Kb) 30040

[startup+1060.09 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 6826 0 0 0 105895 50 0 0 25 0 1 0 1855904975 28585984 6813 4294967295 134512640 135094434 3221224432 3221223056 134557585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 6979 6813 145 145 0 6834 0
[pid=5669] vsize: 27916
Current children cumulated CPU time (s) 1059.45
Current children cumulated vsize (Kb) 30040

[startup+1070.09 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 6827 0 0 0 106895 50 0 0 25 0 1 0 1855904975 28585984 6814 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 6979 6814 145 145 0 6834 0
[pid=5669] vsize: 27916
Current children cumulated CPU time (s) 1069.45
Current children cumulated vsize (Kb) 30040

[startup+1080.09 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 6829 0 0 0 107895 50 0 0 25 0 1 0 1855904975 28585984 6816 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 6979 6816 145 145 0 6834 0
[pid=5669] vsize: 27916
Current children cumulated CPU time (s) 1079.45
Current children cumulated vsize (Kb) 30040

[startup+1090.09 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 6829 0 0 0 108896 50 0 0 25 0 1 0 1855904975 28585984 6816 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 6979 6816 145 145 0 6834 0
[pid=5669] vsize: 27916
Current children cumulated CPU time (s) 1089.46
Current children cumulated vsize (Kb) 30040

[startup+1100.09 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 6829 0 0 0 109896 50 0 0 25 0 1 0 1855904975 28585984 6816 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 6979 6816 145 145 0 6834 0
[pid=5669] vsize: 27916
Current children cumulated CPU time (s) 1099.46
Current children cumulated vsize (Kb) 30040

[startup+1110.09 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 6829 0 0 0 110896 50 0 0 25 0 1 0 1855904975 28585984 6816 4294967295 134512640 135094434 3221224432 3221223088 134557813 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 6979 6816 145 145 0 6834 0
[pid=5669] vsize: 27916
Current children cumulated CPU time (s) 1109.46
Current children cumulated vsize (Kb) 30040

[startup+1120.09 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 6829 0 0 0 111896 50 0 0 25 0 1 0 1855904975 28585984 6816 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 6979 6816 145 145 0 6834 0
[pid=5669] vsize: 27916
Current children cumulated CPU time (s) 1119.46
Current children cumulated vsize (Kb) 30040

[startup+1130.09 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 6829 0 0 0 112897 50 0 0 25 0 1 0 1855904975 28585984 6816 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 6979 6816 145 145 0 6834 0
[pid=5669] vsize: 27916
Current children cumulated CPU time (s) 1129.47
Current children cumulated vsize (Kb) 30040

[startup+1140.09 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 6829 0 0 0 113897 50 0 0 25 0 1 0 1855904975 28585984 6816 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 6979 6816 145 145 0 6834 0
[pid=5669] vsize: 27916
Current children cumulated CPU time (s) 1139.47
Current children cumulated vsize (Kb) 30040

[startup+1150.09 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 6829 0 0 0 114897 50 0 0 25 0 1 0 1855904975 28585984 6816 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 6979 6816 145 145 0 6834 0
[pid=5669] vsize: 27916
Current children cumulated CPU time (s) 1149.47
Current children cumulated vsize (Kb) 30040

[startup+1160.09 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 6829 0 0 0 115897 50 0 0 25 0 1 0 1855904975 28585984 6816 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 6979 6816 145 145 0 6834 0
[pid=5669] vsize: 27916
Current children cumulated CPU time (s) 1159.47
Current children cumulated vsize (Kb) 30040

[startup+1170.1 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 6829 0 0 0 116898 50 0 0 25 0 1 0 1855904975 28585984 6816 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 6979 6816 145 145 0 6834 0
[pid=5669] vsize: 27916
Current children cumulated CPU time (s) 1169.48
Current children cumulated vsize (Kb) 30040

[startup+1180.1 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 6829 0 0 0 117898 50 0 0 25 0 1 0 1855904975 28585984 6816 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 6979 6816 145 145 0 6834 0
[pid=5669] vsize: 27916
Current children cumulated CPU time (s) 1179.48
Current children cumulated vsize (Kb) 30040

[startup+1190.1 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 6829 0 0 0 118898 50 0 0 25 0 1 0 1855904975 28585984 6816 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 6979 6816 145 145 0 6834 0
[pid=5669] vsize: 27916
Current children cumulated CPU time (s) 1189.48
Current children cumulated vsize (Kb) 30040

[startup+1200.1 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 6829 0 0 0 119898 50 0 0 25 0 1 0 1855904975 28585984 6816 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 6979 6816 145 145 0 6834 0
[pid=5669] vsize: 27916
Current children cumulated CPU time (s) 1199.48
Current children cumulated vsize (Kb) 30040

[startup+1210.1 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 6829 0 0 0 120899 50 0 0 25 0 1 0 1855904975 28585984 6816 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 6979 6816 145 145 0 6834 0
[pid=5669] vsize: 27916
Current children cumulated CPU time (s) 1209.49
Current children cumulated vsize (Kb) 30040



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.1 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 5669
Raw data (/proc/5665/stat): 5665 (minisat+_script) S 5664 5665 19818 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855904970 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5665/statm): 531 226 485 147 0 384 0
[pid=5665] vsize: 2124
Raw data (/proc/5669/stat): 5669 (minisat+_64-bit) R 5665 5665 19818 0 -1 0 6829 0 0 0 120899 50 0 0 25 0 1 0 1855904975 28585984 6816 4294967295 134512640 135094434 3221224432 3221222896 134780803 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5669/statm): 6979 6816 145 145 0 6834 0
[pid=5669] vsize: 27916
Current children cumulated CPU time (s) 1209.49
Current children cumulated vsize (Kb) 30040

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

Child status: 10
Real time (s): 1210.12
CPU time (s): 1209.51
CPU user time (s): 1208.99
CPU system time (s): 0.517921
CPU usage (%): 99.9499
Max. virtual memory (cumulated for all children) (Kb): 30040

Verifier Data

ERROR: no interpretation found !