Some explanations

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

General information on the benchmark

Nameweb/www.nlsde.buaa.edu.cn/~kexu/benchmarks/frb35-17-opb/normalized-frb35-17-5.opb
MD5SUM70070c820bc7d178cc8f33b42e0deead
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function -30
Optimality of the best value was proved NO
Number of terms in the objective function 595
Biggest coefficient in the objective function 1
Number of bits for the biggest coefficient in the objective function 1
Sum of the numbers in the objective function 595
Number of bits of the sum of numbers in the objective function 10
Biggest number in a constraint 1
Number of bits of the biggest number in a constraint 1
Biggest sum of numbers in a constraint 595
Number of bits of the biggest sum of numbers10
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1195.03
Number of variables595
Total number of constraints28143
Number of constraints which are clauses28143
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint2
Maximum length of a constraint2

Trace number 2287

Launcher Data

LAUNCH ON wulflinc28 THE 2005-09-18 18:42:46 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2693 boxname=wulflinc28 idbench=349 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  70070c820bc7d178cc8f33b42e0deead  /oldhome/oroussel/tmp/wulflinc28/normalized-frb35-17-5.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc28/normalized-frb35-17-5.opb
IDLAUNCH: 2693
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.077
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.077
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:        930284 kB
Buffers:         33892 kB
Cached:          42320 kB
SwapCached:        696 kB
Active:          61420 kB
Inactive:        17368 kB
HighTotal:      131008 kB
HighFree:        85064 kB
LowTotal:       903652 kB
LowFree:        845220 kB
SwapTotal:     2097640 kB
SwapFree:      2096372 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5812 kB
Slab:            19956 kB
Committed_AS:    64164 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-18 19:02:56 (client local time) WITH STATUS 10 IN 1209.6 SECONDS
stats: 2693 7 1209.6 10

Solver Data

