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-20-10/MIPLIB/miplib2003/normalized-mps-v2-20-10-markshare2.opb
MD5SUMc00b2eef1eabd5880b83093b756a5dd4
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 93184
Optimality of the best value was proved NO
Number of terms in the objective function 210
Biggest coefficient in the objective function 536870912
Number of bits for the biggest coefficient in the objective function 30
Sum of the numbers in the objective function 7516192761
Number of bits of the sum of numbers in the objective function 33
Biggest number in a constraint 536870912
Number of bits of the biggest number in a constraint 30
Biggest sum of numbers in a constraint 7516192761
Number of bits of the biggest sum of numbers33
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1195.24
Number of variables270
Total number of constraints67
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)60
Number of constraints which are nor clauses,nor cardinality constraints7
Minimum length of a constraint1
Maximum length of a constraint90

Trace number 3912

Launcher Data

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        899476 kB
Buffers:         34508 kB
Cached:          71256 kB
SwapCached:        792 kB
Active:          50592 kB
Inactive:        57852 kB
HighTotal:      131008 kB
HighFree:        58688 kB
LowTotal:       903652 kB
LowFree:        840788 kB
SwapTotal:     2097892 kB
SwapFree:      2096664 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5740 kB
Slab:            21044 kB
Committed_AS:    64132 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-19 04:01:17 (client local time) WITH STATUS 10 IN 1209.76 SECONDS
stats: 2917 7 1209.76 10

Solver Data

