Some explanations

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

General information on the benchmark

Namemps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-rgn.opb
MD5SUMe7e8123aa394c0918878e05410d4daeb
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 67200
Optimality of the best value was proved NO
Number of terms in the objective function 920
Biggest coefficient in the objective function 24576
Number of bits for the biggest coefficient in the objective function 15
Sum of the numbers in the objective function 1986400
Number of bits of the sum of numbers in the objective function 21
Biggest number in a constraint 3200000000
Number of bits of the biggest number in a constraint 32
Biggest sum of numbers in a constraint 29101875011
Number of bits of the biggest sum of numbers35
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1236.27
Number of variables1020
Total number of constraints204
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)104
Number of constraints which are nor clauses,nor cardinality constraints100
Minimum length of a constraint1
Maximum length of a constraint103

Trace number 6229

Launcher Data

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        887192 kB
Buffers:         25976 kB
Cached:          92364 kB
SwapCached:        660 kB
Active:          33288 kB
Inactive:        87552 kB
HighTotal:      131008 kB
HighFree:        35196 kB
LowTotal:       903652 kB
LowFree:        851996 kB
SwapTotal:     2097640 kB
SwapFree:      2096408 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5820 kB
Slab:            20892 kB
Committed_AS:    64164 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-20 04:57:15 (client local time) WITH STATUS 10 IN 1208.71 SECONDS
stats: 3390 7 1208.71 10

Solver Data