c Parsing PB file...
c Converting 28143 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ...............................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   28143    56286 |    9381       0        0     nan |  0.000 % |
c ==============================================================================
c Found solution: -21
c ---[   0]---> Sorter-cost:26814     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   56290   122394 |   18763       0        0     nan |  0.000 % |
c |       100 |   55818   121416 |   20639      78      529     6.8 |  1.319 % |
c |       250 |   55350   120416 |   22703     201     1432     7.1 |  2.831 % |
c |       475 |   54323   118193 |   24973     376     3383     9.0 |  5.942 % |
c ==============================================================================
c Found solution: -26
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       678 |   53263   115977 |   17754     507     5021     9.9 |  5.942 % |
c |       778 |   52841   115047 |   19529     588     6229    10.6 | 11.045 % |
c |       928 |   52322   113884 |   21482     715     7585    10.6 | 12.707 % |
c |      1153 |   51428   111886 |   23630     895     9815    11.0 | 15.557 % |
c |      1490 |   49468   107434 |   25993    1105    12672    11.5 | 22.140 % |
c |      1996 |   47638   103232 |   28592    1527    18207    11.9 | 28.026 % |
c |      2756 |   44784    96705 |   31452    2088    27733    13.3 | 37.330 % |
c |      3895 |   41359    88683 |   34597    2945    40667    13.8 | 48.818 % |
c ==============================================================================
c Found solution: -27
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4578 |   40279    86235 |   13426    3372    48651    14.4 | 48.818 % |
c |      4678 |   39986    85593 |   14768    3439    49906    14.5 | 53.601 % |
c |      4828 |   39929    85464 |   16245    3585    53525    14.9 | 53.786 % |
c |      5053 |   39738    84989 |   17870    3769    58890    15.6 | 54.485 % |
c |      5390 |   39304    83962 |   19657    3970    63529    16.0 | 55.987 % |
c |      5897 |   38689    82488 |   21622    4286    73190    17.1 | 58.330 % |
c |      6656 |   37185    78940 |   23784    4674    86185    18.4 | 63.301 % |
c |      7795 |   36622    77561 |   26163    5675   129966    22.9 | 65.275 % |
c |      9504 |   35725    75401 |   28779    7136   192067    26.9 | 68.457 % |
c ==============================================================================
c Found solution: -28
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     10440 |   35152    73982 |   11717    7917   243425    30.7 | 68.457 % |
c |     10540 |   35113    73891 |   12888    7988   246532    30.9 | 70.655 % |
c |     10690 |   35113    73891 |   14177    8138   257579    31.7 | 70.655 % |
c |     10915 |   35077    73801 |   15595    8322   262608    31.6 | 70.789 % |
c |     11252 |   34978    73564 |   17154    8601   274225    31.9 | 71.134 % |
c ==============================================================================
c Found solution: -29
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11391 |   34971    73570 |   11657    8688   275965    31.8 | 71.134 % |
c |     11491 |   34902    73413 |   12822    8759   278380    31.8 | 71.445 % |
c |     11641 |   34902    73413 |   14104    8909   284047    31.9 | 71.446 % |
c |     11867 |   34896    73399 |   15515    9119   294059    32.2 | 71.466 % |
c |     12204 |   34763    73092 |   17067    9394   321190    34.2 | 71.903 % |
c |     12711 |   34609    72711 |   18773    9712   337264    34.7 | 72.472 % |
c |     13470 |   34605    72698 |   20651   10457   386838    37.0 | 72.487 % |
c |     14610 |   34380    72154 |   22716   11454   436165    38.1 | 73.293 % |
c |     16319 |   33765    70670 |   24987   12907   541843    42.0 | 75.434 % |
c ==============================================================================
c Found solution: -30
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     16658 |   33651    70365 |   11217   13078   538486    41.2 | 75.434 % |
c |     16758 |   33651    70365 |   12338   13178   543720    41.3 | 75.826 % |
c |     16908 |   33598    70240 |   13572   13315   549004    41.2 | 76.011 % |
c |     17133 |   33492    69992 |   14929   13474   555912    41.3 | 76.371 % |
c |     17471 |   33492    69992 |   16422   13812   572516    41.5 | 76.370 % |
c |     17978 |   33390    69747 |   18065   14288   590646    41.3 | 76.730 % |
c |     18737 |   33266    69453 |   19871   15005   645411    43.0 | 77.151 % |
c |     19876 |   33263    69446 |   21858   16138   775398    48.0 | 77.161 % |
c |     21586 |   33025    68873 |   24044   17787   883974    49.7 | 78.013 % |
c |     24149 |   33025    68873 |   26449   20350  1110021    54.5 | 78.013 % |
c |     27994 |   33025    68873 |   29094   24195  1446802    59.8 | 78.013 % |
c |     33762 |   32912    68606 |   32003   29913  1976061    66.1 | 78.408 % |
c |     42412 |   32688    68047 |   35203   38230  2602127    68.1 | 79.250 % |
c ==============================================================================
c Found solution: -31
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     54813 |   32709    68118 |   10903   50607  3631857    71.8 | 79.250 % |
c |     54913 |   32665    68010 |   11993   17614  1027595    58.3 | 79.420 % |
c |     55063 |   32665    68010 |   13192   17764  1033328    58.2 | 79.420 % |
c |     55288 |   32632    67926 |   14511   17973  1042889    58.0 | 79.537 % |
c |     55625 |   32632    67926 |   15963   18310  1077898    58.9 | 79.537 % |
c |     56133 |   32626    67909 |   17559   18796  1115938    59.4 | 79.563 % |
c |     56892 |   32626    67909 |   19315   19555  1163074    59.5 | 79.563 % |
c |     58031 |   32585    67812 |   21246   20688  1247141    60.3 | 79.706 % |
c |     59739 |   32585    67812 |   23371   22396  1358285    60.6 | 79.706 % |
c ==============================================================================
c Found solution: -32
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     61766 |   32459    67492 |   10819   24393  1480169    60.7 | 79.706 % |
c |     61866 |   32459    67492 |   11900   24493  1483862    60.6 | 80.152 % |
c |     62016 |   32422    67401 |   13090   24627  1493869    60.7 | 80.285 % |
c |     62241 |   32400    67340 |   14400   24844  1515014    61.0 | 80.372 % |
c |     62579 |   32361    67247 |   15840   25167  1534905    61.0 | 80.510 % |
c |     63085 |   32361    67247 |   17424   25673  1569859    61.1 | 80.510 % |
c |     63845 |   32361    67247 |   19166   26433  1617338    61.2 | 80.510 % |
c |     64985 |   32361    67247 |   21083   27573  1724425    62.5 | 80.510 % |
c |     66693 |   32361    67247 |   23191   29281  1823567    62.3 | 80.510 % |
c |     69255 |   32361    67247 |   25510   31843  2022398    63.5 | 80.510 % |
c |     73099 |   32266    67009 |   28061   35630  2258988    63.4 | 80.852 % |
c |     78867 |   32266    67009 |   30867   41398  2541641    61.4 | 80.852 % |
c |     87517 |   32261    66998 |   33954   17592   605784    34.4 | 80.868 % |
c |    100493 |   32145    66707 |   37350   30555  1527180    50.0 | 81.251 % |
c |    119954 |   32136    66686 |   41085   50010  2776028    55.5 | 81.282 % |
c |    149146 |   32059    66501 |   45193   39406  2390640    60.7 | 81.558 % |
c |    192935 |   32018    66406 |   49713   40611  2365930    58.3 | 81.696 % |
c ==============================================================================
c Found solution: -33
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    234340 |   31964    66282 |   10654   33803  1904300    56.3 | 81.696 % |
c |    234440 |   31964    66282 |   11719   16070   660384    41.1 | 81.909 % |
c |    234590 |   31939    66229 |   12891   16216   667281    41.1 | 81.980 % |
c |    234817 |   31939    66229 |   14180   16443   680004    41.4 | 81.980 % |
c |    235155 |   31853    66019 |   15598   16755   688813    41.1 | 82.286 % |
c |    235661 |   31853    66019 |   17158   17261   714839    41.4 | 82.286 % |
c |    236420 |   31848    66006 |   18874   18019   754497    41.9 | 82.307 % |
c |    237559 |   31848    66006 |   20761   19158   827477    43.2 | 82.307 % |
c |    239268 |   31848    66006 |   22837   20867   941214    45.1 | 82.307 % |
c |    241830 |   31845    65999 |   25121   23424  1134066    48.4 | 82.317 % |
c |    245674 |   31832    65966 |   27633   27261  1379284    50.6 | 82.368 % |
c |    251442 |   31821    65939 |   30397   33025  1770495    53.6 | 82.409 % |
c |    260091 |   31723    65693 |   33436   41618  2363593    56.8 | 82.781 % |
c |    273065 |   31702    65642 |   36780   21888  1194237    54.6 | 82.858 % |
c |    292526 |   31595    65388 |   40458   41329  2455787    59.4 | 83.236 % |
c |    321718 |   31590    65375 |   44504   31574  1206245    38.2 | 83.256 % |
c |    365507 |   31587    65368 |   48954   33871  1201100    35.5 | 83.266 % |
c |    431191 |   31587    65368 |   53850   55118  1835677    33.3 | 83.266 % |
c |    529717 |   31516    65201 |   59235   54938  1748182    31.8 | 83.511 % |

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/2176/stat): 2176 (minisat+_script) R 2175 2176 20115 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1843512947 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/2176/statm): 174 3 169 147 0 27 0
[pid=2176] 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=2177
New process pid=2178
New process pid=2179
execve syscall for /bin/sed executable
One traced child (pid=2178) 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=2179) exited with status: 0
One traced child (pid=2177) exited with status: 0
New process pid=2180
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc28/normalized-frb35-17-5.opb

[startup+10.0042 s]
Raw data (loadavg): 0.93 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 2157 0 0 0 981 7 0 0 25 0 1 0 1843512952 9723904 2144 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/2180/statm): 2374 2144 145 145 0 2229 0
[pid=2180] vsize: 9496
Current children cumulated CPU time (s) 9.89
Current children cumulated vsize (Kb) 11620

[startup+20.0059 s]
Raw data (loadavg): 0.94 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 2261 0 0 0 1979 8 0 0 25 0 1 0 1843512952 10158080 2248 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 2480 2248 145 145 0 2335 0
[pid=2180] vsize: 9920
Current children cumulated CPU time (s) 19.88
Current children cumulated vsize (Kb) 12044

[startup+30.0065 s]
Raw data (loadavg): 0.95 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 2741 0 0 0 2971 11 0 0 25 0 1 0 1843512952 12124160 2728 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 2960 2728 145 145 0 2815 0
[pid=2180] vsize: 11840
Current children cumulated CPU time (s) 29.83
Current children cumulated vsize (Kb) 13964

[startup+40.0072 s]
Raw data (loadavg): 0.96 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 3321 0 0 0 3962 15 0 0 25 0 1 0 1843512952 14536704 3308 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 3549 3308 145 145 0 3404 0
[pid=2180] vsize: 14196
Current children cumulated CPU time (s) 39.78
Current children cumulated vsize (Kb) 16320

