Some explanations

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

General information on the benchmark

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

Trace number 2292

Launcher Data

LAUNCH ON wulflinc21 THE 2005-09-18 18:45:15 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2698 boxname=wulflinc21 idbench=354 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  38d41fdbe49543e8928c5210e4323f00  /oldhome/oroussel/tmp/wulflinc21/normalized-frb40-19-5.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc21/normalized-frb40-19-5.opb
IDLAUNCH: 2698
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.161
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	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.161
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:        893708 kB
Buffers:         35092 kB
Cached:          78308 kB
SwapCached:        908 kB
Active:          79892 kB
Inactive:        36168 kB
HighTotal:      131008 kB
HighFree:        56560 kB
LowTotal:       903652 kB
LowFree:        837148 kB
SwapTotal:     2097892 kB
SwapFree:      2096472 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5804 kB
Slab:            19200 kB
Committed_AS:    64332 kB
PageTables:        340 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-18 19:05:25 (client local time) WITH STATUS 10 IN 1209.33 SECONDS
stats: 2698 7 1209.33 10

Solver Data

c Parsing PB file...
c Converting 41619 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ...................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   41619    83238 |   13873       0        0     nan |  0.000 % |
c ==============================================================================
c Found solution: -27
c ---[   0]---> Sorter-cost:35010     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   77738   168085 |   25912       0        0     nan |  0.000 % |
c |       100 |   77393   167370 |   28503      74      614     8.3 |  0.753 % |
c |       250 |   76571   165604 |   31353     182     1860    10.2 |  2.662 % |
c |       475 |   75416   163089 |   34488     361     3656    10.1 |  5.412 % |
c |       812 |   73469   158808 |   37937     588     7576    12.9 | 10.134 % |
c |      1318 |   71470   154363 |   41731     995    12456    12.5 | 15.052 % |
c |      2077 |   68055   146635 |   45904    1571    21571    13.7 | 23.713 % |
c ==============================================================================
c Found solution: -30
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2368 |   66345   142775 |   22115    1722    23486    13.6 | 23.713 % |
c |      2468 |   65954   141886 |   24326    1798    24101    13.4 | 29.188 % |
c |      2618 |   65428   140687 |   26759    1916    26017    13.6 | 30.521 % |
c |      2843 |   64784   139204 |   29435    2104    29300    13.9 | 32.202 % |
c |      3180 |   63783   136936 |   32378    2343    33178    14.2 | 34.720 % |
c |      3686 |   62671   134380 |   35616    2764    38470    13.9 | 37.600 % |
c |      4445 |   60688   129777 |   39178    3385    46444    13.7 | 42.715 % |
c ==============================================================================
c Found solution: -31
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4942 |   59952   128172 |   19984    3811    62121    16.3 | 42.715 % |
c |      5042 |   59679   127517 |   21982    3894    63964    16.4 | 45.623 % |
c |      5192 |   59303   126633 |   24180    4014    65656    16.4 | 46.620 % |
c |      5417 |   58170   123919 |   26598    4092    67984    16.6 | 49.720 % |
c |      5755 |   57394   122041 |   29258    4355    72331    16.6 | 51.880 % |
c |      6261 |   56683   120374 |   32184    4714    77744    16.5 | 53.783 % |
c |      7020 |   54571   115370 |   35402    5132    87529    17.1 | 59.526 % |
c |      8159 |   53100   111874 |   38943    6005   106837    17.8 | 63.555 % |
c |      9867 |   51361   107721 |   42837    7233   142892    19.8 | 68.277 % |
c ==============================================================================
c Found solution: -32
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11787 |   49479   103125 |   16493    8440   181552    21.5 | 68.277 % |
c |     11887 |   49297   102693 |   18142    8475   182904    21.6 | 74.014 % |
c |     12037 |   49131   102301 |   19956    8543   185298    21.7 | 74.456 % |
c |     12262 |   49025   102033 |   21952    8701   189426    21.8 | 74.770 % |
c |     12602 |   48860   101631 |   24147    8952   197477    22.1 | 75.240 % |
c |     13108 |   48811   101518 |   26562    9438   225449    23.9 | 75.369 % |
c ==============================================================================
c Found solution: -33
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     13835 |   48637   101137 |   16212   10042   261315    26.0 | 75.369 % |
c |     13935 |   48570   100975 |   17833   10127   264156    26.1 | 76.055 % |
c |     14085 |   48570   100975 |   19616   10277   269303    26.2 | 76.055 % |
c |     14312 |   48535   100890 |   21578   10475   276829    26.4 | 76.156 % |
c |     14649 |   48224   100143 |   23735   10596   283579    26.8 | 77.024 % |
c |     15155 |   47936    99449 |   26109   10862   295418    27.2 | 77.815 % |
c |     15915 |   47936    99449 |   28720   11622   352382    30.3 | 77.815 % |
c ==============================================================================
c Found solution: -34
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     16092 |   47809    99110 |   15936   11694   348286    29.8 | 77.815 % |
c |     16193 |   47809    99110 |   17529   11795   351047    29.8 | 78.162 % |
c |     16343 |   47809    99110 |   19282   11945   358187    30.0 | 78.162 % |
c |     16568 |   47699    98850 |   21210   12069   366809    30.4 | 78.463 % |
c |     16907 |   47699    98850 |   23331   12408   381170    30.7 | 78.463 % |
c |     17413 |   47691    98830 |   25665   12893   410134    31.8 | 78.487 % |
c |     18172 |   47570    98547 |   28231   13507   456879    33.8 | 78.813 % |
c |     19312 |   47514    98418 |   31054   14523   514679    35.4 | 78.957 % |
c |     21020 |   47429    98213 |   34160   16152   617687    38.2 | 79.194 % |
c |     23582 |   47246    97781 |   37576   18577   833388    44.9 | 79.692 % |
c |     27427 |   47199    97655 |   41333   22352  1265776    56.6 | 79.845 % |
c |     33193 |   47092    97395 |   45467   28078  1866446    66.5 | 80.150 % |
c |     41842 |   46935    97003 |   50013   36506  2578978    70.6 | 80.608 % |
c |     54816 |   46775    96601 |   55015   49208  3834743    77.9 | 81.078 % |
c ==============================================================================
c Found solution: -35
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     66599 |   46701    96441 |   15567   60446  4917752    81.4 | 81.078 % |
c |     66699 |   46701    96441 |   17123   18649  1166349    62.5 | 81.358 % |
c |     66849 |   46701    96441 |   18836   18799  1175990    62.6 | 81.358 % |
c |     67075 |   46701    96441 |   20719   19025  1183368    62.2 | 81.358 % |
c |     67412 |   46698    96434 |   22791   19361  1203497    62.2 | 81.366 % |
c |     67920 |   46667    96361 |   25070   19848  1238599    62.4 | 81.450 % |
c |     68680 |   46645    96307 |   27577   20600  1270078    61.7 | 81.514 % |
c |     69819 |   46584    96158 |   30335   21676  1347252    62.2 | 81.690 % |
c |     71527 |   46518    95998 |   33369   23343  1512076    64.8 | 81.874 % |
c |     74089 |   46518    95998 |   36706   25905  1789120    69.1 | 81.874 % |
c |     77933 |   46488    95928 |   40376   29711  2161793    72.8 | 81.954 % |
c |     83701 |   46272    95398 |   44414   35390  2699227    76.3 | 82.566 % |
c |     92350 |   46247    95337 |   48855   43978  3619619    82.3 | 82.639 % |
c |    105326 |   46247    95337 |   53741   56954  5420125    95.2 | 82.638 % |
c ==============================================================================
c Found solution: -36
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    109573 |   46236    95289 |   15412   61020  6058538    99.3 | 82.638 % |
c |    109673 |   46236    95289 |   16953   17964  1912579   106.5 | 82.676 % |
c |    109824 |   46236    95289 |   18648   18115  1920817   106.0 | 82.676 % |
c |    110050 |   46236    95289 |   20513   18341  1933595   105.4 | 82.676 % |
c |    110387 |   46221    95254 |   22564   18674  1951460   104.5 | 82.716 % |
c |    110894 |   46221    95254 |   24821   19181  1987235   103.6 | 82.716 % |
c |    111653 |   46221    95254 |   27303   19940  2051460   102.9 | 82.716 % |
c |    112792 |   46174    95141 |   30033   21056  2143668   101.8 | 82.844 % |
c |    114503 |   46174    95141 |   33036   22767  2317315   101.8 | 82.844 % |
c |    117066 |   46174    95141 |   36340   25330  2565419   101.3 | 82.844 % |
c |    120910 |   46140    95059 |   39974   29170  2926517   100.3 | 82.940 % |
c |    126676 |   46140    95059 |   43972   34936  3469893    99.3 | 82.940 % |
c ==============================================================================
c Found solution: -37
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    128815 |   46161    95117 |   15387   37075  3702991    99.9 | 82.940 % |
c |    128916 |   46161    95117 |   16925   17069  1143112    67.0 | 82.903 % |
c |    129066 |   46161    95117 |   18618   17219  1153278    67.0 | 82.903 % |
c |    129293 |   46161    95117 |   20480   17446  1162668    66.6 | 82.903 % |
c |    129630 |   46126    95028 |   22528   17771  1187614    66.8 | 83.011 % |
c |    130137 |   46126    95028 |   24780   18278  1223931    67.0 | 83.011 % |
c |    130896 |   46051    94848 |   27259   19008  1237330    65.1 | 83.219 % |
c |    132035 |   46015    94758 |   29984   20133  1322301    65.7 | 83.315 % |
c |    133744 |   46015    94758 |   32983   21842  1465933    67.1 | 83.315 % |
c |    136307 |   46015    94758 |   36281   24405  1721914    70.6 | 83.315 % |
c |    140151 |   46015    94758 |   39909   28249  2009666    71.1 | 83.315 % |
c |    145918 |   46013    94754 |   43900   34014  2543986    74.8 | 83.319 % |
c |    154568 |   45959    94626 |   48290   42576  3184772    74.8 | 83.467 % |
c |    167543 |   45913    94520 |   53120   55540  4225297    76.1 | 83.587 % |
c |    187005 |   45913    94520 |   58432   75002  6244640    83.3 | 83.587 % |
c |    216198 |   45876    94429 |   64275   44973  3102677    69.0 | 83.694 % |
c |    259987 |   45876    94429 |   70702   22219  1193746    53.7 | 83.694 % |
c |    325671 |   45838    94339 |   77773   87896  5215189    59.3 | 83.798 % |
c ==============================================================================
c Found solution: -38
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    362744 |   45824    94273 |   15274   45452  1802921    39.7 | 83.798 % |
c |    362845 |   45824    94273 |   16801   20765   632823    30.5 | 83.844 % |
c |    362996 |   45824    94273 |   18481   20916   640662    30.6 | 83.844 % |
c |    363222 |   45824    94273 |   20329   21142   649300    30.7 | 83.844 % |
c |    363560 |   45824    94273 |   22362   21480   662066    30.8 | 83.844 % |
c |    364066 |   45824    94273 |   24598   21986   685062    31.2 | 83.844 % |
c |    364826 |   45824    94273 |   27058   22746   727210    32.0 | 83.844 % |
c |    365965 |   45824    94273 |   29764   23885   810735    33.9 | 83.844 % |
c |    367674 |   45824    94273 |   32741   25594   906072    35.4 | 83.844 % |
c |    370236 |   45824    94273 |   36015   28156  1054352    37.4 | 83.844 % |
c |    374082 |   45737    94058 |   39616   31979  1334937    41.7 | 84.083 % |
c |    379848 |   45698    93956 |   43578   37273  1691710    45.4 | 84.203 % |
c |    388498 |   45694    93948 |   47936   45919  2503857    54.5 | 84.211 % |
c |    401472 |   45694    93948 |   52729   58893  3447993    58.5 | 84.211 % |
c |    420934 |   45643    93821 |   58002   23036   699613    30.4 | 84.363 % |
c |    450126 |   45640    93814 |   63803   52227  1837279    35.2 | 84.371 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -C760 -C759 -C758 -C757 -C756 -C755 -C754 -C753 -C752 -C751 -C750 -C749 -C748 -C747 -C746 -C745 C744 -C743 -C742 -C741 -C740 -C739 -C738 -C737 -C736 -C735 -C734 -C733 -C732 -C731 -C730 -C729 -C728 C727 -C726 -C725 -C724 -C723 -C722 -C721 -C720 -C719 -C718 -C717 -C716 -C715 -C714 -C713 -C712 -C711 -C710 -C709 -C708 C707 -C706 -C705 -C704 -C703 -C702 -C701 -C700 -C699 -C698 -C697 -C696 -C695 -C694 -C693 -C692 -C691 C690 -C689 -C688 -C687 -C686 -C685 -C684 -C683 -C682 -C681 -C680 -C679 -C678 -C677 -C676 C675 -C674 -C673 -C672 -C671 -C670 -C669 -C668 -C667 -C666 -C665 -C664 -C663 C662 -C661 -C660 -C659 -C658 -C657 -C656 -C655 -C654 -C653 -C652 -C651 -C650 -C649 -C648 -C647 -C646 -C645 -C644 -C643 -C642 -C641 -C640 -C639 -C638 -C637 -C636 -C635 -C634 C633 -C632 -C631 -C630 -C629 -C628 -C627 -C626 -C625 -C624 -C623 -C622 -C621 -C620 -C619 -C618 -C617 -C616 -C615 C614 -C613 -C612 -C611 -C610 -C609 -C608 -C607 -C606 -C605 -C604 -C603 -C602 -C601 -C600 -C599 -C598 -C597 C596 -C595 -C594 -C593 -C592 -C591 -C590 -C589 -C588 -C587 -C586 -C585 -C584 -C583 -C582 -C581 -C580 -C579 -C578 -C577 -C576 -C575 -C574 -C573 C572 -C571 C570 -C569 -C568 -C567 -C566 -C565 -C564 -C563 -C562 -C561 -C560 -C559 -C558 -C557 -C556 -C555 -C554 -C553 -C552 -C551 -C550 -C549 -C548 -C547 -C546 -C545 -C544 -C543 -C542 -C541 -C540 -C539 -C538 -C537 -C536 -C535 -C534 C533 -C532 -C531 -C530 -C529 -C528 -C527 -C526 -C525 -C524 -C523 -C522 -C521 -C520 -C519 -C518 -C517 -C516 -C515 -C514 -C513 -C512 -C511 -C510 -C509 -C508 -C507 -C506 -C505 C504 -C503 -C502 -C501 -C500 -C499 -C498 -C497 -C496 -C495 -C494 -C493 -C492 -C491 -C490 -C489 -C488 -C487 -C486 -C485 -C484 -C483 -C482 -C481 -C480 -C479 -C478 -C477 C476 -C475 -C474 -C473 C472 -C471 -C470 -C469 -C468 -C467 -C466 -C465 -C464 -C463 -C462 -C461 -C460 -C459 -C458 -C457 -C456 -C455 -C454 -C453 -C452 -C451 -C450 -C449 -C448 -C447 -C446 -C445 -C444 C443 -C442 -C441 -C440 -C439 -C438 -C437 -C436 -C435 -C434 -C433 -C432 -C431 C430 -C429 -C428 -C427 -C426 -C425 -C424 -C423 -C422 -C421 -C420 -C419 -C418 -C417 -C416 C415 -C414 -C413 -C412 -C411 -C410 -C409 -C408 -C407 -C406 -C405 -C404 -C403 -C402 -C401 -C400 C399 -C398 -C397 -C396 -C395 -C394 -C393 -C392 -C391 -C390 -C389 -C388 -C387 -C386 -C385 -C384 -C383 -C382 -C381 -C380 -C379 C378 -C377 -C376 -C375 -C374 -C373 -C372 -C371 -C370 -C369 -C368 -C367 -C366 -C365 -C364 -C363 -C362 -C361 -C360 -C359 -C358 -C357 -C356 -C355 -C354 -C353 -C352 -C351 -C350 -C349 -C348 C347 -C346 -C345 -C344 -C343 -C342 -C341 -C340 -C339 -C338 -C337 -C336 -C335 -C334 -C333 -C332 -C331 -C330 -C329 -C328 C327 -C326 -C325 -C324 -C323 -C322 -C321 -C320 -C319 -C318 C317 -C316 -C315 -C314 -C313 -C312 -C311 -C310 -C309 -C308 -C307 -C306 -C305 -C304 -C303 C302 -C301 -C300 -C299 -C298 -C297 -C296 -C295 -C294 -C293 -C292 -C291 -C290 -C289 -C288 -C287 -C286 -C285 -C284 -C283 -C282 -C281 -C280 -C279 -C278 -C277 -C276 -C275 -C274 -C273 -C272 C271 -C270 -C269 -C268 -C267 -C266 C265 -C264 -C263 -C262 -C261 -C260 -C259 -C258 -C257 -C256 -C255 -C254 -C253 -C252 -C251 -C250 -C249 -C248 -C247 -C246 -C245 -C244 -C243 -C242 -C241 -C240 -C239 -C238 C237 -C236 -C235 -C234 -C233 -C232 -C231 -C230 -C229 -C228 -C227 -C226 -C225 C224 -C223 -C222 -C221 -C220 -C219 -C218 -C217 -C216 -C215 -C214 -C213 -C212 -C211 -C210 -C209 -C208 -C207 -C206 -C205 -C204 -C203 -C202 -C201 -C200 -C199 -C198 -C197 -C196 -C195 -C194 C193 -C192 -C191 -C190 -C189 -C188 -C187 -C186 -C185 -C184 -C183 C182 -C181 -C180 -C179 -C178 -C177 -C176 -C175 -C174 -C173 -C172 -C171 -C170 -C169 C168 -C167 -C166 -C165 -C164 -C163 -C162 -C161 -C160 -C159 -C158 -C157 -C156 -C155 -C154 -C153 -C152 -C151 -C150 -C149 -C148 -C147 -C146 -C145 -C144 -C143 -C142 C141 -C140 -C139 -C138 -C137 -C136 -C135 -C134 -C133 -C132 -C131 -C130 -C129 -C128 -C127 C126 -C125 -C124 -C123 -C122 -C121 -C120 -C119 -C118 -C117 -C116 -C115 -C114 -C113 -C112 -C111 -C110 -C109 -C108 -C107 -C106 -C105 -C104 -C103 -C102 -C101 -C100 -C99 -C98 -C97 -C96 -C95 -C94 -C93 -C92 -C91 -C90 -C89 -C88 -C87 -C86 -C85 -C84 C83 -C82 -C81 -C80 -C79 -C78 -C77 -C76 -C75

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/30869/stat): 30869 (minisat+_script) R 30868 30869 20602 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1720787154 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/30869/statm): 174 3 169 147 0 27 0
[pid=30869] 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=30870
New process pid=30871
New process pid=30872
execve syscall for /bin/sed executable
One traced child (pid=30871) 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=30872) exited with status: 0
One traced child (pid=30870) exited with status: 0
New process pid=30873
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc21/normalized-frb40-19-5.opb