c Parsing PB file...
c Converting 124 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ####################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 123]---> BDD-cost:   13
c ---[ 122]---> BDD-cost:   13
c ---[ 121]---> BDD-cost:   13
c ---[ 120]---> BDD-cost:   13
c ---[ 119]---> BDD-cost:   13
c ---[ 118]---> BDD-cost:   13
c ---[ 117]---> BDD-cost:   13
c ---[ 116]---> BDD-cost:   13
c ---[ 115]---> BDD-cost:   13
c ---[ 114]---> BDD-cost:   13
c ---[ 113]---> BDD-cost:   13
c ---[ 112]---> BDD-cost:   13
c ---[ 111]---> BDD-cost:   13
c ---[ 110]---> BDD-cost:   13
c ---[ 109]---> BDD-cost:   13
c ---[ 108]---> BDD-cost:   13
c ---[ 107]---> BDD-cost:   13
c ---[ 106]---> BDD-cost:   13
c ---[ 105]---> BDD-cost:   13
c ---[ 104]---> BDD-cost:   13
c ---[ 103]---> BDD-cost:    8
c ---[ 102]---> BDD-cost:    8
c ---[ 101]---> BDD-cost:    8
c ---[ 100]---> BDD-cost:    8
c ---[  99]---> BDD-cost:    8
c ---[  98]---> BDD-cost:    8
c ---[  97]---> BDD-cost:    8
c ---[  96]---> BDD-cost:    8
c ---[  95]---> BDD-cost:    8
c ---[  94]---> BDD-cost:    8
c ---[  93]---> BDD-cost:    8
c ---[  92]---> BDD-cost:    8
c ---[  91]---> BDD-cost:    8
c ---[  90]---> BDD-cost:    8
c ---[  89]---> BDD-cost:    8
c ---[  88]---> BDD-cost:    8
c ---[  87]---> BDD-cost:    8
c ---[  86]---> BDD-cost:    8
c ---[  85]---> BDD-cost:    8
c ---[  84]---> BDD-cost:    8
c ---[  83]---> BDD-cost:    8
c ---[  82]---> BDD-cost:    8
c ---[  81]---> BDD-cost:    8
c ---[  80]---> BDD-cost:    8
c ---[  79]---> BDD-cost:    8
c ---[  78]---> BDD-cost:    8
c ---[  77]---> BDD-cost:    8
c ---[  76]---> BDD-cost:    8
c ---[  75]---> BDD-cost:    8
c ---[  74]---> BDD-cost:    8
c ---[  73]---> BDD-cost:    8
c ---[  72]---> BDD-cost:    8
c ---[  71]---> BDD-cost:    8
c ---[  70]---> BDD-cost:    8
c ---[  69]---> BDD-cost:    8
c ---[  68]---> BDD-cost:    8
c ---[  67]---> BDD-cost:    8
c ---[  66]---> BDD-cost:    8
c ---[  65]---> BDD-cost:    8
c ---[  64]---> BDD-cost:    8
c ---[  63]---> BDD-cost:   13
c ---[  62]---> BDD-cost:   13
c ---[  61]---> BDD-cost:   13
c ---[  60]---> BDD-cost:   13
c ---[  59]---> BDD-cost:   13
c ---[  58]---> BDD-cost:   13
c ---[  57]---> BDD-cost:   13
c ---[  56]---> BDD-cost:   13
c ---[  55]---> BDD-cost:   13
c ---[  54]---> BDD-cost:   13
c ---[  53]---> BDD-cost:   13
c ---[  52]---> BDD-cost:   13
c ---[  51]---> BDD-cost:   13
c ---[  50]---> BDD-cost:   13
c ---[  49]---> BDD-cost:   13
c ---[  48]---> BDD-cost:   13
c ---[  47]---> BDD-cost:   13
c ---[  46]---> BDD-cost:   13
c ---[  45]---> BDD-cost:   13
c ---[  44]---> BDD-cost:   13
c ---[  42]---> BDD-cost:  228
c ---[  40]---> BDD-cost:  906
c ---[  38]---> BDD-cost:  906
c ---[  36]---> BDD-cost:  906
c ---[  34]---> BDD-cost:  906
c ---[  32]---> BDD-cost:  906
c ---[  30]---> BDD-cost:  906
c ---[  28]---> BDD-cost:  906
c ---[  26]---> BDD-cost:  906
c ---[  24]---> BDD-cost:  906
c ---[  23]---> BDD-cost:   47
c ---[  21]---> BDD-cost:  906
c ---[  19]---> BDD-cost:  906
c ---[  17]---> BDD-cost:  906
c ---[  15]---> BDD-cost:  906
c ---[  13]---> BDD-cost:  906
c ---[  11]---> BDD-cost:  906
c ---[  10]---> BDD-cost:   47
c ---[   9]---> BDD-cost:   47
c ---[   8]---> BDD-cost:   47
c ---[   6]---> BDD-cost:  228
c ---[   4]---> BDD-cost:  228
c ---[   2]---> BDD-cost:  228
c ---[   0]---> BDD-cost:  228
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   40259   113278 |   13419       0        0     nan |  0.000 % |
c |       100 |   40118   112996 |   14760      92      564     6.1 |  0.951 % |
c |       250 |   40103   112966 |   16236     240     1981     8.3 |  0.998 % |
c |       477 |   40092   112944 |   17860     466     5702    12.2 |  1.031 % |
c |       814 |   40092   112944 |   19646     803    17649    22.0 |  1.031 % |
c |      1322 |   40092   112944 |   21611    1311    27839    21.2 |  1.031 % |
c |      2083 |   40092   112944 |   23772    2072    38233    18.5 |  1.031 % |
c |      3223 |   39997   112751 |   26149    3200    52692    16.5 |  1.247 % |
c |      4932 |   39983   112722 |   28764    4908    86494    17.6 |  1.254 % |
c |      7498 |   39909   112571 |   31641    7459   133322    17.9 |  1.483 % |
c |     11343 |   39891   112535 |   34805   11301   187175    16.6 |  1.537 % |
c |     17110 |   39766   112261 |   38285   17004   338276    19.9 |  1.874 % |
c |     25759 |   39746   112220 |   42114   25652   792984    30.9 |  1.881 % |
c |     38734 |   39746   112220 |   46326   38627  1026727    26.6 |  1.881 % |
c |     58198 |   39619   111941 |   50958   22540   676426    30.0 |  2.002 % |
c |     87390 |   39602   111907 |   56054   51730  1239064    24.0 |  2.056 % |
c |    131179 |   39292   111258 |   61659   50028  1324784    26.5 |  2.596 % |
c |    196863 |   39125   110902 |   67825   63381  1605437    25.3 |  3.034 % |
c |    295389 |   38687   109943 |   74608   50436  1436146    28.5 |  3.978 % |
c |    443178 |   38500   109542 |   82069   64703  1786871    27.6 |  4.402 % |
c ==============================================================================
c Found solution: 814378
c ---[   0]---> Sorter-cost:66120     Base: 2 2 2 2 2 2 3 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    658244 |  220981   535504 |   73660   52875  3351582    63.4 |  4.402 % |
c |    658344 |  220973   535488 |   81026   52973  3352621    63.3 |  1.005 % |
c |    658495 |  220952   535443 |   89128   53122  3353583    63.1 |  1.005 % |
c |    658720 |  220952   535443 |   98041   53347  3357206    62.9 |  1.005 % |
c |    659058 |  220952   535443 |  107845   53685  3362862    62.6 |  1.005 % |
c |    659564 |  220952   535443 |  118630   54191  3371925    62.2 |  1.005 % |
c |    660323 |  220952   535443 |  130493   54950  3394228    61.8 |  1.005 % |
c |    661462 |  220952   535443 |  143542   56089  3432961    61.2 |  1.005 % |
c |    663171 |  220952   535443 |  157896   57798  3459088    59.8 |  1.005 % |
c |    665733 |  220952   535443 |  173686   60360  3528174    58.5 |  1.005 % |
c |    669577 |  220952   535443 |  191055   64204  3606827    56.2 |  1.005 % |
c |    675343 |  220952   535443 |  210160   69970  3682771    52.6 |  1.005 % |
c |    683992 |  220952   535443 |  231176   78619  3957858    50.3 |  1.005 % |
c |    696967 |  220952   535443 |  254294   91594  4746587    51.8 |  1.005 % |
c |    716429 |  220935   535406 |  279723  111045  5477152    49.3 |  1.016 % |
c |    745621 |  220935   535406 |  307696  140237  6912181    49.3 |  1.016 % |
c |    789411 |  220903   535339 |  338465  184022  9087383    49.4 |  1.035 % |
c ==============================================================================
c Found solution: 448098
c ---[   0]---> Sorter-cost:   12     Base: 2 2 2 2 2 2 3 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    805474 |  221600   537386 |   73866  200085  9691724    48.4 |  1.035 % |
c |    805576 |  221600   537386 |   81252   22706   518069    22.8 |  1.031 % |
c |    805727 |  221600   537386 |   89377   22857   519321    22.7 |  1.031 % |
c |    805952 |  221600   537386 |   98315   23082   522059    22.6 |  1.031 % |
c |    806290 |  221600   537386 |  108147   23420   525041    22.4 |  1.031 % |
c |    806797 |  221600   537386 |  118961   23927   529488    22.1 |  1.031 % |
c |    807556 |  221518   537202 |  130858   24683   541108    21.9 |  1.058 % |
c |    808695 |  221477   537108 |  143943   25821   552112    21.4 |  1.071 % |
c |    810404 |  221477   537108 |  158338   27530   582434    21.2 |  1.071 % |
c |    812969 |  221477   537108 |  174172   30095   668074    22.2 |  1.071 % |
c |    816814 |  221477   537108 |  191589   33940   772663    22.8 |  1.071 % |
c |    822580 |  221477   537108 |  210748   39706  1057784    26.6 |  1.071 % |
c |    831229 |  221477   537108 |  231823   48355  1421889    29.4 |  1.071 % |
c |    844203 |  221477   537108 |  255005   61329  1917977    31.3 |  1.071 % |
c |    863664 |  221477   537108 |  280506   80790  2407543    29.8 |  1.071 % |
c |    892856 |  221381   536907 |  308556  109946  3371240    30.7 |  1.129 % |
c ==============================================================================
c Found solution: 233250
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 3 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    897055 |  221462   537101 |   73820  114145  3524606    30.9 |  1.129 % |
c |    897155 |  221462   537101 |   81202   27724   519075    18.7 |  1.129 % |
c |    897305 |  221462   537101 |   89322   27874   520470    18.7 |  1.129 % |
c |    897530 |  221462   537101 |   98254   28099   522245    18.6 |  1.129 % |
c |    897868 |  221171   536443 |  108079   28404   524583    18.5 |  1.232 % |
c |    898374 |  221171   536443 |  118887   28910   538384    18.6 |  1.232 % |
c |    899133 |  221171   536443 |  130776   29669   549995    18.5 |  1.232 % |
c |    900273 |  221171   536443 |  143854   30809   561146    18.2 |  1.232 % |
c |    901981 |  221171   536443 |  158239   32517   592744    18.2 |  1.232 % |
c |    904543 |  221171   536443 |  174063   35079   710858    20.3 |  1.232 % |
c |    908389 |  221171   536443 |  191470   38925   853279    21.9 |  1.232 % |
c |    914155 |  221171   536443 |  210617   44691  1111469    24.9 |  1.232 % |
c |    922804 |  221171   536443 |  231678   53340  1322266    24.8 |  1.232 % |
c |    935778 |  221134   536360 |  254846   66304  1882902    28.4 |  1.254 % |
c |    955240 |  221134   536360 |  280331   85766  2967169    34.6 |  1.254 % |
c |    984432 |  221107   536306 |  308364  114945  4194533    36.5 |  1.270 % |
c ==============================================================================
c Found solution: 233162
c ---[   0]---> Sorter-cost:   11     Base: 2 2 2 2 2 2 3 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    988122 |  221125   536453 |   73708  118635  4301809    36.3 |  1.270 % |
c |    988222 |  221123   536449 |   81078   30375   683144    22.5 |  1.273 % |
c |    988372 |  221123   536449 |   89186   30525   684026    22.4 |  1.273 % |
c |    988597 |  221123   536449 |   98105   30750   686137    22.3 |  1.273 % |
c |    988934 |  220944   536046 |  107915   31076   688900    22.2 |  1.334 % |
c |    989440 |  220944   536046 |  118707   31582   693327    22.0 |  1.334 % |
c |    990201 |  220944   536046 |  130578   32343   703900    21.8 |  1.334 % |
c |    991340 |  220944   536046 |  143636   33482   716103    21.4 |  1.334 % |
c |    993048 |  220944   536046 |  157999   35190   774995    22.0 |  1.334 % |
c |    995610 |  220932   536019 |  173799   37751   921702    24.4 |  1.338 % |
c |    999454 |  220932   536019 |  191179   41595  1028393    24.7 |  1.338 % |
c |   1005222 |  220932   536019 |  210297   47363  2188043    46.2 |  1.338 % |
c |   1013873 |  220932   536019 |  231327   56014  2367858    42.3 |  1.338 % |
c |   1026847 |  220932   536019 |  254460   68988  3142624    45.6 |  1.338 % |
c |   1046310 |  220932   536019 |  279906   88451  4144431    46.9 |  1.338 % |
c ==============================================================================
c Found solution: 216484
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 2 2 2 3 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |   1047505 |  220617   535311 |   73539   89627  4182324    46.7 |  1.338 % |
c |   1047606 |  220617   535311 |   80892   32998   660591    20.0 |  1.471 % |
c |   1047757 |  220617   535311 |   88982   33149   662245    20.0 |  1.471 % |
c |   1047982 |  220617   535311 |   97880   33374   664248    19.9 |  1.471 % |
c |   1048319 |  220617   535311 |  107668   33711   668588    19.8 |  1.471 % |
c |   1048825 |  220617   535311 |  118435   34217   674919    19.7 |  1.471 % |
c |   1049584 |  220280   534537 |  130278   34959   688719    19.7 |  1.609 % |
c |   1050724 |  220280   534537 |  143306   36099   723586    20.0 |  1.609 % |
c |   1052432 |  220280   534537 |  157637   37807   783850    20.7 |  1.609 % |
c |   1054994 |  220280   534537 |  173401   40369   858493    21.3 |  1.609 % |
c |   1058838 |  220280   534537 |  190741   44213  1043337    23.6 |  1.609 % |
c |   1064606 |  220280   534537 |  209815   49981  1280146    25.6 |  1.609 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v TA1_bit_7 TA1_bit_6 TA1_bit_5 TA1_bit_4 TA1_bit_3 TA1_bit_2 -TA1_bit_1 -TA1_bit0 -TA1_bit1 TA1_bit2 -TA1_bit3 -TA1_bit4 -TA1_bit5 -TA1_bit6 TA2_bit_7 TA2_bit_6 TA2_bit_5 TA2_bit_4 TA2_bit_3 TA2_bit_2 -TA2_bit_1 -TA2_bit0 -TA2_bit1 TA2_bit2 -TA2_bit3 -TA2_bit4 -TA2_bit5 -TA2_bit6 TA3_bit_7 TA3_bit_6 TA3_bit_5 TA3_bit_4 TA3_bit_3 TA3_bit_2 -TA3_bit_1 -TA3_bit0 TA3_bit1 -TA3_bit2 -TA3_bit3 -TA3_bit4 -TA3_bit5 -TA3_bit6 TA4_bit_7 TA4_bit_6 TA4_bit_5 TA4_bit_4 TA4_bit_3 TA4_bit_2 -TA4_bit_1 TA4_bit0 -TA4_bit1 -TA4_bit2 -TA4_bit3 -TA4_bit4 -TA4_bit5 -TA4_bit6 TB1_bit_7 TB1_bit_6 TB1_bit_5 TB1_bit_4 TB1_bit_3 TB1_bit_2 -TB1_bit_1 -TB1_bit0 -TB1_bit1 TB1_bit2 TB1_bit3 -TB1_bit4 -TB1_bit5 -TB1_bit6 TB2_bit_7 TB2_bit_6 TB2_bit_5 TB2_bit_4 TB2_bit_3 TB2_bit_2 TB2_bit_1 -TB2_bit0 -TB2_bit1 -TB2_bit2 -TB2_bit3 -TB2_bit4 -TB2_bit5 -TB2_bit6 TB3_bit_7 TB3_bit_6 TB3_bit_5 TB3_bit_4 TB3_bit_3 TB3_bit_2 -TB3_bit_1 -TB3_bit0 TB3_bit1 -TB3_bit2 -TB3_bit3 -TB3_bit4 -TB3_bit5 -TB3_bit6 TB4_bit_7 TB4_bit_6 TB4_bit_5 TB4_bit_4 TB4_bit_3 TB4_bit_2 -TB4_bit_1 -TB4_bit0 TB4_bit1 TB4_bit2 -TB4_bit3 -TB4_bit4 -TB4_bit5 -TB4_bit6 -TC1_bit_7 TC1_bit_6 -TC1_bit_5 TC1_bit_4 TC1_bit_3 TC1_bit_2 -TC1_bit_1 -TC1_bit0 -TC1_bit1 TC1_bit2 TC1_bit3 -TC1_bit4 -TC1_bit5 -TC1_bit6 -TC2_bit_7 TC2_bit_6 TC2_bit_5 TC2_bit_4 TC2_bit_3 TC2_bit_2 -TC2_bit_1 TC2_bit0 -TC2_bit1 TC2_bit2 TC2_bit3 -TC2_bit4 -TC2_bit5 -TC2_bit6 TC3_bit_7 TC3_bit_6 TC3_bit_5 TC3_bit_4 TC3_bit_3 TC3_bit_2 -TC3_bit_1 TC3_bit0 -TC3_bit1 TC3_bit2 TC3_bit3 -TC3_bit4 -TC3_bit5 -TC3_bit6 TC4_bit_7 TC4_bit_6 TC4_bit_5 TC4_bit_4 TC4_bit_3 TC4_bit_2 -TC4_bit_1 TC4_bit0 TC4_bit1 TC4_bit2 TC4_bit3 -TC4_bit4 -TC4_bit5 -TC4_bit6 TD1_bit_7 TD1_bit_6 TD1_bit_5 TD1_bit_4 TD1_bit_3 TD1_bit_2 -TD1_bit_1 -TD1_bit0 TD1_bit1 TD1_bit2 TD1_bit3 -TD1_bit4 -TD1_bit5 -TD1_bit6 TD2_bit_7 TD2_bit_6 TD2_bit_5 TD2_bit_4 TD2_bit_3 TD2_bit_2 -TD2_bit_1 TD2_bit0 -TD2_bit1 TD2_bit2 TD2_bit3 TD2_bit4 -TD2_bit5 -TD2_bit6 TD3_bit_7 TD3_bit_6 TD3_bit_5 TD3_bit_4 TD3_bit_3 TD3_bit_2 -TD3_bit_1 -TD3_bit0 TD3_bit1 TD3_bit2 -TD3_bit3 -TD3_bit4 -TD3_bit5 -TD3_bit6 TD4_bit_7 TD4_bit_6 TD4_bit_5 TD4_bit_4 TD4_bit_3 TD4_bit_2 -TD4_bit_1 TD4_bit0 TD4_bit1 TD4_bit2 TD4_bit3 -TD4_bit4 -TD4_bit5 -TD4_bit6 TE1_bit_7 TE1_bit_6 TE1_bit_5 TE1_bit_4 TE1_bit_3 TE1_bit_2 -TE1_bit_1 -TE1_bit0 TE1_bit1 TE1_bit2 -TE1_bit3 -TE1_bit4 -TE1_bit5 -TE1_bit6 TE2_bit_7 TE2_bit_6 TE2_bit_5 TE2_bit_4 TE2_bit_3 TE2_bit_2 -TE2_bit_1 -TE2_bit0 TE2_bit1 TE2_bit2 TE2_bit3 -TE2_bit4 -TE2_bit5 -TE2_bit6 TE3_bit_7 TE3_bit_6 TE3_bit_5 TE3_bit_4 TE3_bit_3 TE3_bit_2 -TE3_bit_1 -TE3_bit0 TE3_bit1 TE3_bit2 -TE3_bit3 -TE3_bit4 -TE3_bit5 -TE3_bit6 TE4_bit_7 TE4_bit_6 TE4_bit_5 TE4_bit_4 TE4_bit_3 TE4_bit_2 -TE4_bit_1 -TE4_bit0 -TE4_bit1 TE4_bit2 -TE4_bit3 -TE4_bit4 -TE4_bit5 -TE4_bit6 UA1_bit_7 UA1_bit_6 UA1_bit_5 UA1_bit_4 UA1_bit_3 UA1_bit_2 -UA1_bit_1 UA1_bit0 -UA1_bit1 UA2_bit_7 UA2_bit_6 UA2_bit_5 UA2_bit_4 UA2_bit_3 UA2_bit_2 -UA2_bit_1 -UA2_bit0 -UA2_bit1 UA3_bit_7 UA3_bit_6 UA3_bit_5 UA3_bit_4 UA3_bit_3 UA3_bit_2 UA3_bit_1 -UA3_bit0 -UA3_bit1 UA4_bit_7 UA4_bit_6 UA4_bit_5 UA4_bit_4 UA4_bit_3 UA4_bit_2 -UA4_bit_1 -UA4_bit0 -UA4_bit1 UB1_bit_7 UB1_bit_6 UB1_bit_5 UB1_bit_4 UB1_bit_3 UB1_bit_2 -UB1_bit_1 UB1_bit0 -UB1_bit1 UB2_bit_7 UB2_bit_6 UB2_bit_5 UB2_bit_4 UB2_bit_3 UB2_bit_2 UB2_bit_1 UB2_bit0 -UB2_bit1 UB3_bit_7 UB3_bit_6 UB3_bit_5 UB3_bit_4 UB3_bit_3 UB3_bit_2 UB3_bit_1 -UB3_bit0 -UB3_bit1 UB4_bit_7 UB4_bit_6 UB4_bit_5 UB4_bit_4 UB4_bit_3 UB4_bit_2 -UB4_bit_1 -UB4_bit0 -UB4_bit1 -UC1_bit_7 -UC1_bit_6 UC1_bit_5 UC1_bit_4 UC1_bit_3 UC1_bit_2 -UC1_bit_1 UC1_bit0 -UC1_bit1 -UC2_bit_7 -UC2_bit_6 UC2_bit_5 UC2_bit_4 UC2_bit_3 UC2_bit_2 -UC2_bit_1 UC2_bit0 -UC2_bit1 UC3_bit_7 -UC3_bit_6 UC3_bit_5 UC3_bit_4 UC3_bit_3 UC3_bit_2 -UC3_bit_1 -UC3_bit0 -UC3_bit1 UC4_bit_7 -UC4_bit_6 UC4_bit_5 UC4_bit_4 UC4_bit_3 UC4_bit_2 -UC4_bit_1 -UC4_bit0 -UC4_bit1 UD1_bit_7 UD1_bit_6 UD1_bit_5 UD1_bit_4 UD1_bit_3 UD1_bit_2 -UD1_bit_1 -UD1_bit0 -UD1_bit1 UD2_bit_7 UD2_bit_6 UD2_bit_5 UD2_bit_4 UD2_bit_3 UD2_bit_2 -UD2_bit_1 UD2_bit0 -UD2_bit1 UD3_bit_7 UD3_bit_6 UD3_bit_5 UD3_bit_4 UD3_bit_3 UD3_bit_2 UD3_bit_1 UD3_bit0 -UD3_bit1 UD4_bit_7 UD4_bit_6 UD4_bit_5 UD4_bit_4 UD4_bit_3 UD4_bit_2 UD4_bit_1 UD4_bit0 -UD4_bit1 UE1_bit_7 UE1_bit_6 UE1_bit_5 UE1_bit_4 UE1_bit_3 UE1_bit_2 -UE1_bit_1 -UE1_bit0 -UE1_bit1 UE2_bit_7 UE2_bit_6 UE2_bit_5 UE2_bit_4 UE2_bit_3 UE2_bit_2 UE2_bit_1 -UE2_bit0 -UE2_bit1 UE3_bit_7 UE3_bit_6 UE3_bit_5 UE3_bit_4 UE3_bit_3 UE3_bit_2 -UE3_bit_1 -UE3_bit0 -UE3_bit1 UE4_bit_7 UE4_bit_6 UE4_bit_5 UE4_bit_4 UE4_bit_3 UE4_bit_2 UE4_bit_1 -UE4_bit0 -UE4_bit1 VA1_bit_7 VA1_bit_6 VA1_bit_5 VA1_bit_4 VA1_bit_3 VA1_bit_2 -VA1_bit_1 -VA1_bit0 -VA1_bit1 VA2_bit_7 VA2_bit_6 VA2_bit_5 VA2_bit_4 VA2_bit_3 VA2_bit_2 -VA2_bit_1 -VA2_bit0 -VA2_bit1 VA3_bit_7 VA3_bit_6 VA3_bit_5 VA3_bit_4 VA3_bit_3 VA3_bit_2 -VA3_bit_1 -VA3_bit0 -VA3_bit1 VA4_bit_7 VA4_bit_6 VA4_bit_5 VA4_bit_4 VA4_bit_3 VA4_bit_2 -VA4_bit_1 VA4_bit0 -VA4_bit1 VB1_bit_7 VB1_bit_6 VB1_bit_5 VB1_bit_4 VB1_bit_3 VB1_bit_2 VB1_bit_1 -VB1_bit0 -VB1_bit1 VB2_bit_7 VB2_bit_6 VB2_bit_5 VB2_bit_4 VB2_bit_3 VB2_bit_2 -VB2_bit_1 VB2_bit0 -VB2_bit1 VB3_bit_7 VB3_bit_6 VB3_bit_5 VB3_bit_4 VB3_bit_3 VB3_bit_2 -VB3_bit_1 VB3_bit0 -VB3_bit1 VB4_bit_7 VB4_bit_6 VB4_bit_5 VB4_bit_4 VB4_bit_3 VB4_bit_2 -VB4_bit_1 -VB4_bit0 -VB4_bit1 VC1_bit_7 -VC1_bit_6 VC1_bit_5 VC1_bit_4 VC1_bit_3 VC1_bit_2 VC1_bit_1 VC1_bit0 -VC1_bit1 VC2_bit_7 -VC2_bit_6 VC2_bit_5 VC2_bit_4 VC2_bit_3 VC2_bit_2 -VC2_bit_1 -VC2_bit0 -VC2_bit1 VC3_bit_7 -VC3_bit_6 VC3_bit_5 VC3_bit_4 VC3_bit_3 VC3_bit_2 VC3_bit_1 -VC3_bit0 -VC3_bit1 VC4_bit_7 -VC4_bit_6 VC4_bit_5 VC4_bit_4 VC4_bit_3 VC4_bit_2 -VC4_bit_1 VC4_bit0 -VC4_bit1 VD1_bit_7 VD1_bit_6 VD1_bit_5 VD1_bit_4 VD1_bit_3 VD1_bit_2 VD1_bit_1 -VD1_bit0 -VD1_bit1 VD2_bit_7 VD2_bit_6 VD2_bit_5 VD2_bit_4 VD2_bit_3 VD2_bit_2 -VD2_bit_1 VD2_bit0 -VD2_bit1 VD3_bit_7 VD3_bit_6 VD3_bit_5 VD3_bit_4 VD3_bit_3 VD3_bit_2 -VD3_bit_1 VD3_bit0 -VD3_bit1 VD4_bit_7 VD4_bit_6 VD4_bit_5 VD4_bit_4 VD4_bit_3 VD4_bit_2 VD4_bit_1 VD4_bit0 -VD4_bit1 VE1_bit_7 VE1_bit_6 VE1_bit_5 VE1_bit_4 VE1_bit_3 VE1_bit_2 VE1_bit_1 VE1_bit0 -VE1_bit1 VE2_bit_7 VE2_bit_6 VE2_bit_5 VE2_bit_4 VE2_bit_3 VE2_bit_2 VE2_bit_1 VE2_bit0 -VE2_bit1 VE3_bit_7 VE3_bit_6 VE3_bit_5 VE3_bit_4 VE3_bit_3 VE3_bit_2 -VE3_bit_1 -VE3_bit0 -VE3_bit1 VE4_bit_7 VE4_bit_6 VE4_bit_5 VE4_bit_4 VE4_bit_3 VE4_bit_2 -VE4_bit_1 VE4_bit0 -VE4_bit1 WA1_bit_7 WA1_bit_6 WA1_bit_5 WA1_bit_4 WA1_bit_3 WA1_bit_2 WA1_bit_1 -WA1_bit0 -WA1_bit1 -WA1_bit2 WA1_bit3 -WA1_bit4 -WA1_bit5 -WA1_bit6 WA2_bit_7 WA2_bit_6 WA2_bit_5 WA2_bit_4 WA2_bit_3 WA2_bit_2 -WA2_bit_1 WA2_bit0 WA2_bit1 -WA2_bit2 WA2_bit3 -WA2_bit4 -WA2_bit5 -WA2_bit6 WA3_bit_7 WA3_bit_6 WA3_bit_5 WA3_bit_4 WA3_bit_3 WA3_bit_2 -WA3_bit_1 WA3_bit0 -WA3_bit1 WA3_bit2 WA3_bit3 -WA3_bit4 -WA3_bit5 -WA3_bit6 WA4_bit_7 WA4_bit_6 WA4_bit_5 WA4_bit_4 WA4_bit_3 WA4_bit_2 -WA4_bit_1 -WA4_bit0 WA4_bit1 WA4_bit2 WA4_bit3 -WA4_bit4 -WA4_bit5 -WA4_bit6 WB1_bit_7 WB1_bit_6 WB1_bit_5 WB1_bit_4 WB1_bit_3 WB1_bit_2 -WB1_bit_1 -WB1_bit0 -WB1_bit1 -WB1_bit2 -WB1_bit3 WB1_bit4 -WB1_bit5 -WB1_bit6 WB2_bit_7 WB2_bit_6 WB2_bit_5 WB2_bit_4 WB2_bit_3 WB2_bit_2 -WB2_bit_1 -WB2_bit0 -WB2_bit1 -WB2_bit2 WB2_bit3 -WB2_bit4 -WB2_bit5 -WB2_bit6 WB3_bit_7 WB3_bit_6 WB3_bit_5 WB3_bit_4 WB3_bit_3 WB3_bit_2 -WB3_bit_1 -WB3_bit0 -WB3_bit1 WB3_bit2 WB3_bit3 -WB3_bit4 -WB3_bit5 -WB3_bit6 WB4_bit_7 WB4_bit_6 WB4_bit_5 WB4_bit_4 WB4_bit_3 WB4_bit_2 -WB4_bit_1 -WB4_bit0 -WB4_bit1 WB4_bit2 -WB4_bit3 WB4_bit4 -WB4_bit5 -WB4_bit6 WC1_bit_7 -WC1_bit_6 -WC1_bit_5 WC1_bit_4 WC1_bit_3 WC1_bit_2 -WC1_bit_1 WC1_bit0 WC1_bit1 WC1_bit2 WC1_bit3 -WC1_bit4 -WC1_bit5 -WC1_bit6 WC2_bit_7 -WC2_bit_6 WC2_bit_5 WC2_bit_4 WC2_bit_3 WC2_bit_2 -WC2_bit_1 WC2_bit0 -WC2_bit1 WC2_bit2 -WC2_bit3 WC2_bit4 -WC2_bit5 -WC2_bit6 WC3_bit_7 WC3_bit_6 WC3_bit_5 WC3_bit_4 WC3_bit_3 WC3_bit_2 -WC3_bit_1 WC3_bit0 WC3_bit1 WC3_bit2 -WC3_bit3 WC3_bit4 -WC3_bit5 -WC3_bit6 WC4_bit_7 WC4_bit_6 WC4_bit_5 WC4_bit_4 WC4_bit_3 WC4_bit_2 -WC4_bit_1 -WC4_bit0 -WC4_bit1 WC4_bit2 WC4_bit3 WC4_bit4 -WC4_bit5 -WC4_bit6 WD1_bit_7 WD1_bit_6 WD1_bit_5 WD1_bit_4 WD1_bit_3 WD1_bit_2 -WD1_bit_1 WD1_bit0 -WD1_bit1 -

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/21619/stat): 21619 (minisat+_script) R 21618 21619 20115 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1855720588 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/21619/statm): 174 3 169 147 0 27 0
[pid=21619] 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=21620
New process pid=21621
New process pid=21622
execve syscall for /bin/sed executable
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
One traced child (pid=21621) exited with status: 0
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=21622) exited with status: 0
One traced child (pid=21620) exited with status: 0
New process pid=21623
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-13-7-rgn.opb