c Parsing PB file...
c Converting 14 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #######
c   -- Clauses(.)/Splits(s): (none)
c ---[  12]---> Adder-cost: 354   maxlim: 3452927   bits: 23/22
c ---[  10]---> Adder-cost: 380   maxlim: 3689471   bits: 23/22
c ---[   8]---> Adder-cost: 350   maxlim: 3561471   bits: 23/22
c ---[   6]---> Adder-cost: 340   maxlim: 3823615   bits: 23/22
c ---[   4]---> Adder-cost: 390   maxlim: 3614719   bits: 23/22
c ---[   2]---> Adder-cost: 358   maxlim: 3749887   bits: 23/22
c ---[   0]---> Adder-cost: 374   maxlim: 3556351   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   17222    61228 |    5740       0        0     nan |  0.000 % |
c |       100 |   17214    61202 |    6314      99      310     3.1 | 12.761 % |
c ==============================================================================
c Found solution: 9929728
c ---[   0]---> Sorter-cost: 1069     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       170 |   19863    67394 |    6621     169      862     5.1 | 12.761 % |
c |       270 |   19847    67342 |    7283     267     1398     5.2 |  9.797 % |
c ==============================================================================
c Found solution: 9154560
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       390 |   19874    67444 |    6624     387     3000     7.8 |  9.797 % |
c ==============================================================================
c Found solution: 9147392
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       420 |   19888    67485 |    6629     417     6353    15.2 |  9.797 % |
c |       520 |   19888    67485 |    7291     517    10812    20.9 |  9.776 % |
c ==============================================================================
c Found solution: 7954432
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       552 |   19902    67521 |    6634     549    12623    23.0 |  9.776 % |
c ==============================================================================
c Found solution: 7805952
c ---[   0]---> Sorter-cost:   11     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       598 |   19914    67554 |    6638     595    16053    27.0 |  9.776 % |
c |       699 |   19890    67476 |    7301     693    28096    40.5 |  9.863 % |
c |       851 |   19882    67450 |    8031     844    41822    49.6 |  9.888 % |
c ==============================================================================
c Found solution: 7643136
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       986 |   19894    67479 |    6631     979    63040    64.4 |  9.888 % |
c ==============================================================================
c Found solution: 6888448
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1042 |   19906    67503 |    6635    1034    67129    64.9 |  9.888 % |
c |      1144 |   19906    67503 |    7298    1136    81563    71.8 |  9.914 % |
c |      1295 |   19906    67503 |    8028    1287    98275    76.4 |  9.914 % |
c |      1520 |   19898    67477 |    8831    1511   117286    77.6 |  9.939 % |
c |      1858 |   19898    67477 |    9714    1849   140264    75.9 |  9.939 % |
c |      2364 |   19898    67477 |   10685    2355   182832    77.6 |  9.939 % |
c |      3123 |   19898    67477 |   11754    3114   256165    82.3 |  9.939 % |
c ==============================================================================
c Found solution: 5861376
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3469 |   19904    67486 |    6634    3459   283309    81.9 |  9.939 % |
c |      3569 |   19904    67486 |    7297    3559   300055    84.3 |  9.967 % |
c |      3720 |   19904    67486 |    8027    3710   307885    83.0 |  9.967 % |
c |      3945 |   19904    67486 |    8829    3935   344859    87.6 |  9.967 % |
c |      4282 |   19904    67486 |    9712    4272   396303    92.8 |  9.967 % |
c |      4789 |   19904    67486 |   10684    4779   432588    90.5 |  9.967 % |
c |      5548 |   19904    67486 |   11752    5538   541320    97.7 |  9.967 % |
c ==============================================================================
c Found solution: 5195776
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5997 |   19918    67523 |    6639    5987   601231   100.4 |  9.967 % |
c |      6098 |   19918    67523 |    7302    6088   618703   101.6 |  9.970 % |
c |      6249 |   19918    67523 |    8033    6239   626932   100.5 |  9.970 % |
c |      6475 |   19910    67497 |    8836    6464   656309   101.5 |  9.995 % |
c |      6812 |   19910    67497 |    9720    6801   696089   102.4 |  9.995 % |
c |      7320 |   19910    67497 |   10692    7309   731836   100.1 |  9.995 % |
c |      8082 |   19910    67497 |   11761    8071   795887    98.6 |  9.995 % |
c |      9221 |   19910    67497 |   12937    9210   908038    98.6 |  9.995 % |
c |     10930 |   19910    67497 |   14231   10919  1103571   101.1 |  9.995 % |
c |     13493 |   19910    67497 |   15654   13482  1375845   102.1 |  9.995 % |
c |     17337 |   19910    67497 |   17219    8787   834221    94.9 |  9.995 % |
c |     23104 |   19880    67401 |   18941   14550  1340020    92.1 | 10.095 % |
c |     31753 |   19880    67401 |   20836   12937  1343299   103.8 | 10.095 % |
c ==============================================================================
c Found solution: 5003264
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     32527 |   19890    67428 |    6630   13711  1411626   103.0 | 10.095 % |
c |     32627 |   19890    67428 |    7293    6956   715766   102.9 | 10.105 % |
c |     32778 |   19890    67428 |    8022    7107   727028   102.3 | 10.105 % |
c |     33003 |   19890    67428 |    8824    7332   754819   102.9 | 10.105 % |
c |     33341 |   19890    67428 |    9706    7670   787535   102.7 | 10.105 % |
c |     33847 |   19890    67428 |   10677    8176   839414   102.7 | 10.105 % |
c |     34607 |   19890    67428 |   11745    8936   873644    97.8 | 10.105 % |
c |     35747 |   19890    67428 |   12919   10076   941502    93.4 | 10.105 % |
c ==============================================================================
c Found solution: 4755456
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     35779 |   19904    67460 |    6634   10108   942640    93.3 | 10.105 % |
c |     35879 |   19904    67460 |    7297    5154   282091    54.7 | 10.110 % |
c |     36030 |   19904    67460 |    8027    5305   293923    55.4 | 10.110 % |
c |     36258 |   19904    67460 |    8829    5533   315402    57.0 | 10.110 % |
c |     36595 |   19904    67460 |    9712    5870   343649    58.5 | 10.110 % |
c |     37103 |   19896    67434 |   10684    6377   396528    62.2 | 10.135 % |
c |     37862 |   19896    67434 |   11752    7136   463376    64.9 | 10.135 % |
c |     39001 |   19896    67434 |   12927    8275   565260    68.3 | 10.135 % |
c ==============================================================================
c Found solution: 4734976
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     39899 |   19909    67464 |    6636    9173   639714    69.7 | 10.135 % |
c ==============================================================================
c Found solution: 3594240
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     39906 |   19920    67491 |    6640    4594   288279    62.8 | 10.135 % |
c |     40008 |   19920    67491 |    7304    4696   295775    63.0 | 10.150 % |
c |     40158 |   19920    67491 |    8034    4846   308279    63.6 | 10.150 % |
c |     40384 |   19920    67491 |    8837    5072   332107    65.5 | 10.150 % |
c |     40721 |   19920    67491 |    9721    5409   357102    66.0 | 10.150 % |
c |     41227 |   19920    67491 |   10693    5915   380151    64.3 | 10.150 % |
c |     41988 |   19920    67491 |   11763    6676   455590    68.2 | 10.150 % |
c ==============================================================================
c Found solution: 3588096
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     42026 |   19928    67511 |    6642    6714   457571    68.2 | 10.150 % |
c |     42126 |   19928    67511 |    7306    6814   470595    69.1 | 10.162 % |
c |     42276 |   19928    67511 |    8036    6964   479269    68.8 | 10.162 % |
c |     42501 |   19928    67511 |    8840    7189   491049    68.3 | 10.162 % |
c |     42839 |   19928    67511 |    9724    7527   539920    71.7 | 10.162 % |
c |     43346 |   19928    67511 |   10697    8034   570107    71.0 | 10.162 % |
c |     44105 |   19928    67511 |   11766    8793   627248    71.3 | 10.162 % |
c |     45245 |   19928    67511 |   12943    9933   697751    70.2 | 10.162 % |
c ==============================================================================
c Found solution: 2887680
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     45267 |   19940    67539 |    6646    9955   698020    70.1 | 10.162 % |
c |     45369 |   19940    67539 |    7310    5080   268355    52.8 | 10.172 % |
c |     45519 |   19940    67539 |    8041    5230   273672    52.3 | 10.172 % |
c |     45744 |   19940    67539 |    8845    5455   303851    55.7 | 10.172 % |
c |     46082 |   19940    67539 |    9730    5793   324113    55.9 | 10.172 % |
c |     46589 |   19940    67539 |   10703    6300   343830    54.6 | 10.172 % |
c |     47349 |   19940    67539 |   11773    7060   403882    57.2 | 10.172 % |
c |     48488 |   19932    67513 |   12951    8198   536289    65.4 | 10.196 % |
c |     50196 |   19924    67487 |   14246    9905   614440    62.0 | 10.221 % |
c |     52762 |   19918    67469 |   15670   12470   771014    61.8 | 10.246 % |
c |     56606 |   19918    67469 |   17238   16314  1003494    61.5 | 10.246 % |
c ==============================================================================
c Found solution: 2847744
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     57500 |   19929    67497 |    6643   17208  1113811    64.7 | 10.246 % |
c |     57601 |   19929    67497 |    7307    4403   226769    51.5 | 10.253 % |
c |     57751 |   19929    67497 |    8038    4553   240342    52.8 | 10.253 % |
c |     57976 |   19929    67497 |    8841    4778   248307    52.0 | 10.253 % |
c |     58313 |   19929    67497 |    9726    5115   266177    52.0 | 10.253 % |
c |     58819 |   19929    67497 |   10698    5621   301876    53.7 | 10.253 % |
c |     59580 |   19929    67497 |   11768    6382   405638    63.6 | 10.253 % |
c |     60719 |   19929    67497 |   12945    7521   468128    62.2 | 10.253 % |
c |     62427 |   19929    67497 |   14239    9229   530637    57.5 | 10.253 % |
c |     64989 |   19929    67497 |   15663   11791   930394    78.9 | 10.253 % |
c ==============================================================================
c Found solution: 2835456
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     68346 |   19941    67526 |    6647   15148  1223872    80.8 | 10.253 % |
c |     68447 |   19941    67526 |    7311    3888   198569    51.1 | 10.258 % |
c |     68597 |   19941    67526 |    8042    4038   203731    50.5 | 10.258 % |
c |     68824 |   19941    67526 |    8847    4265   220342    51.7 | 10.258 % |
c |     69162 |   19941    67526 |    9731    4603   235771    51.2 | 10.258 % |
c |     69669 |   19941    67526 |   10705    5110   253501    49.6 | 10.258 % |
c |     70428 |   19941    67526 |   11775    5869   306369    52.2 | 10.258 % |
c |     71569 |   19937    67517 |   12953    7009   426770    60.9 | 10.282 % |
c |     73277 |   19937    67517 |   14248    8717   529658    60.8 | 10.282 % |
c |     75839 |   19937    67517 |   15673   11279   655327    58.1 | 10.282 % |
c ==============================================================================
c Found solution: 2778112
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     77546 |   19948    67544 |    6649   12986   731385    56.3 | 10.282 % |
c |     77646 |   19948    67544 |    7313    6593   247614    37.6 | 10.289 % |
c |     77797 |   19948    67544 |    8045    6744   256608    38.0 | 10.289 % |
c |     78023 |   19948    67544 |    8849    6970   268841    38.6 | 10.289 % |
c |     78362 |   19948    67544 |    9734    7309   280051    38.3 | 10.289 % |
c |     78868 |   19942    67531 |   10708    7813   298870    38.3 | 10.339 % |
c |     79627 |   19942    67531 |   11779    8572   342608    40.0 | 10.339 % |
c |     80766 |   19942    67531 |   12957    9711   439104    45.2 | 10.339 % |
c |     82475 |   19936    67513 |   14252   11419   560031    49.0 | 10.364 % |
c |     85038 |   19936    67513 |   15677   13982   704208    50.4 | 10.364 % |
c |     88882 |   19924    67486 |   17245    9494   573325    60.4 | 10.438 % |
c |     94648 |   19924    67486 |   18970   15260   955968    62.6 | 10.438 % |
c |    103297 |   19916    67460 |   20867   13789   713329    51.7 | 10.463 % |
c |    116272 |   19910    67442 |   22954   15743   751219    47.7 | 10.487 % |
c ==============================================================================
c Found solution: 2522112
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    127359 |   19922    67471 |    6640   14702   794493    54.0 | 10.487 % |
c |    127459 |   19922    67471 |    7304    3776   127552    33.8 | 10.494 % |
c |    127609 |   19922    67471 |    8034    3926   129716    33.0 | 10.494 % |
c |    127835 |   19922    67471 |    8837    4152   156130    37.6 | 10.494 % |
c |    128172 |   19912    67449 |    9721    4485   164235    36.6 | 10.568 % |
c |    128679 |   19912    67449 |   10693    4992   183225    36.7 | 10.568 % |
c |    129440 |   19912    67449 |   11763    5753   205051    35.6 | 10.568 % |
c |    130579 |   19912    67449 |   12939    6892   257149    37.3 | 10.568 % |
c |    132287 |   19912    67449 |   14233    8600   340347    39.6 | 10.568 % |
c |    134854 |   19912    67449 |   15656   11167   490010    43.9 | 10.568 % |
c |    138701 |   19912    67449 |   17222   15014   707463    47.1 | 10.568 % |
c |    144468 |   19912    67449 |   18944   11874   493715    41.6 | 10.568 % |
c ==============================================================================
c Found solution: 2021376
c ---[   0]---> Sorter-cost:    3     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    149824 |   19918    67463 |    6639   17230   725431    42.1 | 10.568 % |
c |    149924 |   19918    67463 |    7302    4408   152704    34.6 | 10.582 % |
c |    150074 |   19918    67463 |    8033    4558   155333    34.1 | 10.582 % |
c |    150302 |   19918    67463 |    8836    4786   165404    34.6 | 10.582 % |
c |    150640 |   19918    67463 |    9720    5124   180854    35.3 | 10.582 % |
c |    151147 |   19904    67426 |   10692    5627   198519    35.3 | 10.681 % |
c |    151906 |   19904    67426 |   11761    6386   231775    36.3 | 10.681 % |
c |    153045 |   19904    67426 |   12937    7525   270866    36.0 | 10.681 % |
c |    154753 |   19904    67426 |   14231    9233   344640    37.3 | 10.681 % |
c |    157316 |   19904    67426 |   15654   11796   468997    39.8 | 10.681 % |
c |    161161 |   19904    67426 |   17219   15641   682108    43.6 | 10.681 % |
c |    166928 |   19904    67426 |   18941   12371   584652    47.3 | 10.681 % |
c |    175577 |   19904    67426 |   20836   10965   555413    50.7 | 10.681 % |
c |    188551 |   19904    67426 |   22919   13084   624549    47.7 | 10.681 % |
c |    208015 |   19895    67399 |   25211   20521  1335297    65.1 | 10.730 % |
c |    237207 |   19895    67399 |   27732   23675  1338137    56.5 | 10.730 % |
c |    280999 |   19868    67339 |   30506   22421  1362077    60.8 | 10.927 % |
c ==============================================================================
c Found solution: 1964032
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    337469 |   19877    67361 |    6625   27521  1615060    58.7 | 10.927 % |
c |    337571 |   19877    67361 |    7287    6983   298754    42.8 | 10.941 % |
c |    337722 |   19877    67361 |    8016    7134   304165    42.6 | 10.941 % |
c |    337948 |   19877    67361 |    8817    7360   309684    42.1 | 10.941 % |
c ==============================================================================
c Found solution: 818176
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    338139 |   19831    67198 |    6610    7544   315949    41.9 | 10.941 % |
c |    338239 |   19831    67198 |    7271    3872   117087    30.2 | 11.128 % |
c |    338389 |   19809    67148 |    7998    4020   118738    29.5 | 11.275 % |
c |    338614 |   19809    67148 |    8797    4245   122647    28.9 | 11.275 % |
c |    338952 |   19809    67148 |    9677    4583   134194    29.3 | 11.275 % |
c |    339458 |   19809    67148 |   10645    5089   150331    29.5 | 11.275 % |
c |    340217 |   19809    67148 |   11710    5848   169574    29.0 | 11.275 % |
c |    341356 |   19809    67148 |   12881    6987   201444    28.8 | 11.275 % |
c |    343064 |   19809    67148 |   14169    8695   267895    30.8 | 11.275 % |
c |    345627 |   19781    67084 |   15586   11254   356949    31.7 | 11.497 % |
c |    349471 |   19757    67031 |   17144   15086   500268    33.2 | 11.694 % |
c |    355239 |   19713    66930 |   18859   11909   399091    33.5 | 12.063 % |
c |    363889 |   19713    66930 |   20745   10449   365385    35.0 | 12.063 % |
c |    376863 |   19661    66810 |   22819   12706   515813    40.6 | 12.506 % |
c |    396324 |   19661    66810 |   25101   20102  1154823    57.4 | 12.506 % |
c ==============================================================================
c Found solution: 790528
c ---[   0]---> Sorter-cost:    2     Base: 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    397868 |   19664    66818 |    6554   21646  1262196    58.3 | 12.506 % |
c |    397968 |   19647    66780 |    7209    5511   243966    44.3 | 12.645 % |
c |    398119 |   19647    66780 |    7930    5662   245316    43.3 | 12.645 % |
c |    398345 |   19647    66780 |    8723    5888   250643    42.6 | 12.645 % |
c |    398684 |   19647    66780 |    9595    6227   258778    41.6 | 12.645 % |
c |    399190 |   19647    66780 |   10555    6733   276773    41.1 | 12.645 % |
c |    399949 |   19647    66780 |   11610    7492   299025    39.9 | 12.645 % |
c |    401089 |   19647    66780 |   12771    8632   333558    38.6 | 12.645 % |
c |    402797 |   19647    66780 |   14049   10340   410168    39.7 | 12.645 % |
c |    405360 |   19647    66780 |   15453   12903   533783    41.4 | 12.645 % |
c |    409205 |   19647    66780 |   16999    8408   351582    41.8 | 12.645 % |
c |    414971 |   19612    66701 |   18699   14170   623685    44.0 | 12.891 % |
c |    423622 |   19612    66701 |   20569   12588   579955    46.1 | 12.891 % |
c |    436596 |   19612    66701 |   22626   14760   726082    49.2 | 12.891 % |
c |    456060 |   19612    66701 |   24888   22396  1079856    48.2 | 12.891 % |
c |    485253 |   19592    66654 |   27377   25538  1323214    51.8 | 13.087 % |
c |    529042 |   19574    66614 |   30115   24738  1096257    44.3 | 13.235 % |
c ==============================================================================
c Found solution: 580608
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    530944 |   19580    66629 |    6526   26640  1206714    45.3 | 13.235 % |
c |    531044 |   19580    66629 |    7178    6606   240336    36.4 | 13.250 % |
c |    531196 |   19580    66629 |    7896    6758   243751    36.1 | 13.250 % |
c |    531421 |   19580    66629 |    8686    6983   247742    35.5 | 13.250 % |
c |    531758 |   19580    66629 |    9554    7320   256616    35.1 | 13.250 % |
c |    532264 |   19580    66629 |   10510    7826   269328    34.4 | 13.250 % |
c |    533026 |   19580    66629 |   11561    8588   288887    33.6 | 13.250 % |
c |    534165 |   19580    66629 |   12717    9727   322283    33.1 | 13.250 % |
c |    535877 |   19580    66629 |   13989   11439   383971    33.6 | 13.250 % |
c |    538439 |   19580    66629 |   15387   14001   485193    34.7 | 13.250 % |
c |    542284 |   19580    66629 |   16926    9703   309759    31.9 | 13.250 % |
c |    548052 |   19580    66629 |   18619   15471   577157    37.3 | 13.250 % |
c |    556702 |   19580    66629 |   20481   14388   611959    42.5 | 13.250 % |
c |    569677 |   19580    66629 |   22529   16607   882005    53.1 | 13.250 % |
c |    589138 |   19580    66629 |   24782   12766   455111    35.7 | 13.250 % |
c |    618332 |   19568    66602 |   27260   15694   694024    44.2 | 13.348 % |
c |    662121 |   19568    66602 |   29986   16216   706500    43.6 | 13.348 % |
c |    727805 |   19514    66480 |   32985   14865   654057    44.0 | 13.766 % |
c ==============================================================================
c Found solution: 550912
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    758120 |   19515    66482 |    6505   24867  1269806    51.1 | 13.766 % |
c |    758220 |   19515    66482 |    7155    6317   262163    41.5 | 13.808 % |
c |    758371 |   19515    66482 |    7871    6468   265260    41.0 | 13.808 % |
c |    758596 |   19515    66482 |    8658    6693   272564    40.7 | 13.808 % |
c |    758933 |   19515    66482 |    9523    7030   281856    40.1 | 13.808 % |
c |    759439 |   19501    66449 |   10476    7534   293604    39.0 | 13.931 % |
c |    760198 |   19501    66449 |   11524    8293   317919    38.3 | 13.931 % |
c |    761337 |   19501    66449 |   12676    9432   355218    37.7 | 13.931 % |
c |    763045 |   19501    66449 |   13944   11140   405332    36.4 | 13.931 % |
c |    765608 |   19501    66449 |   15338   13703   537756    39.2 | 13.931 % |
c |    769453 |   19501    66449 |   16872    9424   333768    35.4 | 13.931 % |
c |    775219 |   19501    66449 |   18559   15190   597919    39.4 | 13.931 % |
c |    783868 |   19501    66449 |   20415   14112   581917    41.2 | 13.931 % |
c |    796847 |   19487    66417 |   22457   16563   719045    43.4 | 14.054 % |
c |    816309 |   19487    66417 |   24702   12590   506929    40.3 | 14.054 % |

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/27340/stat): 27340 (minisat+_script) R 27339 27340 19818 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1846722449 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/27340/statm): 174 3 169 147 0 27 0
[pid=27340] 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=27341
New process pid=27342
New process pid=27343
execve syscall for /bin/sed executable
One traced child (pid=27342) 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=27343) exited with status: 0
One traced child (pid=27341) exited with status: 0
New process pid=27344
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-20-10-markshare2.opb