[startup+50.0079 s]
Raw data (loadavg): 0.96 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 3903 0 0 0 4951 19 0 0 19 0 1 0 1843512952 16896000 3890 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 4125 3890 145 145 0 3980 0
[pid=2180] vsize: 16500
Current children cumulated CPU time (s) 49.71
Current children cumulated vsize (Kb) 18624

[startup+60.0086 s]
Raw data (loadavg): 0.97 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 4463 0 0 0 5942 23 0 0 25 0 1 0 1843512952 19169280 4450 4294967295 134512640 135094434 3221224448 3221223104 134558126 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 4680 4450 145 145 0 4535 0
[pid=2180] vsize: 18720
Current children cumulated CPU time (s) 59.66
Current children cumulated vsize (Kb) 20844

[startup+70.0092 s]
Raw data (loadavg): 0.97 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 4855 0 0 0 6935 26 0 0 25 0 1 0 1843512952 20885504 4842 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 5099 4842 145 145 0 4954 0
[pid=2180] vsize: 20396
Current children cumulated CPU time (s) 69.62
Current children cumulated vsize (Kb) 22520

[startup+80.0099 s]
Raw data (loadavg): 0.98 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 5252 0 0 0 7926 30 0 0 25 0 1 0 1843512952 22495232 5239 4294967295 134512640 135094434 3221224448 3221223040 134556904 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 5492 5239 145 145 0 5347 0
[pid=2180] vsize: 21968
Current children cumulated CPU time (s) 79.57
Current children cumulated vsize (Kb) 24092

[startup+90.0106 s]
Raw data (loadavg): 0.98 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 5641 0 0 0 8919 33 0 0 25 0 1 0 1843512952 24072192 5628 4294967295 134512640 135094434 3221224448 3221223136 134554709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 5877 5628 145 145 0 5732 0
[pid=2180] vsize: 23508
Current children cumulated CPU time (s) 89.53
Current children cumulated vsize (Kb) 25632

[startup+100.011 s]
Raw data (loadavg): 0.98 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 6053 0 0 0 9913 35 0 0 25 0 1 0 1843512952 25739264 6040 4294967295 134512640 135094434 3221224448 3221223104 134558011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 6284 6040 145 145 0 6139 0
[pid=2180] vsize: 25136
Current children cumulated CPU time (s) 99.49
Current children cumulated vsize (Kb) 27260

[startup+110.013 s]
Raw data (loadavg): 0.98 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 6189 0 0 0 10911 36 0 0 25 0 1 0 1843512952 26292224 6176 4294967295 134512640 135094434 3221224448 3221223104 134558019 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 6419 6176 145 145 0 6274 0
[pid=2180] vsize: 25676
Current children cumulated CPU time (s) 109.48
Current children cumulated vsize (Kb) 27800