[startup+10.0028 s]
Raw data (loadavg): 0.93 0.96 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 2780 0 0 0 977 10 0 0 25 0 1 0 1720787159 12185600 2767 4294967295 134512640 135094434 3221224448 3221223072 134557636 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 2975 2767 145 145 0 2830 0
[pid=30873] vsize: 11900
Current children cumulated CPU time (s) 9.87
Current children cumulated vsize (Kb) 14024

[startup+20.0035 s]
Raw data (loadavg): 0.94 0.96 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 2887 0 0 0 1977 10 0 0 25 0 1 0 1720787159 12759040 2874 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 3115 2874 145 145 0 2970 0
[pid=30873] vsize: 12460
Current children cumulated CPU time (s) 19.87
Current children cumulated vsize (Kb) 14584

[startup+30.0042 s]
Raw data (loadavg): 0.95 0.96 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 2910 0 0 0 2976 11 0 0 25 0 1 0 1720787159 12853248 2897 4294967295 134512640 135094434 3221224448 3221223060 134563055 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 3138 2897 145 145 0 2993 0
[pid=30873] vsize: 12552
Current children cumulated CPU time (s) 29.87
Current children cumulated vsize (Kb) 14676

[startup+40.0039 s]
Raw data (loadavg): 0.96 0.96 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 3117 0 0 0 3973 12 0 0 25 0 1 0 1720787159 13819904 3104 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 3374 3104 145 145 0 3229 0
[pid=30873] vsize: 13496
Current children cumulated CPU time (s) 39.85
Current children cumulated vsize (Kb) 15620