[startup+10.0032 s]
Raw data (loadavg): 0.93 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 1102 0 0 0 980 6 0 0 25 0 1 0 1846722454 4890624 1089 4294967295 134512640 135094434 3221224432 3221223088 134557920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27344/statm): 1194 1089 145 145 0 1049 0
[pid=27344] vsize: 4776
Current children cumulated CPU time (s) 9.87
Current children cumulated vsize (Kb) 6900

[startup+20.005 s]
Raw data (loadavg): 0.94 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 1593 0 0 0 1970 11 0 0 25 0 1 0 1846722454 6918144 1580 4294967295 134512640 135094434 3221224432 3221223088 134557863 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27344/statm): 1689 1580 145 145 0 1544 0
[pid=27344] vsize: 6756
Current children cumulated CPU time (s) 19.82
Current children cumulated vsize (Kb) 8880

[startup+30.0058 s]
Raw data (loadavg): 0.95 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 2040 0 0 0 2962 14 0 0 25 0 1 0 1846722454 8732672 2027 4294967295 134512640 135094434 3221224432 3221223024 134556789 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27344/statm): 2132 2027 145 145 0 1987 0
[pid=27344] vsize: 8528
Current children cumulated CPU time (s) 29.77
Current children cumulated vsize (Kb) 10652