[startup+120.014 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 6209 0 0 0 11911 36 0 0 25 0 1 0 1843512952 26451968 6196 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 6458 6196 145 145 0 6313 0
[pid=2180] vsize: 25832
Current children cumulated CPU time (s) 119.48
Current children cumulated vsize (Kb) 27956

[startup+130.013 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 6209 0 0 0 12911 36 0 0 25 0 1 0 1843512952 26451968 6196 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 6458 6196 145 145 0 6313 0
[pid=2180] vsize: 25832
Current children cumulated CPU time (s) 129.48
Current children cumulated vsize (Kb) 27956

[startup+140.014 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 6209 0 0 0 13911 36 0 0 25 0 1 0 1843512952 26451968 6196 4294967295 134512640 135094434 3221224448 3221223040 134557393 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 6458 6196 145 145 0 6313 0
[pid=2180] vsize: 25832
Current children cumulated CPU time (s) 139.48
Current children cumulated vsize (Kb) 27956

[startup+150.015 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 6209 0 0 0 14911 36 0 0 25 0 1 0 1843512952 26451968 6196 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 6458 6196 145 145 0 6313 0
[pid=2180] vsize: 25832
Current children cumulated CPU time (s) 149.48
Current children cumulated vsize (Kb) 27956

[startup+160.015 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 6209 0 0 0 15911 36 0 0 25 0 1 0 1843512952 26451968 6196 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 6458 6196 145 145 0 6313 0
[pid=2180] vsize: 25832
Current children cumulated CPU time (s) 159.48
Current children cumulated vsize (Kb) 27956

[startup+170.016 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 6209 0 0 0 16912 36 0 0 25 0 1 0 1843512952 26451968 6196 4294967295 134512640 135094434 3221224448 3221223120 134556073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 6458 6196 145 145 0 6313 0
[pid=2180] vsize: 25832
Current children cumulated CPU time (s) 169.49
Current children cumulated vsize (Kb) 27956

[startup+180.017 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 6209 0 0 0 17912 36 0 0 25 0 1 0 1843512952 26451968 6196 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 6458 6196 145 145 0 6313 0
[pid=2180] vsize: 25832
Current children cumulated CPU time (s) 179.49
Current children cumulated vsize (Kb) 27956

[startup+190.018 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 6209 0 0 0 18912 36 0 0 25 0 1 0 1843512952 26451968 6196 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 6458 6196 145 145 0 6313 0
[pid=2180] vsize: 25832
Current children cumulated CPU time (s) 189.49
Current children cumulated vsize (Kb) 27956

[startup+200.019 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 6209 0 0 0 19912 36 0 0 25 0 1 0 1843512952 26451968 6196 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 6458 6196 145 145 0 6313 0
[pid=2180] vsize: 25832
Current children cumulated CPU time (s) 199.49
Current children cumulated vsize (Kb) 27956

[startup+210.02 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 6209 0 0 0 20913 36 0 0 25 0 1 0 1843512952 26451968 6196 4294967295 134512640 135094434 3221224448 3221223104 134558016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 6458 6196 145 145 0 6313 0
[pid=2180] vsize: 25832
Current children cumulated CPU time (s) 209.5
Current children cumulated vsize (Kb) 27956

[startup+220.02 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 6209 0 0 0 21913 36 0 0 25 0 1 0 1843512952 26451968 6196 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 6458 6196 145 145 0 6313 0
[pid=2180] vsize: 25832
Current children cumulated CPU time (s) 219.5
Current children cumulated vsize (Kb) 27956

[startup+230.02 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 6210 0 0 0 22913 36 0 0 25 0 1 0 1843512952 26451968 6197 4294967295 134512640 135094434 3221224448 3221223040 134557273 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 6458 6197 145 145 0 6313 0
[pid=2180] vsize: 25832
Current children cumulated CPU time (s) 229.5
Current children cumulated vsize (Kb) 27956

[startup+240.021 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 6214 0 0 0 23913 36 0 0 25 0 1 0 1843512952 26451968 6201 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 6458 6201 145 145 0 6313 0
[pid=2180] vsize: 25832
Current children cumulated CPU time (s) 239.5
Current children cumulated vsize (Kb) 27956

[startup+250.021 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 6216 0 0 0 24913 36 0 0 25 0 1 0 1843512952 26451968 6203 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 6458 6203 145 145 0 6313 0
[pid=2180] vsize: 25832
Current children cumulated CPU time (s) 249.5
Current children cumulated vsize (Kb) 27956

[startup+260.023 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 6216 0 0 0 25914 36 0 0 25 0 1 0 1843512952 26451968 6203 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 6458 6203 145 145 0 6313 0
[pid=2180] vsize: 25832
Current children cumulated CPU time (s) 259.51
Current children cumulated vsize (Kb) 27956

[startup+270.024 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 6216 0 0 0 26914 36 0 0 25 0 1 0 1843512952 26451968 6203 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 6458 6203 145 145 0 6313 0
[pid=2180] vsize: 25832
Current children cumulated CPU time (s) 269.51
Current children cumulated vsize (Kb) 27956

[startup+280.024 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 6216 0 0 0 27914 36 0 0 25 0 1 0 1843512952 26451968 6203 4294967295 134512640 135094434 3221224448 3221223040 134557230 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 6458 6203 145 145 0 6313 0
[pid=2180] vsize: 25832
Current children cumulated CPU time (s) 279.51
Current children cumulated vsize (Kb) 27956

[startup+290.025 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 6216 0 0 0 28914 36 0 0 25 0 1 0 1843512952 26451968 6203 4294967295 134512640 135094434 3221224448 3221223040 134557202 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 6458 6203 145 145 0 6313 0
[pid=2180] vsize: 25832
Current children cumulated CPU time (s) 289.51
Current children cumulated vsize (Kb) 27956

[startup+300.026 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 6216 0 0 0 29915 36 0 0 25 0 1 0 1843512952 26451968 6203 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 6458 6203 145 145 0 6313 0
[pid=2180] vsize: 25832
Current children cumulated CPU time (s) 299.52
Current children cumulated vsize (Kb) 27956

[startup+310.027 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 6216 0 0 0 30915 36 0 0 25 0 1 0 1843512952 26451968 6203 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 6458 6203 145 145 0 6313 0
[pid=2180] vsize: 25832
Current children cumulated CPU time (s) 309.52
Current children cumulated vsize (Kb) 27956

[startup+320.027 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 6216 0 0 0 31915 36 0 0 25 0 1 0 1843512952 26451968 6203 4294967295 134512640 135094434 3221224448 3221223104 134558013 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 6458 6203 145 145 0 6313 0
[pid=2180] vsize: 25832
Current children cumulated CPU time (s) 319.52
Current children cumulated vsize (Kb) 27956

[startup+330.028 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 6231 0 0 0 32915 36 0 0 25 0 1 0 1843512952 26529792 6218 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 6477 6218 145 145 0 6332 0
[pid=2180] vsize: 25908
Current children cumulated CPU time (s) 329.52
Current children cumulated vsize (Kb) 28032

[startup+340.029 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 6247 0 0 0 33915 36 0 0 25 0 1 0 1843512952 26611712 6234 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 6497 6234 145 145 0 6352 0
[pid=2180] vsize: 25988
Current children cumulated CPU time (s) 339.52
Current children cumulated vsize (Kb) 28112

[startup+350.029 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 6430 0 0 0 34913 37 0 0 25 0 1 0 1843512952 27373568 6417 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 6683 6417 145 145 0 6538 0
[pid=2180] vsize: 26732
Current children cumulated CPU time (s) 349.51
Current children cumulated vsize (Kb) 28856

[startup+360.031 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 6561 0 0 0 35911 38 0 0 25 0 1 0 1843512952 27897856 6548 4294967295 134512640 135094434 3221224448 3221223040 134551780 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 6811 6548 145 145 0 6666 0
[pid=2180] vsize: 27244
Current children cumulated CPU time (s) 359.5
Current children cumulated vsize (Kb) 29368

[startup+370.032 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 6561 0 0 0 36911 38 0 0 25 0 1 0 1843512952 27897856 6548 4294967295 134512640 135094434 3221224448 3221223136 134554739 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 6811 6548 145 145 0 6666 0
[pid=2180] vsize: 27244
Current children cumulated CPU time (s) 369.5
Current children cumulated vsize (Kb) 29368

[startup+380.032 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 6561 0 0 0 37911 38 0 0 25 0 1 0 1843512952 27897856 6548 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 6811 6548 145 145 0 6666 0
[pid=2180] vsize: 27244
Current children cumulated CPU time (s) 379.5
Current children cumulated vsize (Kb) 29368

[startup+390.033 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 6573 0 0 0 38911 38 0 0 25 0 1 0 1843512952 27963392 6560 4294967295 134512640 135094434 3221224448 3221223072 134557587 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 6827 6560 145 145 0 6682 0
[pid=2180] vsize: 27308
Current children cumulated CPU time (s) 389.5
Current children cumulated vsize (Kb) 29432

[startup+400.035 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 6574 0 0 0 39912 38 0 0 25 0 1 0 1843512952 27963392 6561 4294967295 134512640 135094434 3221224448 3221223072 134557636 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 6827 6561 145 145 0 6682 0
[pid=2180] vsize: 27308
Current children cumulated CPU time (s) 399.51
Current children cumulated vsize (Kb) 29432

[startup+410.036 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 6575 0 0 0 40912 38 0 0 25 0 1 0 1843512952 27963392 6562 4294967295 134512640 135094434 3221224448 3221223120 134555666 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 6827 6562 145 145 0 6682 0
[pid=2180] vsize: 27308
Current children cumulated CPU time (s) 409.51
Current children cumulated vsize (Kb) 29432

[startup+420.037 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 6576 0 0 0 41912 38 0 0 25 0 1 0 1843512952 27963392 6563 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 6827 6563 145 145 0 6682 0
[pid=2180] vsize: 27308
Current children cumulated CPU time (s) 419.51
Current children cumulated vsize (Kb) 29432

[startup+430.038 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 6891 0 0 0 42906 40 0 0 25 0 1 0 1843512952 29257728 6878 4294967295 134512640 135094434 3221224448 3221223120 134555260 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 7143 6878 145 145 0 6998 0
[pid=2180] vsize: 28572
Current children cumulated CPU time (s) 429.47
Current children cumulated vsize (Kb) 30696

[startup+440.039 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7264 0 0 0 43900 43 0 0 25 0 1 0 1843512952 30785536 7251 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 7516 7251 145 145 0 7371 0
[pid=2180] vsize: 30064
Current children cumulated CPU time (s) 439.44
Current children cumulated vsize (Kb) 32188

[startup+450.04 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7559 0 0 0 44895 45 0 0 25 0 1 0 1843512952 31981568 7546 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 7808 7546 145 145 0 7663 0
[pid=2180] vsize: 31232
Current children cumulated CPU time (s) 449.41
Current children cumulated vsize (Kb) 33356

[startup+460.041 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7636 0 0 0 45893 46 0 0 25 0 1 0 1843512952 32550912 7623 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 7947 7623 145 145 0 7802 0
[pid=2180] vsize: 31788
Current children cumulated CPU time (s) 459.4
Current children cumulated vsize (Kb) 33912

[startup+470.041 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7636 0 0 0 46893 46 0 0 25 0 1 0 1843512952 32550912 7623 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 7947 7623 145 145 0 7802 0
[pid=2180] vsize: 31788
Current children cumulated CPU time (s) 469.4
Current children cumulated vsize (Kb) 33912

[startup+480.042 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7636 0 0 0 47894 46 0 0 25 0 1 0 1843512952 32550912 7623 4294967295 134512640 135094434 3221224448 3221223104 134558218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 7947 7623 145 145 0 7802 0
[pid=2180] vsize: 31788
Current children cumulated CPU time (s) 479.41
Current children cumulated vsize (Kb) 33912

[startup+490.043 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7636 0 0 0 48894 46 0 0 25 0 1 0 1843512952 32550912 7623 4294967295 134512640 135094434 3221224448 3221223040 134557040 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 7947 7623 145 145 0 7802 0
[pid=2180] vsize: 31788
Current children cumulated CPU time (s) 489.41
Current children cumulated vsize (Kb) 33912

[startup+500.043 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7636 0 0 0 49894 46 0 0 25 0 1 0 1843512952 32550912 7623 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 7947 7623 145 145 0 7802 0
[pid=2180] vsize: 31788
Current children cumulated CPU time (s) 499.41
Current children cumulated vsize (Kb) 33912

[startup+510.045 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7636 0 0 0 50894 46 0 0 25 0 1 0 1843512952 32550912 7623 4294967295 134512640 135094434 3221224448 3221223104 134557978 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 7947 7623 145 145 0 7802 0
[pid=2180] vsize: 31788
Current children cumulated CPU time (s) 509.41
Current children cumulated vsize (Kb) 33912

[startup+520.046 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7636 0 0 0 51895 46 0 0 25 0 1 0 1843512952 32550912 7623 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 7947 7623 145 145 0 7802 0
[pid=2180] vsize: 31788
Current children cumulated CPU time (s) 519.42
Current children cumulated vsize (Kb) 33912

[startup+530.047 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7636 0 0 0 52895 46 0 0 25 0 1 0 1843512952 32550912 7623 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 7947 7623 145 145 0 7802 0
[pid=2180] vsize: 31788
Current children cumulated CPU time (s) 529.42
Current children cumulated vsize (Kb) 33912

[startup+540.048 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7636 0 0 0 53895 46 0 0 25 0 1 0 1843512952 32550912 7623 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 7947 7623 145 145 0 7802 0
[pid=2180] vsize: 31788
Current children cumulated CPU time (s) 539.42
Current children cumulated vsize (Kb) 33912

[startup+550.049 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7636 0 0 0 54895 46 0 0 25 0 1 0 1843512952 32550912 7623 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 7947 7623 145 145 0 7802 0
[pid=2180] vsize: 31788
Current children cumulated CPU time (s) 549.42
Current children cumulated vsize (Kb) 33912

[startup+560.051 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7636 0 0 0 55896 46 0 0 25 0 1 0 1843512952 32550912 7623 4294967295 134512640 135094434 3221224448 3221223104 134557866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 7947 7623 145 145 0 7802 0
[pid=2180] vsize: 31788
Current children cumulated CPU time (s) 559.43
Current children cumulated vsize (Kb) 33912

[startup+570.051 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7636 0 0 0 56896 46 0 0 25 0 1 0 1843512952 32550912 7623 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 7947 7623 145 145 0 7802 0
[pid=2180] vsize: 31788
Current children cumulated CPU time (s) 569.43
Current children cumulated vsize (Kb) 33912

[startup+580.051 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7636 0 0 0 57896 46 0 0 25 0 1 0 1843512952 32550912 7623 4294967295 134512640 135094434 3221224448 3221223104 134558013 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 7947 7623 145 145 0 7802 0
[pid=2180] vsize: 31788
Current children cumulated CPU time (s) 579.43
Current children cumulated vsize (Kb) 33912

[startup+590.052 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7636 0 0 0 58896 46 0 0 25 0 1 0 1843512952 32550912 7623 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 7947 7623 145 145 0 7802 0
[pid=2180] vsize: 31788
Current children cumulated CPU time (s) 589.43
Current children cumulated vsize (Kb) 33912

[startup+600.052 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7636 0 0 0 59896 46 0 0 25 0 1 0 1843512952 32550912 7623 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 7947 7623 145 145 0 7802 0
[pid=2180] vsize: 31788
Current children cumulated CPU time (s) 599.43
Current children cumulated vsize (Kb) 33912

[startup+610.054 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7636 0 0 0 60897 46 0 0 25 0 1 0 1843512952 32550912 7623 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 7947 7623 145 145 0 7802 0
[pid=2180] vsize: 31788
Current children cumulated CPU time (s) 609.44
Current children cumulated vsize (Kb) 33912

[startup+620.055 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7636 0 0 0 61897 46 0 0 25 0 1 0 1843512952 32550912 7623 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 7947 7623 145 145 0 7802 0
[pid=2180] vsize: 31788
Current children cumulated CPU time (s) 619.44
Current children cumulated vsize (Kb) 33912

[startup+630.055 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7636 0 0 0 62897 46 0 0 25 0 1 0 1843512952 32550912 7623 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 7947 7623 145 145 0 7802 0
[pid=2180] vsize: 31788
Current children cumulated CPU time (s) 629.44
Current children cumulated vsize (Kb) 33912

[startup+640.056 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7637 0 0 0 63898 46 0 0 25 0 1 0 1843512952 32550912 7624 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 7947 7624 145 145 0 7802 0
[pid=2180] vsize: 31788
Current children cumulated CPU time (s) 639.45
Current children cumulated vsize (Kb) 33912

[startup+650.057 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7637 0 0 0 64898 46 0 0 25 0 1 0 1843512952 32550912 7624 4294967295 134512640 135094434 3221224448 3221223104 134558402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 7947 7624 145 145 0 7802 0
[pid=2180] vsize: 31788
Current children cumulated CPU time (s) 649.45
Current children cumulated vsize (Kb) 33912

[startup+660.057 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7637 0 0 0 65898 46 0 0 25 0 1 0 1843512952 32550912 7624 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 7947 7624 145 145 0 7802 0
[pid=2180] vsize: 31788
Current children cumulated CPU time (s) 659.45
Current children cumulated vsize (Kb) 33912

[startup+670.058 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7637 0 0 0 66898 46 0 0 25 0 1 0 1843512952 32550912 7624 4294967295 134512640 135094434 3221224448 3221223104 134557937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 7947 7624 145 145 0 7802 0
[pid=2180] vsize: 31788
Current children cumulated CPU time (s) 669.45
Current children cumulated vsize (Kb) 33912

[startup+680.059 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7637 0 0 0 67899 46 0 0 25 0 1 0 1843512952 32550912 7624 4294967295 134512640 135094434 3221224448 3221223072 134562057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 7947 7624 145 145 0 7802 0
[pid=2180] vsize: 31788
Current children cumulated CPU time (s) 679.46
Current children cumulated vsize (Kb) 33912

[startup+690.059 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7637 0 0 0 68899 46 0 0 25 0 1 0 1843512952 32550912 7624 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 7947 7624 145 145 0 7802 0
[pid=2180] vsize: 31788
Current children cumulated CPU time (s) 689.46
Current children cumulated vsize (Kb) 33912

[startup+700.06 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7637 0 0 0 69899 46 0 0 25 0 1 0 1843512952 32550912 7624 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 7947 7624 145 145 0 7802 0
[pid=2180] vsize: 31788
Current children cumulated CPU time (s) 699.46
Current children cumulated vsize (Kb) 33912

[startup+710.062 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7637 0 0 0 70899 46 0 0 25 0 1 0 1843512952 32550912 7624 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 7947 7624 145 145 0 7802 0
[pid=2180] vsize: 31788
Current children cumulated CPU time (s) 709.46
Current children cumulated vsize (Kb) 33912

[startup+720.062 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7637 0 0 0 71899 46 0 0 25 0 1 0 1843512952 32550912 7624 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 7947 7624 145 145 0 7802 0
[pid=2180] vsize: 31788
Current children cumulated CPU time (s) 719.46
Current children cumulated vsize (Kb) 33912

[startup+730.062 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7638 0 0 0 72900 46 0 0 25 0 1 0 1843512952 32550912 7625 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 7947 7625 145 145 0 7802 0
[pid=2180] vsize: 31788
Current children cumulated CPU time (s) 729.47
Current children cumulated vsize (Kb) 33912

[startup+740.063 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7638 0 0 0 73900 46 0 0 25 0 1 0 1843512952 32550912 7625 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 7947 7625 145 145 0 7802 0
[pid=2180] vsize: 31788
Current children cumulated CPU time (s) 739.47
Current children cumulated vsize (Kb) 33912

[startup+750.063 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7638 0 0 0 74900 46 0 0 25 0 1 0 1843512952 32550912 7625 4294967295 134512640 135094434 3221224448 3221223040 134556826 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 7947 7625 145 145 0 7802 0
[pid=2180] vsize: 31788
Current children cumulated CPU time (s) 749.47
Current children cumulated vsize (Kb) 33912

[startup+760.064 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7638 0 0 0 75900 46 0 0 25 0 1 0 1843512952 32550912 7625 4294967295 134512640 135094434 3221224448 3221223104 134558184 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 7947 7625 145 145 0 7802 0
[pid=2180] vsize: 31788
Current children cumulated CPU time (s) 759.47
Current children cumulated vsize (Kb) 33912

[startup+770.065 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7638 0 0 0 76901 46 0 0 25 0 1 0 1843512952 32550912 7625 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 7947 7625 145 145 0 7802 0
[pid=2180] vsize: 31788
Current children cumulated CPU time (s) 769.48
Current children cumulated vsize (Kb) 33912

[startup+780.065 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7638 0 0 0 77901 46 0 0 25 0 1 0 1843512952 32550912 7625 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 7947 7625 145 145 0 7802 0
[pid=2180] vsize: 31788
Current children cumulated CPU time (s) 779.48
Current children cumulated vsize (Kb) 33912

[startup+790.066 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7640 0 0 0 78901 46 0 0 25 0 1 0 1843512952 32550912 7627 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 7947 7627 145 145 0 7802 0
[pid=2180] vsize: 31788
Current children cumulated CPU time (s) 789.48
Current children cumulated vsize (Kb) 33912

[startup+800.067 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7640 0 0 0 79901 46 0 0 25 0 1 0 1843512952 32550912 7627 4294967295 134512640 135094434 3221224448 3221223100 134558036 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 7947 7627 145 145 0 7802 0
[pid=2180] vsize: 31788
Current children cumulated CPU time (s) 799.48
Current children cumulated vsize (Kb) 33912

[startup+810.067 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7641 0 0 0 80902 46 0 0 25 0 1 0 1843512952 32550912 7628 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 7947 7628 145 145 0 7802 0
[pid=2180] vsize: 31788
Current children cumulated CPU time (s) 809.49
Current children cumulated vsize (Kb) 33912

[startup+820.068 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7641 0 0 0 81902 46 0 0 25 0 1 0 1843512952 32550912 7628 4294967295 134512640 135094434 3221224448 3221223120 134555599 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 7947 7628 145 145 0 7802 0
[pid=2180] vsize: 31788
Current children cumulated CPU time (s) 819.49
Current children cumulated vsize (Kb) 33912

[startup+830.069 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7641 0 0 0 82902 46 0 0 25 0 1 0 1843512952 32550912 7628 4294967295 134512640 135094434 3221224448 3221223120 134555568 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 7947 7628 145 145 0 7802 0
[pid=2180] vsize: 31788
Current children cumulated CPU time (s) 829.49
Current children cumulated vsize (Kb) 33912

[startup+840.07 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7641 0 0 0 83902 46 0 0 25 0 1 0 1843512952 32550912 7628 4294967295 134512640 135094434 3221224448 3221223040 134557219 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 7947 7628 145 145 0 7802 0
[pid=2180] vsize: 31788
Current children cumulated CPU time (s) 839.49
Current children cumulated vsize (Kb) 33912

[startup+850.07 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7641 0 0 0 84903 46 0 0 25 0 1 0 1843512952 32550912 7628 4294967295 134512640 135094434 3221224448 3221223104 134557937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 7947 7628 145 145 0 7802 0
[pid=2180] vsize: 31788
Current children cumulated CPU time (s) 849.5
Current children cumulated vsize (Kb) 33912

[startup+860.072 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7641 0 0 0 85903 46 0 0 25 0 1 0 1843512952 32550912 7628 4294967295 134512640 135094434 3221224448 3221223120 134556317 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 7947 7628 145 145 0 7802 0
[pid=2180] vsize: 31788
Current children cumulated CPU time (s) 859.5
Current children cumulated vsize (Kb) 33912

[startup+870.073 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7641 0 0 0 86903 46 0 0 25 0 1 0 1843512952 32550912 7628 4294967295 134512640 135094434 3221224448 3221223092 134558040 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 7947 7628 145 145 0 7802 0
[pid=2180] vsize: 31788
Current children cumulated CPU time (s) 869.5
Current children cumulated vsize (Kb) 33912

[startup+880.072 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7641 0 0 0 87903 46 0 0 25 0 1 0 1843512952 32550912 7628 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 7947 7628 145 145 0 7802 0
[pid=2180] vsize: 31788
Current children cumulated CPU time (s) 879.5
Current children cumulated vsize (Kb) 33912

[startup+890.074 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7641 0 0 0 88903 46 0 0 25 0 1 0 1843512952 32550912 7628 4294967295 134512640 135094434 3221224448 3221223104 134558221 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 7947 7628 145 145 0 7802 0
[pid=2180] vsize: 31788
Current children cumulated CPU time (s) 889.5
Current children cumulated vsize (Kb) 33912

[startup+900.075 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7642 0 0 0 89903 46 0 0 25 0 1 0 1843512952 32550912 7629 4294967295 134512640 135094434 3221224448 3221223120 134556452 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 7947 7629 145 145 0 7802 0
[pid=2180] vsize: 31788
Current children cumulated CPU time (s) 899.5
Current children cumulated vsize (Kb) 33912

[startup+910.075 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7645 0 0 0 90904 46 0 0 25 0 1 0 1843512952 32550912 7632 4294967295 134512640 135094434 3221224448 3221223040 134551454 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 7947 7632 145 145 0 7802 0
[pid=2180] vsize: 31788
Current children cumulated CPU time (s) 909.51
Current children cumulated vsize (Kb) 33912

[startup+920.077 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7645 0 0 0 91904 46 0 0 25 0 1 0 1843512952 32550912 7632 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 7947 7632 145 145 0 7802 0
[pid=2180] vsize: 31788
Current children cumulated CPU time (s) 919.51
Current children cumulated vsize (Kb) 33912

[startup+930.078 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7645 0 0 0 92904 46 0 0 25 0 1 0 1843512952 32550912 7632 4294967295 134512640 135094434 3221224448 3221223104 134557956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 7947 7632 145 145 0 7802 0
[pid=2180] vsize: 31788
Current children cumulated CPU time (s) 929.51
Current children cumulated vsize (Kb) 33912

[startup+940.078 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7645 0 0 0 93904 46 0 0 25 0 1 0 1843512952 32550912 7632 4294967295 134512640 135094434 3221224448 3221223040 134557230 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 7947 7632 145 145 0 7802 0
[pid=2180] vsize: 31788
Current children cumulated CPU time (s) 939.51
Current children cumulated vsize (Kb) 33912

[startup+950.079 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7645 0 0 0 94905 46 0 0 25 0 1 0 1843512952 32550912 7632 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 7947 7632 145 145 0 7802 0
[pid=2180] vsize: 31788
Current children cumulated CPU time (s) 949.52
Current children cumulated vsize (Kb) 33912

[startup+960.079 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7645 0 0 0 95905 46 0 0 25 0 1 0 1843512952 32550912 7632 4294967295 134512640 135094434 3221224448 3221223104 134558254 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 7947 7632 145 145 0 7802 0
[pid=2180] vsize: 31788
Current children cumulated CPU time (s) 959.52
Current children cumulated vsize (Kb) 33912

[startup+970.079 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7645 0 0 0 96905 46 0 0 25 0 1 0 1843512952 32550912 7632 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 7947 7632 145 145 0 7802 0
[pid=2180] vsize: 31788
Current children cumulated CPU time (s) 969.52
Current children cumulated vsize (Kb) 33912

[startup+980.08 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7645 0 0 0 97905 46 0 0 25 0 1 0 1843512952 32550912 7632 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 7947 7632 145 145 0 7802 0
[pid=2180] vsize: 31788
Current children cumulated CPU time (s) 979.52
Current children cumulated vsize (Kb) 33912

[startup+990.082 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7645 0 0 0 98905 46 0 0 25 0 1 0 1843512952 32550912 7632 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 7947 7632 145 145 0 7802 0
[pid=2180] vsize: 31788
Current children cumulated CPU time (s) 989.52
Current children cumulated vsize (Kb) 33912

[startup+1000.08 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7645 0 0 0 99906 46 0 0 25 0 1 0 1843512952 32550912 7632 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 7947 7632 145 145 0 7802 0
[pid=2180] vsize: 31788
Current children cumulated CPU time (s) 999.53
Current children cumulated vsize (Kb) 33912

[startup+1010.08 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7645 0 0 0 100906 46 0 0 25 0 1 0 1843512952 32550912 7632 4294967295 134512640 135094434 3221224448 3221223136 134554687 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 7947 7632 145 145 0 7802 0
[pid=2180] vsize: 31788
Current children cumulated CPU time (s) 1009.53
Current children cumulated vsize (Kb) 33912

[startup+1020.08 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7645 0 0 0 101906 46 0 0 25 0 1 0 1843512952 32550912 7632 4294967295 134512640 135094434 3221224448 3221223040 134551454 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 7947 7632 145 145 0 7802 0
[pid=2180] vsize: 31788
Current children cumulated CPU time (s) 1019.53
Current children cumulated vsize (Kb) 33912

[startup+1030.08 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7645 0 0 0 102906 46 0 0 25 0 1 0 1843512952 32550912 7632 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 7947 7632 145 145 0 7802 0
[pid=2180] vsize: 31788
Current children cumulated CPU time (s) 1029.53
Current children cumulated vsize (Kb) 33912

[startup+1040.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7645 0 0 0 103907 46 0 0 25 0 1 0 1843512952 32550912 7632 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 7947 7632 145 145 0 7802 0
[pid=2180] vsize: 31788
Current children cumulated CPU time (s) 1039.54
Current children cumulated vsize (Kb) 33912

[startup+1050.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7645 0 0 0 104907 46 0 0 25 0 1 0 1843512952 32550912 7632 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 7947 7632 145 145 0 7802 0
[pid=2180] vsize: 31788
Current children cumulated CPU time (s) 1049.54
Current children cumulated vsize (Kb) 33912

[startup+1060.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7645 0 0 0 105907 46 0 0 25 0 1 0 1843512952 32550912 7632 4294967295 134512640 135094434 3221224448 3221223072 134557604 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 7947 7632 145 145 0 7802 0
[pid=2180] vsize: 31788
Current children cumulated CPU time (s) 1059.54
Current children cumulated vsize (Kb) 33912

[startup+1070.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7645 0 0 0 106907 46 0 0 25 0 1 0 1843512952 32550912 7632 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 7947 7632 145 145 0 7802 0
[pid=2180] vsize: 31788
Current children cumulated CPU time (s) 1069.54
Current children cumulated vsize (Kb) 33912

[startup+1080.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7645 0 0 0 107908 46 0 0 25 0 1 0 1843512952 32550912 7632 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 7947 7632 145 145 0 7802 0
[pid=2180] vsize: 31788
Current children cumulated CPU time (s) 1079.55
Current children cumulated vsize (Kb) 33912

[startup+1090.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7645 0 0 0 108908 46 0 0 25 0 1 0 1843512952 32550912 7632 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 7947 7632 145 145 0 7802 0
[pid=2180] vsize: 31788
Current children cumulated CPU time (s) 1089.55
Current children cumulated vsize (Kb) 33912

[startup+1100.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7645 0 0 0 109908 47 0 0 25 0 1 0 1843512952 32550912 7632 4294967295 134512640 135094434 3221224448 3221223136 134554739 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 7947 7632 145 145 0 7802 0
[pid=2180] vsize: 31788
Current children cumulated CPU time (s) 1099.56
Current children cumulated vsize (Kb) 33912

[startup+1110.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7645 0 0 0 110908 47 0 0 25 0 1 0 1843512952 32550912 7632 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 7947 7632 145 145 0 7802 0
[pid=2180] vsize: 31788
Current children cumulated CPU time (s) 1109.56
Current children cumulated vsize (Kb) 33912

[startup+1120.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7645 0 0 0 111908 47 0 0 25 0 1 0 1843512952 32550912 7632 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 7947 7632 145 145 0 7802 0
[pid=2180] vsize: 31788
Current children cumulated CPU time (s) 1119.56
Current children cumulated vsize (Kb) 33912

[startup+1130.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7646 0 0 0 112908 47 0 0 25 0 1 0 1843512952 32550912 7633 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 7947 7633 145 145 0 7802 0
[pid=2180] vsize: 31788
Current children cumulated CPU time (s) 1129.56
Current children cumulated vsize (Kb) 33912

[startup+1140.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7649 0 0 0 113909 47 0 0 25 0 1 0 1843512952 32550912 7636 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 7947 7636 145 145 0 7802 0
[pid=2180] vsize: 31788
Current children cumulated CPU time (s) 1139.57
Current children cumulated vsize (Kb) 33912

[startup+1150.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7650 0 0 0 114909 47 0 0 25 0 1 0 1843512952 32550912 7637 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 7947 7637 145 145 0 7802 0
[pid=2180] vsize: 31788
Current children cumulated CPU time (s) 1149.57
Current children cumulated vsize (Kb) 33912

[startup+1160.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7650 0 0 0 115909 47 0 0 25 0 1 0 1843512952 32550912 7637 4294967295 134512640 135094434 3221224448 3221223104 134557937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 7947 7637 145 145 0 7802 0
[pid=2180] vsize: 31788
Current children cumulated CPU time (s) 1159.57
Current children cumulated vsize (Kb) 33912

[startup+1170.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7650 0 0 0 116909 47 0 0 25 0 1 0 1843512952 32550912 7637 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 7947 7637 145 145 0 7802 0
[pid=2180] vsize: 31788
Current children cumulated CPU time (s) 1169.57
Current children cumulated vsize (Kb) 33912

[startup+1180.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7650 0 0 0 117910 47 0 0 25 0 1 0 1843512952 32550912 7637 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 7947 7637 145 145 0 7802 0
[pid=2180] vsize: 31788
Current children cumulated CPU time (s) 1179.58
Current children cumulated vsize (Kb) 33912

[startup+1190.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7650 0 0 0 118910 47 0 0 25 0 1 0 1843512952 32550912 7637 4294967295 134512640 135094434 3221224448 3221223104 134557937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 7947 7637 145 145 0 7802 0
[pid=2180] vsize: 31788
Current children cumulated CPU time (s) 1189.58
Current children cumulated vsize (Kb) 33912

[startup+1200.1 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7650 0 0 0 119910 47 0 0 25 0 1 0 1843512952 32550912 7637 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 7947 7637 145 145 0 7802 0
[pid=2180] vsize: 31788
Current children cumulated CPU time (s) 1199.58
Current children cumulated vsize (Kb) 33912

[startup+1210.1 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7650 0 0 0 120910 47 0 0 25 0 1 0 1843512952 32550912 7637 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 7947 7637 145 145 0 7802 0
[pid=2180] vsize: 31788
Current children cumulated CPU time (s) 1209.58
Current children cumulated vsize (Kb) 33912



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.1 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 2180
Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/2176/statm): 531 226 485 147 0 384 0
[pid=2176] vsize: 2124
Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7650 0 0 0 120911 47 0 0 25 0 1 0 1843512952 32550912 7637 4294967295 134512640 135094434 3221224448 3221223120 134555943 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/2180/statm): 7947 7637 145 145 0 7802 0
[pid=2180] vsize: 31788
Current children cumulated CPU time (s) 1209.59
Current children cumulated vsize (Kb) 33912

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

Child status: 10
Real time (s): 1210.12
CPU time (s): 1209.6
CPU user time (s): 1209.11
CPU system time (s): 0.485926
CPU usage (%): 99.9572
Max. virtual memory (cumulated for all children) (Kb): 33912

Verifier Data

ERROR: no interpretation found !