[startup+50.0046 s]
Raw data (loadavg): 0.96 0.96 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 3671 0 0 0 4963 16 0 0 25 0 1 0 1720787159 16125952 3658 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 3937 3658 145 145 0 3792 0
[pid=30873] vsize: 15748
Current children cumulated CPU time (s) 49.79
Current children cumulated vsize (Kb) 17872

[startup+60.0053 s]
Raw data (loadavg): 0.97 0.96 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 4384 0 0 0 5952 21 0 0 25 0 1 0 1720787159 19021824 4371 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 4644 4371 145 145 0 4499 0
[pid=30873] vsize: 18576
Current children cumulated CPU time (s) 59.73
Current children cumulated vsize (Kb) 20700

[startup+70.0059 s]
Raw data (loadavg): 0.97 0.96 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 4920 0 0 0 6943 25 0 0 25 0 1 0 1720787159 21200896 4907 4294967295 134512640 135094434 3221224448 3221223072 134557685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 5176 4907 145 145 0 5031 0
[pid=30873] vsize: 20704
Current children cumulated CPU time (s) 69.68
Current children cumulated vsize (Kb) 22828

[startup+80.0066 s]
Raw data (loadavg): 0.98 0.96 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 5431 0 0 0 7934 29 0 0 25 0 1 0 1720787159 23404544 5418 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 5714 5418 145 145 0 5569 0
[pid=30873] vsize: 22856
Current children cumulated CPU time (s) 79.63
Current children cumulated vsize (Kb) 24980