[startup+40.0066 s]
Raw data (loadavg): 0.95 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 2414 0 0 0 3954 17 0 0 25 0 1 0 1846722454 10256384 2401 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27344/statm): 2504 2401 145 145 0 2359 0
[pid=27344] vsize: 10016
Current children cumulated CPU time (s) 39.72
Current children cumulated vsize (Kb) 12140

[startup+50.0083 s]
Raw data (loadavg): 0.96 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 2543 0 0 0 4951 19 0 0 25 0 1 0 1846722454 10842112 2530 4294967295 134512640 135094434 3221224432 3221223088 134557882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27344/statm): 2647 2530 145 145 0 2502 0
[pid=27344] vsize: 10588
Current children cumulated CPU time (s) 49.71
Current children cumulated vsize (Kb) 12712

[startup+60.0091 s]
Raw data (loadavg): 0.97 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 2543 0 0 0 5950 19 0 0 25 0 1 0 1846722454 10842112 2530 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27344/statm): 2647 2530 145 145 0 2502 0
[pid=27344] vsize: 10588
Current children cumulated CPU time (s) 59.7
Current children cumulated vsize (Kb) 12712

[startup+70.0109 s]
Raw data (loadavg): 0.97 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 2621 0 0 0 6948 20 0 0 25 0 1 0 1846722454 11157504 2608 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27344/statm): 2724 2608 145 145 0 2579 0
[pid=27344] vsize: 10896
Current children cumulated CPU time (s) 69.69
Current children cumulated vsize (Kb) 13020

[startup+80.0117 s]
Raw data (loadavg): 0.98 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 2948 0 0 0 7941 24 0 0 25 0 1 0 1846722454 12488704 2935 4294967295 134512640 135094434 3221224432 3221223024 134557191 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 3049 2935 145 145 0 2904 0
[pid=27344] vsize: 12196
Current children cumulated CPU time (s) 79.66
Current children cumulated vsize (Kb) 14320

[startup+90.0125 s]
Raw data (loadavg): 0.98 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 2948 0 0 0 8941 25 0 0 25 0 1 0 1846722454 12488704 2935 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 3049 2935 145 145 0 2904 0
[pid=27344] vsize: 12196
Current children cumulated CPU time (s) 89.67
Current children cumulated vsize (Kb) 14320

[startup+100.013 s]
Raw data (loadavg): 0.98 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 2948 0 0 0 9941 25 0 0 25 0 1 0 1846722454 12488704 2935 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 3049 2935 145 145 0 2904 0
[pid=27344] vsize: 12196
Current children cumulated CPU time (s) 99.67
Current children cumulated vsize (Kb) 14320

[startup+110.014 s]
Raw data (loadavg): 0.98 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 2948 0 0 0 10940 25 0 0 25 0 1 0 1846722454 12488704 2935 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 3049 2935 145 145 0 2904 0
[pid=27344] vsize: 12196
Current children cumulated CPU time (s) 109.66
Current children cumulated vsize (Kb) 14320

