Some explanations

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

General information on the benchmark

Namemps-v2-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-misc07.opb
MD5SUMa3dd3cd7dd293e24bffaff8bb73da54c
Bench Categoryoptimization, medium integers (OPTMEDINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 1408128
Optimality of the best value was proved NO
Number of terms in the objective function 21
Biggest coefficient in the objective function 1048576
Number of bits for the biggest coefficient in the objective function 21
Sum of the numbers in the objective function 2097151
Number of bits of the sum of numbers in the objective function 21
Biggest number in a constraint 1048576
Number of bits of the biggest number in a constraint 21
Biggest sum of numbers in a constraint 11486079
Number of bits of the biggest sum of numbers24
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1189.01
Number of variables280
Total number of constraints471
Number of constraints which are clauses127
Number of constraints which are cardinality constraints (but not clauses)272
Number of constraints which are nor clauses,nor cardinality constraints72
Minimum length of a constraint1
Maximum length of a constraint253

Trace number 6142

Launcher Data

LAUNCH ON wulflinc17 THE 2005-09-20 03:46:27 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3304 boxname=wulflinc17 idbench=960 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  a3dd3cd7dd293e24bffaff8bb73da54c  /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-13-7-misc07.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-13-7-misc07.opb
IDLAUNCH: 3304
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
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.072
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:        911408 kB
Buffers:         14472 kB
Cached:          81164 kB
SwapCached:        516 kB
Active:          26208 kB
Inactive:        71848 kB
HighTotal:      131008 kB
HighFree:        50204 kB
LowTotal:       903652 kB
LowFree:        861204 kB
SwapTotal:     2097892 kB
SwapFree:      2096676 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5664 kB
Slab:            19604 kB
Committed_AS:    64316 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-20 04:06:37 (client local time) WITH STATUS 10 IN 1210.01 SECONDS
stats: 3304 7 1210.01 10

Solver Data

c Parsing PB file...
c Converting 247 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ###################################
c   -- Clauses(.)/Splits(s): ...............................................................................................................................
c ---[ 245]---> Adder-cost: 1695   maxlim: 1048703   bits: 22/21
c ---[ 244]---> BDD-cost:  239
c ---[ 233]---> BDD-cost:  239
c ---[ 200]---> Sorter-cost:  127     Base:
c ---[ 197]---> Sorter-cost:  127     Base:
c ---[ 195]---> Sorter-cost:  127     Base:
c ---[ 193]---> Sorter-cost:  127     Base:
c ---[ 191]---> Sorter-cost:  127     Base:
c ---[ 189]---> Sorter-cost:  127     Base:
c ---[ 187]---> Sorter-cost:  127     Base:
c ---[ 185]---> Sorter-cost:  127     Base:
c ---[ 183]---> Sorter-cost:  127     Base:
c ---[ 181]---> Sorter-cost:  127     Base:
c ---[ 179]---> Sorter-cost:  127     Base:
c ---[ 176]---> Sorter-cost:  127     Base:
c ---[ 174]---> Sorter-cost:  127     Base:
c ---[ 172]---> Sorter-cost:  127     Base:
c ---[ 170]---> Sorter-cost:  127     Base:
c ---[ 168]---> Sorter-cost:  127     Base:
c ---[ 166]---> Sorter-cost:  127     Base:
c ---[ 164]---> Sorter-cost:  127     Base:
c ---[ 162]---> Sorter-cost:  127     Base:
c ---[ 160]---> Sorter-cost:  127     Base:
c ---[ 158]---> Sorter-cost:  127     Base:
c ---[ 155]---> Sorter-cost:  127     Base:
c ---[ 153]---> Sorter-cost:  127     Base:
c ---[ 151]---> Sorter-cost:  127     Base:
c ---[ 149]---> Sorter-cost:  127     Base:
c ---[ 147]---> Sorter-cost:  127     Base:
c ---[ 145]---> Sorter-cost:  127     Base:
c ---[ 144]---> BDD-cost:   23
c ---[ 143]---> BDD-cost:   23
c ---[ 142]---> BDD-cost:   23
c ---[ 141]---> BDD-cost:    7
c ---[ 139]---> BDD-cost:    7
c ---[ 138]---> BDD-cost:   50
c ---[ 137]---> BDD-cost:   27
c ---[ 136]---> BDD-cost:   27
c ---[ 135]---> BDD-cost:   27
c ---[ 134]---> BDD-cost:   27
c ---[ 133]---> BDD-cost:   27
c ---[ 132]---> BDD-cost:   50
c ---[ 131]---> BDD-cost:   50
c ---[ 130]---> BDD-cost:   50
c ---[ 128]---> BDD-cost:   27
c ---[ 127]---> BDD-cost:   27
c ---[ 126]---> BDD-cost:   27
c ---[ 125]---> BDD-cost:   48
c ---[ 124]---> BDD-cost:   48
c ---[ 123]---> BDD-cost:   48
c ---[ 122]---> BDD-cost:   27
c ---[ 121]---> BDD-cost:   27
c ---[ 120]---> BDD-cost:   27
c ---[ 119]---> BDD-cost:   50
c ---[ 117]---> BDD-cost:   50
c ---[ 116]---> BDD-cost:   50
c ---[ 115]---> BDD-cost:   27
c ---[ 114]---> BDD-cost:   27
c ---[ 113]---> BDD-cost:   27
c ---[ 112]---> BDD-cost:   48
c ---[ 111]---> BDD-cost:   48
c ---[ 110]---> BDD-cost:   48
c ---[ 109]---> BDD-cost:   27
c ---[ 108]---> BDD-cost:   27
c ---[ 106]---> BDD-cost:   51
c ---[ 104]---> BDD-cost:   27
c ---[ 103]---> BDD-cost:   50
c ---[ 102]---> BDD-cost:   50
c ---[ 101]---> BDD-cost:   50
c ---[ 100]---> BDD-cost:   27
c ---[  99]---> BDD-cost:   27
c ---[  98]---> BDD-cost:   27
c ---[  97]---> BDD-cost:   48
c ---[  96]---> BDD-cost:   48
c ---[  95]---> BDD-cost:   48
c ---[  93]---> BDD-cost:   27
c ---[  92]---> BDD-cost:   27
c ---[  91]---> BDD-cost:   27
c ---[  81]---> BDD-cost:   51
c ---[  69]---> BDD-cost:   51
c ---[  57]---> BDD-cost:   51
c ---[  45]---> BDD-cost:   51
c ---[  33]---> BDD-cost:   51
c ---[  21]---> BDD-cost:   51
c ---[  10]---> BDD-cost:  216
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   25782    84321 |    8594       0        0     nan |  0.000 % |
c |       100 |   25752    84253 |    9453      98     6192    63.2 |  2.792 % |
c ==============================================================================
c Found solution: 1583488
c ---[   0]---> BDD-cost:   13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       220 |   25767    84288 |    8589     218    12443    57.1 |  2.792 % |
c ==============================================================================
c Found solution: 1580928
c ---[   0]---> BDD-cost:   12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       268 |   25776    84312 |    8592     266    20437    76.8 |  2.792 % |
c |       368 |   25776    84312 |    9451     366    22162    60.6 |  2.817 % |
c |       518 |   25776    84312 |   10396     516    29655    57.5 |  2.817 % |
c |       744 |   25776    84312 |   11435     742    42680    57.5 |  2.817 % |
c ==============================================================================
c Found solution: 1508608
c ---[   0]---> BDD-cost:   12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       870 |   25789    84343 |    8596     868    48024    55.3 |  2.817 % |
c |       970 |   25789    84343 |    9455     968    60363    62.4 |  2.829 % |
c |      1120 |   25778    84319 |   10401    1117    68505    61.3 |  2.872 % |
c |      1347 |   25778    84319 |   11441    1344    77932    58.0 |  2.872 % |
c |      1684 |   25778    84319 |   12585    1681   103593    61.6 |  2.872 % |
c |      2190 |   25778    84319 |   13843    2187   126927    58.0 |  2.872 % |
c |      2950 |   25767    84295 |   15228    2946   212260    72.1 |  2.916 % |
c |      4090 |   25767    84295 |   16751    4086   295763    72.4 |  2.916 % |
c |      5798 |   25731    84167 |   18426    5787   492222    85.1 |  2.945 % |
c ==============================================================================
c Found solution: 1477248
c ---[   0]---> BDD-cost:   13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7454 |   25683    83993 |    8561    7434   643106    86.5 |  2.945 % |
c |      7556 |   25683    83993 |    9417    7536   659060    87.5 |  3.056 % |
c |      7706 |   25683    83993 |   10358    7686   665481    86.6 |  3.056 % |
c |      7931 |   25683    83993 |   11394    7911   690952    87.3 |  3.056 % |
c |      8270 |   25672    83969 |   12534    8249   707791    85.8 |  3.099 % |
c |      8776 |   25672    83969 |   13787    8755   792296    90.5 |  3.099 % |
c |      9537 |   25618    83822 |   15166    9509   863713    90.8 |  3.243 % |
c |     10678 |   25536    83532 |   16682   10641   946280    88.9 |  3.358 % |
c |     12386 |   25503    83415 |   18351   12346  1087746    88.1 |  3.387 % |
c |     14949 |   25449    83245 |   20186   14900  1399535    93.9 |  3.488 % |
c |     18793 |   25395    83098 |   22205   18736  1754727    93.7 |  3.632 % |
c ==============================================================================
c Found solution: 1475328
c ---[   0]---> BDD-cost:   12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20218 |   25398    83107 |    8466   20160  1881199    93.3 |  3.632 % |
c |     20322 |   25398    83107 |    9312    5144   289617    56.3 |  3.686 % |
c |     20472 |   25398    83107 |   10243    5294   299464    56.6 |  3.686 % |
c |     20697 |   25398    83107 |   11268    5519   320431    58.1 |  3.686 % |
c |     21034 |   25387    83083 |   12395    5854   334549    57.1 |  3.729 % |
c |     21540 |   25387    83083 |   13634    6360   407264    64.0 |  3.729 % |
c |     22300 |   25354    82966 |   14998    7118   497542    69.9 |  3.758 % |
c |     23439 |   25343    82942 |   16497    8256   599062    72.6 |  3.801 % |
c |     25148 |   25316    82847 |   18147    9957   832837    83.6 |  3.830 % |
c |     27712 |   25316    82847 |   19962   12521  1060640    84.7 |  3.830 % |
c |     31557 |   25316    82847 |   21958   16366  1691483   103.4 |  3.830 % |
c ==============================================================================
c Found solution: 1460608
c ---[   0]---> BDD-cost:    8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     34542 |   25294    82772 |    8431   19345  1961844   101.4 |  3.830 % |
c |     34643 |   25294    82772 |    9274    4938   275109    55.7 |  3.899 % |
c |     34793 |   25294    82772 |   10201    5088   277980    54.6 |  3.899 % |
c |     35019 |   25294    82772 |   11221    5314   292878    55.1 |  3.899 % |
c |     35357 |   25294    82772 |   12343    5652   319785    56.6 |  3.899 % |
c |     35863 |   25294    82772 |   13578    6158   364356    59.2 |  3.899 % |
c |     36623 |   25294    82772 |   14936    6918   441267    63.8 |  3.899 % |
c |     37763 |   25294    82772 |   16429    8058   574366    71.3 |  3.899 % |
c ==============================================================================
c Found solution: 1458688
c ---[   0]---> BDD-cost:   11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     38579 |   25307    82802 |    8435    8874   681730    76.8 |  3.899 % |
c |     38679 |   25307    82802 |    9278    4537   324758    71.6 |  3.910 % |
c |     38830 |   25296    82778 |   10206    4686   329928    70.4 |  3.953 % |
c |     39055 |   25280    82743 |   11226    4907   340655    69.4 |  4.025 % |
c |     39392 |   25204    82492 |   12349    5238   355692    67.9 |  4.168 % |
c ==============================================================================
c Found solution: 1438848
c ---[   0]---> BDD-cost:   12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     39556 |   25216    82524 |    8405    5402   383073    70.9 |  4.168 % |
c |     39656 |   25173    82401 |    9245    5496   384861    70.0 |  4.279 % |
c |     39806 |   25173    82401 |   10170    5646   400312    70.9 |  4.279 % |
c |     40032 |   25151    82353 |   11187    5868   408033    69.5 |  4.365 % |
c |     40369 |   25106    82252 |   12305    6197   430376    69.4 |  4.566 % |
c |     40875 |   25106    82252 |   13536    6703   493435    73.6 |  4.566 % |
c |     41634 |   25106    82252 |   14889    7462   569328    76.3 |  4.566 % |
c |     42773 |   25106    82252 |   16378    8601   707090    82.2 |  4.566 % |
c |     44481 |   25032    82007 |   18016   10298   853239    82.9 |  4.709 % |
c |     47043 |   25021    81983 |   19818   12858  1115212    86.7 |  4.752 % |
c |     50892 |   24980    81840 |   21800   16699  1507898    90.3 |  4.824 % |
c ==============================================================================
c Found solution: 1431808
c ---[   0]---> BDD-cost:   11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     53691 |   24988    81862 |    8329   19495  1771927    90.9 |  4.824 % |
c |     53791 |   24988    81862 |    9161    4974   265913    53.5 |  4.847 % |
c |     53941 |   24988    81862 |   10078    5124   269820    52.7 |  4.847 % |
c |     54167 |   24988    81862 |   11085    5350   286961    53.6 |  4.847 % |
c |     54504 |   24958    81794 |   12194    5679   304170    53.6 |  4.962 % |
c |     55010 |   24958    81794 |   13413    6185   351539    56.8 |  4.962 % |
c |     55769 |   24958    81794 |   14755    6944   416677    60.0 |  4.962 % |
c |     56909 |   24958    81794 |   16230    8084   562839    69.6 |  4.962 % |
c |     58619 |   24947    81770 |   17853    9793   735565    75.1 |  5.005 % |
c |     61182 |   24920    81700 |   19639   12351   959102    77.7 |  5.091 % |
c |     65026 |   24907    81671 |   21603   16193  1315910    81.3 |  5.148 % |
c |     70795 |   24907    81671 |   23763   21962  1922551    87.5 |  5.148 % |
c |     79447 |   24865    81540 |   26139   18016  1482239    82.3 |  5.234 % |
c |     92423 |   24801    81385 |   28753   16615  1259492    75.8 |  5.464 % |
c ==============================================================================
c Found solution: 1427968
c ---[   0]---> BDD-cost:   10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    107128 |   24723    81184 |    8241   16283  1157306    71.1 |  5.464 % |
c |    107230 |   24723    81184 |    9065    8244   476372    57.8 |  5.758 % |
c |    107382 |   24723    81184 |    9971    8396   489220    58.3 |  5.759 % |
c |    107608 |   24723    81184 |   10968    8622   522291    60.6 |  5.759 % |
c |    107945 |   24723    81184 |   12065    8959   555312    62.0 |  5.758 % |
c |    108452 |   24723    81184 |   13272    9466   618197    65.3 |  5.759 % |
c |    109212 |   24678    81023 |   14599   10221   672039    65.8 |  5.787 % |
c |    110351 |   24678    81023 |   16059   11360   765864    67.4 |  5.787 % |
c |    112060 |   24678    81023 |   17665   13069  1024443    78.4 |  5.787 % |
c |    114622 |   24620    80894 |   19431   15623  1365937    87.4 |  6.031 % |
c |    118467 |   24590    80816 |   21375   19460  1763317    90.6 |  6.131 % |
c |    124235 |   24590    80816 |   23512   14161  1019179    72.0 |  6.131 % |
c |    132891 |   24551    80683 |   25863   22813  1779717    78.0 |  6.203 % |
c |    145865 |   24551    80683 |   28450   22536  2054772    91.2 |  6.203 % |
c ==============================================================================
c Found solution: 1423488
c ---[   0]---> BDD-cost:   11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    146568 |   24563    80714 |    8187   23239  2124527    91.4 |  6.203 % |
c |    146668 |   24563    80714 |    9005    5910   256320    43.4 |  6.210 % |
c |    146819 |   24563    80714 |    9906    6061   262458    43.3 |  6.210 % |
c |    147044 |   24463    80383 |   10896    6275   285602    45.5 |  6.410 % |
c |    147381 |   24423    80256 |   11986    6604   292865    44.3 |  6.496 % |
c |    147887 |   24423    80256 |   13185    7110   338836    47.7 |  6.496 % |
c |    148646 |   24423    80256 |   14503    7869   435930    55.4 |  6.496 % |
c |    149788 |   24423    80256 |   15954    9011   542343    60.2 |  6.496 % |
c |    151497 |   24406    80218 |   17549   10719   752216    70.2 |  6.567 % |
c |    154060 |   24386    80171 |   19304   13280   990365    74.6 |  6.639 % |
c |    157906 |   24386    80171 |   21234   17126  1287121    75.2 |  6.639 % |
c |    163672 |   24340    80044 |   23358   11559   700256    60.6 |  6.796 % |
c |    172321 |   24340    80044 |   25694   20208  1333788    66.0 |  6.796 % |
c |    185296 |   24314    79967 |   28263   19623  1161767    59.2 |  6.854 % |
c |    204758 |   24314    79967 |   31090   23903  1595766    66.8 |  6.854 % |
c |    233951 |   24224    79722 |   34199   21100  1491804    70.7 |  7.154 % |
c ==============================================================================
c Found solution: 1420288
c ---[   0]---> BDD-cost:   10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    269048 |   24088    79244 |    8029   16815  1491486    88.7 |  7.154 % |
c |    269148 |   24088    79244 |    8831    8508   640879    75.3 |  7.459 % |
c |    269298 |   24088    79244 |    9715    8658   661275    76.4 |  7.459 % |
c |    269523 |   24088    79244 |   10686    8883   678039    76.3 |  7.459 % |
c |    269860 |   24088    79244 |   11755    9220   719171    78.0 |  7.460 % |
c |    270367 |   24088    79244 |   12930    9727   729922    75.0 |  7.459 % |
c |    271127 |   24088    79244 |   14223   10487   840546    80.2 |  7.459 % |
c |    272266 |   24073    79211 |   15646   11624   968142    83.3 |  7.516 % |
c |    273975 |   24073    79211 |   17210   13333  1152071    86.4 |  7.516 % |
c |    276537 |   24045    79149 |   18931   15889  1433911    90.2 |  7.631 % |
c |    280383 |   23865    78603 |   20825   19704  1796107    91.2 |  8.117 % |
c |    286151 |   23865    78603 |   22907   14391  1054594    73.3 |  8.117 % |
c |    294801 |   23865    78603 |   25198   23041  1954414    84.8 |  8.117 % |
c |    307776 |   23854    78579 |   27718   22285  2001861    89.8 |  8.159 % |
c |    327237 |   23847    78564 |   30490   27154  2268727    83.6 |  8.188 % |
c |    356429 |   23803    78464 |   33539   24241  1688878    69.7 |  8.402 % |
c ==============================================================================
c Found solution: 1416448
c ---[   0]---> BDD-cost:   10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    384550 |   23765    78382 |    7921   32917  2863259    87.0 |  8.402 % |
c |    384650 |   23754    78358 |    8713    7690   702581    91.4 |  8.665 % |
c |    384801 |   23754    78358 |    9584    7841   714078    91.1 |  8.665 % |
c |    385027 |   23754    78358 |   10542    8067   743664    92.2 |  8.665 % |
c |    385364 |   23754    78358 |   11597    8404   790915    94.1 |  8.665 % |
c |    385870 |   23678    78088 |   12756    8901   805477    90.5 |  8.822 % |
c |    386631 |   23678    78088 |   14032    9662   860772    89.1 |  8.822 % |
c |    387773 |   23678    78088 |   15435   10804  1046707    96.9 |  8.822 % |
c |    389481 |   23678    78088 |   16979   12512  1164690    93.1 |  8.822 % |
c |    392043 |   23678    78088 |   18677   15074  1561117   103.6 |  8.822 % |
c |    395887 |   23678    78088 |   20545   18918  1996674   105.5 |  8.822 % |
c |    401654 |   23678    78088 |   22599   13746  1222434    88.9 |  8.822 % |
c |    410306 |   23665    78059 |   24859   22395  2137343    95.4 |  8.879 % |
c |    423280 |   23647    77997 |   27345   21922  2153316    98.2 |  8.908 % |

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/6746/stat): 6746 (minisat+_script) R 6745 6746 19316 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1855431038 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/6746/statm): 174 3 169 147 0 27 0
[pid=6746] 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=6747
New process pid=6748
New process pid=6749
execve syscall for /bin/sed executable
One traced child (pid=6748) 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=6749) exited with status: 0
One traced child (pid=6747) exited with status: 0
New process pid=6750
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-13-7-misc07.opb