[startup+10.0029 s]
Raw data (loadavg): 0.82 0.93 0.90 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 2289 0 0 0 971 11 0 0 25 0 1 0 1855720593 9605120 2218 4294967295 134512640 135094434 3221224448 3221223104 134558232 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 2345 2218 145 145 0 2200 0
[pid=21623] vsize: 9380
Current children cumulated CPU time (s) 9.83
Current children cumulated vsize (Kb) 11504

[startup+20.0046 s]
Raw data (loadavg): 0.85 0.93 0.90 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 2945 0 0 0 1962 14 0 0 25 0 1 0 1855720593 12386304 2874 4294967295 134512640 135094434 3221224448 3221223120 134555855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21623/statm): 3024 2874 145 145 0 2879 0
[pid=21623] vsize: 12096
Current children cumulated CPU time (s) 19.77
Current children cumulated vsize (Kb) 14220

[startup+30.0063 s]
Raw data (loadavg): 0.87 0.93 0.90 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 3274 0 0 0 2956 17 0 0 25 0 1 0 1855720593 13709312 3203 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 3347 3203 145 145 0 3202 0
[pid=21623] vsize: 13388
Current children cumulated CPU time (s) 29.74
Current children cumulated vsize (Kb) 15512

[startup+40.007 s]
Raw data (loadavg): 0.89 0.93 0.90 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 3302 0 0 0 3956 17 0 0 25 0 1 0 1855720593 13840384 3231 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 3379 3231 145 145 0 3234 0
[pid=21623] vsize: 13516
Current children cumulated CPU time (s) 39.74
Current children cumulated vsize (Kb) 15640