[startup+120.016 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 2948 0 0 0 11940 26 0 0 25 0 1 0 1846722454 12488704 2935 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 3049 2935 145 145 0 2904 0
[pid=27344] vsize: 12196
Current children cumulated CPU time (s) 119.67
Current children cumulated vsize (Kb) 14320

[startup+130.017 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 2948 0 0 0 12940 26 0 0 25 0 1 0 1846722454 12488704 2935 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 3049 2935 145 145 0 2904 0
[pid=27344] vsize: 12196
Current children cumulated CPU time (s) 129.67
Current children cumulated vsize (Kb) 14320

[startup+140.017 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 2948 0 0 0 13939 27 0 0 25 0 1 0 1846722454 12488704 2935 4294967295 134512640 135094434 3221224432 3221223088 134557920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27344/statm): 3049 2935 145 145 0 2904 0
[pid=27344] vsize: 12196
Current children cumulated CPU time (s) 139.67
Current children cumulated vsize (Kb) 14320

[startup+150.019 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 2948 0 0 0 14938 27 0 0 25 0 1 0 1846722454 12488704 2935 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 3049 2935 145 145 0 2904 0
[pid=27344] vsize: 12196
Current children cumulated CPU time (s) 149.66
Current children cumulated vsize (Kb) 14320

[startup+160.02 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 2948 0 0 0 15938 27 0 0 25 0 1 0 1846722454 12488704 2935 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 3049 2935 145 145 0 2904 0
[pid=27344] vsize: 12196
Current children cumulated CPU time (s) 159.66
Current children cumulated vsize (Kb) 14320

[startup+170.021 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 2949 0 0 0 16938 27 0 0 25 0 1 0 1846722454 12488704 2936 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 3049 2936 145 145 0 2904 0
[pid=27344] vsize: 12196
Current children cumulated CPU time (s) 169.66
Current children cumulated vsize (Kb) 14320

[startup+180.022 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 2949 0 0 0 17938 27 0 0 25 0 1 0 1846722454 12488704 2936 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 3049 2936 145 145 0 2904 0
[pid=27344] vsize: 12196
Current children cumulated CPU time (s) 179.66
Current children cumulated vsize (Kb) 14320

[startup+190.022 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 2949 0 0 0 18938 28 0 0 25 0 1 0 1846722454 12488704 2936 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 3049 2936 145 145 0 2904 0
[pid=27344] vsize: 12196
Current children cumulated CPU time (s) 189.67
Current children cumulated vsize (Kb) 14320

[startup+200.023 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 2949 0 0 0 19938 28 0 0 25 0 1 0 1846722454 12488704 2936 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 3049 2936 145 145 0 2904 0
[pid=27344] vsize: 12196
Current children cumulated CPU time (s) 199.67
Current children cumulated vsize (Kb) 14320

[startup+210.024 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 2949 0 0 0 20939 28 0 0 25 0 1 0 1846722454 12488704 2936 4294967295 134512640 135094434 3221224432 3221223088 134557903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 3049 2936 145 145 0 2904 0
[pid=27344] vsize: 12196
Current children cumulated CPU time (s) 209.68
Current children cumulated vsize (Kb) 14320

[startup+220.026 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 2951 0 0 0 21938 28 0 0 25 0 1 0 1846722454 12488704 2938 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 3049 2938 145 145 0 2904 0
[pid=27344] vsize: 12196
Current children cumulated CPU time (s) 219.67
Current children cumulated vsize (Kb) 14320

[startup+230.027 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 2951 0 0 0 22939 28 0 0 25 0 1 0 1846722454 12488704 2938 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 3049 2938 145 145 0 2904 0
[pid=27344] vsize: 12196
Current children cumulated CPU time (s) 229.68
Current children cumulated vsize (Kb) 14320

[startup+240.027 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 2953 0 0 0 23939 28 0 0 25 0 1 0 1846722454 12488704 2940 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 3049 2940 145 145 0 2904 0
[pid=27344] vsize: 12196
Current children cumulated CPU time (s) 239.68
Current children cumulated vsize (Kb) 14320

[startup+250.028 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 2953 0 0 0 24939 29 0 0 25 0 1 0 1846722454 12488704 2940 4294967295 134512640 135094434 3221224432 3221223104 134556073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 3049 2940 145 145 0 2904 0
[pid=27344] vsize: 12196
Current children cumulated CPU time (s) 249.69
Current children cumulated vsize (Kb) 14320

[startup+260.029 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 2953 0 0 0 25939 29 0 0 25 0 1 0 1846722454 12488704 2940 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 3049 2940 145 145 0 2904 0
[pid=27344] vsize: 12196
Current children cumulated CPU time (s) 259.69
Current children cumulated vsize (Kb) 14320

[startup+270.03 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 2953 0 0 0 26939 29 0 0 25 0 1 0 1846722454 12488704 2940 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 3049 2940 145 145 0 2904 0
[pid=27344] vsize: 12196
Current children cumulated CPU time (s) 269.69
Current children cumulated vsize (Kb) 14320

[startup+280.03 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 2953 0 0 0 27939 29 0 0 25 0 1 0 1846722454 12488704 2940 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 3049 2940 145 145 0 2904 0
[pid=27344] vsize: 12196
Current children cumulated CPU time (s) 279.69
Current children cumulated vsize (Kb) 14320

[startup+290.031 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 2953 0 0 0 28939 29 0 0 25 0 1 0 1846722454 12488704 2940 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 3049 2940 145 145 0 2904 0
[pid=27344] vsize: 12196
Current children cumulated CPU time (s) 289.69
Current children cumulated vsize (Kb) 14320

[startup+300.032 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 2953 0 0 0 29939 29 0 0 25 0 1 0 1846722454 12488704 2940 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 3049 2940 145 145 0 2904 0
[pid=27344] vsize: 12196
Current children cumulated CPU time (s) 299.69
Current children cumulated vsize (Kb) 14320

[startup+310.033 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 2953 0 0 0 30939 30 0 0 25 0 1 0 1846722454 12488704 2940 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 3049 2940 145 145 0 2904 0
[pid=27344] vsize: 12196
Current children cumulated CPU time (s) 309.7
Current children cumulated vsize (Kb) 14320

[startup+320.034 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 2953 0 0 0 31939 30 0 0 25 0 1 0 1846722454 12488704 2940 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 3049 2940 145 145 0 2904 0
[pid=27344] vsize: 12196
Current children cumulated CPU time (s) 319.7
Current children cumulated vsize (Kb) 14320

[startup+330.034 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 2953 0 0 0 32940 30 0 0 25 0 1 0 1846722454 12488704 2940 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 3049 2940 145 145 0 2904 0
[pid=27344] vsize: 12196
Current children cumulated CPU time (s) 329.71
Current children cumulated vsize (Kb) 14320

[startup+340.034 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 2953 0 0 0 33939 30 0 0 25 0 1 0 1846722454 12488704 2940 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 3049 2940 145 145 0 2904 0
[pid=27344] vsize: 12196
Current children cumulated CPU time (s) 339.7
Current children cumulated vsize (Kb) 14320

[startup+350.035 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 2954 0 0 0 34940 30 0 0 25 0 1 0 1846722454 12488704 2941 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 3049 2941 145 145 0 2904 0
[pid=27344] vsize: 12196
Current children cumulated CPU time (s) 349.71
Current children cumulated vsize (Kb) 14320

[startup+360.036 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 2954 0 0 0 35940 30 0 0 25 0 1 0 1846722454 12488704 2941 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27344/statm): 3049 2941 145 145 0 2904 0
[pid=27344] vsize: 12196
Current children cumulated CPU time (s) 359.71
Current children cumulated vsize (Kb) 14320

[startup+370.038 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 2955 0 0 0 36939 31 0 0 25 0 1 0 1846722454 12488704 2942 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 3049 2942 145 145 0 2904 0
[pid=27344] vsize: 12196
Current children cumulated CPU time (s) 369.71
Current children cumulated vsize (Kb) 14320

[startup+380.038 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 2955 0 0 0 37939 31 0 0 25 0 1 0 1846722454 12488704 2942 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 3049 2942 145 145 0 2904 0
[pid=27344] vsize: 12196
Current children cumulated CPU time (s) 379.71
Current children cumulated vsize (Kb) 14320

[startup+390.039 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 3080 0 0 0 38937 31 0 0 25 0 1 0 1846722454 12992512 3067 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 3172 3067 145 145 0 3027 0
[pid=27344] vsize: 12688
Current children cumulated CPU time (s) 389.69
Current children cumulated vsize (Kb) 14812

[startup+400.04 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 3103 0 0 0 39937 32 0 0 25 0 1 0 1846722454 13090816 3090 4294967295 134512640 135094434 3221224432 3221223024 134557416 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 3196 3090 145 145 0 3051 0
[pid=27344] vsize: 12784
Current children cumulated CPU time (s) 399.7
Current children cumulated vsize (Kb) 14908

[startup+410.04 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 3110 0 0 0 40937 32 0 0 25 0 1 0 1846722454 13123584 3097 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 3204 3097 145 145 0 3059 0
[pid=27344] vsize: 12816
Current children cumulated CPU time (s) 409.7
Current children cumulated vsize (Kb) 14940

[startup+420.041 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 3110 0 0 0 41937 32 0 0 25 0 1 0 1846722454 13123584 3097 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 3204 3097 145 145 0 3059 0
[pid=27344] vsize: 12816
Current children cumulated CPU time (s) 419.7
Current children cumulated vsize (Kb) 14940

[startup+430.042 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 3110 0 0 0 42937 32 0 0 25 0 1 0 1846722454 13123584 3097 4294967295 134512640 135094434 3221224432 3221223104 134556266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 3204 3097 145 145 0 3059 0
[pid=27344] vsize: 12816
Current children cumulated CPU time (s) 429.7
Current children cumulated vsize (Kb) 14940

[startup+440.042 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 3110 0 0 0 43938 32 0 0 25 0 1 0 1846722454 13123584 3097 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 3204 3097 145 145 0 3059 0
[pid=27344] vsize: 12816
Current children cumulated CPU time (s) 439.71
Current children cumulated vsize (Kb) 14940

[startup+450.043 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 3113 0 0 0 44938 32 0 0 25 0 1 0 1846722454 13139968 3100 4294967295 134512640 135094434 3221224432 3221223088 134557920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 3208 3100 145 145 0 3063 0
[pid=27344] vsize: 12832
Current children cumulated CPU time (s) 449.71
Current children cumulated vsize (Kb) 14956

[startup+460.044 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 3198 0 0 0 45937 33 0 0 25 0 1 0 1846722454 13488128 3185 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27344/statm): 3293 3185 145 145 0 3148 0
[pid=27344] vsize: 13172
Current children cumulated CPU time (s) 459.71
Current children cumulated vsize (Kb) 15296

[startup+470.046 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 3304 0 0 0 46935 34 0 0 25 0 1 0 1846722454 13914112 3291 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27344/statm): 3397 3291 145 145 0 3252 0
[pid=27344] vsize: 13588
Current children cumulated CPU time (s) 469.7
Current children cumulated vsize (Kb) 15712

[startup+480.047 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 3311 0 0 0 47935 34 0 0 25 0 1 0 1846722454 13942784 3298 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27344/statm): 3404 3298 145 145 0 3259 0
[pid=27344] vsize: 13616
Current children cumulated CPU time (s) 479.7
Current children cumulated vsize (Kb) 15740

[startup+490.048 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 3319 0 0 0 48934 35 0 0 25 0 1 0 1846722454 13983744 3306 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27344/statm): 3414 3306 145 145 0 3269 0
[pid=27344] vsize: 13656
Current children cumulated CPU time (s) 489.7
Current children cumulated vsize (Kb) 15780

[startup+500.05 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 3319 0 0 0 49934 35 0 0 25 0 1 0 1846722454 13983744 3306 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27344/statm): 3414 3306 145 145 0 3269 0
[pid=27344] vsize: 13656
Current children cumulated CPU time (s) 499.7
Current children cumulated vsize (Kb) 15780

[startup+510.051 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 3319 0 0 0 50934 35 0 0 25 0 1 0 1846722454 13983744 3306 4294967295 134512640 135094434 3221224432 3221222976 134562152 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27344/statm): 3414 3306 145 145 0 3269 0
[pid=27344] vsize: 13656
Current children cumulated CPU time (s) 509.7
Current children cumulated vsize (Kb) 15780

[startup+520.052 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 3347 0 0 0 51933 36 0 0 25 0 1 0 1846722454 14098432 3334 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27344/statm): 3442 3334 145 145 0 3297 0
[pid=27344] vsize: 13768
Current children cumulated CPU time (s) 519.7
Current children cumulated vsize (Kb) 15892

[startup+530.053 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 3359 0 0 0 52933 36 0 0 25 0 1 0 1846722454 14147584 3346 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27344/statm): 3454 3346 145 145 0 3309 0
[pid=27344] vsize: 13816
Current children cumulated CPU time (s) 529.7
Current children cumulated vsize (Kb) 15940

[startup+540.054 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 3359 0 0 0 53932 36 0 0 25 0 1 0 1846722454 14147584 3346 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27344/statm): 3454 3346 145 145 0 3309 0
[pid=27344] vsize: 13816
Current children cumulated CPU time (s) 539.69
Current children cumulated vsize (Kb) 15940

[startup+550.055 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 3359 0 0 0 54932 37 0 0 25 0 1 0 1846722454 14147584 3346 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 3454 3346 145 145 0 3309 0
[pid=27344] vsize: 13816
Current children cumulated CPU time (s) 549.7
Current children cumulated vsize (Kb) 15940

[startup+560.055 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 3359 0 0 0 55932 37 0 0 25 0 1 0 1846722454 14147584 3346 4294967295 134512640 135094434 3221224432 3221223088 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 3454 3346 145 145 0 3309 0
[pid=27344] vsize: 13816
Current children cumulated CPU time (s) 559.7
Current children cumulated vsize (Kb) 15940

[startup+570.056 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 3359 0 0 0 56932 37 0 0 25 0 1 0 1846722454 14147584 3346 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 3454 3346 145 145 0 3309 0
[pid=27344] vsize: 13816
Current children cumulated CPU time (s) 569.7
Current children cumulated vsize (Kb) 15940

[startup+580.057 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 3359 0 0 0 57932 37 0 0 25 0 1 0 1846722454 14147584 3346 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 3454 3346 145 145 0 3309 0
[pid=27344] vsize: 13816
Current children cumulated CPU time (s) 579.7
Current children cumulated vsize (Kb) 15940

[startup+590.057 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 3359 0 0 0 58932 37 0 0 25 0 1 0 1846722454 14147584 3346 4294967295 134512640 135094434 3221224432 3221223088 134557890 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 3454 3346 145 145 0 3309 0
[pid=27344] vsize: 13816
Current children cumulated CPU time (s) 589.7
Current children cumulated vsize (Kb) 15940

[startup+600.058 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 3359 0 0 0 59932 38 0 0 25 0 1 0 1846722454 14147584 3346 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 3454 3346 145 145 0 3309 0
[pid=27344] vsize: 13816
Current children cumulated CPU time (s) 599.71
Current children cumulated vsize (Kb) 15940

[startup+610.058 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 3359 0 0 0 60932 38 0 0 25 0 1 0 1846722454 14147584 3346 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 3454 3346 145 145 0 3309 0
[pid=27344] vsize: 13816
Current children cumulated CPU time (s) 609.71
Current children cumulated vsize (Kb) 15940

[startup+620.059 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 3359 0 0 0 61933 38 0 0 25 0 1 0 1846722454 14147584 3346 4294967295 134512640 135094434 3221224432 3221223088 134558398 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 3454 3346 145 145 0 3309 0
[pid=27344] vsize: 13816
Current children cumulated CPU time (s) 619.72
Current children cumulated vsize (Kb) 15940

[startup+630.06 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 3359 0 0 0 62933 38 0 0 25 0 1 0 1846722454 14147584 3346 4294967295 134512640 135094434 3221224432 3221223088 134558153 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 3454 3346 145 145 0 3309 0
[pid=27344] vsize: 13816
Current children cumulated CPU time (s) 629.72
Current children cumulated vsize (Kb) 15940

[startup+640.061 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 3359 0 0 0 63933 38 0 0 25 0 1 0 1846722454 14147584 3346 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 3454 3346 145 145 0 3309 0
[pid=27344] vsize: 13816
Current children cumulated CPU time (s) 639.72
Current children cumulated vsize (Kb) 15940

[startup+650.062 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 3359 0 0 0 64933 38 0 0 25 0 1 0 1846722454 14147584 3346 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 3454 3346 145 145 0 3309 0
[pid=27344] vsize: 13816
Current children cumulated CPU time (s) 649.72
Current children cumulated vsize (Kb) 15940

[startup+660.062 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 3359 0 0 0 65933 38 0 0 25 0 1 0 1846722454 14147584 3346 4294967295 134512640 135094434 3221224432 3221223056 134557717 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 3454 3346 145 145 0 3309 0
[pid=27344] vsize: 13816
Current children cumulated CPU time (s) 659.72
Current children cumulated vsize (Kb) 15940

[startup+670.063 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 3359 0 0 0 66934 38 0 0 25 0 1 0 1846722454 14147584 3346 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 3454 3346 145 145 0 3309 0
[pid=27344] vsize: 13816
Current children cumulated CPU time (s) 669.73
Current children cumulated vsize (Kb) 15940

[startup+680.064 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 3359 0 0 0 67932 40 0 0 25 0 1 0 1846722454 14147584 3346 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 3454 3346 145 145 0 3309 0
[pid=27344] vsize: 13816
Current children cumulated CPU time (s) 679.73
Current children cumulated vsize (Kb) 15940

[startup+690.064 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 3359 0 0 0 68932 40 0 0 25 0 1 0 1846722454 14147584 3346 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 3454 3346 145 145 0 3309 0
[pid=27344] vsize: 13816
Current children cumulated CPU time (s) 689.73
Current children cumulated vsize (Kb) 15940

[startup+700.065 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 3359 0 0 0 69932 40 0 0 25 0 1 0 1846722454 14147584 3346 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 3454 3346 145 145 0 3309 0
[pid=27344] vsize: 13816
Current children cumulated CPU time (s) 699.73
Current children cumulated vsize (Kb) 15940

[startup+710.065 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 3359 0 0 0 70932 41 0 0 25 0 1 0 1846722454 14147584 3346 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 3454 3346 145 145 0 3309 0
[pid=27344] vsize: 13816
Current children cumulated CPU time (s) 709.74
Current children cumulated vsize (Kb) 15940

[startup+720.066 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 3359 0 0 0 71932 41 0 0 25 0 1 0 1846722454 14147584 3346 4294967295 134512640 135094434 3221224432 3221223024 134556851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 3454 3346 145 145 0 3309 0
[pid=27344] vsize: 13816
Current children cumulated CPU time (s) 719.74
Current children cumulated vsize (Kb) 15940

[startup+730.067 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 3381 0 0 0 72932 41 0 0 25 0 1 0 1846722454 14237696 3368 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 3476 3368 145 145 0 3331 0
[pid=27344] vsize: 13904
Current children cumulated CPU time (s) 729.74
Current children cumulated vsize (Kb) 16028

[startup+740.068 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 3381 0 0 0 73932 41 0 0 25 0 1 0 1846722454 14237696 3368 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 3476 3368 145 145 0 3331 0
[pid=27344] vsize: 13904
Current children cumulated CPU time (s) 739.74
Current children cumulated vsize (Kb) 16028

[startup+750.069 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 3388 0 0 0 74932 41 0 0 25 0 1 0 1846722454 14266368 3375 4294967295 134512640 135094434 3221224432 3221223088 134557934 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 3483 3375 145 145 0 3338 0
[pid=27344] vsize: 13932
Current children cumulated CPU time (s) 749.74
Current children cumulated vsize (Kb) 16056

[startup+760.069 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 3454 0 0 0 75930 42 0 0 25 0 1 0 1846722454 14536704 3441 4294967295 134512640 135094434 3221224432 3221223024 134551868 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 3549 3441 145 145 0 3404 0
[pid=27344] vsize: 14196
Current children cumulated CPU time (s) 759.73
Current children cumulated vsize (Kb) 16320

[startup+770.07 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 3454 0 0 0 76930 42 0 0 25 0 1 0 1846722454 14536704 3441 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 3549 3441 145 145 0 3404 0
[pid=27344] vsize: 14196
Current children cumulated CPU time (s) 769.73
Current children cumulated vsize (Kb) 16320

[startup+780.071 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 3454 0 0 0 77931 42 0 0 25 0 1 0 1846722454 14536704 3441 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 3549 3441 145 145 0 3404 0
[pid=27344] vsize: 14196
Current children cumulated CPU time (s) 779.74
Current children cumulated vsize (Kb) 16320

[startup+790.072 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 3500 0 0 0 78930 43 0 0 25 0 1 0 1846722454 14725120 3487 4294967295 134512640 135094434 3221224432 3221223104 134556523 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 3595 3487 145 145 0 3450 0
[pid=27344] vsize: 14380
Current children cumulated CPU time (s) 789.74
Current children cumulated vsize (Kb) 16504

[startup+800.073 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 3500 0 0 0 79930 43 0 0 25 0 1 0 1846722454 14725120 3487 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 3595 3487 145 145 0 3450 0
[pid=27344] vsize: 14380
Current children cumulated CPU time (s) 799.74
Current children cumulated vsize (Kb) 16504

[startup+810.072 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 3500 0 0 0 80930 43 0 0 25 0 1 0 1846722454 14725120 3487 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 3595 3487 145 145 0 3450 0
[pid=27344] vsize: 14380
Current children cumulated CPU time (s) 809.74
Current children cumulated vsize (Kb) 16504

[startup+820.074 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 3500 0 0 0 81930 44 0 0 25 0 1 0 1846722454 14725120 3487 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 3595 3487 145 145 0 3450 0
[pid=27344] vsize: 14380
Current children cumulated CPU time (s) 819.75
Current children cumulated vsize (Kb) 16504

[startup+830.075 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 3500 0 0 0 82930 44 0 0 25 0 1 0 1846722454 14725120 3487 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 3595 3487 145 145 0 3450 0
[pid=27344] vsize: 14380
Current children cumulated CPU time (s) 829.75
Current children cumulated vsize (Kb) 16504

[startup+840.076 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 3500 0 0 0 83930 44 0 0 25 0 1 0 1846722454 14725120 3487 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 3595 3487 145 145 0 3450 0
[pid=27344] vsize: 14380
Current children cumulated CPU time (s) 839.75
Current children cumulated vsize (Kb) 16504

[startup+850.077 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 3500 0 0 0 84930 44 0 0 25 0 1 0 1846722454 14725120 3487 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 3595 3487 145 145 0 3450 0
[pid=27344] vsize: 14380
Current children cumulated CPU time (s) 849.75
Current children cumulated vsize (Kb) 16504

[startup+860.077 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 3500 0 0 0 85930 44 0 0 25 0 1 0 1846722454 14725120 3487 4294967295 134512640 135094434 3221224432 3221223088 134558246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 3595 3487 145 145 0 3450 0
[pid=27344] vsize: 14380
Current children cumulated CPU time (s) 859.75
Current children cumulated vsize (Kb) 16504

[startup+870.078 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 3500 0 0 0 86930 44 0 0 25 0 1 0 1846722454 14725120 3487 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 3595 3487 145 145 0 3450 0
[pid=27344] vsize: 14380
Current children cumulated CPU time (s) 869.75
Current children cumulated vsize (Kb) 16504

[startup+880.079 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 3500 0 0 0 87930 45 0 0 25 0 1 0 1846722454 14725120 3487 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 3595 3487 145 145 0 3450 0
[pid=27344] vsize: 14380
Current children cumulated CPU time (s) 879.76
Current children cumulated vsize (Kb) 16504

[startup+890.08 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 3500 0 0 0 88931 45 0 0 25 0 1 0 1846722454 14725120 3487 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 3595 3487 145 145 0 3450 0
[pid=27344] vsize: 14380
Current children cumulated CPU time (s) 889.77
Current children cumulated vsize (Kb) 16504

[startup+900.08 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 3500 0 0 0 89931 45 0 0 25 0 1 0 1846722454 14725120 3487 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 3595 3487 145 145 0 3450 0
[pid=27344] vsize: 14380
Current children cumulated CPU time (s) 899.77
Current children cumulated vsize (Kb) 16504

[startup+910.081 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 3500 0 0 0 90931 45 0 0 25 0 1 0 1846722454 14725120 3487 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 3595 3487 145 145 0 3450 0
[pid=27344] vsize: 14380
Current children cumulated CPU time (s) 909.77
Current children cumulated vsize (Kb) 16504

[startup+920.082 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 3500 0 0 0 91931 45 0 0 25 0 1 0 1846722454 14725120 3487 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 3595 3487 145 145 0 3450 0
[pid=27344] vsize: 14380
Current children cumulated CPU time (s) 919.77
Current children cumulated vsize (Kb) 16504

[startup+930.083 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 3500 0 0 0 92931 45 0 0 25 0 1 0 1846722454 14725120 3487 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 3595 3487 145 145 0 3450 0
[pid=27344] vsize: 14380
Current children cumulated CPU time (s) 929.77
Current children cumulated vsize (Kb) 16504

[startup+940.084 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 3500 0 0 0 93931 45 0 0 25 0 1 0 1846722454 14725120 3487 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 3595 3487 145 145 0 3450 0
[pid=27344] vsize: 14380
Current children cumulated CPU time (s) 939.77
Current children cumulated vsize (Kb) 16504

[startup+950.084 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 3500 0 0 0 94931 45 0 0 25 0 1 0 1846722454 14725120 3487 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 3595 3487 145 145 0 3450 0
[pid=27344] vsize: 14380
Current children cumulated CPU time (s) 949.77
Current children cumulated vsize (Kb) 16504

[startup+960.085 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 3500 0 0 0 95931 46 0 0 25 0 1 0 1846722454 14725120 3487 4294967295 134512640 135094434 3221224432 3221223088 134557945 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 3595 3487 145 145 0 3450 0
[pid=27344] vsize: 14380
Current children cumulated CPU time (s) 959.78
Current children cumulated vsize (Kb) 16504

[startup+970.086 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 3500 0 0 0 96931 46 0 0 25 0 1 0 1846722454 14725120 3487 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 3595 3487 145 145 0 3450 0
[pid=27344] vsize: 14380
Current children cumulated CPU time (s) 969.78
Current children cumulated vsize (Kb) 16504

[startup+980.087 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 3500 0 0 0 97931 46 0 0 25 0 1 0 1846722454 14725120 3487 4294967295 134512640 135094434 3221224432 3221223088 134558181 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27344/statm): 3595 3487 145 145 0 3450 0
[pid=27344] vsize: 14380
Current children cumulated CPU time (s) 979.78
Current children cumulated vsize (Kb) 16504

[startup+990.088 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 3549 0 0 0 98930 46 0 0 25 0 1 0 1846722454 14929920 3536 4294967295 134512640 135094434 3221224432 3221223088 134558162 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27344/statm): 3645 3536 145 145 0 3500 0
[pid=27344] vsize: 14580
Current children cumulated CPU time (s) 989.77
Current children cumulated vsize (Kb) 16704

[startup+1000.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 3549 0 0 0 99930 46 0 0 25 0 1 0 1846722454 14929920 3536 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 3645 3536 145 145 0 3500 0
[pid=27344] vsize: 14580
Current children cumulated CPU time (s) 999.77
Current children cumulated vsize (Kb) 16704

[startup+1010.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 3605 0 0 0 100929 47 0 0 25 0 1 0 1846722454 15159296 3592 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 3701 3592 145 145 0 3556 0
[pid=27344] vsize: 14804
Current children cumulated CPU time (s) 1009.77
Current children cumulated vsize (Kb) 16928

[startup+1020.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 3813 0 0 0 101924 49 0 0 25 0 1 0 1846722454 16011264 3800 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 3909 3800 145 145 0 3764 0
[pid=27344] vsize: 15636
Current children cumulated CPU time (s) 1019.74
Current children cumulated vsize (Kb) 17760

[startup+1030.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 3813 0 0 0 102924 49 0 0 25 0 1 0 1846722454 16011264 3800 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 3909 3800 145 145 0 3764 0
[pid=27344] vsize: 15636
Current children cumulated CPU time (s) 1029.74
Current children cumulated vsize (Kb) 17760

[startup+1040.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 3817 0 0 0 103924 49 0 0 25 0 1 0 1846722454 16027648 3804 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 3913 3804 145 145 0 3768 0
[pid=27344] vsize: 15652
Current children cumulated CPU time (s) 1039.74
Current children cumulated vsize (Kb) 17776

[startup+1050.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 4064 0 0 0 104919 52 0 0 25 0 1 0 1846722454 17043456 4051 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 4161 4051 145 145 0 4016 0
[pid=27344] vsize: 16644
Current children cumulated CPU time (s) 1049.72
Current children cumulated vsize (Kb) 18768

[startup+1060.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 4087 0 0 0 105918 52 0 0 25 0 1 0 1846722454 17137664 4074 4294967295 134512640 135094434 3221224432 3221223120 134554685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 4184 4074 145 145 0 4039 0
[pid=27344] vsize: 16736
Current children cumulated CPU time (s) 1059.71
Current children cumulated vsize (Kb) 18860

[startup+1070.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 4087 0 0 0 106918 52 0 0 25 0 1 0 1846722454 17137664 4074 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 4184 4074 145 145 0 4039 0
[pid=27344] vsize: 16736
Current children cumulated CPU time (s) 1069.71
Current children cumulated vsize (Kb) 18860

[startup+1080.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 4087 0 0 0 107918 52 0 0 25 0 1 0 1846722454 17137664 4074 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 4184 4074 145 145 0 4039 0
[pid=27344] vsize: 16736
Current children cumulated CPU time (s) 1079.71
Current children cumulated vsize (Kb) 18860

[startup+1090.1 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 4087 0 0 0 108918 53 0 0 25 0 1 0 1846722454 17137664 4074 4294967295 134512640 135094434 3221224432 3221223024 134557300 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 4184 4074 145 145 0 4039 0
[pid=27344] vsize: 16736
Current children cumulated CPU time (s) 1089.72
Current children cumulated vsize (Kb) 18860

[startup+1100.1 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 4087 0 0 0 109918 53 0 0 25 0 1 0 1846722454 17137664 4074 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 4184 4074 145 145 0 4039 0
[pid=27344] vsize: 16736
Current children cumulated CPU time (s) 1099.72
Current children cumulated vsize (Kb) 18860

[startup+1110.1 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 4120 0 0 0 110919 53 0 0 25 0 1 0 1846722454 17399808 4107 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 4248 4107 145 145 0 4103 0
[pid=27344] vsize: 16992
Current children cumulated CPU time (s) 1109.73
Current children cumulated vsize (Kb) 19116

[startup+1120.1 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 4121 0 0 0 111919 53 0 0 25 0 1 0 1846722454 17399808 4108 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 4248 4108 145 145 0 4103 0
[pid=27344] vsize: 16992
Current children cumulated CPU time (s) 1119.73
Current children cumulated vsize (Kb) 19116

[startup+1130.1 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 4121 0 0 0 112919 53 0 0 25 0 1 0 1846722454 17399808 4108 4294967295 134512640 135094434 3221224432 3221223088 134557984 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 4248 4108 145 145 0 4103 0
[pid=27344] vsize: 16992
Current children cumulated CPU time (s) 1129.73
Current children cumulated vsize (Kb) 19116

[startup+1140.1 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 4121 0 0 0 113919 53 0 0 25 0 1 0 1846722454 17399808 4108 4294967295 134512640 135094434 3221224432 3221223056 134557717 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 4248 4108 145 145 0 4103 0
[pid=27344] vsize: 16992
Current children cumulated CPU time (s) 1139.73
Current children cumulated vsize (Kb) 19116

[startup+1150.1 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 4121 0 0 0 114919 53 0 0 25 0 1 0 1846722454 17399808 4108 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 4248 4108 145 145 0 4103 0
[pid=27344] vsize: 16992
Current children cumulated CPU time (s) 1149.73
Current children cumulated vsize (Kb) 19116

[startup+1160.1 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 4121 0 0 0 115919 54 0 0 25 0 1 0 1846722454 17399808 4108 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 4248 4108 145 145 0 4103 0
[pid=27344] vsize: 16992
Current children cumulated CPU time (s) 1159.74
Current children cumulated vsize (Kb) 19116

[startup+1170.1 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 4121 0 0 0 116919 54 0 0 25 0 1 0 1846722454 17399808 4108 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 4248 4108 145 145 0 4103 0
[pid=27344] vsize: 16992
Current children cumulated CPU time (s) 1169.74
Current children cumulated vsize (Kb) 19116

[startup+1180.1 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 4121 0 0 0 117919 54 0 0 25 0 1 0 1846722454 17399808 4108 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 4248 4108 145 145 0 4103 0
[pid=27344] vsize: 16992
Current children cumulated CPU time (s) 1179.74
Current children cumulated vsize (Kb) 19116

[startup+1190.1 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 4121 0 0 0 118919 54 0 0 25 0 1 0 1846722454 17399808 4108 4294967295 134512640 135094434 3221224432 3221223088 134557972 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 4248 4108 145 145 0 4103 0
[pid=27344] vsize: 16992
Current children cumulated CPU time (s) 1189.74
Current children cumulated vsize (Kb) 19116

[startup+1200.1 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 4121 0 0 0 119920 54 0 0 25 0 1 0 1846722454 17399808 4108 4294967295 134512640 135094434 3221224432 3221223104 134556266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 4248 4108 145 145 0 4103 0
[pid=27344] vsize: 16992
Current children cumulated CPU time (s) 1199.75
Current children cumulated vsize (Kb) 19116

[startup+1210.11 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 4121 0 0 0 120920 54 0 0 25 0 1 0 1846722454 17399808 4108 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 4248 4108 145 145 0 4103 0
[pid=27344] vsize: 16992
Current children cumulated CPU time (s) 1209.75
Current children cumulated vsize (Kb) 19116



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.11 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 27344
Raw data (/proc/27340/stat): 27340 (minisat+_script) S 27339 27340 19818 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1846722449 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27340/statm): 531 226 485 147 0 384 0
[pid=27340] vsize: 2124
Raw data (/proc/27344/stat): 27344 (minisat+_64-bit) R 27340 27340 19818 0 -1 0 4121 0 0 0 120920 54 0 0 25 0 1 0 1846722454 17399808 4108 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27344/statm): 4248 4108 145 145 0 4103 0
[pid=27344] vsize: 16992
Current children cumulated CPU time (s) 1209.75
Current children cumulated vsize (Kb) 19116

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

Child status: 10
Real time (s): 1210.12
CPU time (s): 1209.76
CPU user time (s): 1209.21
CPU system time (s): 0.555915
CPU usage (%): 99.9705
Max. virtual memory (cumulated for all children) (Kb): 19116

Verifier Data

ERROR: no interpretation found !