[startup+10.0037 s]
Raw data (loadavg): 1.11 1.01 0.98 2/57 6750
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 1624 0 0 0 979 6 0 0 25 0 1 0 1855431043 6725632 1526 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 1642 1526 145 145 0 1497 0
[pid=6750] vsize: 6568
Current children cumulated CPU time (s) 9.86
Current children cumulated vsize (Kb) 8692

[startup+20.0053 s]
Raw data (loadavg): 1.10 1.01 0.98 2/57 6750
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 2189 0 0 0 1969 10 0 0 25 0 1 0 1855431043 9052160 2091 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6750/statm): 2210 2091 145 145 0 2065 0
[pid=6750] vsize: 8840
Current children cumulated CPU time (s) 19.8
Current children cumulated vsize (Kb) 10964

[startup+30.0059 s]
Raw data (loadavg): 1.08 1.01 0.98 2/57 6750
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 2692 0 0 0 2959 14 0 0 25 0 1 0 1855431043 11096064 2594 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 2709 2594 145 145 0 2564 0
[pid=6750] vsize: 10836
Current children cumulated CPU time (s) 29.74
Current children cumulated vsize (Kb) 12960

[startup+40.0065 s]
Raw data (loadavg): 1.07 1.01 0.98 2/57 6750
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 3153 0 0 0 3950 19 0 0 25 0 1 0 1855431043 13033472 3055 4294967295 134512640 135094434 3221224432 3221223088 134558172 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 3182 3055 145 145 0 3037 0
[pid=6750] vsize: 12728
Current children cumulated CPU time (s) 39.7
Current children cumulated vsize (Kb) 14852