[startup+50.0076 s]
Raw data (loadavg): 0.90 0.93 0.90 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 3361 0 0 0 4956 18 0 0 25 0 1 0 1855720593 14082048 3290 4294967295 134512640 135094434 3221224448 3221223040 134557219 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 3438 3290 145 145 0 3293 0
[pid=21623] vsize: 13752
Current children cumulated CPU time (s) 49.75
Current children cumulated vsize (Kb) 15876

[startup+60.0083 s]
Raw data (loadavg): 0.92 0.94 0.90 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 3647 0 0 0 5953 19 0 0 25 0 1 0 1855720593 15290368 3576 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 3733 3576 145 145 0 3588 0
[pid=21623] vsize: 14932
Current children cumulated CPU time (s) 59.73
Current children cumulated vsize (Kb) 17056

[startup+70.01 s]
Raw data (loadavg): 0.93 0.94 0.90 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 3676 0 0 0 6953 19 0 0 25 0 1 0 1855720593 15421440 3605 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 3765 3605 145 145 0 3620 0
[pid=21623] vsize: 15060
Current children cumulated CPU time (s) 69.73
Current children cumulated vsize (Kb) 17184

[startup+80.0107 s]
Raw data (loadavg): 0.94 0.94 0.90 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 4302 0 0 0 7944 22 0 0 25 0 1 0 1855720593 17965056 4231 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 4386 4231 145 145 0 4241 0
[pid=21623] vsize: 17544
Current children cumulated CPU time (s) 79.67
Current children cumulated vsize (Kb) 19668

[startup+90.0114 s]
Raw data (loadavg): 0.95 0.94 0.90 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 4401 0 0 0 8943 23 0 0 25 0 1 0 1855720593 18620416 4330 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 4546 4330 145 145 0 4401 0
[pid=21623] vsize: 18184
Current children cumulated CPU time (s) 89.67
Current children cumulated vsize (Kb) 20308