[startup+90.0063 s]
Raw data (loadavg): 0.98 0.96 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 5937 0 0 0 8925 32 0 0 25 0 1 0 1720787159 25456640 5924 4294967295 134512640 135094434 3221224448 3221223104 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 6215 5924 145 145 0 6070 0
[pid=30873] vsize: 24860
Current children cumulated CPU time (s) 89.57
Current children cumulated vsize (Kb) 26984

[startup+100.007 s]
Raw data (loadavg): 0.98 0.96 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 6375 0 0 0 9917 36 0 0 25 0 1 0 1720787159 27238400 6362 4294967295 134512640 135094434 3221224448 3221223072 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30873/statm): 6650 6362 145 145 0 6505 0
[pid=30873] vsize: 26600
Current children cumulated CPU time (s) 99.53
Current children cumulated vsize (Kb) 28724

[startup+110.008 s]
Raw data (loadavg): 0.98 0.97 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 6860 0 0 0 10906 40 0 0 25 0 1 0 1720787159 29204480 6847 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 7130 6847 145 145 0 6985 0
[pid=30873] vsize: 28520
Current children cumulated CPU time (s) 109.46
Current children cumulated vsize (Kb) 30644

[startup+120.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 7255 0 0 0 11899 43 0 0 25 0 1 0 1720787159 30806016 7242 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 7521 7242 145 145 0 7376 0
[pid=30873] vsize: 30084
Current children cumulated CPU time (s) 119.42
Current children cumulated vsize (Kb) 32208

[startup+130.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 7639 0 0 0 12891 46 0 0 25 0 1 0 1720787159 32366592 7626 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 7902 7626 145 145 0 7757 0
[pid=30873] vsize: 31608
Current children cumulated CPU time (s) 129.37
Current children cumulated vsize (Kb) 33732

[startup+140.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 7907 0 0 0 13884 49 0 0 25 0 1 0 1720787159 33452032 7894 4294967295 134512640 135094434 3221224448 3221223104 134558210 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 8167 7894 145 145 0 8022 0
[pid=30873] vsize: 32668
Current children cumulated CPU time (s) 139.33
Current children cumulated vsize (Kb) 34792

[startup+150.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 8264 0 0 0 14879 51 0 0 25 0 1 0 1720787159 34902016 8251 4294967295 134512640 135094434 3221224448 3221223040 134557219 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 8521 8251 145 145 0 8376 0
[pid=30873] vsize: 34084
Current children cumulated CPU time (s) 149.3
Current children cumulated vsize (Kb) 36208

[startup+160.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 8264 0 0 0 15879 51 0 0 25 0 1 0 1720787159 34902016 8251 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 8521 8251 145 145 0 8376 0
[pid=30873] vsize: 34084
Current children cumulated CPU time (s) 159.3
Current children cumulated vsize (Kb) 36208

[startup+170.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 8264 0 0 0 16879 51 0 0 25 0 1 0 1720787159 34902016 8251 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 8521 8251 145 145 0 8376 0
[pid=30873] vsize: 34084
Current children cumulated CPU time (s) 169.3
Current children cumulated vsize (Kb) 36208

[startup+180.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 8264 0 0 0 17879 51 0 0 25 0 1 0 1720787159 34902016 8251 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 8521 8251 145 145 0 8376 0
[pid=30873] vsize: 34084
Current children cumulated CPU time (s) 179.3
Current children cumulated vsize (Kb) 36208

[startup+190.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 8264 0 0 0 18879 51 0 0 25 0 1 0 1720787159 34902016 8251 4294967295 134512640 135094434 3221224448 3221223104 134557866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 8521 8251 145 145 0 8376 0
[pid=30873] vsize: 34084
Current children cumulated CPU time (s) 189.3
Current children cumulated vsize (Kb) 36208

[startup+200.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 8264 0 0 0 19880 51 0 0 25 0 1 0 1720787159 34902016 8251 4294967295 134512640 135094434 3221224448 3221223060 134563055 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 8521 8251 145 145 0 8376 0
[pid=30873] vsize: 34084
Current children cumulated CPU time (s) 199.31
Current children cumulated vsize (Kb) 36208

[startup+210.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 8264 0 0 0 20880 51 0 0 25 0 1 0 1720787159 34902016 8251 4294967295 134512640 135094434 3221224448 3221223136 134785033 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 8521 8251 145 145 0 8376 0
[pid=30873] vsize: 34084
Current children cumulated CPU time (s) 209.31
Current children cumulated vsize (Kb) 36208

[startup+220.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 8264 0 0 0 21880 51 0 0 25 0 1 0 1720787159 34902016 8251 4294967295 134512640 135094434 3221224448 3221223104 134558221 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 8521 8251 145 145 0 8376 0
[pid=30873] vsize: 34084
Current children cumulated CPU time (s) 219.31
Current children cumulated vsize (Kb) 36208

[startup+230.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 8423 0 0 0 22877 53 0 0 25 0 1 0 1720787159 35553280 8410 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 8680 8410 145 145 0 8535 0
[pid=30873] vsize: 34720
Current children cumulated CPU time (s) 229.3
Current children cumulated vsize (Kb) 36844

[startup+240.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 8879 0 0 0 23869 57 0 0 25 0 1 0 1720787159 37421056 8866 4294967295 134512640 135094434 3221224448 3221223040 134556826 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 9136 8866 145 145 0 8991 0
[pid=30873] vsize: 36544
Current children cumulated CPU time (s) 239.26
Current children cumulated vsize (Kb) 38668

[startup+250.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 9375 0 0 0 24859 61 0 0 25 0 1 0 1720787159 39452672 9362 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 9632 9362 145 145 0 9487 0
[pid=30873] vsize: 38528
Current children cumulated CPU time (s) 249.2
Current children cumulated vsize (Kb) 40652

[startup+260.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 9574 0 0 0 25857 62 0 0 25 0 1 0 1720787159 40267776 9561 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 9831 9561 145 145 0 9686 0
[pid=30873] vsize: 39324
Current children cumulated CPU time (s) 259.19
Current children cumulated vsize (Kb) 41448

[startup+270.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 9574 0 0 0 26857 62 0 0 25 0 1 0 1720787159 40267776 9561 4294967295 134512640 135094434 3221224448 3221223104 134558246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 9831 9561 145 145 0 9686 0
[pid=30873] vsize: 39324
Current children cumulated CPU time (s) 269.19
Current children cumulated vsize (Kb) 41448

[startup+280.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 9574 0 0 0 27857 62 0 0 25 0 1 0 1720787159 40267776 9561 4294967295 134512640 135094434 3221224448 3221223120 134556317 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 9831 9561 145 145 0 9686 0
[pid=30873] vsize: 39324
Current children cumulated CPU time (s) 279.19
Current children cumulated vsize (Kb) 41448

[startup+290.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 9574 0 0 0 28857 62 0 0 25 0 1 0 1720787159 40267776 9561 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 9831 9561 145 145 0 9686 0
[pid=30873] vsize: 39324
Current children cumulated CPU time (s) 289.19
Current children cumulated vsize (Kb) 41448

[startup+300.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 9574 0 0 0 29857 62 0 0 25 0 1 0 1720787159 40267776 9561 4294967295 134512640 135094434 3221224448 3221223104 134558169 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 9831 9561 145 145 0 9686 0
[pid=30873] vsize: 39324
Current children cumulated CPU time (s) 299.19
Current children cumulated vsize (Kb) 41448

[startup+310.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 9574 0 0 0 30858 62 0 0 25 0 1 0 1720787159 40267776 9561 4294967295 134512640 135094434 3221224448 3221223104 134558126 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 9831 9561 145 145 0 9686 0
[pid=30873] vsize: 39324
Current children cumulated CPU time (s) 309.2
Current children cumulated vsize (Kb) 41448

[startup+320.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 9574 0 0 0 31858 62 0 0 25 0 1 0 1720787159 40267776 9561 4294967295 134512640 135094434 3221224448 3221223072 134562139 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 9831 9561 145 145 0 9686 0
[pid=30873] vsize: 39324
Current children cumulated CPU time (s) 319.2
Current children cumulated vsize (Kb) 41448

[startup+330.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 9574 0 0 0 32858 63 0 0 25 0 1 0 1720787159 40267776 9561 4294967295 134512640 135094434 3221224448 3221223120 134555568 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 9831 9561 145 145 0 9686 0
[pid=30873] vsize: 39324
Current children cumulated CPU time (s) 329.21
Current children cumulated vsize (Kb) 41448

[startup+340.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 9574 0 0 0 33858 63 0 0 25 0 1 0 1720787159 40267776 9561 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 9831 9561 145 145 0 9686 0
[pid=30873] vsize: 39324
Current children cumulated CPU time (s) 339.21
Current children cumulated vsize (Kb) 41448

[startup+350.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 9574 0 0 0 34859 63 0 0 25 0 1 0 1720787159 40267776 9561 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 9831 9561 145 145 0 9686 0
[pid=30873] vsize: 39324
Current children cumulated CPU time (s) 349.22
Current children cumulated vsize (Kb) 41448

[startup+360.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 9574 0 0 0 35859 63 0 0 25 0 1 0 1720787159 40267776 9561 4294967295 134512640 135094434 3221224448 3221223104 134557934 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 9831 9561 145 145 0 9686 0
[pid=30873] vsize: 39324
Current children cumulated CPU time (s) 359.22
Current children cumulated vsize (Kb) 41448

[startup+370.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 9574 0 0 0 36859 63 0 0 25 0 1 0 1720787159 40267776 9561 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 9831 9561 145 145 0 9686 0
[pid=30873] vsize: 39324
Current children cumulated CPU time (s) 369.22
Current children cumulated vsize (Kb) 41448

[startup+380.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 9574 0 0 0 37859 63 0 0 25 0 1 0 1720787159 40267776 9561 4294967295 134512640 135094434 3221224448 3221223120 134556515 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 9831 9561 145 145 0 9686 0
[pid=30873] vsize: 39324
Current children cumulated CPU time (s) 379.22
Current children cumulated vsize (Kb) 41448

[startup+390.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 9574 0 0 0 38859 63 0 0 25 0 1 0 1720787159 40267776 9561 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 9831 9561 145 145 0 9686 0
[pid=30873] vsize: 39324
Current children cumulated CPU time (s) 389.22
Current children cumulated vsize (Kb) 41448

[startup+400.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 9577 0 0 0 39860 63 0 0 25 0 1 0 1720787159 40267776 9564 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 9831 9564 145 145 0 9686 0
[pid=30873] vsize: 39324
Current children cumulated CPU time (s) 399.23
Current children cumulated vsize (Kb) 41448

[startup+410.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 9580 0 0 0 40860 63 0 0 25 0 1 0 1720787159 40529920 9567 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 9895 9567 145 145 0 9750 0
[pid=30873] vsize: 39580
Current children cumulated CPU time (s) 409.23
Current children cumulated vsize (Kb) 41704

[startup+420.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 9583 0 0 0 41860 63 0 0 25 0 1 0 1720787159 40529920 9570 4294967295 134512640 135094434 3221224448 3221223104 134557937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 9895 9570 145 145 0 9750 0
[pid=30873] vsize: 39580
Current children cumulated CPU time (s) 419.23
Current children cumulated vsize (Kb) 41704

[startup+430.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 9753 0 0 0 42857 64 0 0 25 0 1 0 1720787159 41213952 9740 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 10062 9740 145 145 0 9917 0
[pid=30873] vsize: 40248
Current children cumulated CPU time (s) 429.21
Current children cumulated vsize (Kb) 42372

[startup+440.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 10035 0 0 0 43852 65 0 0 25 0 1 0 1720787159 42356736 10022 4294967295 134512640 135094434 3221224448 3221223104 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 10341 10022 145 145 0 10196 0
[pid=30873] vsize: 41364
Current children cumulated CPU time (s) 439.17
Current children cumulated vsize (Kb) 43488

[startup+450.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 10265 0 0 0 44848 68 0 0 25 0 1 0 1720787159 43298816 10252 4294967295 134512640 135094434 3221224448 3221223104 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 10571 10252 145 145 0 10426 0
[pid=30873] vsize: 42284
Current children cumulated CPU time (s) 449.16
Current children cumulated vsize (Kb) 44408

[startup+460.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 10316 0 0 0 45847 68 0 0 25 0 1 0 1720787159 43511808 10303 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 10623 10303 145 145 0 10478 0
[pid=30873] vsize: 42492
Current children cumulated CPU time (s) 459.15
Current children cumulated vsize (Kb) 44616

[startup+470.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 10316 0 0 0 46847 68 0 0 25 0 1 0 1720787159 43511808 10303 4294967295 134512640 135094434 3221224448 3221223040 134557219 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 10623 10303 145 145 0 10478 0
[pid=30873] vsize: 42492
Current children cumulated CPU time (s) 469.15
Current children cumulated vsize (Kb) 44616

[startup+480.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 10316 0 0 0 47847 68 0 0 25 0 1 0 1720787159 43511808 10303 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 10623 10303 145 145 0 10478 0
[pid=30873] vsize: 42492
Current children cumulated CPU time (s) 479.15
Current children cumulated vsize (Kb) 44616

[startup+490.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 10316 0 0 0 48848 68 0 0 25 0 1 0 1720787159 43511808 10303 4294967295 134512640 135094434 3221224448 3221223040 134556904 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 10623 10303 145 145 0 10478 0
[pid=30873] vsize: 42492
Current children cumulated CPU time (s) 489.16
Current children cumulated vsize (Kb) 44616

[startup+500.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 10316 0 0 0 49848 68 0 0 25 0 1 0 1720787159 43511808 10303 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 10623 10303 145 145 0 10478 0
[pid=30873] vsize: 42492
Current children cumulated CPU time (s) 499.16
Current children cumulated vsize (Kb) 44616

[startup+510.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 10316 0 0 0 50848 68 0 0 25 0 1 0 1720787159 43511808 10303 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 10623 10303 145 145 0 10478 0
[pid=30873] vsize: 42492
Current children cumulated CPU time (s) 509.16
Current children cumulated vsize (Kb) 44616

[startup+520.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 10316 0 0 0 51848 68 0 0 25 0 1 0 1720787159 43511808 10303 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 10623 10303 145 145 0 10478 0
[pid=30873] vsize: 42492
Current children cumulated CPU time (s) 519.16
Current children cumulated vsize (Kb) 44616

[startup+530.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 10316 0 0 0 52848 68 0 0 25 0 1 0 1720787159 43511808 10303 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 10623 10303 145 145 0 10478 0
[pid=30873] vsize: 42492
Current children cumulated CPU time (s) 529.16
Current children cumulated vsize (Kb) 44616

[startup+540.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 10316 0 0 0 53849 68 0 0 25 0 1 0 1720787159 43511808 10303 4294967295 134512640 135094434 3221224448 3221223040 134556837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 10623 10303 145 145 0 10478 0
[pid=30873] vsize: 42492
Current children cumulated CPU time (s) 539.17
Current children cumulated vsize (Kb) 44616

[startup+550.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 10316 0 0 0 54849 68 0 0 25 0 1 0 1720787159 43511808 10303 4294967295 134512640 135094434 3221224448 3221223104 134558019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 10623 10303 145 145 0 10478 0
[pid=30873] vsize: 42492
Current children cumulated CPU time (s) 549.17
Current children cumulated vsize (Kb) 44616

[startup+560.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 10321 0 0 0 55849 68 0 0 25 0 1 0 1720787159 43544576 10308 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 10631 10308 145 145 0 10486 0
[pid=30873] vsize: 42524
Current children cumulated CPU time (s) 559.17
Current children cumulated vsize (Kb) 44648

[startup+570.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 10321 0 0 0 56849 68 0 0 25 0 1 0 1720787159 43544576 10308 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 10631 10308 145 145 0 10486 0
[pid=30873] vsize: 42524
Current children cumulated CPU time (s) 569.17
Current children cumulated vsize (Kb) 44648

[startup+580.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 10321 0 0 0 57850 68 0 0 25 0 1 0 1720787159 43544576 10308 4294967295 134512640 135094434 3221224448 3221223040 134557230 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 10631 10308 145 145 0 10486 0
[pid=30873] vsize: 42524
Current children cumulated CPU time (s) 579.18
Current children cumulated vsize (Kb) 44648

[startup+590.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 10321 0 0 0 58850 68 0 0 25 0 1 0 1720787159 43544576 10308 4294967295 134512640 135094434 3221224448 3221223104 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 10631 10308 145 145 0 10486 0
[pid=30873] vsize: 42524
Current children cumulated CPU time (s) 589.18
Current children cumulated vsize (Kb) 44648

[startup+600.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 10321 0 0 0 59850 68 0 0 25 0 1 0 1720787159 43544576 10308 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 10631 10308 145 145 0 10486 0
[pid=30873] vsize: 42524
Current children cumulated CPU time (s) 599.18
Current children cumulated vsize (Kb) 44648

[startup+610.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 10321 0 0 0 60850 68 0 0 25 0 1 0 1720787159 43544576 10308 4294967295 134512640 135094434 3221224448 3221223104 134558019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 10631 10308 145 145 0 10486 0
[pid=30873] vsize: 42524
Current children cumulated CPU time (s) 609.18
Current children cumulated vsize (Kb) 44648

[startup+620.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 10322 0 0 0 61850 68 0 0 25 0 1 0 1720787159 43544576 10309 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 10631 10309 145 145 0 10486 0
[pid=30873] vsize: 42524
Current children cumulated CPU time (s) 619.18
Current children cumulated vsize (Kb) 44648

[startup+630.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 10331 0 0 0 62851 68 0 0 25 0 1 0 1720787159 43577344 10318 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 10639 10318 145 145 0 10494 0
[pid=30873] vsize: 42556
Current children cumulated CPU time (s) 629.19
Current children cumulated vsize (Kb) 44680

[startup+640.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 10334 0 0 0 63851 68 0 0 25 0 1 0 1720787159 43577344 10321 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 10639 10321 145 145 0 10494 0
[pid=30873] vsize: 42556
Current children cumulated CPU time (s) 639.19
Current children cumulated vsize (Kb) 44680

[startup+650.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 10336 0 0 0 64851 68 0 0 25 0 1 0 1720787159 43577344 10323 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 10639 10323 145 145 0 10494 0
[pid=30873] vsize: 42556
Current children cumulated CPU time (s) 649.19
Current children cumulated vsize (Kb) 44680

[startup+660.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 10336 0 0 0 65851 68 0 0 25 0 1 0 1720787159 43577344 10323 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30873/statm): 10639 10323 145 145 0 10494 0
[pid=30873] vsize: 42556
Current children cumulated CPU time (s) 659.19
Current children cumulated vsize (Kb) 44680

[startup+670.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 10336 0 0 0 66850 68 0 0 25 0 1 0 1720787159 43577344 10323 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 10639 10323 145 145 0 10494 0
[pid=30873] vsize: 42556
Current children cumulated CPU time (s) 669.18
Current children cumulated vsize (Kb) 44680

[startup+680.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 10336 0 0 0 67850 68 0 0 25 0 1 0 1720787159 43577344 10323 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 10639 10323 145 145 0 10494 0
[pid=30873] vsize: 42556
Current children cumulated CPU time (s) 679.18
Current children cumulated vsize (Kb) 44680

[startup+690.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 10336 0 0 0 68851 68 0 0 25 0 1 0 1720787159 43577344 10323 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 10639 10323 145 145 0 10494 0
[pid=30873] vsize: 42556
Current children cumulated CPU time (s) 689.19
Current children cumulated vsize (Kb) 44680

[startup+700.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 10336 0 0 0 69851 68 0 0 25 0 1 0 1720787159 43577344 10323 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 10639 10323 145 145 0 10494 0
[pid=30873] vsize: 42556
Current children cumulated CPU time (s) 699.19
Current children cumulated vsize (Kb) 44680

[startup+710.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 10336 0 0 0 70851 68 0 0 25 0 1 0 1720787159 43577344 10323 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 10639 10323 145 145 0 10494 0
[pid=30873] vsize: 42556
Current children cumulated CPU time (s) 709.19
Current children cumulated vsize (Kb) 44680

[startup+720.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 10336 0 0 0 71851 68 0 0 25 0 1 0 1720787159 43577344 10323 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 10639 10323 145 145 0 10494 0
[pid=30873] vsize: 42556
Current children cumulated CPU time (s) 719.19
Current children cumulated vsize (Kb) 44680

[startup+730.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 10336 0 0 0 72851 68 0 0 25 0 1 0 1720787159 43577344 10323 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 10639 10323 145 145 0 10494 0
[pid=30873] vsize: 42556
Current children cumulated CPU time (s) 729.19
Current children cumulated vsize (Kb) 44680

[startup+740.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 10336 0 0 0 73852 68 0 0 25 0 1 0 1720787159 43577344 10323 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 10639 10323 145 145 0 10494 0
[pid=30873] vsize: 42556
Current children cumulated CPU time (s) 739.2
Current children cumulated vsize (Kb) 44680

[startup+750.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 10336 0 0 0 74852 68 0 0 25 0 1 0 1720787159 43577344 10323 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 10639 10323 145 145 0 10494 0
[pid=30873] vsize: 42556
Current children cumulated CPU time (s) 749.2
Current children cumulated vsize (Kb) 44680

[startup+760.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 10336 0 0 0 75852 68 0 0 25 0 1 0 1720787159 43577344 10323 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 10639 10323 145 145 0 10494 0
[pid=30873] vsize: 42556
Current children cumulated CPU time (s) 759.2
Current children cumulated vsize (Kb) 44680

[startup+770.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 10336 0 0 0 76852 68 0 0 25 0 1 0 1720787159 43577344 10323 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 10639 10323 145 145 0 10494 0
[pid=30873] vsize: 42556
Current children cumulated CPU time (s) 769.2
Current children cumulated vsize (Kb) 44680

[startup+780.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 10336 0 0 0 77853 68 0 0 25 0 1 0 1720787159 43577344 10323 4294967295 134512640 135094434 3221224448 3221223104 134557884 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 10639 10323 145 145 0 10494 0
[pid=30873] vsize: 42556
Current children cumulated CPU time (s) 779.21
Current children cumulated vsize (Kb) 44680

[startup+790.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 10336 0 0 0 78853 68 0 0 25 0 1 0 1720787159 43577344 10323 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 10639 10323 145 145 0 10494 0
[pid=30873] vsize: 42556
Current children cumulated CPU time (s) 789.21
Current children cumulated vsize (Kb) 44680

[startup+800.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 10336 0 0 0 79853 68 0 0 25 0 1 0 1720787159 43577344 10323 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 10639 10323 145 145 0 10494 0
[pid=30873] vsize: 42556
Current children cumulated CPU time (s) 799.21
Current children cumulated vsize (Kb) 44680

[startup+810.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 10336 0 0 0 80853 68 0 0 25 0 1 0 1720787159 43577344 10323 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 10639 10323 145 145 0 10494 0
[pid=30873] vsize: 42556
Current children cumulated CPU time (s) 809.21
Current children cumulated vsize (Kb) 44680

[startup+820.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 10336 0 0 0 81853 68 0 0 25 0 1 0 1720787159 43577344 10323 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 10639 10323 145 145 0 10494 0
[pid=30873] vsize: 42556
Current children cumulated CPU time (s) 819.21
Current children cumulated vsize (Kb) 44680

[startup+830.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 10336 0 0 0 82854 68 0 0 25 0 1 0 1720787159 43577344 10323 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 10639 10323 145 145 0 10494 0
[pid=30873] vsize: 42556
Current children cumulated CPU time (s) 829.22
Current children cumulated vsize (Kb) 44680

[startup+840.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 10357 0 0 0 83853 69 0 0 25 0 1 0 1720787159 43708416 10344 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30873/statm): 10671 10344 145 145 0 10526 0
[pid=30873] vsize: 42684
Current children cumulated CPU time (s) 839.22
Current children cumulated vsize (Kb) 44808

[startup+850.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 10360 0 0 0 84853 69 0 0 25 0 1 0 1720787159 43708416 10347 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 10671 10347 145 145 0 10526 0
[pid=30873] vsize: 42684
Current children cumulated CPU time (s) 849.22
Current children cumulated vsize (Kb) 44808

[startup+860.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 10364 0 0 0 85853 69 0 0 25 0 1 0 1720787159 43708416 10351 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 10671 10351 145 145 0 10526 0
[pid=30873] vsize: 42684
Current children cumulated CPU time (s) 859.22
Current children cumulated vsize (Kb) 44808

[startup+870.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 10367 0 0 0 86853 69 0 0 25 0 1 0 1720787159 43708416 10354 4294967295 134512640 135094434 3221224448 3221223040 134556859 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 10671 10354 145 145 0 10526 0
[pid=30873] vsize: 42684
Current children cumulated CPU time (s) 869.22
Current children cumulated vsize (Kb) 44808

[startup+880.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 10369 0 0 0 87853 69 0 0 25 0 1 0 1720787159 43708416 10356 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 10671 10356 145 145 0 10526 0
[pid=30873] vsize: 42684
Current children cumulated CPU time (s) 879.22
Current children cumulated vsize (Kb) 44808

[startup+890.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 10370 0 0 0 88854 69 0 0 25 0 1 0 1720787159 43708416 10357 4294967295 134512640 135094434 3221224448 3221223104 134557840 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 10671 10357 145 145 0 10526 0
[pid=30873] vsize: 42684
Current children cumulated CPU time (s) 889.23
Current children cumulated vsize (Kb) 44808

[startup+900.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 10370 0 0 0 89854 69 0 0 25 0 1 0 1720787159 43708416 10357 4294967295 134512640 135094434 3221224448 3221223072 134557585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 10671 10357 145 145 0 10526 0
[pid=30873] vsize: 42684
Current children cumulated CPU time (s) 899.23
Current children cumulated vsize (Kb) 44808

[startup+910.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 10370 0 0 0 90854 69 0 0 25 0 1 0 1720787159 43708416 10357 4294967295 134512640 135094434 3221224448 3221223060 134563049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 10671 10357 145 145 0 10526 0
[pid=30873] vsize: 42684
Current children cumulated CPU time (s) 909.23
Current children cumulated vsize (Kb) 44808

[startup+920.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 10370 0 0 0 91854 69 0 0 25 0 1 0 1720787159 43708416 10357 4294967295 134512640 135094434 3221224448 3221223120 134556266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 10671 10357 145 145 0 10526 0
[pid=30873] vsize: 42684
Current children cumulated CPU time (s) 919.23
Current children cumulated vsize (Kb) 44808

[startup+930.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 10370 0 0 0 92855 69 0 0 25 0 1 0 1720787159 43708416 10357 4294967295 134512640 135094434 3221224448 3221223104 134557903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 10671 10357 145 145 0 10526 0
[pid=30873] vsize: 42684
Current children cumulated CPU time (s) 929.24
Current children cumulated vsize (Kb) 44808

[startup+940.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30873
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 10370 0 0 0 93855 69 0 0 25 0 1 0 1720787159 43708416 10357 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 10671 10357 145 145 0 10526 0
[pid=30873] vsize: 42684
Current children cumulated CPU time (s) 939.24
Current children cumulated vsize (Kb) 44808

[startup+950.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30875
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 10370 0 0 0 94855 69 0 0 25 0 1 0 1720787159 43708416 10357 4294967295 134512640 135094434 3221224448 3221223120 134556073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 10671 10357 145 145 0 10526 0
[pid=30873] vsize: 42684
Current children cumulated CPU time (s) 949.24
Current children cumulated vsize (Kb) 44808

[startup+960.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30875
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 10370 0 0 0 95855 69 0 0 25 0 1 0 1720787159 43708416 10357 4294967295 134512640 135094434 3221224448 3221223040 134557040 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 10671 10357 145 145 0 10526 0
[pid=30873] vsize: 42684
Current children cumulated CPU time (s) 959.24
Current children cumulated vsize (Kb) 44808

[startup+970.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30875
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 10370 0 0 0 96855 69 0 0 25 0 1 0 1720787159 43708416 10357 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 10671 10357 145 145 0 10526 0
[pid=30873] vsize: 42684
Current children cumulated CPU time (s) 969.24
Current children cumulated vsize (Kb) 44808

[startup+980.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30875
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 10370 0 0 0 97855 69 0 0 25 0 1 0 1720787159 43708416 10357 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 10671 10357 145 145 0 10526 0
[pid=30873] vsize: 42684
Current children cumulated CPU time (s) 979.24
Current children cumulated vsize (Kb) 44808

[startup+990.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30875
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 10370 0 0 0 98855 69 0 0 25 0 1 0 1720787159 43708416 10357 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 10671 10357 145 145 0 10526 0
[pid=30873] vsize: 42684
Current children cumulated CPU time (s) 989.24
Current children cumulated vsize (Kb) 44808

[startup+1000.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30875
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 10370 0 0 0 99856 69 0 0 25 0 1 0 1720787159 43708416 10357 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 10671 10357 145 145 0 10526 0
[pid=30873] vsize: 42684
Current children cumulated CPU time (s) 999.25
Current children cumulated vsize (Kb) 44808

[startup+1010.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30875
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 10370 0 0 0 100856 69 0 0 25 0 1 0 1720787159 43708416 10357 4294967295 134512640 135094434 3221224448 3221223104 134558126 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 10671 10357 145 145 0 10526 0
[pid=30873] vsize: 42684
Current children cumulated CPU time (s) 1009.25
Current children cumulated vsize (Kb) 44808

[startup+1020.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30875
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 10370 0 0 0 101856 69 0 0 25 0 1 0 1720787159 43708416 10357 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 10671 10357 145 145 0 10526 0
[pid=30873] vsize: 42684
Current children cumulated CPU time (s) 1019.25
Current children cumulated vsize (Kb) 44808

[startup+1030.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30875
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 10370 0 0 0 102856 69 0 0 25 0 1 0 1720787159 43708416 10357 4294967295 134512640 135094434 3221224448 3221223104 134557928 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 10671 10357 145 145 0 10526 0
[pid=30873] vsize: 42684
Current children cumulated CPU time (s) 1029.25
Current children cumulated vsize (Kb) 44808

[startup+1040.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30875
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 10370 0 0 0 103856 69 0 0 25 0 1 0 1720787159 43708416 10357 4294967295 134512640 135094434 3221224448 3221223136 134554687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 10671 10357 145 145 0 10526 0
[pid=30873] vsize: 42684
Current children cumulated CPU time (s) 1039.25
Current children cumulated vsize (Kb) 44808

[startup+1050.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30875
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 10370 0 0 0 104857 69 0 0 25 0 1 0 1720787159 43708416 10357 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 10671 10357 145 145 0 10526 0
[pid=30873] vsize: 42684
Current children cumulated CPU time (s) 1049.26
Current children cumulated vsize (Kb) 44808

[startup+1060.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30875
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 10370 0 0 0 105857 69 0 0 25 0 1 0 1720787159 43708416 10357 4294967295 134512640 135094434 3221224448 3221223072 134557696 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 10671 10357 145 145 0 10526 0
[pid=30873] vsize: 42684
Current children cumulated CPU time (s) 1059.26
Current children cumulated vsize (Kb) 44808

[startup+1070.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30875
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 10370 0 0 0 106857 69 0 0 25 0 1 0 1720787159 43708416 10357 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 10671 10357 145 145 0 10526 0
[pid=30873] vsize: 42684
Current children cumulated CPU time (s) 1069.26
Current children cumulated vsize (Kb) 44808

[startup+1080.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30875
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 10370 0 0 0 107857 69 0 0 25 0 1 0 1720787159 43708416 10357 4294967295 134512640 135094434 3221224448 3221223072 134557696 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 10671 10357 145 145 0 10526 0
[pid=30873] vsize: 42684
Current children cumulated CPU time (s) 1079.26
Current children cumulated vsize (Kb) 44808

[startup+1090.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30875
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 10370 0 0 0 108857 69 0 0 25 0 1 0 1720787159 43708416 10357 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 10671 10357 145 145 0 10526 0
[pid=30873] vsize: 42684
Current children cumulated CPU time (s) 1089.26
Current children cumulated vsize (Kb) 44808

[startup+1100.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30875
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 10370 0 0 0 109858 69 0 0 25 0 1 0 1720787159 43708416 10357 4294967295 134512640 135094434 3221224448 3221223072 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 10671 10357 145 145 0 10526 0
[pid=30873] vsize: 42684
Current children cumulated CPU time (s) 1099.27
Current children cumulated vsize (Kb) 44808

[startup+1110.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30875
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 10370 0 0 0 110858 69 0 0 25 0 1 0 1720787159 43708416 10357 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 10671 10357 145 145 0 10526 0
[pid=30873] vsize: 42684
Current children cumulated CPU time (s) 1109.27
Current children cumulated vsize (Kb) 44808

[startup+1120.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30875
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 10370 0 0 0 111858 69 0 0 25 0 1 0 1720787159 43708416 10357 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 10671 10357 145 145 0 10526 0
[pid=30873] vsize: 42684
Current children cumulated CPU time (s) 1119.27
Current children cumulated vsize (Kb) 44808

[startup+1130.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30875
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 10370 0 0 0 112858 69 0 0 25 0 1 0 1720787159 43708416 10357 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 10671 10357 145 145 0 10526 0
[pid=30873] vsize: 42684
Current children cumulated CPU time (s) 1129.27
Current children cumulated vsize (Kb) 44808

[startup+1140.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30875
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 10370 0 0 0 113858 69 0 0 25 0 1 0 1720787159 43708416 10357 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 10671 10357 145 145 0 10526 0
[pid=30873] vsize: 42684
Current children cumulated CPU time (s) 1139.27
Current children cumulated vsize (Kb) 44808

[startup+1150.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30875
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 10370 0 0 0 114859 69 0 0 25 0 1 0 1720787159 43708416 10357 4294967295 134512640 135094434 3221224448 3221223104 134557875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 10671 10357 145 145 0 10526 0
[pid=30873] vsize: 42684
Current children cumulated CPU time (s) 1149.28
Current children cumulated vsize (Kb) 44808

[startup+1160.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30875
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 10370 0 0 0 115859 69 0 0 25 0 1 0 1720787159 43708416 10357 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 10671 10357 145 145 0 10526 0
[pid=30873] vsize: 42684
Current children cumulated CPU time (s) 1159.28
Current children cumulated vsize (Kb) 44808

[startup+1170.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30875
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 10370 0 0 0 116859 69 0 0 25 0 1 0 1720787159 43708416 10357 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 10671 10357 145 145 0 10526 0
[pid=30873] vsize: 42684
Current children cumulated CPU time (s) 1169.28
Current children cumulated vsize (Kb) 44808

[startup+1180.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30875
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 10370 0 0 0 117860 69 0 0 25 0 1 0 1720787159 43708416 10357 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 10671 10357 145 145 0 10526 0
[pid=30873] vsize: 42684
Current children cumulated CPU time (s) 1179.29
Current children cumulated vsize (Kb) 44808

[startup+1190.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30875
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 10380 0 0 0 118860 69 0 0 25 0 1 0 1720787159 43773952 10367 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 10687 10367 145 145 0 10542 0
[pid=30873] vsize: 42748
Current children cumulated CPU time (s) 1189.29
Current children cumulated vsize (Kb) 44872

[startup+1200.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30875
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 10380 0 0 0 119860 69 0 0 25 0 1 0 1720787159 43773952 10367 4294967295 134512640 135094434 3221224448 3221223104 134557917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 10687 10367 145 145 0 10542 0
[pid=30873] vsize: 42748
Current children cumulated CPU time (s) 1199.29
Current children cumulated vsize (Kb) 44872

[startup+1210.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30875
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 10380 0 0 0 120860 69 0 0 25 0 1 0 1720787159 43773952 10367 4294967295 134512640 135094434 3221224448 3221223040 134556817 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 10687 10367 145 145 0 10542 0
[pid=30873] vsize: 42748
Current children cumulated CPU time (s) 1209.29
Current children cumulated vsize (Kb) 44872



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 30875
Raw data (/proc/30869/stat): 30869 (minisat+_script) S 30868 30869 20602 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1720787154 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30869/statm): 531 226 485 147 0 384 0
[pid=30869] vsize: 2124
Raw data (/proc/30873/stat): 30873 (minisat+_64-bit) R 30869 30869 20602 0 -1 0 10380 0 0 0 120860 69 0 0 25 0 1 0 1720787159 43773952 10367 4294967295 134512640 135094434 3221224448 3221223104 134558221 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30873/statm): 10687 10367 145 145 0 10542 0
[pid=30873] vsize: 42748
Current children cumulated CPU time (s) 1209.29
Current children cumulated vsize (Kb) 44872

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

Child status: 10
Real time (s): 1210.09
CPU time (s): 1209.33
CPU user time (s): 1208.61
CPU system time (s): 0.71989
CPU usage (%): 99.9371
Max. virtual memory (cumulated for all children) (Kb): 44872

Verifier Data

ERROR: no interpretation found !