[startup+50.0071 s]
Raw data (loadavg): 1.06 1.01 0.98 2/57 6750
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 3195 0 0 0 4949 19 0 0 25 0 1 0 1855431043 13201408 3097 4294967295 134512640 135094434 3221224432 3221223024 134556958 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 3223 3097 145 145 0 3078 0
[pid=6750] vsize: 12892
Current children cumulated CPU time (s) 49.69
Current children cumulated vsize (Kb) 15016

[startup+60.0087 s]
Raw data (loadavg): 1.05 1.01 0.98 2/57 6750
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 3195 0 0 0 5948 20 0 0 25 0 1 0 1855431043 13201408 3097 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 3223 3097 145 145 0 3078 0
[pid=6750] vsize: 12892
Current children cumulated CPU time (s) 59.69
Current children cumulated vsize (Kb) 15016

[startup+70.0093 s]
Raw data (loadavg): 1.04 1.01 0.98 2/57 6750
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 3335 0 0 0 6946 21 0 0 25 0 1 0 1855431043 13770752 3237 4294967295 134512640 135094434 3221224432 3221223056 134562051 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 3362 3237 145 145 0 3217 0
[pid=6750] vsize: 13448
Current children cumulated CPU time (s) 69.68
Current children cumulated vsize (Kb) 15572

[startup+80.0099 s]
Raw data (loadavg): 1.03 1.01 0.98 2/57 6750
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 3335 0 0 0 7945 22 0 0 25 0 1 0 1855431043 13770752 3237 4294967295 134512640 135094434 3221224432 3221223056 134562152 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 3362 3237 145 145 0 3217 0
[pid=6750] vsize: 13448
Current children cumulated CPU time (s) 79.68
Current children cumulated vsize (Kb) 15572

[startup+90.0115 s]
Raw data (loadavg): 1.03 1.01 0.98 2/57 6750
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 3335 0 0 0 8945 22 0 0 25 0 1 0 1855431043 13770752 3237 4294967295 134512640 135094434 3221224432 3221223104 134555568 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 3362 3237 145 145 0 3217 0
[pid=6750] vsize: 13448
Current children cumulated CPU time (s) 89.68
Current children cumulated vsize (Kb) 15572