[startup+100.012 s]
Raw data (loadavg): 0.96 0.94 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 4425 0 0 0 9943 23 0 0 25 0 1 0 1855720593 18735104 4354 4294967295 134512640 135094434 3221224448 3221223104 134557882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 4574 4354 145 145 0 4429 0
[pid=21623] vsize: 18296
Current children cumulated CPU time (s) 99.67
Current children cumulated vsize (Kb) 20420

[startup+110.013 s]
Raw data (loadavg): 0.96 0.94 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 4488 0 0 0 10942 24 0 0 25 0 1 0 1855720593 19030016 4417 4294967295 134512640 135094434 3221224448 3221223104 134558126 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 4646 4417 145 145 0 4501 0
[pid=21623] vsize: 18584
Current children cumulated CPU time (s) 109.67
Current children cumulated vsize (Kb) 20708

[startup+120.013 s]
Raw data (loadavg): 0.97 0.94 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 4621 0 0 0 11941 24 0 0 25 0 1 0 1855720593 19570688 4550 4294967295 134512640 135094434 3221224448 3221223072 134557691 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 4778 4550 145 145 0 4633 0
[pid=21623] vsize: 19112
Current children cumulated CPU time (s) 119.66
Current children cumulated vsize (Kb) 21236

[startup+130.014 s]
Raw data (loadavg): 0.97 0.95 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 4622 0 0 0 12942 24 0 0 25 0 1 0 1855720593 19570688 4551 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 4778 4551 145 145 0 4633 0
[pid=21623] vsize: 19112
Current children cumulated CPU time (s) 129.67
Current children cumulated vsize (Kb) 21236

[startup+140.015 s]
Raw data (loadavg): 0.98 0.95 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 4730 0 0 0 13941 24 0 0 25 0 1 0 1855720593 20070400 4659 4294967295 134512640 135094434 3221224448 3221223040 134557363 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 4900 4659 145 145 0 4755 0
[pid=21623] vsize: 19600
Current children cumulated CPU time (s) 139.66
Current children cumulated vsize (Kb) 21724

[startup+150.015 s]
Raw data (loadavg): 0.98 0.95 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 5382 0 0 0 14931 30 0 0 25 0 1 0 1855720593 22769664 5311 4294967295 134512640 135094434 3221224448 3221222368 134562749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 5559 5311 145 145 0 5414 0
[pid=21623] vsize: 22236
Current children cumulated CPU time (s) 149.62
Current children cumulated vsize (Kb) 24360

[startup+160.015 s]
Raw data (loadavg): 0.98 0.95 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 5382 0 0 0 15932 30 0 0 25 0 1 0 1855720593 22769664 5311 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 5559 5311 145 145 0 5414 0
[pid=21623] vsize: 22236
Current children cumulated CPU time (s) 159.63
Current children cumulated vsize (Kb) 24360

[startup+170.016 s]
Raw data (loadavg): 0.98 0.95 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 5428 0 0 0 16932 30 0 0 25 0 1 0 1855720593 22974464 5357 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 5609 5357 145 145 0 5464 0
[pid=21623] vsize: 22436
Current children cumulated CPU time (s) 169.63
Current children cumulated vsize (Kb) 24560