[startup+100.012 s]
Raw data (loadavg): 1.02 1.01 0.98 2/57 6750
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 3335 0 0 0 9945 22 0 0 25 0 1 0 1855431043 13770752 3237 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 3362 3237 145 145 0 3217 0
[pid=6750] vsize: 13448
Current children cumulated CPU time (s) 99.68
Current children cumulated vsize (Kb) 15572

[startup+110.014 s]
Raw data (loadavg): 1.02 1.00 0.98 2/57 6750
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 3335 0 0 0 10944 23 0 0 25 0 1 0 1855431043 13770752 3237 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 3362 3237 145 145 0 3217 0
[pid=6750] vsize: 13448
Current children cumulated CPU time (s) 109.68
Current children cumulated vsize (Kb) 15572

[startup+120.015 s]
Raw data (loadavg): 1.10 1.02 0.98 2/57 6750
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 3335 0 0 0 11944 23 0 0 25 0 1 0 1855431043 13770752 3237 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 3362 3237 145 145 0 3217 0
[pid=6750] vsize: 13448
Current children cumulated CPU time (s) 119.68
Current children cumulated vsize (Kb) 15572

[startup+130.016 s]
Raw data (loadavg): 1.08 1.02 0.98 2/57 6750
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 3335 0 0 0 12944 23 0 0 25 0 1 0 1855431043 13770752 3237 4294967295 134512640 135094434 3221224432 3221223024 134557236 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 3362 3237 145 145 0 3217 0
[pid=6750] vsize: 13448
Current children cumulated CPU time (s) 129.68
Current children cumulated vsize (Kb) 15572

[startup+140.017 s]
Raw data (loadavg): 1.07 1.02 0.98 2/57 6750
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 3335 0 0 0 13943 24 0 0 25 0 1 0 1855431043 13770752 3237 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 3362 3237 145 145 0 3217 0
[pid=6750] vsize: 13448
Current children cumulated CPU time (s) 139.68
Current children cumulated vsize (Kb) 15572

[startup+150.017 s]
Raw data (loadavg): 1.06 1.02 0.98 2/57 6750
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 3434 0 0 0 14942 25 0 0 25 0 1 0 1855431043 14172160 3336 4294967295 134512640 135094434 3221224432 3221223088 134557903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 3460 3336 145 145 0 3315 0
[pid=6750] vsize: 13840
Current children cumulated CPU time (s) 149.68
Current children cumulated vsize (Kb) 15964

[startup+160.018 s]
Raw data (loadavg): 1.20 1.05 0.99 3/60 6791
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 3754 0 0 0 15926 36 0 0 19 0 1 0 1855431043 15482880 3656 4294967295 134512640 135094434 3221224432 3221222160 134562860 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6750/statm): 3780 3656 145 145 0 3635 0
[pid=6750] vsize: 15120
Current children cumulated CPU time (s) 159.63
Current children cumulated vsize (Kb) 17244

[startup+170.018 s]
Raw data (loadavg): 1.17 1.05 0.99 2/57 6801
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 3754 0 0 0 16925 38 0 0 25 0 1 0 1855431043 15482880 3656 4294967295 134512640 135094434 3221224432 3221223024 134557512 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 3780 3656 145 145 0 3635 0
[pid=6750] vsize: 15120
Current children cumulated CPU time (s) 169.64
Current children cumulated vsize (Kb) 17244

[startup+180.019 s]
Raw data (loadavg): 1.14 1.05 0.99 2/57 6801
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 3761 0 0 0 17925 38 0 0 25 0 1 0 1855431043 15515648 3663 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 3788 3663 145 145 0 3643 0
[pid=6750] vsize: 15152
Current children cumulated CPU time (s) 179.64
Current children cumulated vsize (Kb) 17276

[startup+190.019 s]
Raw data (loadavg): 1.12 1.04 0.99 2/57 6801
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 3768 0 0 0 18925 38 0 0 25 0 1 0 1855431043 15548416 3670 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 3796 3670 145 145 0 3651 0
[pid=6750] vsize: 15184
Current children cumulated CPU time (s) 189.64
Current children cumulated vsize (Kb) 17308

[startup+200.02 s]
Raw data (loadavg): 1.10 1.04 0.99 2/57 6801
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 3924 0 0 0 19923 39 0 0 25 0 1 0 1855431043 16195584 3826 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 3954 3826 145 145 0 3809 0
[pid=6750] vsize: 15816
Current children cumulated CPU time (s) 199.63
Current children cumulated vsize (Kb) 17940

[startup+210.022 s]
Raw data (loadavg): 1.09 1.04 0.99 2/57 6801
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 4240 0 0 0 20916 42 0 0 25 0 1 0 1855431043 17477632 4142 4294967295 134512640 135094434 3221224432 3221223104 134555606 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 4267 4142 145 145 0 4122 0
[pid=6750] vsize: 17068
Current children cumulated CPU time (s) 209.59
Current children cumulated vsize (Kb) 19192

[startup+220.022 s]
Raw data (loadavg): 1.07 1.04 0.99 2/57 6801
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 4240 0 0 0 21916 42 0 0 25 0 1 0 1855431043 17477632 4142 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 4267 4142 145 145 0 4122 0
[pid=6750] vsize: 17068
Current children cumulated CPU time (s) 219.59
Current children cumulated vsize (Kb) 19192

[startup+230.023 s]
Raw data (loadavg): 1.06 1.04 0.99 2/57 6803
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 4240 0 0 0 22916 42 0 0 25 0 1 0 1855431043 17477632 4142 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 4267 4142 145 145 0 4122 0
[pid=6750] vsize: 17068
Current children cumulated CPU time (s) 229.59
Current children cumulated vsize (Kb) 19192

[startup+240.024 s]
Raw data (loadavg): 1.05 1.03 0.99 2/57 6805
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 4287 0 0 0 23916 42 0 0 25 0 1 0 1855431043 17686528 4189 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 4318 4189 145 145 0 4173 0
[pid=6750] vsize: 17272
Current children cumulated CPU time (s) 239.59
Current children cumulated vsize (Kb) 19396

[startup+250.024 s]
Raw data (loadavg): 1.04 1.03 0.99 2/57 6805
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 4323 0 0 0 24916 43 0 0 25 0 1 0 1855431043 17866752 4225 4294967295 134512640 135094434 3221224432 3221223088 134557872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 4362 4225 145 145 0 4217 0
[pid=6750] vsize: 17448
Current children cumulated CPU time (s) 249.6
Current children cumulated vsize (Kb) 19572

[startup+260.026 s]
Raw data (loadavg): 1.04 1.03 0.99 2/57 6805
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 4379 0 0 0 25916 43 0 0 25 0 1 0 1855431043 18161664 4281 4294967295 134512640 135094434 3221224432 3221223088 134556605 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 4434 4281 145 145 0 4289 0
[pid=6750] vsize: 17736
Current children cumulated CPU time (s) 259.6
Current children cumulated vsize (Kb) 19860

[startup+270.026 s]
Raw data (loadavg): 1.03 1.03 0.99 2/57 6805
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 4379 0 0 0 26916 43 0 0 25 0 1 0 1855431043 18161664 4281 4294967295 134512640 135094434 3221224432 3221223104 134556279 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 4434 4281 145 145 0 4289 0
[pid=6750] vsize: 17736
Current children cumulated CPU time (s) 269.6
Current children cumulated vsize (Kb) 19860

[startup+280.026 s]
Raw data (loadavg): 1.02 1.03 0.99 2/57 6805
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 4379 0 0 0 27916 43 0 0 25 0 1 0 1855431043 18161664 4281 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 4434 4281 145 145 0 4289 0
[pid=6750] vsize: 17736
Current children cumulated CPU time (s) 279.6
Current children cumulated vsize (Kb) 19860

[startup+290.026 s]
Raw data (loadavg): 1.02 1.03 0.99 2/57 6805
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 4379 0 0 0 28917 43 0 0 25 0 1 0 1855431043 18161664 4281 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 4434 4281 145 145 0 4289 0
[pid=6750] vsize: 17736
Current children cumulated CPU time (s) 289.61
Current children cumulated vsize (Kb) 19860

[startup+300.027 s]
Raw data (loadavg): 1.02 1.03 0.99 2/57 6805
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 4379 0 0 0 29917 43 0 0 25 0 1 0 1855431043 18161664 4281 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 4434 4281 145 145 0 4289 0
[pid=6750] vsize: 17736
Current children cumulated CPU time (s) 299.61
Current children cumulated vsize (Kb) 19860

[startup+310.028 s]
Raw data (loadavg): 1.01 1.02 0.99 2/57 6805
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 4380 0 0 0 30916 43 0 0 25 0 1 0 1855431043 18161664 4282 4294967295 134512640 135094434 3221224432 3221223104 134556317 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 4434 4282 145 145 0 4289 0
[pid=6750] vsize: 17736
Current children cumulated CPU time (s) 309.6
Current children cumulated vsize (Kb) 19860

[startup+320.028 s]
Raw data (loadavg): 1.01 1.02 0.99 2/57 6805
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 4382 0 0 0 31916 43 0 0 25 0 1 0 1855431043 18161664 4284 4294967295 134512640 135094434 3221224432 3221223024 134557500 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 4434 4284 145 145 0 4289 0
[pid=6750] vsize: 17736
Current children cumulated CPU time (s) 319.6
Current children cumulated vsize (Kb) 19860

[startup+330.029 s]
Raw data (loadavg): 1.01 1.02 0.99 2/57 6805
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 4382 0 0 0 32916 43 0 0 25 0 1 0 1855431043 18161664 4284 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 4434 4284 145 145 0 4289 0
[pid=6750] vsize: 17736
Current children cumulated CPU time (s) 329.6
Current children cumulated vsize (Kb) 19860

[startup+340.029 s]
Raw data (loadavg): 1.01 1.02 0.99 2/57 6805
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 4382 0 0 0 33916 43 0 0 25 0 1 0 1855431043 18161664 4284 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 4434 4284 145 145 0 4289 0
[pid=6750] vsize: 17736
Current children cumulated CPU time (s) 339.6
Current children cumulated vsize (Kb) 19860

[startup+350.029 s]
Raw data (loadavg): 1.01 1.02 0.99 2/57 6805
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 4382 0 0 0 34917 43 0 0 25 0 1 0 1855431043 18161664 4284 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 4434 4284 145 145 0 4289 0
[pid=6750] vsize: 17736
Current children cumulated CPU time (s) 349.61
Current children cumulated vsize (Kb) 19860

[startup+360.03 s]
Raw data (loadavg): 1.00 1.02 0.99 2/57 6805
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 4382 0 0 0 35917 43 0 0 25 0 1 0 1855431043 18161664 4284 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 4434 4284 145 145 0 4289 0
[pid=6750] vsize: 17736
Current children cumulated CPU time (s) 359.61
Current children cumulated vsize (Kb) 19860

[startup+370.03 s]
Raw data (loadavg): 1.00 1.02 0.99 2/57 6805
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 4382 0 0 0 36917 43 0 0 25 0 1 0 1855431043 18161664 4284 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 4434 4284 145 145 0 4289 0
[pid=6750] vsize: 17736
Current children cumulated CPU time (s) 369.61
Current children cumulated vsize (Kb) 19860

[startup+380.031 s]
Raw data (loadavg): 1.00 1.02 0.99 2/57 6805
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 4382 0 0 0 37917 43 0 0 25 0 1 0 1855431043 18161664 4284 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 4434 4284 145 145 0 4289 0
[pid=6750] vsize: 17736
Current children cumulated CPU time (s) 379.61
Current children cumulated vsize (Kb) 19860

[startup+390.031 s]
Raw data (loadavg): 1.00 1.02 0.99 2/57 6805
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 4382 0 0 0 38917 43 0 0 25 0 1 0 1855431043 18161664 4284 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 4434 4284 145 145 0 4289 0
[pid=6750] vsize: 17736
Current children cumulated CPU time (s) 389.61
Current children cumulated vsize (Kb) 19860

[startup+400.032 s]
Raw data (loadavg): 1.00 1.02 0.99 2/57 6805
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 4382 0 0 0 39917 43 0 0 25 0 1 0 1855431043 18161664 4284 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 4434 4284 145 145 0 4289 0
[pid=6750] vsize: 17736
Current children cumulated CPU time (s) 399.61
Current children cumulated vsize (Kb) 19860

[startup+410.033 s]
Raw data (loadavg): 1.00 1.01 0.99 2/57 6805
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 4382 0 0 0 40918 43 0 0 25 0 1 0 1855431043 18161664 4284 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 4434 4284 145 145 0 4289 0
[pid=6750] vsize: 17736
Current children cumulated CPU time (s) 409.62
Current children cumulated vsize (Kb) 19860

[startup+420.033 s]
Raw data (loadavg): 1.00 1.01 0.99 2/57 6805
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 4382 0 0 0 41918 43 0 0 25 0 1 0 1855431043 18161664 4284 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 4434 4284 145 145 0 4289 0
[pid=6750] vsize: 17736
Current children cumulated CPU time (s) 419.62
Current children cumulated vsize (Kb) 19860

[startup+430.034 s]
Raw data (loadavg): 1.00 1.01 0.99 2/57 6805
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 4382 0 0 0 42918 43 0 0 25 0 1 0 1855431043 18161664 4284 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 4434 4284 145 145 0 4289 0
[pid=6750] vsize: 17736
Current children cumulated CPU time (s) 429.62
Current children cumulated vsize (Kb) 19860

[startup+440.034 s]
Raw data (loadavg): 1.00 1.01 0.99 2/57 6805
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 4383 0 0 0 43918 43 0 0 25 0 1 0 1855431043 18161664 4285 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 4434 4285 145 145 0 4289 0
[pid=6750] vsize: 17736
Current children cumulated CPU time (s) 439.62
Current children cumulated vsize (Kb) 19860

[startup+450.035 s]
Raw data (loadavg): 1.00 1.01 0.99 2/57 6805
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 4426 0 0 0 44918 43 0 0 25 0 1 0 1855431043 18374656 4328 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 4486 4328 145 145 0 4341 0
[pid=6750] vsize: 17944
Current children cumulated CPU time (s) 449.62
Current children cumulated vsize (Kb) 20068

[startup+460.036 s]
Raw data (loadavg): 1.00 1.01 0.99 2/57 6805
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 4476 0 0 0 45918 43 0 0 25 0 1 0 1855431043 18636800 4378 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 4550 4378 145 145 0 4405 0
[pid=6750] vsize: 18200
Current children cumulated CPU time (s) 459.62
Current children cumulated vsize (Kb) 20324

[startup+470.036 s]
Raw data (loadavg): 1.00 1.01 0.99 2/57 6805
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 4502 0 0 0 46919 43 0 0 25 0 1 0 1855431043 18767872 4404 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 4582 4404 145 145 0 4437 0
[pid=6750] vsize: 18328
Current children cumulated CPU time (s) 469.63
Current children cumulated vsize (Kb) 20452

[startup+480.036 s]
Raw data (loadavg): 1.00 1.01 0.99 2/57 6805
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 4551 0 0 0 47919 43 0 0 25 0 1 0 1855431043 19025920 4453 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6750/statm): 4645 4453 145 145 0 4500 0
[pid=6750] vsize: 18580
Current children cumulated CPU time (s) 479.63
Current children cumulated vsize (Kb) 20704

[startup+490.036 s]
Raw data (loadavg): 1.00 1.01 0.99 2/57 6807
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 4551 0 0 0 48918 44 0 0 25 0 1 0 1855431043 19025920 4453 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6750/statm): 4645 4453 145 145 0 4500 0
[pid=6750] vsize: 18580
Current children cumulated CPU time (s) 489.63
Current children cumulated vsize (Kb) 20704

[startup+500.037 s]
Raw data (loadavg): 1.00 1.01 0.99 2/57 6807
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 4564 0 0 0 49917 45 0 0 25 0 1 0 1855431043 19091456 4466 4294967295 134512640 135094434 3221224432 3221223120 134554736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6750/statm): 4661 4466 145 145 0 4516 0
[pid=6750] vsize: 18644
Current children cumulated CPU time (s) 499.63
Current children cumulated vsize (Kb) 20768

[startup+510.038 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 6807
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 4575 0 0 0 50917 45 0 0 25 0 1 0 1855431043 19156992 4477 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6750/statm): 4677 4477 145 145 0 4532 0
[pid=6750] vsize: 18708
Current children cumulated CPU time (s) 509.63
Current children cumulated vsize (Kb) 20832