[startup+180.017 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 5516 0 0 0 17931 30 0 0 25 0 1 0 1855720593 23396352 5445 4294967295 134512640 135094434 3221224448 3221223040 134557236 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 5712 5445 145 145 0 5567 0
[pid=21623] vsize: 22848
Current children cumulated CPU time (s) 179.62
Current children cumulated vsize (Kb) 24972

[startup+190.017 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 5898 0 0 0 18926 33 0 0 25 0 1 0 1855720593 24907776 5827 4294967295 134512640 135094434 3221224448 3221223104 134557875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 6081 5827 145 145 0 5936 0
[pid=21623] vsize: 24324
Current children cumulated CPU time (s) 189.6
Current children cumulated vsize (Kb) 26448

[startup+200.018 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 5899 0 0 0 19926 33 0 0 25 0 1 0 1855720593 24907776 5828 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 6081 5828 145 145 0 5936 0
[pid=21623] vsize: 24324
Current children cumulated CPU time (s) 199.6
Current children cumulated vsize (Kb) 26448

[startup+210.019 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 5899 0 0 0 20927 33 0 0 25 0 1 0 1855720593 24907776 5828 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 6081 5828 145 145 0 5936 0
[pid=21623] vsize: 24324
Current children cumulated CPU time (s) 209.61
Current children cumulated vsize (Kb) 26448

[startup+220.02 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 5911 0 0 0 21927 33 0 0 25 0 1 0 1855720593 24973312 5840 4294967295 134512640 135094434 3221224448 3221222992 134779266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 6097 5840 145 145 0 5952 0
[pid=21623] vsize: 24388
Current children cumulated CPU time (s) 219.61
Current children cumulated vsize (Kb) 26512

[startup+230.021 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 5911 0 0 0 22927 33 0 0 25 0 1 0 1855720593 24973312 5840 4294967295 134512640 135094434 3221224448 3221223104 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 6097 5840 145 145 0 5952 0
[pid=21623] vsize: 24388
Current children cumulated CPU time (s) 229.61
Current children cumulated vsize (Kb) 26512

[startup+240.021 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 5911 0 0 0 23927 33 0 0 25 0 1 0 1855720593 24973312 5840 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 6097 5840 145 145 0 5952 0
[pid=21623] vsize: 24388
Current children cumulated CPU time (s) 239.61
Current children cumulated vsize (Kb) 26512

[startup+250.021 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 5911 0 0 0 24928 33 0 0 25 0 1 0 1855720593 24973312 5840 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 6097 5840 145 145 0 5952 0
[pid=21623] vsize: 24388
Current children cumulated CPU time (s) 249.62
Current children cumulated vsize (Kb) 26512

[startup+260.022 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 5911 0 0 0 25928 33 0 0 25 0 1 0 1855720593 24973312 5840 4294967295 134512640 135094434 3221224448 3221223072 134557598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 6097 5840 145 145 0 5952 0
[pid=21623] vsize: 24388
Current children cumulated CPU time (s) 259.62
Current children cumulated vsize (Kb) 26512

[startup+270.023 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 6352 0 0 0 26920 37 0 0 25 0 1 0 1855720593 26791936 6281 4294967295 134512640 135094434 3221224448 3221223040 134551434 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 6541 6281 145 145 0 6396 0
[pid=21623] vsize: 26164
Current children cumulated CPU time (s) 269.58
Current children cumulated vsize (Kb) 28288

[startup+280.023 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 6386 0 0 0 27920 37 0 0 25 0 1 0 1855720593 26955776 6315 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 6581 6315 145 145 0 6436 0
[pid=21623] vsize: 26324
Current children cumulated CPU time (s) 279.58
Current children cumulated vsize (Kb) 28448

[startup+290.024 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 6447 0 0 0 28921 37 0 0 25 0 1 0 1855720593 27283456 6376 4294967295 134512640 135094434 3221224448 3221223120 134556543 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 6661 6376 145 145 0 6516 0
[pid=21623] vsize: 26644
Current children cumulated CPU time (s) 289.59
Current children cumulated vsize (Kb) 28768

[startup+300.025 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 6481 0 0 0 29921 37 0 0 25 0 1 0 1855720593 27545600 6410 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 6725 6410 145 145 0 6580 0
[pid=21623] vsize: 26900
Current children cumulated CPU time (s) 299.59
Current children cumulated vsize (Kb) 29024

[startup+310.025 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 6534 0 0 0 30921 37 0 0 25 0 1 0 1855720593 27807744 6463 4294967295 134512640 135094434 3221224448 3221223120 134556257 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 6789 6463 145 145 0 6644 0
[pid=21623] vsize: 27156
Current children cumulated CPU time (s) 309.59
Current children cumulated vsize (Kb) 29280

[startup+320.026 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 6536 0 0 0 31921 37 0 0 25 0 1 0 1855720593 27807744 6465 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 6789 6465 145 145 0 6644 0
[pid=21623] vsize: 27156
Current children cumulated CPU time (s) 319.59
Current children cumulated vsize (Kb) 29280

[startup+330.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 6778 0 0 0 32918 39 0 0 25 0 1 0 1855720593 28794880 6707 4294967295 134512640 135094434 3221224448 3221223104 134557937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 7030 6707 145 145 0 6885 0
[pid=21623] vsize: 28120
Current children cumulated CPU time (s) 329.58
Current children cumulated vsize (Kb) 30244

[startup+340.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 6786 0 0 0 33918 39 0 0 25 0 1 0 1855720593 28827648 6715 4294967295 134512640 135094434 3221224448 3221223072 134557717 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 7038 6715 145 145 0 6893 0
[pid=21623] vsize: 28152
Current children cumulated CPU time (s) 339.58
Current children cumulated vsize (Kb) 30276

[startup+350.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 6794 0 0 0 34919 39 0 0 25 0 1 0 1855720593 28860416 6723 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 7046 6723 145 145 0 6901 0
[pid=21623] vsize: 28184
Current children cumulated CPU time (s) 349.59
Current children cumulated vsize (Kb) 30308

[startup+360.029 s]
Raw data (loadavg): 0.99 0.97 0.91 1/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) T 21619 21619 20115 0 -1 0 6942 0 0 0 35916 40 0 0 25 0 1 0 1855720593 29474816 6871 4294967295 134512640 135094434 3221224448 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/21623/statm): 7196 6871 145 145 0 7051 0
[pid=21623] vsize: 28784
Current children cumulated CPU time (s) 359.57
Current children cumulated vsize (Kb) 30908

[startup+370.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 7492 0 0 0 36908 43 0 0 25 0 1 0 1855720593 31703040 7421 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 7740 7421 145 145 0 7595 0
[pid=21623] vsize: 30960
Current children cumulated CPU time (s) 369.52
Current children cumulated vsize (Kb) 33084

[startup+380.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 7492 0 0 0 37909 43 0 0 25 0 1 0 1855720593 31703040 7421 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 7740 7421 145 145 0 7595 0
[pid=21623] vsize: 30960
Current children cumulated CPU time (s) 379.53
Current children cumulated vsize (Kb) 33084

[startup+390.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 7502 0 0 0 38909 43 0 0 25 0 1 0 1855720593 31768576 7431 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 7756 7431 145 145 0 7611 0
[pid=21623] vsize: 31024
Current children cumulated CPU time (s) 389.53
Current children cumulated vsize (Kb) 33148

[startup+400.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 7727 0 0 0 39905 45 0 0 25 0 1 0 1855720593 32690176 7656 4294967295 134512640 135094434 3221224448 3221223040 134556817 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 7981 7656 145 145 0 7836 0
[pid=21623] vsize: 31924
Current children cumulated CPU time (s) 399.51
Current children cumulated vsize (Kb) 34048

[startup+410.032 s]
Raw data (loadavg): 0.99 0.97 0.91 1/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) T 21619 21619 20115 0 -1 0 11639 0 0 0 40873 60 0 0 23 0 1 0 1855720593 49553408 11442 4294967295 134512640 135094434 3221224448 3221184220 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/21623/statm): 12098 11442 145 145 0 11953 0
[pid=21623] vsize: 48392
Current children cumulated CPU time (s) 409.34
Current children cumulated vsize (Kb) 50516

[startup+420.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 13394 0 0 0 41855 68 0 0 25 0 1 0 1855720593 59834368 13197 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 14608 13197 145 145 0 14463 0
[pid=21623] vsize: 58432
Current children cumulated CPU time (s) 419.24
Current children cumulated vsize (Kb) 60556

[startup+430.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 13570 0 0 0 42852 69 0 0 25 0 1 0 1855720593 60555264 13373 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 14784 13373 145 145 0 14639 0
[pid=21623] vsize: 59136
Current children cumulated CPU time (s) 429.22
Current children cumulated vsize (Kb) 61260

[startup+440.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 13694 0 0 0 43850 70 0 0 25 0 1 0 1855720593 61059072 13497 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 14907 13497 145 145 0 14762 0
[pid=21623] vsize: 59628
Current children cumulated CPU time (s) 439.21
Current children cumulated vsize (Kb) 61752

[startup+450.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 13762 0 0 0 44849 71 0 0 25 0 1 0 1855720593 61341696 13565 4294967295 134512640 135094434 3221224448 3221223072 134557724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 14976 13565 145 145 0 14831 0
[pid=21623] vsize: 59904
Current children cumulated CPU time (s) 449.21
Current children cumulated vsize (Kb) 62028

[startup+460.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 13917 0 0 0 45847 71 0 0 25 0 1 0 1855720593 61943808 13720 4294967295 134512640 135094434 3221224448 3221223060 134563046 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 15123 13720 145 145 0 14978 0
[pid=21623] vsize: 60492
Current children cumulated CPU time (s) 459.19
Current children cumulated vsize (Kb) 62616

[startup+470.036 s]
Raw data (loadavg): 0.99 0.97 0.91 1/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) T 21619 21619 20115 0 -1 0 14280 0 0 0 46841 74 0 0 25 0 1 0 1855720593 63430656 14083 4294967295 134512640 135094434 3221224448 3221222828 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/21623/statm): 15486 14083 145 145 0 15341 0
[pid=21623] vsize: 61944
Current children cumulated CPU time (s) 469.16
Current children cumulated vsize (Kb) 64068

[startup+480.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 14670 0 0 0 47834 77 0 0 25 0 1 0 1855720593 65019904 14473 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 15874 14473 145 145 0 15729 0
[pid=21623] vsize: 63496
Current children cumulated CPU time (s) 479.12
Current children cumulated vsize (Kb) 65620

[startup+490.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 14978 0 0 0 48829 79 0 0 25 0 1 0 1855720593 66281472 14781 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 16182 14781 145 145 0 16037 0
[pid=21623] vsize: 64728
Current children cumulated CPU time (s) 489.09
Current children cumulated vsize (Kb) 66852

[startup+500.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 15219 0 0 0 49825 81 0 0 25 0 1 0 1855720593 67248128 15022 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 16418 15022 145 145 0 16273 0
[pid=21623] vsize: 65672
Current children cumulated CPU time (s) 499.07
Current children cumulated vsize (Kb) 67796

[startup+510.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 15500 0 0 0 50821 83 0 0 25 0 1 0 1855720593 68362240 15303 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 16690 15303 145 145 0 16545 0
[pid=21623] vsize: 66760
Current children cumulated CPU time (s) 509.05
Current children cumulated vsize (Kb) 68884

[startup+520.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 15807 0 0 0 51816 85 0 0 25 0 1 0 1855720593 69632000 15610 4294967295 134512640 135094434 3221224448 3221223040 134557512 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 17000 15610 145 145 0 16855 0
[pid=21623] vsize: 68000
Current children cumulated CPU time (s) 519.02
Current children cumulated vsize (Kb) 70124

[startup+530.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) T 21619 21619 20115 0 -1 0 16605 0 0 0 52802 91 0 0 25 0 1 0 1855720593 72855552 16408 4294967295 134512640 135094434 3221224448 3221222828 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/21623/statm): 17787 16408 145 145 0 17642 0
[pid=21623] vsize: 71148
Current children cumulated CPU time (s) 528.94
Current children cumulated vsize (Kb) 73272

[startup+540.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 17308 0 0 0 53791 95 0 0 25 0 1 0 1855720593 76238848 17111 4294967295 134512640 135094434 3221224448 3221222912 134781066 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 18613 17111 145 145 0 18468 0
[pid=21623] vsize: 74452
Current children cumulated CPU time (s) 538.87
Current children cumulated vsize (Kb) 76576

[startup+550.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 17442 0 0 0 54789 96 0 0 25 0 1 0 1855720593 76779520 17245 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 18745 17245 145 145 0 18600 0
[pid=21623] vsize: 74980
Current children cumulated CPU time (s) 548.86
Current children cumulated vsize (Kb) 77104

[startup+560.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 17651 0 0 0 55785 98 0 0 25 0 1 0 1855720593 77627392 17454 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 18952 17454 145 145 0 18807 0
[pid=21623] vsize: 75808
Current children cumulated CPU time (s) 558.84
Current children cumulated vsize (Kb) 77932

[startup+570.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 17912 0 0 0 56782 99 0 0 25 0 1 0 1855720593 78708736 17715 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 19216 17715 145 145 0 19071 0
[pid=21623] vsize: 76864
Current children cumulated CPU time (s) 568.82
Current children cumulated vsize (Kb) 78988

[startup+580.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 18337 0 0 0 57775 103 0 0 25 0 1 0 1855720593 80437248 18140 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 19638 18140 145 145 0 19493 0
[pid=21623] vsize: 78552
Current children cumulated CPU time (s) 578.79
Current children cumulated vsize (Kb) 80676

[startup+590.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 18475 0 0 0 58773 103 0 0 25 0 1 0 1855720593 80990208 18278 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 19773 18278 145 145 0 19628 0
[pid=21623] vsize: 79092
Current children cumulated CPU time (s) 588.77
Current children cumulated vsize (Kb) 81216

[startup+600.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 18715 0 0 0 59769 105 0 0 25 0 1 0 1855720593 81956864 18518 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 20009 18518 145 145 0 19864 0
[pid=21623] vsize: 80036
Current children cumulated CPU time (s) 598.75
Current children cumulated vsize (Kb) 82160

[startup+610.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 18859 0 0 0 60766 106 0 0 25 0 1 0 1855720593 82530304 18662 4294967295 134512640 135094434 3221224448 3221223104 134557829 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 20149 18662 145 145 0 20004 0
[pid=21623] vsize: 80596
Current children cumulated CPU time (s) 608.73
Current children cumulated vsize (Kb) 82720

[startup+620.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 19103 0 0 0 61762 107 0 0 25 0 1 0 1855720593 83488768 18906 4294967295 134512640 135094434 3221224448 3221223040 134552168 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 20383 18906 145 145 0 20238 0
[pid=21623] vsize: 81532
Current children cumulated CPU time (s) 618.7
Current children cumulated vsize (Kb) 83656

[startup+630.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 19530 0 0 0 62754 111 0 0 25 0 1 0 1855720593 85229568 19333 4294967295 134512640 135094434 3221224448 3221223040 134557263 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 20808 19333 145 145 0 20663 0
[pid=21623] vsize: 83232
Current children cumulated CPU time (s) 628.66
Current children cumulated vsize (Kb) 85356

[startup+640.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 19855 0 0 0 63747 114 0 0 25 0 1 0 1855720593 86544384 19658 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21623/statm): 21129 19658 145 145 0 20984 0
[pid=21623] vsize: 84516
Current children cumulated CPU time (s) 638.62
Current children cumulated vsize (Kb) 86640

[startup+650.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 20183 0 0 0 64740 117 0 0 25 0 1 0 1855720593 87859200 19986 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21623/statm): 21450 19986 145 145 0 21305 0
[pid=21623] vsize: 85800
Current children cumulated CPU time (s) 648.58
Current children cumulated vsize (Kb) 87924

[startup+660.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 20452 0 0 0 65734 119 0 0 25 0 1 0 1855720593 88932352 20255 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 21712 20255 145 145 0 21567 0
[pid=21623] vsize: 86848
Current children cumulated CPU time (s) 658.54
Current children cumulated vsize (Kb) 88972

[startup+670.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21037 0 0 0 66731 122 0 0 25 0 1 0 1855720593 90710016 20675 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 22146 20675 145 145 0 22001 0
[pid=21623] vsize: 88584
Current children cumulated CPU time (s) 668.54
Current children cumulated vsize (Kb) 90708

[startup+680.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21037 0 0 0 67731 122 0 0 25 0 1 0 1855720593 90710016 20675 4294967295 134512640 135094434 3221224448 3221223072 134557660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 22146 20675 145 145 0 22001 0
[pid=21623] vsize: 88584
Current children cumulated CPU time (s) 678.54
Current children cumulated vsize (Kb) 90708

[startup+690.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21037 0 0 0 68731 122 0 0 25 0 1 0 1855720593 90710016 20675 4294967295 134512640 135094434 3221224448 3221223104 134557964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 22146 20675 145 145 0 22001 0
[pid=21623] vsize: 88584
Current children cumulated CPU time (s) 688.54
Current children cumulated vsize (Kb) 90708

[startup+700.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21037 0 0 0 69731 122 0 0 25 0 1 0 1855720593 90710016 20675 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 22146 20675 145 145 0 22001 0
[pid=21623] vsize: 88584
Current children cumulated CPU time (s) 698.54
Current children cumulated vsize (Kb) 90708

[startup+710.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21037 0 0 0 70731 122 0 0 25 0 1 0 1855720593 90710016 20675 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 22146 20675 145 145 0 22001 0
[pid=21623] vsize: 88584
Current children cumulated CPU time (s) 708.54
Current children cumulated vsize (Kb) 90708

[startup+720.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21037 0 0 0 71732 122 0 0 25 0 1 0 1855720593 90710016 20675 4294967295 134512640 135094434 3221224448 3221223104 134558002 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 22146 20675 145 145 0 22001 0
[pid=21623] vsize: 88584
Current children cumulated CPU time (s) 718.55
Current children cumulated vsize (Kb) 90708

[startup+730.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21037 0 0 0 72732 122 0 0 25 0 1 0 1855720593 90710016 20675 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 22146 20675 145 145 0 22001 0
[pid=21623] vsize: 88584
Current children cumulated CPU time (s) 728.55
Current children cumulated vsize (Kb) 90708

[startup+740.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21037 0 0 0 73732 122 0 0 25 0 1 0 1855720593 90710016 20675 4294967295 134512640 135094434 3221224448 3221223072 134557714 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 22146 20675 145 145 0 22001 0
[pid=21623] vsize: 88584
Current children cumulated CPU time (s) 738.55
Current children cumulated vsize (Kb) 90708

[startup+750.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21037 0 0 0 74732 122 0 0 25 0 1 0 1855720593 90710016 20675 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 22146 20675 145 145 0 22001 0
[pid=21623] vsize: 88584
Current children cumulated CPU time (s) 748.55
Current children cumulated vsize (Kb) 90708

[startup+760.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21037 0 0 0 75732 122 0 0 25 0 1 0 1855720593 90710016 20675 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 22146 20675 145 145 0 22001 0
[pid=21623] vsize: 88584
Current children cumulated CPU time (s) 758.55
Current children cumulated vsize (Kb) 90708

[startup+770.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21037 0 0 0 76733 122 0 0 25 0 1 0 1855720593 90710016 20675 4294967295 134512640 135094434 3221224448 3221223104 134558016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 22146 20675 145 145 0 22001 0
[pid=21623] vsize: 88584
Current children cumulated CPU time (s) 768.56
Current children cumulated vsize (Kb) 90708

[startup+780.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21037 0 0 0 77733 122 0 0 25 0 1 0 1855720593 90710016 20675 4294967295 134512640 135094434 3221224448 3221223080 134557561 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 22146 20675 145 145 0 22001 0
[pid=21623] vsize: 88584
Current children cumulated CPU time (s) 778.56
Current children cumulated vsize (Kb) 90708

[startup+790.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21037 0 0 0 78733 122 0 0 25 0 1 0 1855720593 90710016 20675 4294967295 134512640 135094434 3221224448 3221223104 134558013 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 22146 20675 145 145 0 22001 0
[pid=21623] vsize: 88584
Current children cumulated CPU time (s) 788.56
Current children cumulated vsize (Kb) 90708

[startup+800.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21037 0 0 0 79733 122 0 0 25 0 1 0 1855720593 90710016 20675 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 22146 20675 145 145 0 22001 0
[pid=21623] vsize: 88584
Current children cumulated CPU time (s) 798.56
Current children cumulated vsize (Kb) 90708

[startup+810.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21038 0 0 0 80734 122 0 0 25 0 1 0 1855720593 90710016 20676 4294967295 134512640 135094434 3221224448 3221223040 134556812 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 22146 20676 145 145 0 22001 0
[pid=21623] vsize: 88584
Current children cumulated CPU time (s) 808.57
Current children cumulated vsize (Kb) 90708

[startup+820.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21038 0 0 0 81734 122 0 0 25 0 1 0 1855720593 90710016 20676 4294967295 134512640 135094434 3221224448 3221223072 134557728 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 22146 20676 145 145 0 22001 0
[pid=21623] vsize: 88584
Current children cumulated CPU time (s) 818.57
Current children cumulated vsize (Kb) 90708

[startup+830.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21041 0 0 0 82734 122 0 0 25 0 1 0 1855720593 90710016 20679 4294967295 134512640 135094434 3221224448 3221223104 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 22146 20679 145 145 0 22001 0
[pid=21623] vsize: 88584
Current children cumulated CPU time (s) 828.57
Current children cumulated vsize (Kb) 90708

[startup+840.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21041 0 0 0 83734 122 0 0 25 0 1 0 1855720593 90710016 20679 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 22146 20679 145 145 0 22001 0
[pid=21623] vsize: 88584
Current children cumulated CPU time (s) 838.57
Current children cumulated vsize (Kb) 90708

[startup+850.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21041 0 0 0 84734 122 0 0 25 0 1 0 1855720593 90710016 20679 4294967295 134512640 135094434 3221224448 3221223060 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 22146 20679 145 145 0 22001 0
[pid=21623] vsize: 88584
Current children cumulated CPU time (s) 848.57
Current children cumulated vsize (Kb) 90708

[startup+860.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21041 0 0 0 85735 122 0 0 25 0 1 0 1855720593 90710016 20679 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 22146 20679 145 145 0 22001 0
[pid=21623] vsize: 88584
Current children cumulated CPU time (s) 858.58
Current children cumulated vsize (Kb) 90708

[startup+870.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21041 0 0 0 86735 122 0 0 25 0 1 0 1855720593 90710016 20679 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 22146 20679 145 145 0 22001 0
[pid=21623] vsize: 88584
Current children cumulated CPU time (s) 868.58
Current children cumulated vsize (Kb) 90708

[startup+880.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21041 0 0 0 87735 122 0 0 25 0 1 0 1855720593 90710016 20679 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 22146 20679 145 145 0 22001 0
[pid=21623] vsize: 88584
Current children cumulated CPU time (s) 878.58
Current children cumulated vsize (Kb) 90708

[startup+890.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21041 0 0 0 88736 122 0 0 25 0 1 0 1855720593 90710016 20679 4294967295 134512640 135094434 3221224448 3221223136 134554788 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 22146 20679 145 145 0 22001 0
[pid=21623] vsize: 88584
Current children cumulated CPU time (s) 888.59
Current children cumulated vsize (Kb) 90708

[startup+900.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21041 0 0 0 89736 122 0 0 25 0 1 0 1855720593 90710016 20679 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 22146 20679 145 145 0 22001 0
[pid=21623] vsize: 88584
Current children cumulated CPU time (s) 898.59
Current children cumulated vsize (Kb) 90708

[startup+910.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21041 0 0 0 90736 122 0 0 25 0 1 0 1855720593 90710016 20679 4294967295 134512640 135094434 3221224448 3221223104 134558004 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 22146 20679 145 145 0 22001 0
[pid=21623] vsize: 88584
Current children cumulated CPU time (s) 908.59
Current children cumulated vsize (Kb) 90708

[startup+920.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21042 0 0 0 91736 122 0 0 25 0 1 0 1855720593 90710016 20680 4294967295 134512640 135094434 3221224448 3221223072 134557696 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 22146 20680 145 145 0 22001 0
[pid=21623] vsize: 88584
Current children cumulated CPU time (s) 918.59
Current children cumulated vsize (Kb) 90708

[startup+930.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21042 0 0 0 92736 122 0 0 25 0 1 0 1855720593 90710016 20680 4294967295 134512640 135094434 3221224448 3221223072 134557650 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 22146 20680 145 145 0 22001 0
[pid=21623] vsize: 88584
Current children cumulated CPU time (s) 928.59
Current children cumulated vsize (Kb) 90708

[startup+940.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21042 0 0 0 93736 122 0 0 25 0 1 0 1855720593 90710016 20680 4294967295 134512640 135094434 3221224448 3221223084 134557639 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 22146 20680 145 145 0 22001 0
[pid=21623] vsize: 88584
Current children cumulated CPU time (s) 938.59
Current children cumulated vsize (Kb) 90708

[startup+950.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21042 0 0 0 94737 122 0 0 25 0 1 0 1855720593 90710016 20680 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 22146 20680 145 145 0 22001 0
[pid=21623] vsize: 88584
Current children cumulated CPU time (s) 948.6
Current children cumulated vsize (Kb) 90708

[startup+960.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21042 0 0 0 95737 122 0 0 25 0 1 0 1855720593 90710016 20680 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 22146 20680 145 145 0 22001 0
[pid=21623] vsize: 88584
Current children cumulated CPU time (s) 958.6
Current children cumulated vsize (Kb) 90708

[startup+970.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21042 0 0 0 96737 122 0 0 25 0 1 0 1855720593 90710016 20680 4294967295 134512640 135094434 3221224448 3221223104 134558411 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 22146 20680 145 145 0 22001 0
[pid=21623] vsize: 88584
Current children cumulated CPU time (s) 968.6
Current children cumulated vsize (Kb) 90708

[startup+980.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21042 0 0 0 97737 122 0 0 25 0 1 0 1855720593 90710016 20680 4294967295 134512640 135094434 3221224448 3221223088 134558269 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 22146 20680 145 145 0 22001 0
[pid=21623] vsize: 88584
Current children cumulated CPU time (s) 978.6
Current children cumulated vsize (Kb) 90708

[startup+990.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21042 0 0 0 98737 122 0 0 25 0 1 0 1855720593 90710016 20680 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 22146 20680 145 145 0 22001 0
[pid=21623] vsize: 88584
Current children cumulated CPU time (s) 988.6
Current children cumulated vsize (Kb) 90708

[startup+1000.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21043 0 0 0 99738 122 0 0 25 0 1 0 1855720593 90710016 20681 4294967295 134512640 135094434 3221224448 3221223072 134562057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 22146 20681 145 145 0 22001 0
[pid=21623] vsize: 88584
Current children cumulated CPU time (s) 998.61
Current children cumulated vsize (Kb) 90708

[startup+1010.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21043 0 0 0 100738 122 0 0 25 0 1 0 1855720593 90710016 20681 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 22146 20681 145 145 0 22001 0
[pid=21623] vsize: 88584
Current children cumulated CPU time (s) 1008.61
Current children cumulated vsize (Kb) 90708

[startup+1020.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21043 0 0 0 101738 122 0 0 25 0 1 0 1855720593 90710016 20681 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 22146 20681 145 145 0 22001 0
[pid=21623] vsize: 88584
Current children cumulated CPU time (s) 1018.61
Current children cumulated vsize (Kb) 90708

[startup+1030.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21043 0 0 0 102738 122 0 0 25 0 1 0 1855720593 90710016 20681 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 22146 20681 145 145 0 22001 0
[pid=21623] vsize: 88584
Current children cumulated CPU time (s) 1028.61
Current children cumulated vsize (Kb) 90708

[startup+1040.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21043 0 0 0 103739 122 0 0 25 0 1 0 1855720593 90710016 20681 4294967295 134512640 135094434 3221224448 3221223104 134557964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 22146 20681 145 145 0 22001 0
[pid=21623] vsize: 88584
Current children cumulated CPU time (s) 1038.62
Current children cumulated vsize (Kb) 90708

[startup+1050.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21043 0 0 0 104739 122 0 0 25 0 1 0 1855720593 90710016 20681 4294967295 134512640 135094434 3221224448 3221223104 134557875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 22146 20681 145 145 0 22001 0
[pid=21623] vsize: 88584
Current children cumulated CPU time (s) 1048.62
Current children cumulated vsize (Kb) 90708

[startup+1060.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21043 0 0 0 105739 122 0 0 25 0 1 0 1855720593 90710016 20681 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 22146 20681 145 145 0 22001 0
[pid=21623] vsize: 88584
Current children cumulated CPU time (s) 1058.62
Current children cumulated vsize (Kb) 90708

[startup+1070.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21043 0 0 0 106739 122 0 0 25 0 1 0 1855720593 90710016 20681 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 22146 20681 145 145 0 22001 0
[pid=21623] vsize: 88584
Current children cumulated CPU time (s) 1068.62
Current children cumulated vsize (Kb) 90708

[startup+1080.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21043 0 0 0 107740 122 0 0 25 0 1 0 1855720593 90710016 20681 4294967295 134512640 135094434 3221224448 3221223104 134557860 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 22146 20681 145 145 0 22001 0
[pid=21623] vsize: 88584
Current children cumulated CPU time (s) 1078.63
Current children cumulated vsize (Kb) 90708

[startup+1090.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21043 0 0 0 108740 122 0 0 25 0 1 0 1855720593 90710016 20681 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 22146 20681 145 145 0 22001 0
[pid=21623] vsize: 88584
Current children cumulated CPU time (s) 1088.63
Current children cumulated vsize (Kb) 90708

[startup+1100.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21043 0 0 0 109740 122 0 0 25 0 1 0 1855720593 90710016 20681 4294967295 134512640 135094434 3221224448 3221223104 134558227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 22146 20681 145 145 0 22001 0
[pid=21623] vsize: 88584
Current children cumulated CPU time (s) 1098.63
Current children cumulated vsize (Kb) 90708

[startup+1110.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21043 0 0 0 110740 122 0 0 25 0 1 0 1855720593 90710016 20681 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 22146 20681 145 145 0 22001 0
[pid=21623] vsize: 88584
Current children cumulated CPU time (s) 1108.63
Current children cumulated vsize (Kb) 90708

[startup+1120.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21043 0 0 0 111740 122 0 0 25 0 1 0 1855720593 90710016 20681 4294967295 134512640 135094434 3221224448 3221223072 134557565 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 22146 20681 145 145 0 22001 0
[pid=21623] vsize: 88584
Current children cumulated CPU time (s) 1118.63
Current children cumulated vsize (Kb) 90708

[startup+1130.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21043 0 0 0 112741 122 0 0 25 0 1 0 1855720593 90710016 20681 4294967295 134512640 135094434 3221224448 3221223120 134556073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 22146 20681 145 145 0 22001 0
[pid=21623] vsize: 88584
Current children cumulated CPU time (s) 1128.64
Current children cumulated vsize (Kb) 90708

[startup+1140.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21043 0 0 0 113741 122 0 0 25 0 1 0 1855720593 90710016 20681 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 22146 20681 145 145 0 22001 0
[pid=21623] vsize: 88584
Current children cumulated CPU time (s) 1138.64
Current children cumulated vsize (Kb) 90708

[startup+1150.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21043 0 0 0 114741 122 0 0 25 0 1 0 1855720593 90710016 20681 4294967295 134512640 135094434 3221224448 3221223104 134561744 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 22146 20681 145 145 0 22001 0
[pid=21623] vsize: 88584
Current children cumulated CPU time (s) 1148.64
Current children cumulated vsize (Kb) 90708

[startup+1160.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21043 0 0 0 115742 122 0 0 25 0 1 0 1855720593 90710016 20681 4294967295 134512640 135094434 3221224448 3221223104 134557950 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 22146 20681 145 145 0 22001 0
[pid=21623] vsize: 88584
Current children cumulated CPU time (s) 1158.65
Current children cumulated vsize (Kb) 90708

[startup+1170.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21045 0 0 0 116742 122 0 0 25 0 1 0 1855720593 90710016 20683 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 22146 20683 145 145 0 22001 0
[pid=21623] vsize: 88584
Current children cumulated CPU time (s) 1168.65
Current children cumulated vsize (Kb) 90708

[startup+1180.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21045 0 0 0 117742 123 0 0 25 0 1 0 1855720593 90710016 20683 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 22146 20683 145 145 0 22001 0
[pid=21623] vsize: 88584
Current children cumulated CPU time (s) 1178.66
Current children cumulated vsize (Kb) 90708

[startup+1190.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21045 0 0 0 118742 123 0 0 25 0 1 0 1855720593 90710016 20683 4294967295 134512640 135094434 3221224448 3221223040 134557494 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 22146 20683 145 145 0 22001 0
[pid=21623] vsize: 88584
Current children cumulated CPU time (s) 1188.66
Current children cumulated vsize (Kb) 90708

[startup+1200.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21045 0 0 0 119742 123 0 0 25 0 1 0 1855720593 90710016 20683 4294967295 134512640 135094434 3221224448 3221223104 134557884 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 22146 20683 145 145 0 22001 0
[pid=21623] vsize: 88584
Current children cumulated CPU time (s) 1198.66
Current children cumulated vsize (Kb) 90708

[startup+1210.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21045 0 0 0 120743 123 0 0 25 0 1 0 1855720593 90710016 20683 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 22146 20683 145 145 0 22001 0
[pid=21623] vsize: 88584
Current children cumulated CPU time (s) 1208.67
Current children cumulated vsize (Kb) 90708



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 21623
Raw data (/proc/21619/stat): 21619 (minisat+_script) S 21618 21619 20115 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1855720588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21619/statm): 531 226 485 147 0 384 0
[pid=21619] vsize: 2124
Raw data (/proc/21623/stat): 21623 (minisat+_64-bit) R 21619 21619 20115 0 -1 0 21045 0 0 0 120743 123 0 0 25 0 1 0 1855720593 90710016 20683 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21623/statm): 22146 20683 145 145 0 22001 0
[pid=21623] vsize: 88584
Current children cumulated CPU time (s) 1208.67
Current children cumulated vsize (Kb) 90708

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

Child status: 10
Real time (s): 1210.14
CPU time (s): 1208.71
CPU user time (s): 1207.44
CPU system time (s): 1.27181
CPU usage (%): 99.8817
Max. virtual memory (cumulated for all children) (Kb): 90708

Verifier Data

ERROR: no interpretation found !