[startup+520.038 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 6807
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 4596 0 0 0 51917 46 0 0 25 0 1 0 1855431043 19288064 4498 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6750/statm): 4709 4498 145 145 0 4564 0
[pid=6750] vsize: 18836
Current children cumulated CPU time (s) 519.64
Current children cumulated vsize (Kb) 20960

[startup+530.039 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 6807
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 4666 0 0 0 52916 46 0 0 25 0 1 0 1855431043 19681280 4568 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6750/statm): 4805 4568 145 145 0 4660 0
[pid=6750] vsize: 19220
Current children cumulated CPU time (s) 529.63
Current children cumulated vsize (Kb) 21344

[startup+540.039 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 6807
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 4696 0 0 0 53916 47 0 0 25 0 1 0 1855431043 19812352 4598 4294967295 134512640 135094434 3221224432 3221223024 134557230 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6750/statm): 4837 4598 145 145 0 4692 0
[pid=6750] vsize: 19348
Current children cumulated CPU time (s) 539.64
Current children cumulated vsize (Kb) 21472

[startup+550.04 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 6807
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 4696 0 0 0 54915 47 0 0 25 0 1 0 1855431043 19812352 4598 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6750/statm): 4837 4598 145 145 0 4692 0
[pid=6750] vsize: 19348
Current children cumulated CPU time (s) 549.63
Current children cumulated vsize (Kb) 21472

[startup+560.041 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 6807
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 4696 0 0 0 55914 49 0 0 25 0 1 0 1855431043 19812352 4598 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 4837 4598 145 145 0 4692 0
[pid=6750] vsize: 19348
Current children cumulated CPU time (s) 559.64
Current children cumulated vsize (Kb) 21472

[startup+570.041 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 6807
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 4696 0 0 0 56914 49 0 0 25 0 1 0 1855431043 19812352 4598 4294967295 134512640 135094434 3221224432 3221223088 134558169 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 4837 4598 145 145 0 4692 0
[pid=6750] vsize: 19348
Current children cumulated CPU time (s) 569.64
Current children cumulated vsize (Kb) 21472

[startup+580.041 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 6807
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 4698 0 0 0 57915 49 0 0 25 0 1 0 1855431043 19812352 4600 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 4837 4600 145 145 0 4692 0
[pid=6750] vsize: 19348
Current children cumulated CPU time (s) 579.65
Current children cumulated vsize (Kb) 21472

[startup+590.042 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 6807
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 4699 0 0 0 58915 49 0 0 25 0 1 0 1855431043 19812352 4601 4294967295 134512640 135094434 3221224432 3221223088 134558022 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 4837 4601 145 145 0 4692 0
[pid=6750] vsize: 19348
Current children cumulated CPU time (s) 589.65
Current children cumulated vsize (Kb) 21472

[startup+600.042 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 6807
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 4699 0 0 0 59915 49 0 0 25 0 1 0 1855431043 19812352 4601 4294967295 134512640 135094434 3221224432 3221223104 134556210 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 4837 4601 145 145 0 4692 0
[pid=6750] vsize: 19348
Current children cumulated CPU time (s) 599.65
Current children cumulated vsize (Kb) 21472

[startup+610.043 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 6807
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 4966 0 0 0 60911 50 0 0 25 0 1 0 1855431043 20905984 4868 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 5104 4868 145 145 0 4959 0
[pid=6750] vsize: 20416
Current children cumulated CPU time (s) 609.62
Current children cumulated vsize (Kb) 22540

[startup+620.043 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 6807
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 5113 0 0 0 61907 51 0 0 25 0 1 0 1855431043 21508096 5015 4294967295 134512640 135094434 3221224432 3221222896 134781535 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 5251 5015 145 145 0 5106 0
[pid=6750] vsize: 21004
Current children cumulated CPU time (s) 619.59
Current children cumulated vsize (Kb) 23128

[startup+630.043 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 6807
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 5113 0 0 0 62908 51 0 0 25 0 1 0 1855431043 21508096 5015 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 5251 5015 145 145 0 5106 0
[pid=6750] vsize: 21004
Current children cumulated CPU time (s) 629.6
Current children cumulated vsize (Kb) 23128

[startup+640.044 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 6807
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 5113 0 0 0 63908 51 0 0 25 0 1 0 1855431043 21508096 5015 4294967295 134512640 135094434 3221224432 3221223056 134557714 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 5251 5015 145 145 0 5106 0
[pid=6750] vsize: 21004
Current children cumulated CPU time (s) 639.6
Current children cumulated vsize (Kb) 23128

[startup+650.044 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 6807
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 5113 0 0 0 64908 51 0 0 25 0 1 0 1855431043 21508096 5015 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 5251 5015 145 145 0 5106 0
[pid=6750] vsize: 21004
Current children cumulated CPU time (s) 649.6
Current children cumulated vsize (Kb) 23128

[startup+660.045 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 6807
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 5355 0 0 0 65904 53 0 0 25 0 1 0 1855431043 22626304 5257 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 5524 5257 145 145 0 5379 0
[pid=6750] vsize: 22096
Current children cumulated CPU time (s) 659.58
Current children cumulated vsize (Kb) 24220

[startup+670.045 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 6807
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 5785 0 0 0 66897 56 0 0 25 0 1 0 1855431043 24375296 5687 4294967295 134512640 135094434 3221224432 3221223024 134551428 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 5951 5687 145 145 0 5806 0
[pid=6750] vsize: 23804
Current children cumulated CPU time (s) 669.54
Current children cumulated vsize (Kb) 25928

[startup+680.046 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 6807
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 5785 0 0 0 67897 56 0 0 25 0 1 0 1855431043 24375296 5687 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 5951 5687 145 145 0 5806 0
[pid=6750] vsize: 23804
Current children cumulated CPU time (s) 679.54
Current children cumulated vsize (Kb) 25928

[startup+690.047 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 6807
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 5785 0 0 0 68897 56 0 0 25 0 1 0 1855431043 24375296 5687 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 5951 5687 145 145 0 5806 0
[pid=6750] vsize: 23804
Current children cumulated CPU time (s) 689.54
Current children cumulated vsize (Kb) 25928

[startup+700.047 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 6807
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 5785 0 0 0 69898 56 0 0 25 0 1 0 1855431043 24375296 5687 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 5951 5687 145 145 0 5806 0
[pid=6750] vsize: 23804
Current children cumulated CPU time (s) 699.55
Current children cumulated vsize (Kb) 25928

[startup+710.049 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 6807
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 5785 0 0 0 70898 56 0 0 25 0 1 0 1855431043 24375296 5687 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 5951 5687 145 145 0 5806 0
[pid=6750] vsize: 23804
Current children cumulated CPU time (s) 709.55
Current children cumulated vsize (Kb) 25928

[startup+720.049 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 6807
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6184 0 0 0 71890 59 0 0 25 0 1 0 1855431043 26009600 6086 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 6350 6086 145 145 0 6205 0
[pid=6750] vsize: 25400
Current children cumulated CPU time (s) 719.5
Current children cumulated vsize (Kb) 27524

[startup+730.05 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 6807
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6263 0 0 0 72888 60 0 0 25 0 1 0 1855431043 26324992 6165 4294967295 134512640 135094434 3221224432 3221223088 134558246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 6427 6165 145 145 0 6282 0
[pid=6750] vsize: 25708
Current children cumulated CPU time (s) 729.49
Current children cumulated vsize (Kb) 27832

[startup+740.052 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 6807
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6263 0 0 0 73889 60 0 0 25 0 1 0 1855431043 26324992 6165 4294967295 134512640 135094434 3221224432 3221223024 134556727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 6427 6165 145 145 0 6282 0
[pid=6750] vsize: 25708
Current children cumulated CPU time (s) 739.5
Current children cumulated vsize (Kb) 27832

[startup+750.052 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 6807
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6263 0 0 0 74889 61 0 0 25 0 1 0 1855431043 26324992 6165 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6750/statm): 6427 6165 145 145 0 6282 0
[pid=6750] vsize: 25708
Current children cumulated CPU time (s) 749.51
Current children cumulated vsize (Kb) 27832

[startup+760.053 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 6807
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6263 0 0 0 75888 61 0 0 25 0 1 0 1855431043 26324992 6165 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 6427 6165 145 145 0 6282 0
[pid=6750] vsize: 25708
Current children cumulated CPU time (s) 759.5
Current children cumulated vsize (Kb) 27832

[startup+770.053 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 6807
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6263 0 0 0 76888 61 0 0 25 0 1 0 1855431043 26324992 6165 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 6427 6165 145 145 0 6282 0
[pid=6750] vsize: 25708
Current children cumulated CPU time (s) 769.5
Current children cumulated vsize (Kb) 27832

[startup+780.054 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 6807
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6263 0 0 0 77888 61 0 0 25 0 1 0 1855431043 26324992 6165 4294967295 134512640 135094434 3221224432 3221223088 134558246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 6427 6165 145 145 0 6282 0
[pid=6750] vsize: 25708
Current children cumulated CPU time (s) 779.5
Current children cumulated vsize (Kb) 27832

[startup+790.054 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 6807
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6263 0 0 0 78889 61 0 0 25 0 1 0 1855431043 26324992 6165 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 6427 6165 145 145 0 6282 0
[pid=6750] vsize: 25708
Current children cumulated CPU time (s) 789.51
Current children cumulated vsize (Kb) 27832

[startup+800.055 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 6807
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6263 0 0 0 79889 61 0 0 25 0 1 0 1855431043 26324992 6165 4294967295 134512640 135094434 3221224432 3221223088 134558129 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 6427 6165 145 145 0 6282 0
[pid=6750] vsize: 25708
Current children cumulated CPU time (s) 799.51
Current children cumulated vsize (Kb) 27832

[startup+810.057 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 6807
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6263 0 0 0 80889 61 0 0 25 0 1 0 1855431043 26324992 6165 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 6427 6165 145 145 0 6282 0
[pid=6750] vsize: 25708
Current children cumulated CPU time (s) 809.51
Current children cumulated vsize (Kb) 27832

[startup+820.057 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 6807
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6263 0 0 0 81889 61 0 0 25 0 1 0 1855431043 26324992 6165 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 6427 6165 145 145 0 6282 0
[pid=6750] vsize: 25708
Current children cumulated CPU time (s) 819.51
Current children cumulated vsize (Kb) 27832

[startup+830.057 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 6807
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6263 0 0 0 82889 61 0 0 25 0 1 0 1855431043 26324992 6165 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 6427 6165 145 145 0 6282 0
[pid=6750] vsize: 25708
Current children cumulated CPU time (s) 829.51
Current children cumulated vsize (Kb) 27832

[startup+840.058 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 6807
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6263 0 0 0 83890 61 0 0 25 0 1 0 1855431043 26324992 6165 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 6427 6165 145 145 0 6282 0
[pid=6750] vsize: 25708
Current children cumulated CPU time (s) 839.52
Current children cumulated vsize (Kb) 27832

[startup+850.058 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 6807
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6263 0 0 0 84890 61 0 0 25 0 1 0 1855431043 26324992 6165 4294967295 134512640 135094434 3221224432 3221223088 134558022 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 6427 6165 145 145 0 6282 0
[pid=6750] vsize: 25708
Current children cumulated CPU time (s) 849.52
Current children cumulated vsize (Kb) 27832

[startup+860.059 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 6807
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6263 0 0 0 85890 61 0 0 25 0 1 0 1855431043 26324992 6165 4294967295 134512640 135094434 3221224432 3221222896 134781514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 6427 6165 145 145 0 6282 0
[pid=6750] vsize: 25708
Current children cumulated CPU time (s) 859.52
Current children cumulated vsize (Kb) 27832

[startup+870.059 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 6807
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6263 0 0 0 86890 61 0 0 25 0 1 0 1855431043 26324992 6165 4294967295 134512640 135094434 3221224432 3221223024 134557416 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 6427 6165 145 145 0 6282 0
[pid=6750] vsize: 25708
Current children cumulated CPU time (s) 869.52
Current children cumulated vsize (Kb) 27832

[startup+880.06 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 6807
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6263 0 0 0 87891 61 0 0 25 0 1 0 1855431043 26324992 6165 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 6427 6165 145 145 0 6282 0
[pid=6750] vsize: 25708
Current children cumulated CPU time (s) 879.53
Current children cumulated vsize (Kb) 27832

[startup+890.061 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 6807
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6263 0 0 0 88891 61 0 0 25 0 1 0 1855431043 26324992 6165 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 6427 6165 145 145 0 6282 0
[pid=6750] vsize: 25708
Current children cumulated CPU time (s) 889.53
Current children cumulated vsize (Kb) 27832

[startup+900.061 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 6807
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6263 0 0 0 89891 61 0 0 25 0 1 0 1855431043 26324992 6165 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 6427 6165 145 145 0 6282 0
[pid=6750] vsize: 25708
Current children cumulated CPU time (s) 899.53
Current children cumulated vsize (Kb) 27832

[startup+910.062 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 6807
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6263 0 0 0 90891 61 0 0 25 0 1 0 1855431043 26324992 6165 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 6427 6165 145 145 0 6282 0
[pid=6750] vsize: 25708
Current children cumulated CPU time (s) 909.53
Current children cumulated vsize (Kb) 27832

[startup+920.062 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 6807
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6264 0 0 0 91892 61 0 0 25 0 1 0 1855431043 26324992 6166 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 6427 6166 145 145 0 6282 0
[pid=6750] vsize: 25708
Current children cumulated CPU time (s) 919.54
Current children cumulated vsize (Kb) 27832

[startup+930.062 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 6807
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6264 0 0 0 92892 61 0 0 25 0 1 0 1855431043 26324992 6166 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 6427 6166 145 145 0 6282 0
[pid=6750] vsize: 25708
Current children cumulated CPU time (s) 929.54
Current children cumulated vsize (Kb) 27832

[startup+940.062 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 6807
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6264 0 0 0 93892 61 0 0 25 0 1 0 1855431043 26324992 6166 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 6427 6166 145 145 0 6282 0
[pid=6750] vsize: 25708
Current children cumulated CPU time (s) 939.54
Current children cumulated vsize (Kb) 27832

[startup+950.063 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 6807
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6264 0 0 0 94892 61 0 0 25 0 1 0 1855431043 26324992 6166 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 6427 6166 145 145 0 6282 0
[pid=6750] vsize: 25708
Current children cumulated CPU time (s) 949.54
Current children cumulated vsize (Kb) 27832

[startup+960.064 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 6807
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6264 0 0 0 95893 61 0 0 25 0 1 0 1855431043 26324992 6166 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 6427 6166 145 145 0 6282 0
[pid=6750] vsize: 25708
Current children cumulated CPU time (s) 959.55
Current children cumulated vsize (Kb) 27832

[startup+970.064 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 6807
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6264 0 0 0 96893 61 0 0 25 0 1 0 1855431043 26324992 6166 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 6427 6166 145 145 0 6282 0
[pid=6750] vsize: 25708
Current children cumulated CPU time (s) 969.55
Current children cumulated vsize (Kb) 27832

[startup+980.065 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 6807
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6265 0 0 0 97932 61 0 0 25 0 1 0 1855431043 26324992 6167 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 6427 6167 145 145 0 6282 0
[pid=6750] vsize: 25708
Current children cumulated CPU time (s) 979.94
Current children cumulated vsize (Kb) 27832

[startup+990.455 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 6807
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6265 0 0 0 98932 61 0 0 25 0 1 0 1855431043 26324992 6167 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 6427 6167 145 145 0 6282 0
[pid=6750] vsize: 25708
Current children cumulated CPU time (s) 989.94
Current children cumulated vsize (Kb) 27832

[startup+1000.46 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 6807
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6265 0 0 0 99932 61 0 0 25 0 1 0 1855431043 26324992 6167 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 6427 6167 145 145 0 6282 0
[pid=6750] vsize: 25708
Current children cumulated CPU time (s) 999.94
Current children cumulated vsize (Kb) 27832

[startup+1010.46 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 6807
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6267 0 0 0 100932 61 0 0 25 0 1 0 1855431043 26324992 6169 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 6427 6169 145 145 0 6282 0
[pid=6750] vsize: 25708
Current children cumulated CPU time (s) 1009.94
Current children cumulated vsize (Kb) 27832

[startup+1020.46 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 6807
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6267 0 0 0 101933 61 0 0 25 0 1 0 1855431043 26324992 6169 4294967295 134512640 135094434 3221224432 3221223056 134557648 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 6427 6169 145 145 0 6282 0
[pid=6750] vsize: 25708
Current children cumulated CPU time (s) 1019.95
Current children cumulated vsize (Kb) 27832

[startup+1030.46 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 6807
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6267 0 0 0 102933 61 0 0 25 0 1 0 1855431043 26324992 6169 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 6427 6169 145 145 0 6282 0
[pid=6750] vsize: 25708
Current children cumulated CPU time (s) 1029.95
Current children cumulated vsize (Kb) 27832

[startup+1040.46 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 6807
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6267 0 0 0 103933 62 0 0 25 0 1 0 1855431043 26324992 6169 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 6427 6169 145 145 0 6282 0
[pid=6750] vsize: 25708
Current children cumulated CPU time (s) 1039.96
Current children cumulated vsize (Kb) 27832

[startup+1050.46 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 6807
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6268 0 0 0 104933 62 0 0 25 0 1 0 1855431043 26324992 6170 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 6427 6170 145 145 0 6282 0
[pid=6750] vsize: 25708
Current children cumulated CPU time (s) 1049.96
Current children cumulated vsize (Kb) 27832

[startup+1060.46 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 6807
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6268 0 0 0 105933 62 0 0 25 0 1 0 1855431043 26324992 6170 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 6427 6170 145 145 0 6282 0
[pid=6750] vsize: 25708
Current children cumulated CPU time (s) 1059.96
Current children cumulated vsize (Kb) 27832

[startup+1070.46 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 6807
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6268 0 0 0 106933 62 0 0 25 0 1 0 1855431043 26324992 6170 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 6427 6170 145 145 0 6282 0
[pid=6750] vsize: 25708
Current children cumulated CPU time (s) 1069.96
Current children cumulated vsize (Kb) 27832

[startup+1080.46 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 6807
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6268 0 0 0 107934 62 0 0 25 0 1 0 1855431043 26324992 6170 4294967295 134512640 135094434 3221224432 3221223056 134557648 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 6427 6170 145 145 0 6282 0
[pid=6750] vsize: 25708
Current children cumulated CPU time (s) 1079.97
Current children cumulated vsize (Kb) 27832

[startup+1090.46 s]
Raw data (loadavg): 1.00 1.00 0.99 2/57 6807
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6268 0 0 0 108934 62 0 0 25 0 1 0 1855431043 26324992 6170 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 6427 6170 145 145 0 6282 0
[pid=6750] vsize: 25708
Current children cumulated CPU time (s) 1089.97
Current children cumulated vsize (Kb) 27832

[startup+1100.46 s]
Raw data (loadavg): 1.07 1.02 1.00 2/57 6807
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6268 0 0 0 109934 62 0 0 25 0 1 0 1855431043 26324992 6170 4294967295 134512640 135094434 3221224432 3221223056 134562108 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 6427 6170 145 145 0 6282 0
[pid=6750] vsize: 25708
Current children cumulated CPU time (s) 1099.97
Current children cumulated vsize (Kb) 27832

[startup+1110.46 s]
Raw data (loadavg): 1.06 1.02 1.00 2/57 6807
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6268 0 0 0 110934 62 0 0 25 0 1 0 1855431043 26324992 6170 4294967295 134512640 135094434 3221224432 3221223088 134557840 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 6427 6170 145 145 0 6282 0
[pid=6750] vsize: 25708
Current children cumulated CPU time (s) 1109.97
Current children cumulated vsize (Kb) 27832

[startup+1120.46 s]
Raw data (loadavg): 1.05 1.01 1.00 2/57 6807
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6268 0 0 0 111934 62 0 0 25 0 1 0 1855431043 26324992 6170 4294967295 134512640 135094434 3221224432 3221223024 134557157 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 6427 6170 145 145 0 6282 0
[pid=6750] vsize: 25708
Current children cumulated CPU time (s) 1119.97
Current children cumulated vsize (Kb) 27832

[startup+1130.46 s]
Raw data (loadavg): 1.04 1.01 1.00 2/57 6807
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6268 0 0 0 112934 62 0 0 25 0 1 0 1855431043 26324992 6170 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 6427 6170 145 145 0 6282 0
[pid=6750] vsize: 25708
Current children cumulated CPU time (s) 1129.97
Current children cumulated vsize (Kb) 27832

[startup+1140.46 s]
Raw data (loadavg): 1.04 1.01 1.00 2/57 6807
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6268 0 0 0 113935 62 0 0 25 0 1 0 1855431043 26324992 6170 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 6427 6170 145 145 0 6282 0
[pid=6750] vsize: 25708
Current children cumulated CPU time (s) 1139.98
Current children cumulated vsize (Kb) 27832

[startup+1150.46 s]
Raw data (loadavg): 1.03 1.01 1.00 2/57 6807
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6268 0 0 0 114935 62 0 0 25 0 1 0 1855431043 26324992 6170 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 6427 6170 145 145 0 6282 0
[pid=6750] vsize: 25708
Current children cumulated CPU time (s) 1149.98
Current children cumulated vsize (Kb) 27832

[startup+1160.46 s]
Raw data (loadavg): 1.02 1.01 1.00 2/57 6807
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6268 0 0 0 115935 62 0 0 25 0 1 0 1855431043 26324992 6170 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 6427 6170 145 145 0 6282 0
[pid=6750] vsize: 25708
Current children cumulated CPU time (s) 1159.98
Current children cumulated vsize (Kb) 27832

[startup+1170.46 s]
Raw data (loadavg): 1.02 1.01 1.00 2/57 6807
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6268 0 0 0 116935 62 0 0 25 0 1 0 1855431043 26324992 6170 4294967295 134512640 135094434 3221224432 3221223024 134556851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 6427 6170 145 145 0 6282 0
[pid=6750] vsize: 25708
Current children cumulated CPU time (s) 1169.98
Current children cumulated vsize (Kb) 27832

[startup+1180.46 s]
Raw data (loadavg): 1.02 1.01 1.00 2/57 6807
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6268 0 0 0 117935 62 0 0 25 0 1 0 1855431043 26324992 6170 4294967295 134512640 135094434 3221224432 3221223088 134557879 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 6427 6170 145 145 0 6282 0
[pid=6750] vsize: 25708
Current children cumulated CPU time (s) 1179.98
Current children cumulated vsize (Kb) 27832

[startup+1190.46 s]
Raw data (loadavg): 1.01 1.01 1.00 2/57 6807
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6269 0 0 0 118936 62 0 0 25 0 1 0 1855431043 26324992 6171 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 6427 6171 145 145 0 6282 0
[pid=6750] vsize: 25708
Current children cumulated CPU time (s) 1189.99
Current children cumulated vsize (Kb) 27832

[startup+1200.46 s]
Raw data (loadavg): 1.01 1.01 1.00 2/57 6807
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6269 0 0 0 119936 62 0 0 25 0 1 0 1855431043 26324992 6171 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 6427 6171 145 145 0 6282 0
[pid=6750] vsize: 25708
Current children cumulated CPU time (s) 1199.99
Current children cumulated vsize (Kb) 27832

[startup+1210.46 s]
Raw data (loadavg): 1.01 1.01 1.00 2/57 6807
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6269 0 0 0 120936 62 0 0 25 0 1 0 1855431043 26324992 6171 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 6427 6171 145 145 0 6282 0
[pid=6750] vsize: 25708
Current children cumulated CPU time (s) 1209.99
Current children cumulated vsize (Kb) 27832



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.47 s]
Raw data (loadavg): 1.01 1.01 1.00 2/57 6807
Raw data (/proc/6746/stat): 6746 (minisat+_script) S 6745 6746 19316 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855431038 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6746/statm): 531 226 485 147 0 384 0
[pid=6746] vsize: 2124
Raw data (/proc/6750/stat): 6750 (minisat+_64-bit) R 6746 6746 19316 0 -1 0 6269 0 0 0 120936 62 0 0 25 0 1 0 1855431043 26324992 6171 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6750/statm): 6427 6171 145 145 0 6282 0
[pid=6750] vsize: 25708
Current children cumulated CPU time (s) 1209.99
Current children cumulated vsize (Kb) 27832

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

Child status: 10
Real time (s): 1210.48
CPU time (s): 1210.01
CPU user time (s): 1209.37
CPU system time (s): 0.638902
CPU usage (%): 99.9607
Max. virtual memory (cumulated for all children) (Kb): 27832

Verifier Data

ERROR: no interpretation found !