Some explanations

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

General information on the benchmark

Namemps-v2-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-gt2.opb
MD5SUMf1382105ee9fb79777762a53cf6a73c1
Bench Categoryoptimization, medium integers (OPTMEDINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 21166
Optimality of the best value was proved YES
Number of terms in the objective function 304
Biggest coefficient in the objective function 62376
Number of bits for the biggest coefficient in the objective function 16
Sum of the numbers in the objective function 3092598
Number of bits of the sum of numbers in the objective function 22
Biggest number in a constraint 62376
Number of bits of the biggest number in a constraint 16
Biggest sum of numbers in a constraint 3092598
Number of bits of the biggest sum of numbers22
Best result obtained on this benchmarkOPTIMUM FOUND
Best CPU time to get the best result obtained on this benchmark18.2432
Number of variables556
Total number of constraints217
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)26
Number of constraints which are nor clauses,nor cardinality constraints191
Minimum length of a constraint1
Maximum length of a constraint48

Trace number 4526

Launcher Data

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        895804 kB
Buffers:         37512 kB
Cached:          73464 kB
SwapCached:        544 kB
Active:          58028 kB
Inactive:        55372 kB
HighTotal:      131008 kB
HighFree:        55020 kB
LowTotal:       903652 kB
LowFree:        840784 kB
SwapTotal:     2097892 kB
SwapFree:      2096672 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5688 kB
Slab:            19828 kB
Committed_AS:    64316 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-19 18:22:26 (client local time) WITH STATUS 10 IN 1208.15 SECONDS
stats: 2978 7 1208.15 10

Solver Data

c Parsing PB file...
c Converting 180 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ........................................................................................ssssssssss
c ---[ 189]---> BDD-cost:    2
c ---[ 188]---> BDD-cost:    2
c ---[ 187]---> BDD-cost:    2
c ---[ 186]---> BDD-cost:    2
c ---[ 185]---> BDD-cost:    2
c ---[ 184]---> BDD-cost:    2
c ---[ 183]---> BDD-cost:    2
c ---[ 182]---> BDD-cost:    2
c ---[ 157]---> BDD-cost:    3
c ---[ 156]---> BDD-cost:    3
c ---[ 155]---> BDD-cost:    3
c ---[ 154]---> BDD-cost:    3
c ---[ 153]---> BDD-cost:    3
c ---[ 152]---> BDD-cost:    3
c ---[ 151]---> BDD-cost:    3
c ---[ 150]---> BDD-cost:    3
c ---[ 149]---> BDD-cost:    3
c ---[ 148]---> BDD-cost:    3
c ---[ 147]---> BDD-cost:    3
c ---[ 146]---> BDD-cost:    3
c ---[ 141]---> BDD-cost:    3
c ---[ 140]---> BDD-cost:    3
c ---[ 139]---> BDD-cost:    3
c ---[ 138]---> BDD-cost:    3
c ---[ 137]---> BDD-cost:    3
c ---[ 136]---> BDD-cost:    3
c ---[ 135]---> BDD-cost:    3
c ---[ 134]---> BDD-cost:    3
c ---[ 120]---> BDD-cost:    2
c ---[ 119]---> BDD-cost:    2
c ---[ 117]---> BDD-cost:    2
c ---[ 113]---> BDD-cost:    2
c ---[ 112]---> BDD-cost:    2
c ---[ 110]---> BDD-cost:    2
c ---[ 106]---> BDD-cost:    2
c ---[ 105]---> BDD-cost:    2
c ---[ 103]---> BDD-cost:    2
c ---[  99]---> BDD-cost:    2
c ---[  98]---> BDD-cost:    2
c ---[  96]---> BDD-cost:    2
c ---[  92]---> BDD-cost:    2
c ---[  91]---> BDD-cost:    2
c ---[  89]---> BDD-cost:    2
c ---[  85]---> BDD-cost:    2
c ---[  84]---> BDD-cost:    2
c ---[  82]---> BDD-cost:    2
c ---[  78]---> BDD-cost:    2
c ---[  77]---> BDD-cost:    2
c ---[  75]---> BDD-cost:    2
c ---[  71]---> BDD-cost:    2
c ---[  70]---> BDD-cost:    2
c ---[  68]---> BDD-cost:    2
c ---[  64]---> BDD-cost:    2
c ---[  63]---> BDD-cost:    2
c ---[  61]---> BDD-cost:    2
c ---[  57]---> BDD-cost:    2
c ---[  56]---> BDD-cost:    2
c ---[  54]---> BDD-cost:    2
c ---[  50]---> BDD-cost:    2
c ---[  49]---> BDD-cost:    2
c ---[  47]---> BDD-cost:    2
c ---[  43]---> BDD-cost:    2
c ---[  42]---> BDD-cost:    2
c ---[  40]---> BDD-cost:    2
c ---[  37]---> BDD-cost:  107
c ---[  36]---> Sorter-cost:  778     Base: 2 2 2
c ---[  35]---> Sorter-cost:  777     Base: 2 2 2
c ---[  34]---> BDD-cost:   21
c ---[  33]---> BDD-cost:  128
c ---[  32]---> BDD-cost:  183
c ---[  31]---> BDD-cost:   25
c ---[  30]---> Sorter-cost:  379     Base: 2 2 2
c ---[  29]---> BDD-cost:  111
c ---[  28]---> BDD-cost:  128
c ---[  27]---> BDD-cost:  105
c ---[  26]---> Sorter-cost:  778     Base: 2 2 2
c ---[  25]---> BDD-cost:  111
c ---[  24]---> BDD-cost:  105
c ---[  23]---> BDD-cost:   54
c ---[  22]---> BDD-cost:   54
c ---[  21]---> BDD-cost:   21
c ---[  15]---> Adder-cost: 273   maxlim: 12127   bits: 15/14
c ---[   9]---> Sorter-cost: 2085     Base: 2 5 2 2 2
c ---[   8]---> BDD-cost:   76
c ---[   7]---> Sorter-cost: 2550     Base: 2 5 2 2 2
c ---[   6]---> Adder-cost: 223   maxlim: 249   bits: 9/8
c ---[   5]---> BDD-cost:   48
c ---[   4]---> BDD-cost:  114
c ---[   3]---> BDD-cost:   55
c ---[   2]---> Sorter-cost: 2935     Base: 2 5 2 2 2 2
c ---[   1]---> Adder-cost: 212   maxlim: 230   bits: 9/8
c ---[   0]---> BDD-cost:   92
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   30742    79537 |   10247       0        0     nan |  0.000 % |
c |       100 |   30742    79537 |   11271     100      544     5.4 |  0.987 % |
c |       250 |   30742    79537 |   12398     250     2459     9.8 |  0.986 % |
c |       477 |   30742    79537 |   13638     477     3973     8.3 |  0.986 % |
c ==============================================================================
c Found solution: 175459
c ---[   0]---> Sorter-cost:92424     Base: 2 2 2 3 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       637 |  284458   671673 |   94819     637    11349    17.8 |  0.986 % |
c |       737 |  284437   671627 |  104300     735    12835    17.5 |  0.117 % |
c |       887 |  284035   670723 |  114730     880    13845    15.7 |  0.221 % |
c |      1114 |  284035   670723 |  126204    1107    15250    13.8 |  0.221 % |
c |      1451 |  284035   670723 |  138824    1444    17597    12.2 |  0.221 % |
c |      1958 |  282828   667995 |  152706    1939    63559    32.8 |  0.549 % |
c |      2717 |  282661   667617 |  167977    2697   148878    55.2 |  0.596 % |
c |      3856 |  271841   642801 |  184775    3781   190178    50.3 |  3.911 % |
c |      5565 |  267485   632765 |  203252    5455   244772    44.9 |  5.294 % |
c |      8129 |  258374   611785 |  223578    7920   366516    46.3 |  8.175 % |
c |     11974 |  255958   606212 |  245936   11748   726453    61.8 |  8.939 % |
c |     17740 |  250695   594032 |  270529   17444  1194291    68.5 | 10.666 % |
c |     26390 |  249167   590517 |  297582   26068  1851301    71.0 | 11.165 % |
c |     39364 |  243608   577673 |  327340   38951  2440127    62.6 | 12.969 % |
c ==============================================================================
c Found solution: 174126
c ---[   0]---> Sorter-cost:70620     Base: 2 2 2 3 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     57904 |  404098   950841 |  134699   57401  4098734    71.4 | 12.969 % |
c |     58008 |  403639   949827 |  148168   57502  4100867    71.3 | 14.245 % |
c |     58159 |  402994   948375 |  162985   57644  4103732    71.2 | 14.375 % |
c |     58384 |  402994   948375 |  179284   57869  4109174    71.0 | 14.375 % |
c |     58721 |  401268   944466 |  197212   58185  4111678    70.7 | 14.715 % |
c |     59229 |  401268   944466 |  216934   58693  4136023    70.5 | 14.715 % |
c |     59988 |  401268   944466 |  238627   59452  4283010    72.0 | 14.715 % |
c |     61127 |  401110   944098 |  262490   60582  4296313    70.9 | 14.748 % |
c |     62836 |  400965   943764 |  288739   62290  4391753    70.5 | 14.776 % |
c |     65398 |  397076   934924 |  317613   64748  4501421    69.5 | 15.543 % |
c |     69242 |  396305   933196 |  349374   68585  4939320    72.0 | 15.693 % |
c ==============================================================================
c Found solution: 172189
c ---[   0]---> Sorter-cost:69141     Base: 2 2 2 3 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     73398 |  544035  1277084 |  181345   72562  5065701    69.8 | 15.693 % |
c |     73498 |  544035  1277084 |  199479   72662  5068684    69.8 | 16.507 % |
c |     73648 |  544035  1277084 |  219427   72812  5070213    69.6 | 16.507 % |
c |     73873 |  543068  1274852 |  241370   72952  5097260    69.9 | 16.641 % |
c |     74210 |  540987  1270145 |  265507   73257  5099628    69.6 | 16.928 % |
c |     74716 |  540190  1268331 |  292057   73706  5103053    69.2 | 17.043 % |
c |     75475 |  536077  1259024 |  321263   74187  5111911    68.9 | 17.612 % |
c |     76614 |  536077  1259024 |  353390   75326  5156748    68.5 | 17.612 % |
c |     78323 |  530933  1247267 |  388729   76556  5221852    68.2 | 18.328 % |
c ==============================================================================
c Found solution: 165654
c ---[   0]---> Sorter-cost:   12     Base: 2 2 2 3 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     78741 |  531464  1248864 |  177154   76974  5254301    68.3 | 18.328 % |
c |     78842 |  530814  1247415 |  194869   77072  5256580    68.2 | 18.396 % |
c |     78994 |  530399  1246465 |  214356   77218  5264119    68.2 | 18.455 % |
c |     79219 |  530399  1246465 |  235791   77443  5280849    68.2 | 18.455 % |
c |     79556 |  530293  1246228 |  259371   77779  5290167    68.0 | 18.466 % |
c |     80062 |  530239  1246109 |  285308   78283  5319511    68.0 | 18.473 % |
c |     80821 |  530239  1246109 |  313839   79042  5399819    68.3 | 18.473 % |
c |     81960 |  530034  1245656 |  345223   80180  5665661    70.7 | 18.500 % |
c |     83669 |  524072  1232048 |  379745   81399  5764458    70.8 | 19.341 % |
c |     86231 |  522340  1228063 |  417719   83937  5900609    70.3 | 19.584 % |
c ==============================================================================
c Found solution: 165192
c ---[   0]---> Sorter-cost:68242     Base: 2 2 2 3 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     87232 |  675287  1583479 |  225095   84938  6115837    72.0 | 19.584 % |
c |     87332 |  675287  1583479 |  247604   85038  6117351    71.9 | 19.030 % |
c |     87483 |  673704  1579889 |  272364   85180  6121380    71.9 | 19.205 % |
c |     87709 |  673704  1579889 |  299601   85406  6147900    72.0 | 19.205 % |
c |     88046 |  673704  1579889 |  329561   85743  6190662    72.2 | 19.205 % |
c |     88553 |  673704  1579889 |  362517   86250  6204900    71.9 | 19.205 % |
c |     89314 |  673704  1579889 |  398769   87011  6265601    72.0 | 19.205 % |
c |     90456 |  668664  1568463 |  438646   88034  6376824    72.4 | 19.756 % |
c |     92164 |  666346  1563278 |  482511   89724  6660716    74.2 | 20.003 % |
c |     94726 |  666346  1563278 |  530762   92286  7009786    76.0 | 20.003 % |
c |     98570 |  664362  1558830 |  583838   96127  7652673    79.6 | 20.223 % |
c ==============================================================================
c Found solution: 164617
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 3 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     98680 |  664408  1559385 |  221469   96237  7659605    79.6 | 20.223 % |
c |     98781 |  664408  1559385 |  243615   96338  7666260    79.6 | 20.222 % |
c |     98931 |  663882  1558213 |  267977   96478  7669094    79.5 | 20.280 % |
c |     99156 |  663882  1558213 |  294775   96703  7674639    79.4 | 20.280 % |
c |     99494 |  663882  1558213 |  324252   97041  7682075    79.2 | 20.280 % |
c |    100000 |  662711  1555549 |  356678   97537  7702428    79.0 | 20.411 % |
c |    100761 |  658022  1544826 |  392345   98090  7724938    78.8 | 20.924 % |
c |    101902 |  657896  1544545 |  431580   99228  7828742    78.9 | 20.939 % |
c |    103612 |  656006  1540264 |  474738  100809  7919978    78.6 | 21.151 % |
c |    106174 |  653447  1534433 |  522212  103311  8338281    80.7 | 21.441 % |
c |    110018 |  653447  1534433 |  574433  107155  8992194    83.9 | 21.441 % |
c |    115784 |  650518  1527749 |  631876  112772  9214928    81.7 | 21.761 % |
c |    124433 |  650518  1527749 |  695064  121421  9889029    81.4 | 21.761 % |
c ==============================================================================
c Found solution: 163483
c ---[   0]---> Sorter-cost:   12     Base: 2 2 2 3 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    131430 |  646191  1517922 |  215397  128336 10361434    80.7 | 21.761 % |
c |    131530 |  646191  1517922 |  236936  128436 10366789    80.7 | 22.242 % |
c |    131680 |  646026  1517552 |  260630  128583 10382200    80.7 | 22.260 % |
c |    131906 |  646026  1517552 |  286693  128809 10384118    80.6 | 22.260 % |
c |    132243 |  646026  1517552 |  315362  129146 10387012    80.4 | 22.260 % |
c |    132750 |  645201  1515676 |  346899  129631 10391486    80.2 | 22.349 % |
c |    133510 |  642926  1510464 |  381588  130236 10419037    80.0 | 22.602 % |
c |    134650 |  642926  1510464 |  419747  131376 10465729    79.7 | 22.602 % |
c ==============================================================================
c Found solution: 161824
c ---[   0]---> Sorter-cost:   12     Base: 2 2 2 3 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    135225 |  642822  1510228 |  214274  131950 10510329    79.7 | 22.602 % |
c |    135328 |  642822  1510228 |  235701  132053 10515914    79.6 | 22.614 % |
c |    135478 |  642047  1508455 |  259271  132190 10518344    79.6 | 22.694 % |
c |    135703 |  642047  1508455 |  285198  132415 10522658    79.5 | 22.694 % |
c |    136040 |  641491  1507180 |  313718  132743 10524190    79.3 | 22.755 % |
c |    136547 |  641393  1506955 |  345090  133249 10584627    79.4 | 22.766 % |
c |    137306 |  641201  1506523 |  379599  134000 10677526    79.7 | 22.785 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -x_0x2e__0x2e__0x2e_0101_bit0 -x_0x2e__0x2e__0x2e_0101_bit1 -x_0x2e__0x2e__0x2e_0101_bit2 -x_0x2e__0x2e__0x2e_0101_bit3 -x_0x2e__0x2e__0x2e_0201_bit0 -x_0x2e__0x2e__0x2e_0201_bit1 -x_0x2e__0x2e__0x2e_0201_bit2 -x_0x2e__0x2e__0x2e_0201_bit3 -x_0x2e__0x2e__0x2e_0301_bit0 -x_0x2e__0x2e__0x2e_0301_bit1 x_0x2e__0x2e__0x2e_0301_bit2 -x_0x2e__0x2e__0x2e_0301_bit3 -x_0x2e__0x2e__0x2e_0401_bit0 -x_0x2e__0x2e__0x2e_0401_bit1 -x_0x2e__0x2e__0x2e_0401_bit2 -x_0x2e__0x2e__0x2e_0401_bit3 -x_0x2e__0x2e__0x2e_0701_bit0 -x_0x2e__0x2e__0x2e_0701_bit1 -x_0x2e__0x2e__0x2e_0701_bit2 -x_0x2e__0x2e__0x2e_0701_bit3 -x_0x2e__0x2e__0x2e_0801_bit0 -x_0x2e__0x2e__0x2e_0801_bit1 -x_0x2e__0x2e__0x2e_0801_bit2 -x_0x2e__0x2e__0x2e_0801_bit3 x_0x2e__0x2e__0x2e_0901_bit0 -x_0x2e__0x2e__0x2e_0901_bit1 x_0x2e__0x2e__0x2e_0901_bit2 -x_0x2e__0x2e__0x2e_0901_bit3 -x_0x2e__0x2e__0x2e_1001_bit0 -x_0x2e__0x2e__0x2e_1001_bit1 -x_0x2e__0x2e__0x2e_1001_bit2 -x_0x2e__0x2e__0x2e_1001_bit3 -x_0x2e__0x2e__0x2e_0102_bit0 -x_0x2e__0x2e__0x2e_0102_bit1 -x_0x2e__0x2e__0x2e_0102_bit2 -x_0x2e__0x2e__0x2e_0102_bit3 -x_0x2e__0x2e__0x2e_0202_bit0 -x_0x2e__0x2e__0x2e_0202_bit1 -x_0x2e__0x2e__0x2e_0202_bit2 -x_0x2e__0x2e__0x2e_0202_bit3 -x_0x2e__0x2e__0x2e_0302_bit0 -x_0x2e__0x2e__0x2e_0302_bit1 -x_0x2e__0x2e__0x2e_0302_bit2 x_0x2e__0x2e__0x2e_0302_bit3 -x_0x2e__0x2e__0x2e_0402_bit0 -x_0x2e__0x2e__0x2e_0402_bit1 -x_0x2e__0x2e__0x2e_0402_bit2 -x_0x2e__0x2e__0x2e_0402_bit3 -x_0x2e__0x2e__0x2e_0502_bit0 -x_0x2e__0x2e__0x2e_0502_bit1 x_0x2e__0x2e__0x2e_0502_bit2 -x_0x2e__0x2e__0x2e_0502_bit3 -x_0x2e__0x2e__0x2e_0602_bit0 -x_0x2e__0x2e__0x2e_0602_bit1 -x_0x2e__0x2e__0x2e_0602_bit2 -x_0x2e__0x2e__0x2e_0602_bit3 -x_0x2e__0x2e__0x2e_0702_bit0 -x_0x2e__0x2e__0x2e_0702_bit1 -x_0x2e__0x2e__0x2e_0702_bit2 -x_0x2e__0x2e__0x2e_0702_bit3 -x_0x2e__0x2e__0x2e_0802_bit0 -x_0x2e__0x2e__0x2e_0802_bit1 -x_0x2e__0x2e__0x2e_0802_bit2 -x_0x2e__0x2e__0x2e_0802_bit3 -x_0x2e__0x2e__0x2e_0902_bit0 -x_0x2e__0x2e__0x2e_0902_bit1 -x_0x2e__0x2e__0x2e_0902_bit2 -x_0x2e__0x2e__0x2e_0902_bit3 -x_0x2e__0x2e__0x2e_1002_bit0 -x_0x2e__0x2e__0x2e_1002_bit1 -x_0x2e__0x2e__0x2e_1002_bit2 -x_0x2e__0x2e__0x2e_1002_bit3 -x_0x2e__0x2e__0x2e_1102_bit0 x_0x2e__0x2e__0x2e_1102_bit1 -x_0x2e__0x2e__0x2e_1102_bit2 -x_0x2e__0x2e__0x2e_1102_bit3 -x_0x2e__0x2e__0x2e_1202_bit0 -x_0x2e__0x2e__0x2e_1202_bit1 -x_0x2e__0x2e__0x2e_1202_bit2 -x_0x2e__0x2e__0x2e_1202_bit3 x_0x2e__0x2e__0x2e_0103_bit0 -x_0x2e__0x2e__0x2e_0103_bit1 -x_0x2e__0x2e__0x2e_0103_bit2 -x_0x2e__0x2e__0x2e_0103_bit3 x_0x2e__0x2e__0x2e_0203_bit0 -x_0x2e__0x2e__0x2e_0203_bit1 x_0x2e__0x2e__0x2e_0203_bit2 -x_0x2e__0x2e__0x2e_0203_bit3 -x_0x2e__0x2e__0x2e_0303_bit0 x_0x2e__0x2e__0x2e_0303_bit1 -x_0x2e__0x2e__0x2e_0303_bit2 -x_0x2e__0x2e__0x2e_0303_bit3 x_0x2e__0x2e__0x2e_0403_bit0 -x_0x2e__0x2e__0x2e_0403_bit1 -x_0x2e__0x2e__0x2e_0403_bit2 -x_0x2e__0x2e__0x2e_0403_bit3 -x_0x2e__0x2e__0x2e_0503_bit0 -x_0x2e__0x2e__0x2e_0503_bit1 -x_0x2e__0x2e__0x2e_0503_bit2 -x_0x2e__0x2e__0x2e_0503_bit3 -x_0x2e__0x2e__0x2e_0603_bit0 -x_0x2e__0x2e__0x2e_0603_bit1 -x_0x2e__0x2e__0x2e_0603_bit2 -x_0x2e__0x2e__0x2e_0603_bit3 x_0x2e__0x2e__0x2e_0703_bit0 -x_0x2e__0x2e__0x2e_0703_bit1 -x_0x2e__0x2e__0x2e_0703_bit2 -x_0x2e__0x2e__0x2e_0703_bit3 x_0x2e__0x2e__0x2e_0803_bit0 -x_0x2e__0x2e__0x2e_0803_bit1 -x_0x2e__0x2e__0x2e_0803_bit2 -x_0x2e__0x2e__0x2e_0803_bit3 -x_0x2e__0x2e__0x2e_0903_bit0 x_0x2e__0x2e__0x2e_0903_bit1 -x_0x2e__0x2e__0x2e_0903_bit2 -x_0x2e__0x2e__0x2e_0903_bit3 x_0x2e__0x2e__0x2e_1003_bit0 -x_0x2e__0x2e__0x2e_1003_bit1 -x_0x2e__0x2e__0x2e_1003_bit2 -x_0x2e__0x2e__0x2e_1003_bit3 -x_0x2e__0x2e__0x2e_1103_bit0 -x_0x2e__0x2e__0x2e_1103_bit1 -x_0x2e__0x2e__0x2e_1103_bit2 -x_0x2e__0x2e__0x2e_1103_bit3 -x_0x2e__0x2e__0x2e_1203_bit0 -x_0x2e__0x2e__0x2e_1203_bit1 -x_0x2e__0x2e__0x2e_1203_bit2 -x_0x2e__0x2e__0x2e_1203_bit3 -x_0x2e__0x2e__0x2e_0104_bit0 -x_0x2e__0x2e__0x2e_0204_bit0 -x_0x2e__0x2e__0x2e_0304_bit0 -x_0x2e__0x2e__0x2e_0404_bit0 -x_0x2e__0x2e__0x2e_0504_bit0 -x_0x2e__0x2e__0x2e_0604_bit0 -x_0x2e__0x2e__0x2e_0704_bit0 -x_0x2e__0x2e__0x2e_0804_bit0 -x_0x2e__0x2e__0x2e_0904_bit0 -x_0x2e__0x2e__0x2e_1004_bit0 -x_0x2e__0x2e__0x2e_1104_bit0 x_0x2e__0x2e__0x2e_1204_bit0 -x_0x2e__0x2e__0x2e_0105_bit0 -x_0x2e__0x2e__0x2e_0105_bit1 -x_0x2e__0x2e__0x2e_0105_bit2 -x_0x2e__0x2e__0x2e_0205_bit0 -x_0x2e__0x2e__0x2e_0205_bit1 -x_0x2e__0x2e__0x2e_0205_bit2 -x_0x2e__0x2e__0x2e_0305_bit0 -x_0x2e__0x2e__0x2e_0305_bit1 -x_0x2e__0x2e__0x2e_0305_bit2 -x_0x2e__0x2e__0x2e_0405_bit0 -x_0x2e__0x2e__0x2e_0405_bit1 -x_0x2e__0x2e__0x2e_0405_bit2 x_0x2e__0x2e__0x2e_0505_bit0 -x_0x2e__0x2e__0x2e_0505_bit1 -x_0x2e__0x2e__0x2e_0505_bit2 x_0x2e__0x2e__0x2e_0605_bit0 -x_0x2e__0x2e__0x2e_0605_bit1 -x_0x2e__0x2e__0x2e_0605_bit2 -x_0x2e__0x2e__0x2e_0705_bit0 -x_0x2e__0x2e__0x2e_0705_bit1 -x_0x2e__0x2e__0x2e_0705_bit2 -x_0x2e__0x2e__0x2e_0805_bit0 -x_0x2e__0x2e__0x2e_0805_bit1 -x_0x2e__0x2e__0x2e_0805_bit2 -x_0x2e__0x2e__0x2e_0905_bit0 -x_0x2e__0x2e__0x2e_0905_bit1 -x_0x2e__0x2e__0x2e_0905_bit2 -x_0x2e__0x2e__0x2e_1005_bit0 -x_0x2e__0x2e__0x2e_1005_bit1 -x_0x2e__0x2e__0x2e_1005_bit2 x_0x2e__0x2e__0x2e_1105_bit0 -x_0x2e__0x2e__0x2e_1105_bit1 -x_0x2e__0x2e__0x2e_1105_bit2 x_0x2e__0x2e__0x2e_1205_bit0 -x_0x2e__0x2e__0x2e_1205_bit1 -x_0x2e__0x2e__0x2e_1205_bit2 -x_0x2e__0x2e__0x2e_0106_bit0 -x_0x2e__0x2e__0x2e_0106_bit1 -x_0x2e__0x2e__0x2e_0106_bit2 -x_0x2e__0x2e__0x2e_0106_bit3 -x_0x2e__0x2e__0x2e_0206_bit0 -x_0x2e__0x2e__0x2e_0206_bit1 -x_0x2e__0x2e__0x2e_0206_bit2 -x_0x2e__0x2e__0x2e_0206_bit3 -x_0x2e__0x2e__0x2e_0306_bit0 -x_0x2e__0x2e__0x2e_0306_bit1 x_0x2e__0x2e__0x2e_0306_bit2 -x_0x2e__0x2e__0x2e_0306_bit3 -x_0x2e__0x2e__0x2e_0406_bit0 -x_0x2e__0x2e__0x2e_0406_bit1 -x_0x2e__0x2e__0x2e_0406_bit2 -x_0x2e__0x2e__0x2e_0406_bit3 -x_0x2e__0x2e__0x2e_0506_bit0 -x_0x2e__0x2e__0x2e_0506_bit1 -x_0x2e__0x2e__0x2e_0506_bit2 -x_0x2e__0x2e__0x2e_0506_bit3 -x_0x2e__0x2e__0x2e_0606_bit0 -x_0x2e__0x2e__0x2e_0606_bit1 -x_0x2e__0x2e__0x2e_0606_bit2 -x_0x2e__0x2e__0x2e_0606_bit3 -x_0x2e__0x2e__0x2e_0706_bit0 -x_0x2e__0x2e__0x2e_0706_bit1 -x_0x2e__0x2e__0x2e_0706_bit2 -x_0x2e__0x2e__0x2e_0706_bit3 -x_0x2e__0x2e__0x2e_0806_bit0 -x_0x2e__0x2e__0x2e_0806_bit1 -x_0x2e__0x2e__0x2e_0806_bit2 -x_0x2e__0x2e__0x2e_0806_bit3 -x_0x2e__0x2e__0x2e_0906_bit0 -x_0x2e__0x2e__0x2e_0906_bit1 x_0x2e__0x2e__0x2e_0906_bit2 -x_0x2e__0x2e__0x2e_0906_bit3 -x_0x2e__0x2e__0x2e_1006_bit0 -x_0x2e__0x2e__0x2e_1006_bit1 -x_0x2e__0x2e__0x2e_1006_bit2 -x_0x2e__0x2e__0x2e_1006_bit3 -x_0x2e__0x2e__0x2e_1106_bit0 -x_0x2e__0x2e__0x2e_1106_bit1 -x_0x2e__0x2e__0x2e_1106_bit2 -x_0x2e__0x2e__0x2e_1106_bit3 -x_0x2e__0x2e__0x2e_1206_bit0 -x_0x2e__0x2e__0x2e_1206_bit1 -x_0x2e__0x2e__0x2e_1206_bit2 -x_0x2e__0x2e__0x2e_1206_bit3 x_0x2e__0x2e__0x2e_0507_bit0 -x_0x2e__0x2e__0x2e_0507_bit1 -x_0x2e__0x2e__0x2e_0507_bit2 x_0x2e__0x2e__0x2e_0607_bit0 -x_0x2e__0x2e__0x2e_0607_bit1 -x_0x2e__0x2e__0x2e_0607_bit2 x_0x2e__0x2e__0x2e_1107_bit0 -x_0x2e__0x2e__0x2e_1107_bit1 -x_0x2e__0x2e__0x2e_1107_bit2 x_0x2e__0x2e__0x2e_1207_bit0 -x_0x2e__0x2e__0x2e_1207_bit1 -x_0x2e__0x2e__0x2e_1207_bit2 -x_0x2e__0x2e__0x2e_0108_bit0 -x_0x2e__0x2e__0x2e_0108_bit1 -x_0x2e__0x2e__0x2e_0108_bit2 -x_0x2e__0x2e__0x2e_0108_bit3 -x_0x2e__0x2e__0x2e_0208_bit0 -x_0x2e__0x2e__0x2e_0208_bit1 -x_0x2e__0x2e__0x2e_0208_bit2 -x_0x2e__0x2e__0x2e_0208_bit3 -x_0x2e__0x2e__0x2e_0308_bit0 x_0x2e__0x2e__0x2e_0308_bit1 -x_0x2e__0x2e__0x2e_0308_bit2 x_0x2e__0x2e__0x2e_0308_bit3 -x_0x2e__0x2e__0x2e_0408_bit0 -x_0x2e__0x2e__0x2e_0408_bit1 -x_0x2e__0x2e__0x2e_0408_bit2 -x_0x2e__0x2e__0x2e_0408_bit3 -x_0x2e__0x2e__0x2e_0708_bit0 -x_0x2e__0x2e__0x2e_0708_bit1 -x_0x2e__0x2e__0x2e_0708_bit2 -x_0x2e__0x2e__0x2e_0708_bit3 -x_0x2e__0x2e__0x2e_0808_bit0 -x_0x2e__0x2e__0x2e_0808_bit1 -x_0x2e__0x2e__0x2e_0808_bit2 -x_0x2e__0x2e__0x2e_0808_bit3 -x_0x2e__0x2e__0x2e_0908_bit0 x_0x2e__0x2e__0x2e_0908_bit1 -x_0x2e__0x2e__0x2e_0908_bit2 -x_0x2e__0x2e__0x2e_0908_bit3 -x_0x2e__0x2e__0x2e_1008_bit0 -x_0x2e__0x2e__0x2e_1008_bit1 -x_0x2e__0x2e__0x2e_1008_bit2 -x_0x2e__0x2e__0x2e_1008_bit3 -x_0x2e__0x2e__0x2e_0109_bit0 -x_0x2e__0x2e__0x2e_0109_bit1 -x_0x2e__0x2e__0x2e_0109_bit2 -x_0x2e__0x2e__0x2e_0209_bit0 -x_0x2e__0x2e__0x2e_0209_bit1 -x_0x2e__0x2e__0x2e_0209_bit2 -x_0x2e__0x2e__0x2e_0309_bit0 -x_0x2e__0x2e__0x2e_0309_bit1 -x_0x2e__0x2e__0x2e_0309_bit2 -x_0x2e__0x2e__0x2e_0409_bit0 -x_0x2e__0x2e__0x2e_0409_bit1 -x_0x2e__0x2e__0x2e_0409_bit2 -x_0x2e__0x2e__0x2e_0509_bit0 -x_0x2e__0x2e__0x2e_0509_bit1 -x_0x2e__0x2e__0x2e_0509_bit2 x_0x2e__0x2e__0x2e_0609_bit0 x_0x2e__0x2e__0x2e_0609_bit1 -x_0x2e__0x2e__0x2e_0609_bit2 -x_0x2e__0x2e__0x2e_0709_bit0 -x_0x2e__0x2e__0x2e_0709_bit1 -x_0x2e__0x2e__0x2e_0709_bit2 x_0x2e__0x2e__0x2e_0809_bit0 -x_0x2e__0x2e__0x2e_0809_bit1 -x_0x2e__0x2e__0x2e_0809_bit2 -x_0x2e__0x2e__0x2e_0909_bit0 -x_0x2e__0x2e__0x2e_0909_bit1 -x_0x2e__0x2e__0x2e_0909_bit2 x_0x2e__0x2e__0x2e_1009_bit0 -x_0x2e__0x2e__0x2e_1009_bit1 -x_0x2e__0x2e__0x2e_1009_bit2 -x_0x2e__0x2e__0x2e_1109_bit0 -x_0x2e__0x2e__0x2e_1109_bit1 -x_0x2e__0x2e__0x2e_1109_bit2 -x_0x2e__0x2e__0x2e_1209_bit0 -x_0x2e__0x2e__0x2e_1209_bit1 -x_0x2e__0x2e__0x2e_1209_bit2 -x_0x2e__0x2e__0x2e_0110_bit0 -x_0x2e__0x2e__0x2e_0110_bit1 x_0x2e__0x2e__0x2e_0110_bit2 -x_0x2e__0x2e__0x2e_0111_bit0 -x_0x2e__0x2e__0x2e_0111_bit1 -x_0x2e__0x2e__0x2e_0111_bit2 -x_0x2e__0x2e__0x2e_0112_bit0 -x_0x2e__0x2e__0x2e_0112_bit1 -x_0x2e__0x2e__0x2e_0112_bit2 -x_0x2e__0x2e__0x2e_0112_bit3 x_0x2e__0x2e__0x2e_0113_bit0 -x_0x2e__0x2e__0x2e_0113_bit1 -x_0x2e__0x2e__0x2e_0113_bit2 -x_0x2e__0x2e__0x2e_0114_bit0 -x_0x2e__0x2e__0x2e_0114_bit1 -x_0x2e__0x2e__0x2e_0114_bit2 -x_0x2e__0x2e__0x2e_0115_bit0 x_0x2e__0x2e__0x2e_0115_bit1 x_0x2e__0x2e__0x2e_0116_bit0 -x_0x2e__0x2e__0x2e_0116_bit1 -x_0x2e__0x2e__0x2e_0117_bit0 -x_0x2e__0x2e__0x2e_0210_bit0 -x_0x2e__0x2e__0x2e_0210_bit1 -x_0x2e__0x2e__0x2e_0210_bit2 -x_0x2e__0x2e__0x2e_0211_bit0 -x_0x2e__0x2e__0x2e_0211_bit1 -x_0x2e__0x2e__0x2e_0211_bit2 -x_0x2e__0x2e__0x2e_0212_bit0 -x_0x2e__0x2e__0x2e_0212_bit1 -x_0x2e__0x2e__0x2e_0212_bit2 -x_0x2e__0x2e__0x2e_0212_bit3 -x_0x2e__0x2e__0x2e_0213_bit0 -x_0x2e__0x2e__0x2e_0213_bit1 -x_0x2e__0x2e__0x2e_0213_bit2 -x_0x2e__0x2e__0x2e_0214_bit0 -x_0x2e__0x2e__0x2e_0214_bit1 -x_0x2e__0x2e__0x2e_0214_bit2 -x_0x2e__0x2e__0x2e_0215_bit0 -x_0x2e__0x2e__0x2e_0215_bit1 -x_0x2e__0x2e__0x2e_0216_bit0 -x_0x2e__0x2e__0x2e_0216_bit1 -x_0x2e__0x2e__0x2e_0217_bit0 -x_0x2e__0x2e__0x2e_0310_bit0 -x_0x2e__0x2e__0x2e_0310_bit1 -x_0x2e__0x2e__0x2e_0310_bit2 -x_0x2e__0x2e__0x2e_0311_bit0 -x_0x2e__0x2e__0x2e_0311_bit1 -x_0x2e__0x2e__0x2e_0311_bit2 -x_0x2e__0x2e__0x2e_0312_bit0 -x_0x2e__0x2e__0x2e_0312_bit1 -x_0x2e__0x2e__0x2e_0312_bit2 -x_0x2e__0x2e__0x2e_0312_bit3 -x_0x2e__0x2e__0x2e_0313_bit0 -x_0x2e__0x2e__0x2e_0313_bit1 -x_0x2e__0x2e__0x2e_0313_bit2 -x_0x2e__0x2e__0x2e_0314_bit0 -x_0x2e__0x2e__0x2e_0314_bit1 -x_0x2e__0x2e__0x2e_0314_bit2 -x_0x2e__0x2e__0x2e_0315_bit0 -x_0x2e__0x2e__0x2e_0315_bit1 -x_0x2e__0x2e__0x2e_0316_bit0 -x_0x2e__0x2e__0x2e_0316_bit1 -x_0x2e__0x2e__0x2e_0317_bit0 -x_0x2e__0x2e__0x2e_0410_bit0 -x_0x2e__0x2e__0x2e_0410_bit1 -x_0x2e__0x2e__0x2e_0410_bit2 -x_0x2e__0x2e__0x2e_0411_bit0 -x_0x2e__0x2e__0x2e_0411_bit1 -x_0x2e__0x2e__0x2e_0411_bit2 -x_0x2e__0x2e__0x2e_0412_bit0 -x_0x2e__0x2e__0x2e_0412_bit1 -x_0x2e__0x2e__0x2e_0412_bit2 x_0x2e__0x2e__0x2e_0412_bit3 -x_0x2e__0x2e__0x2e_0413_bit0 -x_0x2e__0x2e__0x2e_0413_bit1 -x_0x2e__0x2e__0x2e_0413_bit2 -x_0x2e__0x2e__0x2e_0414_bit0 -x_0x2e__0x2e__0x2e_0414_bit1 -x_0x2e__0x2e__0x2e_0414_bit2 -x_0x2e__0x2e__0x2e_0415_bit0 -x_0x2e__0x2e__0x2e_0415_bit1 -x_0x2e__0x2e__0x2e_0416_bit0 -x_0x2e__0x2e__0x2e_0416_bit1 -x_0x2e__0x2e__0x2e_0417_bit0 -x_0x2e__0x2e__0x2e_0510_bit0 -x_0x2e__0x2e__0x2e_0510_bit1 -x_0x2e__0x2e__0x2e_0510_bit2 -x_0x2e__0x2e__0x2e_0511_bit0 -x_0x2e__0x2e__0x2e_0511_bit1 -x_0x2e__0x2e__0x2e_0511_bit2 -x_0x2e__0x2e__0x2e_0512_bit0 -x_0x2e__0x2e__0x2e_0512_bit1 -x_0x2e__0x2e__0x2e_0512_bit2 -x_0x2e__0x2e__0x2e_0512_bit3 -x_0x2e__0x2e__0x2e_0513_bit0 -x_0x2e__0x2e__0x2e_0513_bit1 -x_0x2e__0x2e__0x2e_0513_bit2 -x_0x2e__0x2e__0x2e_0514_bit0 -x_0x2e__0x2e__0x2e_0514_bit1 -x_0x2e__0x2e__0x2e_0514_bit2 -x_0x2e__0x2e__0x2e_0515_bit0 -x_0x2e__0x2e__0x2e_0515_bit1 -x_0x2e__0x2e__0x2e_0516_bit0 -x_0x2e__0x2e__0x2e_0516_bit1 -x_0x2e__0x2e__0x2e_0517_bit0 -x_0x2e__0x2e__0x2e_0610_bit0 -x_0x2e__0x2e__0x2e_0610_bit1 -x_0x2e__0x2e__0x2e_0610_bit2 -x_0x2e__0x2e__0x2e_0611_bit0 -x_0x2e__0x2e__0x2e_0611_bit1 -x_0x2e__0x2e__0x2e_0611_bit2 -x_0x2e__0x2e__0x2e_0612_bit0 -x_0x2e__0x2e__0x2e_0612_bit1 -x_0x2e__0x2e__0x2e_0612_bit2 -x_0x2e__0x2e__0x2e_0612_bit3 -x_0x2e__0x2e__0x2e_0613_bit0 -x_0x2e__0x2e__0x2e_0613_bit1 -x_0x2e__0x2e__0x2e_0613_bit2 -x_0x2e__0x2e__0x2e_0614_bit0 -x_0x2e__0x2e__0x2e_0614_bit1 -x_0x2e__0x2e__0x2e_0614_bit2 -x_0x2e__0x2e__0x2e_0615_bit0 -x_0x2e__0x2e__0x2e_0615_bit1 -x_0x2e__0x2e__0x2e_0616_bit0 -x_0x2e__0x2e__0x2e_0616_bit1 -x_0x2e__0x2e__0x2e_0617_bit0 -x_0x2e__0x2e__0x2e_0710_bit0 -x_0x2e__0x2e__0x2e_0710_bit1 -x_0x2e__0x2e__0x2e_0710_bit2 -x_0x2e__0x2e__0x2e_0711_bit0 -x_0x2e__0x2e__0x2e_0711_bit1 -x_0x2e__0x2e__0x2e_0711_bit2 -x_0x2e__0x2e__0x2e_0712_bit0 -x_0x2e__0x2e__0x2e_0712_bit1 -x_0x2e__0x2e__0x2e_0712_bit2 -x_0x2e__0x2e__0x2e_0712_bit3 x_0x2e__0x2e__0x2e_0713_bit0 -x_0x2e__0x2e__0x2e_0713_bit1 -x_0x2e__0x2e__0x2e_0713_bit2 -x_0x2e__0x2e__0x2e_0714_bit0 x_0x2e__0x2e__0x2e_0714_bit1 -x_0x2e__0x2e__0x2e_0714_bit2 -x_0x2e__0x2e__0x2e_0715_bit0 -x_0x2e__0x2e__0x2e_0715_bit1 -x_0x2e__0x2e__0x2e_0716_bit0 -x_0x2e__0x2e__0x2e_0716_bit1 -x_0x2e__0x2e__0x2e_0717_bit0 -x_0x2e__0x2e__0x2e_0810_bit0 -x_0x2e__0x2e__0x2e_0810_bit1 -x_0x2e__0x2e__0x2e_0810_bit2 -x_0x2e__0x2e__0x2e_0811_bit0 -x_0x2e__0x2e__0x2e_0811_bit1 -x_0x2e__0x2e__0x2e_0811_bit2 -x_0x2e__0x2e__0x2e_0812_bit0 -x_0x2e__0x2e__0x2e_0812_bit1 -x_0x2e__0x2e__0x2e_0812_bit2 -x_0x2e__0x2e__0x2e_0812_bit3 -x_0x2e__0x2e__0x2e_0813_bit0 -x_0x2e__0x2e__0x2e_0813_bit1 -x_0x2e__0x2e__0x2e_0813_bit2 -x_0x2e__0x2e__0x2e_0814_bit0 -x_0x2e__0x2e__0x2e_0814_bit1 -x_0x2e__0x2e__0x2e_0814_bit2 -x_0x2e__0x2e__0x2e_0815_bit0 -x_0x2e__0x2e__0x2e_0815_bit1 -x_0x2e__0x2e__0x2e_0816_bit0 -x_0x2e__0x2e__0x2e_0816_bit1 -x_0x2e__0x2e__0x2e_0817_bit0 x_0x2e__0x2e__0x2e_0910_bit0 -x_0x2e__0x2e__0x2e_0910_bit1 -x_0x2e__0x2e__0x2e_0910_bit2 -x_0x2e__0x2e__0x2e_0911_bit0 -x_0x2e__0x2e__0x2e_0911_bit1 x_0x2e__0x2e__0x2e_0911_bit2 -x_0x2e__0x2e__0x2e_0912_bit0 -x_0x2e__0x2e__0x2e_0912_bit1 -x_0x2e__0x2e__0x2e_0912_bit2 -x_0x2e__0x2e__0x2e_0912_bit3 x_0x2e__0x2e__0x2e_0913_bit0 -x_0x2e__0x2e__0x2e_0913_bit1 -x_0x2e__0x2e__0x2e_0913_bit2 x_0x2e__0x2e__0x2e_0914_bit0 -x_0x2e__0x2e__0x2e_0914_bit1 -x_0x2e__0x2e__0x2e_0914_bit2 -x_0x2e__0x2e__0x2e_0915_bit0 -x_0x2e__0x2e__0x2e_0915_bit1 -x_0x2e__0x2e__0x2e_0916_bit0 -x_0x2e__0x2e__0x2e_0916_bit1 -x_0x2e__0x2e__0x2e_0917_bit0 -x_0x2e__0x2e__0x2e_1010_bit0 -x_0x2e__0x2e__0x2e_1010_bit1 -x_0x2e__0x2e__0x2e_1010_bit2 -x_0x2e__0x2e__0x2e_1011_bit0 -x_0x2e__0x2e__0x2e_1011_bit1 -x_0x2e__0x2e__0x2e_1011_bit2 -x_0x2e__0x2e__0x2e_1012_bit0 -x_0x2e__0x2e__0x2e_1012_bit1 -x_0x2e__0x2e__0x2e_1012_bit2 -x_0x2e__0x2e__0x2e_1012_bit3 -x_0x2e__0x2e__0x2e_1013_bit0 -x_0x2e__0x2e__0x2e_1013_bit1 -x_0x2e__0x2e__0x2e_1013_bit2 -x_0x2e__0x2e__0x2e_1014_bit0 -x_0x2e__0x2e__0x2e_1014_bit1 -x_0x2e__0x2e__0x2e_1014_bit2 -x_0x2e__0x2e__0x2e_1015_bit0 -x_0x2e__0x2e__0x2e_1015_bit1 -x_0x2e__0x2e__0x2e_1016_bit0 -x_0x2e__0x2e__0x2e_1016_bit1 -x_0x2e__0x2e__0x2e_1017_bit0 x_0x2e__0x2e__0x2e_1110_bit0 -x_0x2e__0x2e__0x2e_1110_bit1 -x_0x2e__0x2e__0x2e_1110_bit2 -x_0x2e__0x2e__0x2e_1111_bit0 -x_0x2e__0x2e__0x2e_1111_bit1 -x_0x2e__0x2e__0x2e_1111_bit2 x_0x2e__0x2e__0x2e_1112_bit0 -x_0x2e__0x2e__0x2e_1112_bit1 -x_0x2e__0x2e__0x2e_1112_bit2 -x_0x2e__0x2e__0x2e_1112_bit3 x_0x2e__0x2e__0x2e_1113_bit0 -x_0x2e__0x2e__0x2e_1113_bit1 -x_0x2e__0x2e__0x2e_1113_bit2 -x_0x2e__0x2e__0x2e_1114_bit0 -x_0x2e__0x2e__0x2e_1114_bit1 -x_0x2e__0x2e__0x2e_1114_bit2 -x_0x2e__0x2e__0x2e_1115_bit0 -x_0x2e__0x2e__0x2e_1115_bit1 -x_0x2e__0x2e__0x2e_1116_bit0 -x_0x2e__0x2e__0x2e_1116_bit1 x_0x2e__0x2e__0x2e_1117_bit0 -x_0x2e__0x2e__0x2e_1210_bit0 -x_0x2e__0x2e__0x2e_1210_bit1 -x_0x2e__0x2e__0x2e_1210_bit2 -x_0x2e__0x2e__0x2e_1211_bit0 -x_0x2e__0x2e__0x2e_1211_bit1 -x_0x2e__0x2e__0x2e_1211_bit2 -x_0x2e__0x2e__0x2e_1212_bit0 -x_0x2e__0x2e__0x2e_1212_bit1 -x_0x2e__0x2e__0x2e_1212_bit2 -x_0x2e__0x2e__0x2e_1212_bit3 -x_0x2e__0x2e__0x2e_1213_bit0 -x_0x2e__0x2

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/1733/stat): 1733 (minisat+_script) R 1732 1733 19316 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1851925437 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/1733/statm): 174 3 169 147 0 27 0
[pid=1733] 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=1734
New process pid=1735
New process pid=1736
execve syscall for /bin/sed executable
One traced child (pid=1735) exited with status: 0
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=1736) exited with status: 0
One traced child (pid=1734) exited with status: 0
New process pid=1737
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-20-10-gt2.opb

[startup+10.0031 s]
Raw data (loadavg): 0.93 0.95 0.87 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 8677 0 0 0 933 30 0 0 25 0 1 0 1851925442 36802560 8019 4294967295 134512640 135094434 3221224432 3221223072 134558264 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1737/statm): 8985 8019 145 145 0 8840 0
[pid=1737] vsize: 35940
Current children cumulated CPU time (s) 9.65
Current children cumulated vsize (Kb) 38064

[startup+20.0036 s]
Raw data (loadavg): 0.94 0.96 0.87 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 8866 0 0 0 1930 31 0 0 25 0 1 0 1851925442 37457920 8208 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 9145 8208 145 145 0 9000 0
[pid=1737] vsize: 36580
Current children cumulated CPU time (s) 19.63
Current children cumulated vsize (Kb) 38704

[startup+30.0043 s]
Raw data (loadavg): 0.95 0.96 0.87 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 8920 0 0 0 2928 31 0 0 25 0 1 0 1851925442 37691392 8262 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1737/statm): 9202 8262 145 145 0 9057 0
[pid=1737] vsize: 36808
Current children cumulated CPU time (s) 29.61
Current children cumulated vsize (Kb) 38932

[startup+40.0049 s]
Raw data (loadavg): 0.95 0.96 0.87 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 9009 0 0 0 3926 32 0 0 25 0 1 0 1851925442 38043648 8351 4294967295 134512640 135094434 3221224432 3221223112 134553433 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 9288 8351 145 145 0 9143 0
[pid=1737] vsize: 37152
Current children cumulated CPU time (s) 39.6
Current children cumulated vsize (Kb) 39276

[startup+50.0065 s]
Raw data (loadavg): 0.96 0.96 0.88 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 9231 0 0 0 4923 33 0 0 25 0 1 0 1851925442 38973440 8573 4294967295 134512640 135094434 3221224432 3221223024 134556812 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 9515 8573 145 145 0 9370 0
[pid=1737] vsize: 38060
Current children cumulated CPU time (s) 49.58
Current children cumulated vsize (Kb) 40184

[startup+60.0071 s]
Raw data (loadavg): 0.97 0.96 0.88 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 9392 0 0 0 5921 35 0 0 25 0 1 0 1851925442 39628800 8734 4294967295 134512640 135094434 3221224432 3221223088 134558420 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 9675 8734 145 145 0 9530 0
[pid=1737] vsize: 38700
Current children cumulated CPU time (s) 59.58
Current children cumulated vsize (Kb) 40824

[startup+70.0167 s]
Raw data (loadavg): 0.97 0.96 0.88 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 9479 0 0 0 6920 36 0 0 25 0 1 0 1851925442 39981056 8821 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1737/statm): 9761 8821 145 145 0 9616 0
[pid=1737] vsize: 39044
Current children cumulated CPU time (s) 69.58
Current children cumulated vsize (Kb) 41168

[startup+80.0183 s]
Raw data (loadavg): 0.98 0.96 0.88 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 9801 0 0 0 7914 38 0 0 25 0 1 0 1851925442 41287680 9143 4294967295 134512640 135094434 3221224432 3221223024 134557022 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 10080 9143 145 145 0 9935 0
[pid=1737] vsize: 40320
Current children cumulated CPU time (s) 79.54
Current children cumulated vsize (Kb) 42444

[startup+90.0189 s]
Raw data (loadavg): 0.98 0.96 0.88 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 10008 0 0 0 8911 39 0 0 25 0 1 0 1851925442 42192896 9350 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 10301 9350 145 145 0 10156 0
[pid=1737] vsize: 41204
Current children cumulated CPU time (s) 89.52
Current children cumulated vsize (Kb) 43328

[startup+100.019 s]
Raw data (loadavg): 0.98 0.96 0.88 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 10154 0 0 0 9909 40 0 0 25 0 1 0 1851925442 42786816 9496 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 10446 9496 145 145 0 10301 0
[pid=1737] vsize: 41784
Current children cumulated CPU time (s) 99.51
Current children cumulated vsize (Kb) 43908

[startup+110.02 s]
Raw data (loadavg): 0.98 0.96 0.88 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 10321 0 0 0 10906 42 0 0 25 0 1 0 1851925442 43466752 9663 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 10612 9663 145 145 0 10467 0
[pid=1737] vsize: 42448
Current children cumulated CPU time (s) 109.5
Current children cumulated vsize (Kb) 44572

[startup+120.021 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 10436 0 0 0 11904 42 0 0 25 0 1 0 1851925442 43925504 9778 4294967295 134512640 135094434 3221224432 3221223024 134556982 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 10724 9778 145 145 0 10579 0
[pid=1737] vsize: 42896
Current children cumulated CPU time (s) 119.48
Current children cumulated vsize (Kb) 45020

[startup+130.021 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 10713 0 0 0 12899 44 0 0 25 0 1 0 1851925442 45047808 10055 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 10998 10055 145 145 0 10853 0
[pid=1737] vsize: 43992
Current children cumulated CPU time (s) 129.45
Current children cumulated vsize (Kb) 46116

[startup+140.022 s]
Raw data (loadavg): 0.99 0.97 0.88 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 10773 0 0 0 13897 44 0 0 25 0 1 0 1851925442 45285376 10115 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 11056 10115 145 145 0 10911 0
[pid=1737] vsize: 44224
Current children cumulated CPU time (s) 139.43
Current children cumulated vsize (Kb) 46348

[startup+150.024 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 10980 0 0 0 14893 46 0 0 25 0 1 0 1851925442 46116864 10322 4294967295 134512640 135094434 3221224432 3221223120 134554726 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 11259 10322 145 145 0 11114 0
[pid=1737] vsize: 45036
Current children cumulated CPU time (s) 149.41
Current children cumulated vsize (Kb) 47160

[startup+160.024 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 11264 0 0 0 15889 47 0 0 25 0 1 0 1851925442 47394816 10606 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 11571 10606 145 145 0 11426 0
[pid=1737] vsize: 46284
Current children cumulated CPU time (s) 159.38
Current children cumulated vsize (Kb) 48408

[startup+170.025 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 11507 0 0 0 16885 49 0 0 25 0 1 0 1851925442 48381952 10849 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1737/statm): 11812 10849 145 145 0 11667 0
[pid=1737] vsize: 47248
Current children cumulated CPU time (s) 169.36
Current children cumulated vsize (Kb) 49372

[startup+180.026 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 11785 0 0 0 17881 50 0 0 25 0 1 0 1851925442 49520640 11127 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1737/statm): 12090 11127 145 145 0 11945 0
[pid=1737] vsize: 48360
Current children cumulated CPU time (s) 179.33
Current children cumulated vsize (Kb) 50484

[startup+190.027 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 12002 0 0 0 18879 52 0 0 25 0 1 0 1851925442 50388992 11344 4294967295 134512640 135094434 3221224432 3221223024 134556843 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1737/statm): 12302 11344 145 145 0 12157 0
[pid=1737] vsize: 49208
Current children cumulated CPU time (s) 189.33
Current children cumulated vsize (Kb) 51332

[startup+200.029 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 12201 0 0 0 19877 52 0 0 25 0 1 0 1851925442 51273728 11543 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 12518 11543 145 145 0 12373 0
[pid=1737] vsize: 50072
Current children cumulated CPU time (s) 199.31
Current children cumulated vsize (Kb) 52196

[startup+210.029 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 12283 0 0 0 20876 53 0 0 25 0 1 0 1851925442 51601408 11625 4294967295 134512640 135094434 3221224432 3221223056 134557565 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 12598 11625 145 145 0 12453 0
[pid=1737] vsize: 50392
Current children cumulated CPU time (s) 209.31
Current children cumulated vsize (Kb) 52516

[startup+220.03 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 12386 0 0 0 21873 55 0 0 25 0 1 0 1851925442 52019200 11728 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 12700 11728 145 145 0 12555 0
[pid=1737] vsize: 50800
Current children cumulated CPU time (s) 219.3
Current children cumulated vsize (Kb) 52924

[startup+230.03 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 12505 0 0 0 22870 57 0 0 25 0 1 0 1851925442 52502528 11847 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 12818 11847 145 145 0 12673 0
[pid=1737] vsize: 51272
Current children cumulated CPU time (s) 229.29
Current children cumulated vsize (Kb) 53396

[startup+240.031 s]
Raw data (loadavg): 0.99 0.97 0.89 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 12637 0 0 0 23868 58 0 0 25 0 1 0 1851925442 53039104 11979 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 12949 11979 145 145 0 12804 0
[pid=1737] vsize: 51796
Current children cumulated CPU time (s) 239.28
Current children cumulated vsize (Kb) 53920

[startup+250.032 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 12756 0 0 0 24866 59 0 0 25 0 1 0 1851925442 53510144 12098 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 13064 12098 145 145 0 12919 0
[pid=1737] vsize: 52256
Current children cumulated CPU time (s) 249.27
Current children cumulated vsize (Kb) 54380

[startup+260.033 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 12927 0 0 0 25863 60 0 0 25 0 1 0 1851925442 54214656 12269 4294967295 134512640 135094434 3221224432 3221223104 134556317 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 13236 12269 145 145 0 13091 0
[pid=1737] vsize: 52944
Current children cumulated CPU time (s) 259.25
Current children cumulated vsize (Kb) 55068

[startup+270.034 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 13104 0 0 0 26859 62 0 0 25 0 1 0 1851925442 54935552 12446 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 13412 12446 145 145 0 13267 0
[pid=1737] vsize: 53648
Current children cumulated CPU time (s) 269.23
Current children cumulated vsize (Kb) 55772

[startup+280.034 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 13850 0 0 0 27854 65 0 0 25 0 1 0 1851925442 57036800 12902 4294967295 134512640 135094434 3221224432 3221220928 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 13925 12902 145 145 0 13780 0
[pid=1737] vsize: 55700
Current children cumulated CPU time (s) 279.21
Current children cumulated vsize (Kb) 57824

[startup+290.035 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 19000 0 0 0 28817 83 0 0 25 0 1 0 1851925442 81887232 17722 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1737/statm): 19992 17722 145 145 0 19847 0
[pid=1737] vsize: 79968
Current children cumulated CPU time (s) 289.02
Current children cumulated vsize (Kb) 82092

[startup+300.037 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 19118 0 0 0 29816 83 0 0 25 0 1 0 1851925442 82145280 17840 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 20055 17840 145 145 0 19910 0
[pid=1737] vsize: 80220
Current children cumulated CPU time (s) 299.01
Current children cumulated vsize (Kb) 82344

[startup+310.037 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 19254 0 0 0 30815 84 0 0 25 0 1 0 1851925442 82698240 17976 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 20190 17976 145 145 0 20045 0
[pid=1737] vsize: 80760
Current children cumulated CPU time (s) 309.01
Current children cumulated vsize (Kb) 82884

[startup+320.038 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 19392 0 0 0 31812 85 0 0 25 0 1 0 1851925442 83275776 18114 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 20331 18114 145 145 0 20186 0
[pid=1737] vsize: 81324
Current children cumulated CPU time (s) 318.99
Current children cumulated vsize (Kb) 83448

[startup+330.038 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 19451 0 0 0 32811 86 0 0 25 0 1 0 1851925442 83505152 18173 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 20387 18173 145 145 0 20242 0
[pid=1737] vsize: 81548
Current children cumulated CPU time (s) 328.99
Current children cumulated vsize (Kb) 83672

[startup+340.039 s]
Raw data (loadavg): 0.99 0.97 0.90 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 19516 0 0 0 33810 86 0 0 25 0 1 0 1851925442 83763200 18238 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 20450 18238 145 145 0 20305 0
[pid=1737] vsize: 81800
Current children cumulated CPU time (s) 338.98
Current children cumulated vsize (Kb) 83924

[startup+350.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 19829 0 0 0 34804 89 0 0 25 0 1 0 1851925442 85307392 18551 4294967295 134512640 135094434 3221224432 3221223104 134556410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 20827 18551 145 145 0 20682 0
[pid=1737] vsize: 83308
Current children cumulated CPU time (s) 348.95
Current children cumulated vsize (Kb) 85432

[startup+360.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 20015 0 0 0 35801 90 0 0 25 0 1 0 1851925442 86069248 18737 4294967295 134512640 135094434 3221224432 3221223092 134553497 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 21013 18737 145 145 0 20868 0
[pid=1737] vsize: 84052
Current children cumulated CPU time (s) 358.93
Current children cumulated vsize (Kb) 86176

[startup+370.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 20028 0 0 0 36800 91 0 0 25 0 1 0 1851925442 86118400 18750 4294967295 134512640 135094434 3221224432 3221223056 134557675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 21025 18750 145 145 0 20880 0
[pid=1737] vsize: 84100
Current children cumulated CPU time (s) 368.93
Current children cumulated vsize (Kb) 86224

[startup+380.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 20104 0 0 0 37799 91 0 0 25 0 1 0 1851925442 86441984 18826 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 21104 18826 145 145 0 20959 0
[pid=1737] vsize: 84416
Current children cumulated CPU time (s) 378.92
Current children cumulated vsize (Kb) 86540

[startup+390.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 20118 0 0 0 38799 91 0 0 25 0 1 0 1851925442 86495232 18840 4294967295 134512640 135094434 3221224432 3221223080 134558258 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 21117 18840 145 145 0 20972 0
[pid=1737] vsize: 84468
Current children cumulated CPU time (s) 388.92
Current children cumulated vsize (Kb) 86592

[startup+400.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 25081 0 0 0 39760 111 0 0 25 0 1 0 1851925442 101781504 23513 4294967295 134512640 135094434 3221224432 3221223056 134557685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1737/statm): 24849 23513 145 145 0 24704 0
[pid=1737] vsize: 99396
Current children cumulated CPU time (s) 398.73
Current children cumulated vsize (Kb) 101520

[startup+410.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 25166 0 0 0 40759 112 0 0 25 0 1 0 1851925442 101920768 23598 4294967295 134512640 135094434 3221224432 3221223088 134558402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 24883 23598 145 145 0 24738 0
[pid=1737] vsize: 99532
Current children cumulated CPU time (s) 408.73
Current children cumulated vsize (Kb) 101656

[startup+420.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 25179 0 0 0 41759 112 0 0 25 0 1 0 1851925442 101965824 23611 4294967295 134512640 135094434 3221224432 3221223092 134553491 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 24894 23611 145 145 0 24749 0
[pid=1737] vsize: 99576
Current children cumulated CPU time (s) 418.73
Current children cumulated vsize (Kb) 101700

[startup+430.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 25283 0 0 0 42757 113 0 0 25 0 1 0 1851925442 102354944 23715 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 24989 23715 145 145 0 24844 0
[pid=1737] vsize: 99956
Current children cumulated CPU time (s) 428.72
Current children cumulated vsize (Kb) 102080

[startup+440.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 25316 0 0 0 43757 113 0 0 25 0 1 0 1851925442 102490112 23748 4294967295 134512640 135094434 3221224432 3221223088 134558033 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 25022 23748 145 145 0 24877 0
[pid=1737] vsize: 100088
Current children cumulated CPU time (s) 438.72
Current children cumulated vsize (Kb) 102212

[startup+450.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 26013 0 0 0 44753 116 0 0 25 0 1 0 1851925442 104505344 24155 4294967295 134512640 135094434 3221224432 3221222160 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 25514 24155 145 145 0 25369 0
[pid=1737] vsize: 102056
Current children cumulated CPU time (s) 448.71
Current children cumulated vsize (Kb) 104180

[startup+460.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 26020 0 0 0 45753 116 0 0 25 0 1 0 1851925442 104505344 24162 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 25514 24162 145 145 0 25369 0
[pid=1737] vsize: 102056
Current children cumulated CPU time (s) 458.71
Current children cumulated vsize (Kb) 104180

[startup+470.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 26023 0 0 0 46753 116 0 0 25 0 1 0 1851925442 104505344 24165 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 25514 24165 145 145 0 25369 0
[pid=1737] vsize: 102056
Current children cumulated CPU time (s) 468.71
Current children cumulated vsize (Kb) 104180

[startup+480.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 26025 0 0 0 47754 116 0 0 25 0 1 0 1851925442 104505344 24167 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 25514 24167 145 145 0 25369 0
[pid=1737] vsize: 102056
Current children cumulated CPU time (s) 478.72
Current children cumulated vsize (Kb) 104180

[startup+490.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 26096 0 0 0 48753 116 0 0 25 0 1 0 1851925442 104796160 24238 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 25585 24238 145 145 0 25440 0
[pid=1737] vsize: 102340
Current children cumulated CPU time (s) 488.71
Current children cumulated vsize (Kb) 104464

[startup+500.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 26157 0 0 0 49753 117 0 0 25 0 1 0 1851925442 105041920 24299 4294967295 134512640 135094434 3221224432 3221223024 134557421 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 25645 24299 145 145 0 25500 0
[pid=1737] vsize: 102580
Current children cumulated CPU time (s) 498.72
Current children cumulated vsize (Kb) 104704

[startup+510.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 26221 0 0 0 50752 117 0 0 25 0 1 0 1851925442 105312256 24363 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 25711 24363 145 145 0 25566 0
[pid=1737] vsize: 102844
Current children cumulated CPU time (s) 508.71
Current children cumulated vsize (Kb) 104968

[startup+520.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 26274 0 0 0 51752 117 0 0 25 0 1 0 1851925442 105533440 24416 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 25765 24416 145 145 0 25620 0
[pid=1737] vsize: 103060
Current children cumulated CPU time (s) 518.71
Current children cumulated vsize (Kb) 105184

[startup+530.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 26298 0 0 0 52752 117 0 0 25 0 1 0 1851925442 105623552 24440 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 25787 24440 145 145 0 25642 0
[pid=1737] vsize: 103148
Current children cumulated CPU time (s) 528.71
Current children cumulated vsize (Kb) 105272

[startup+540.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 26330 0 0 0 53751 118 0 0 25 0 1 0 1851925442 105750528 24472 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 25818 24472 145 145 0 25673 0
[pid=1737] vsize: 103272
Current children cumulated CPU time (s) 538.71
Current children cumulated vsize (Kb) 105396

[startup+550.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 26464 0 0 0 54749 119 0 0 25 0 1 0 1851925442 106307584 24606 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 25954 24606 145 145 0 25809 0
[pid=1737] vsize: 103816
Current children cumulated CPU time (s) 548.7
Current children cumulated vsize (Kb) 105940

[startup+560.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 26685 0 0 0 55746 120 0 0 25 0 1 0 1851925442 107208704 24827 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 26174 24827 145 145 0 26029 0
[pid=1737] vsize: 104696
Current children cumulated CPU time (s) 558.68
Current children cumulated vsize (Kb) 106820

[startup+570.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 31465 0 0 0 56709 139 0 0 25 0 1 0 1851925442 140767232 29317 4294967295 134512640 135094434 3221224432 3221223084 134675715 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 34367 29317 145 145 0 34222 0
[pid=1737] vsize: 137468
Current children cumulated CPU time (s) 568.5
Current children cumulated vsize (Kb) 139592

[startup+580.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 31595 0 0 0 57709 140 0 0 25 0 1 0 1851925442 141058048 29447 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 34438 29447 145 145 0 34293 0
[pid=1737] vsize: 137752
Current children cumulated CPU time (s) 578.51
Current children cumulated vsize (Kb) 139876

[startup+590.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 31704 0 0 0 58709 140 0 0 25 0 1 0 1851925442 141488128 29556 4294967295 134512640 135094434 3221224432 3221223088 134558295 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 34543 29556 145 145 0 34398 0
[pid=1737] vsize: 138172
Current children cumulated CPU time (s) 588.51
Current children cumulated vsize (Kb) 140296

[startup+600.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 31757 0 0 0 59708 140 0 0 25 0 1 0 1851925442 141705216 29609 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 34596 29609 145 145 0 34451 0
[pid=1737] vsize: 138384
Current children cumulated CPU time (s) 598.5
Current children cumulated vsize (Kb) 140508

[startup+610.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 31825 0 0 0 60707 141 0 0 25 0 1 0 1851925442 141987840 29677 4294967295 134512640 135094434 3221224432 3221223120 134554709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 34665 29677 145 145 0 34520 0
[pid=1737] vsize: 138660
Current children cumulated CPU time (s) 608.5
Current children cumulated vsize (Kb) 140784

[startup+620.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 31918 0 0 0 61706 141 0 0 25 0 1 0 1851925442 142372864 29770 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 34759 29770 145 145 0 34614 0
[pid=1737] vsize: 139036
Current children cumulated CPU time (s) 618.49
Current children cumulated vsize (Kb) 141160

[startup+630.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 31922 0 0 0 62706 142 0 0 25 0 1 0 1851925442 142389248 29774 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 34763 29774 145 145 0 34618 0
[pid=1737] vsize: 139052
Current children cumulated CPU time (s) 628.5
Current children cumulated vsize (Kb) 141176

[startup+640.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 32140 0 0 0 63703 143 0 0 25 0 1 0 1851925442 143278080 29992 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 34980 29992 145 145 0 34835 0
[pid=1737] vsize: 139920
Current children cumulated CPU time (s) 638.48
Current children cumulated vsize (Kb) 142044

[startup+650.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 32202 0 0 0 64702 143 0 0 25 0 1 0 1851925442 143532032 30054 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 35042 30054 145 145 0 34897 0
[pid=1737] vsize: 140168
Current children cumulated CPU time (s) 648.47
Current children cumulated vsize (Kb) 142292

[startup+660.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 32254 0 0 0 65702 143 0 0 25 0 1 0 1851925442 143745024 30106 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 35094 30106 145 145 0 34949 0
[pid=1737] vsize: 140376
Current children cumulated CPU time (s) 658.47
Current children cumulated vsize (Kb) 142500

[startup+670.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 32347 0 0 0 66700 144 0 0 25 0 1 0 1851925442 144121856 30199 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 35186 30199 145 145 0 35041 0
[pid=1737] vsize: 140744
Current children cumulated CPU time (s) 668.46
Current children cumulated vsize (Kb) 142868

[startup+680.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 32427 0 0 0 67699 145 0 0 25 0 1 0 1851925442 144449536 30279 4294967295 134512640 135094434 3221224432 3221223056 134557685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 35266 30279 145 145 0 35121 0
[pid=1737] vsize: 141064
Current children cumulated CPU time (s) 678.46
Current children cumulated vsize (Kb) 143188

[startup+690.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 32503 0 0 0 68698 146 0 0 25 0 1 0 1851925442 144760832 30355 4294967295 134512640 135094434 3221224432 3221223056 134557717 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 35342 30355 145 145 0 35197 0
[pid=1737] vsize: 141368
Current children cumulated CPU time (s) 688.46
Current children cumulated vsize (Kb) 143492

[startup+700.065 s]
Raw data (loadavg): 1.06 0.99 0.91 1/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) T 1733 1733 19316 0 -1 0 32731 0 0 0 69695 147 0 0 25 0 1 0 1851925442 145674240 30583 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/1737/statm): 35565 30583 145 145 0 35420 0
[pid=1737] vsize: 142260
Current children cumulated CPU time (s) 698.44
Current children cumulated vsize (Kb) 144384

[startup+710.065 s]
Raw data (loadavg): 1.05 0.99 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 33157 0 0 0 70687 150 0 0 25 0 1 0 1851925442 147410944 31009 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 35989 31009 145 145 0 35844 0
[pid=1737] vsize: 143956
Current children cumulated CPU time (s) 708.39
Current children cumulated vsize (Kb) 146080

[startup+720.066 s]
Raw data (loadavg): 1.04 0.99 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 33814 0 0 0 71684 152 0 0 25 0 1 0 1851925442 148598784 31376 4294967295 134512640 135094434 3221224432 3221223024 134556937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 36279 31376 145 145 0 36134 0
[pid=1737] vsize: 145116
Current children cumulated CPU time (s) 718.38
Current children cumulated vsize (Kb) 147240

[startup+730.066 s]
Raw data (loadavg): 1.04 0.99 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 33815 0 0 0 72685 152 0 0 25 0 1 0 1851925442 148598784 31377 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 36279 31377 145 145 0 36134 0
[pid=1737] vsize: 145116
Current children cumulated CPU time (s) 728.39
Current children cumulated vsize (Kb) 147240

[startup+740.067 s]
Raw data (loadavg): 1.03 0.99 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 33816 0 0 0 73685 152 0 0 25 0 1 0 1851925442 148598784 31378 4294967295 134512640 135094434 3221224432 3221223056 134557685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 36279 31378 145 145 0 36134 0
[pid=1737] vsize: 145116
Current children cumulated CPU time (s) 738.39
Current children cumulated vsize (Kb) 147240

[startup+750.068 s]
Raw data (loadavg): 1.03 0.99 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 33816 0 0 0 74685 152 0 0 25 0 1 0 1851925442 148598784 31378 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 36279 31378 145 145 0 36134 0
[pid=1737] vsize: 145116
Current children cumulated CPU time (s) 748.39
Current children cumulated vsize (Kb) 147240

[startup+760.068 s]
Raw data (loadavg): 1.02 0.99 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 33816 0 0 0 75685 152 0 0 25 0 1 0 1851925442 148598784 31378 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 36279 31378 145 145 0 36134 0
[pid=1737] vsize: 145116
Current children cumulated CPU time (s) 758.39
Current children cumulated vsize (Kb) 147240

[startup+770.069 s]
Raw data (loadavg): 1.02 0.99 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 33816 0 0 0 76686 152 0 0 25 0 1 0 1851925442 148598784 31378 4294967295 134512640 135094434 3221224432 3221223068 134557560 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 36279 31378 145 145 0 36134 0
[pid=1737] vsize: 145116
Current children cumulated CPU time (s) 768.4
Current children cumulated vsize (Kb) 147240

[startup+780.069 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 33817 0 0 0 77686 152 0 0 25 0 1 0 1851925442 148598784 31379 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 36279 31379 145 145 0 36134 0
[pid=1737] vsize: 145116
Current children cumulated CPU time (s) 778.4
Current children cumulated vsize (Kb) 147240

[startup+790.069 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 33818 0 0 0 78686 152 0 0 25 0 1 0 1851925442 148598784 31380 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1737/statm): 36279 31380 145 145 0 36134 0
[pid=1737] vsize: 145116
Current children cumulated CPU time (s) 788.4
Current children cumulated vsize (Kb) 147240

[startup+800.071 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 33818 0 0 0 79685 152 0 0 25 0 1 0 1851925442 148598784 31380 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 36279 31380 145 145 0 36134 0
[pid=1737] vsize: 145116
Current children cumulated CPU time (s) 798.39
Current children cumulated vsize (Kb) 147240

[startup+810.072 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 33876 0 0 0 80684 152 0 0 25 0 1 0 1851925442 148811776 31438 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 36331 31438 145 145 0 36186 0
[pid=1737] vsize: 145324
Current children cumulated CPU time (s) 808.38
Current children cumulated vsize (Kb) 147448

[startup+820.072 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 33881 0 0 0 81683 153 0 0 25 0 1 0 1851925442 148832256 31443 4294967295 134512640 135094434 3221224432 3221223092 134553501 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 36336 31443 145 145 0 36191 0
[pid=1737] vsize: 145344
Current children cumulated CPU time (s) 818.38
Current children cumulated vsize (Kb) 147468

[startup+830.072 s]
Raw data (loadavg): 1.00 0.99 0.91 1/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) T 1733 1733 19316 0 -1 0 34151 0 0 0 82677 156 0 0 25 0 1 0 1851925442 149925888 31713 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/1737/statm): 36603 31713 145 145 0 36458 0
[pid=1737] vsize: 146412
Current children cumulated CPU time (s) 828.35
Current children cumulated vsize (Kb) 148536

[startup+840.073 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 34325 0 0 0 83674 158 0 0 25 0 1 0 1851925442 150634496 31887 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 36776 31887 145 145 0 36631 0
[pid=1737] vsize: 147104
Current children cumulated CPU time (s) 838.34
Current children cumulated vsize (Kb) 149228

[startup+850.074 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 34381 0 0 0 84673 158 0 0 25 0 1 0 1851925442 150863872 31943 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 36832 31943 145 145 0 36687 0
[pid=1737] vsize: 147328
Current children cumulated CPU time (s) 848.33
Current children cumulated vsize (Kb) 149452

[startup+860.074 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 34463 0 0 0 85672 159 0 0 25 0 1 0 1851925442 151191552 32025 4294967295 134512640 135094434 3221224432 3221223056 134557645 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 36912 32025 145 145 0 36767 0
[pid=1737] vsize: 147648
Current children cumulated CPU time (s) 858.33
Current children cumulated vsize (Kb) 149772

[startup+870.075 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 34547 0 0 0 86671 160 0 0 25 0 1 0 1851925442 151531520 32109 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 36995 32109 145 145 0 36850 0
[pid=1737] vsize: 147980
Current children cumulated CPU time (s) 868.33
Current children cumulated vsize (Kb) 150104

[startup+880.075 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 34618 0 0 0 87669 161 0 0 25 0 1 0 1851925442 151822336 32180 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 37066 32180 145 145 0 36921 0
[pid=1737] vsize: 148264
Current children cumulated CPU time (s) 878.32
Current children cumulated vsize (Kb) 150388

[startup+890.076 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 34702 0 0 0 88668 161 0 0 25 0 1 0 1851925442 152162304 32264 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 37149 32264 145 145 0 37004 0
[pid=1737] vsize: 148596
Current children cumulated CPU time (s) 888.31
Current children cumulated vsize (Kb) 150720

[startup+900.077 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 34805 0 0 0 89667 162 0 0 25 0 1 0 1851925442 152584192 32367 4294967295 134512640 135094434 3221224432 3221223024 134557275 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 37252 32367 145 145 0 37107 0
[pid=1737] vsize: 149008
Current children cumulated CPU time (s) 898.31
Current children cumulated vsize (Kb) 151132

[startup+910.077 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 34899 0 0 0 90665 163 0 0 25 0 1 0 1851925442 152965120 32461 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 37345 32461 145 145 0 37200 0
[pid=1737] vsize: 149380
Current children cumulated CPU time (s) 908.3
Current children cumulated vsize (Kb) 151504

[startup+920.078 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 34992 0 0 0 91663 164 0 0 25 0 1 0 1851925442 153346048 32554 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 37438 32554 145 145 0 37293 0
[pid=1737] vsize: 149752
Current children cumulated CPU time (s) 918.29
Current children cumulated vsize (Kb) 151876

[startup+930.078 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 35065 0 0 0 92662 165 0 0 25 0 1 0 1851925442 153640960 32627 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 37510 32627 145 145 0 37365 0
[pid=1737] vsize: 150040
Current children cumulated CPU time (s) 928.29
Current children cumulated vsize (Kb) 152164

[startup+940.079 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 35100 0 0 0 93661 165 0 0 25 0 1 0 1851925442 153784320 32662 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 37545 32662 145 145 0 37400 0
[pid=1737] vsize: 150180
Current children cumulated CPU time (s) 938.28
Current children cumulated vsize (Kb) 152304

[startup+950.081 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 35143 0 0 0 94661 166 0 0 25 0 1 0 1851925442 153956352 32705 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 37587 32705 145 145 0 37442 0
[pid=1737] vsize: 150348
Current children cumulated CPU time (s) 948.29
Current children cumulated vsize (Kb) 152472

[startup+960.081 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 35204 0 0 0 95660 166 0 0 25 0 1 0 1851925442 154193920 32766 4294967295 134512640 135094434 3221224432 3221223092 134553487 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 37645 32766 145 145 0 37500 0
[pid=1737] vsize: 150580
Current children cumulated CPU time (s) 958.28
Current children cumulated vsize (Kb) 152704

[startup+970.081 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 35224 0 0 0 96659 166 0 0 25 0 1 0 1851925442 154271744 32786 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 37664 32786 145 145 0 37519 0
[pid=1737] vsize: 150656
Current children cumulated CPU time (s) 968.27
Current children cumulated vsize (Kb) 152780

[startup+980.082 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 35405 0 0 0 97656 168 0 0 25 0 1 0 1851925442 155004928 32967 4294967295 134512640 135094434 3221224432 3221223056 134557621 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 37843 32967 145 145 0 37698 0
[pid=1737] vsize: 151372
Current children cumulated CPU time (s) 978.26
Current children cumulated vsize (Kb) 153496

[startup+990.083 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 35622 0 0 0 98652 169 0 0 25 0 1 0 1851925442 155881472 33184 4294967295 134512640 135094434 3221224432 3221223024 134557238 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 38057 33184 145 145 0 37912 0
[pid=1737] vsize: 152228
Current children cumulated CPU time (s) 988.23
Current children cumulated vsize (Kb) 154352

[startup+1000.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 35857 0 0 0 99647 171 0 0 25 0 1 0 1851925442 156831744 33419 4294967295 134512640 135094434 3221224432 3221223024 134557022 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 38289 33419 145 145 0 38144 0
[pid=1737] vsize: 153156
Current children cumulated CPU time (s) 998.2
Current children cumulated vsize (Kb) 155280

[startup+1010.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 35963 0 0 0 100644 172 0 0 25 0 1 0 1851925442 157261824 33525 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 38394 33525 145 145 0 38249 0
[pid=1737] vsize: 153576
Current children cumulated CPU time (s) 1008.18
Current children cumulated vsize (Kb) 155700

[startup+1020.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 36006 0 0 0 101644 172 0 0 25 0 1 0 1851925442 157470720 33568 4294967295 134512640 135094434 3221224432 3221223120 134554709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 38445 33568 145 145 0 38300 0
[pid=1737] vsize: 153780
Current children cumulated CPU time (s) 1018.18
Current children cumulated vsize (Kb) 155904

[startup+1030.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 36109 0 0 0 102642 173 0 0 25 0 1 0 1851925442 157892608 33671 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 38548 33671 145 145 0 38403 0
[pid=1737] vsize: 154192
Current children cumulated CPU time (s) 1028.17
Current children cumulated vsize (Kb) 156316

[startup+1040.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 36239 0 0 0 103640 174 0 0 25 0 1 0 1851925442 158420992 33801 4294967295 134512640 135094434 3221224432 3221223120 134554793 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 38677 33801 145 145 0 38532 0
[pid=1737] vsize: 154708
Current children cumulated CPU time (s) 1038.16
Current children cumulated vsize (Kb) 156832

[startup+1050.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 36304 0 0 0 104639 175 0 0 25 0 1 0 1851925442 158683136 33866 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 38741 33866 145 145 0 38596 0
[pid=1737] vsize: 154964
Current children cumulated CPU time (s) 1048.16
Current children cumulated vsize (Kb) 157088

[startup+1060.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 36313 0 0 0 105639 175 0 0 25 0 1 0 1851925442 158720000 33875 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 38750 33875 145 145 0 38605 0
[pid=1737] vsize: 155000
Current children cumulated CPU time (s) 1058.16
Current children cumulated vsize (Kb) 157124

[startup+1070.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 36335 0 0 0 106639 175 0 0 25 0 1 0 1851925442 158806016 33897 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 38771 33897 145 145 0 38626 0
[pid=1737] vsize: 155084
Current children cumulated CPU time (s) 1068.16
Current children cumulated vsize (Kb) 157208

[startup+1080.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 36365 0 0 0 107639 175 0 0 25 0 1 0 1851925442 158928896 33927 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 38801 33927 145 145 0 38656 0
[pid=1737] vsize: 155204
Current children cumulated CPU time (s) 1078.16
Current children cumulated vsize (Kb) 157328

[startup+1090.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 36386 0 0 0 108639 175 0 0 25 0 1 0 1851925442 159010816 33948 4294967295 134512640 135094434 3221224432 3221223056 134557669 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 38821 33948 145 145 0 38676 0
[pid=1737] vsize: 155284
Current children cumulated CPU time (s) 1088.16
Current children cumulated vsize (Kb) 157408

[startup+1100.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 36438 0 0 0 109638 176 0 0 25 0 1 0 1851925442 159215616 34000 4294967295 134512640 135094434 3221224432 3221223056 134557565 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 38871 34000 145 145 0 38726 0
[pid=1737] vsize: 155484
Current children cumulated CPU time (s) 1098.16
Current children cumulated vsize (Kb) 157608

[startup+1110.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 37058 0 0 0 110634 178 0 0 25 0 1 0 1851925442 159383552 34034 4294967295 134512640 135094434 3221224432 3221223220 134553508 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 38912 34034 145 145 0 38767 0
[pid=1737] vsize: 155648
Current children cumulated CPU time (s) 1108.14
Current children cumulated vsize (Kb) 157772

[startup+1120.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 37080 0 0 0 111634 178 0 0 25 0 1 0 1851925442 159444992 34056 4294967295 134512640 135094434 3221224432 3221223136 134559013 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 38927 34056 145 145 0 38782 0
[pid=1737] vsize: 155708
Current children cumulated CPU time (s) 1118.14
Current children cumulated vsize (Kb) 157832

[startup+1130.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 37082 0 0 0 112634 178 0 0 25 0 1 0 1851925442 159453184 34058 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/1737/statm): 38929 34058 145 145 0 38784 0
[pid=1737] vsize: 155716
Current children cumulated CPU time (s) 1128.14
Current children cumulated vsize (Kb) 157840

[startup+1140.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 37108 0 0 0 113631 179 0 0 25 0 1 0 1851925442 159555584 34084 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 38954 34084 145 145 0 38809 0
[pid=1737] vsize: 155816
Current children cumulated CPU time (s) 1138.12
Current children cumulated vsize (Kb) 157940

[startup+1150.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 37143 0 0 0 114631 180 0 0 25 0 1 0 1851925442 159698944 34119 4294967295 134512640 135094434 3221224432 3221223120 134554709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 38989 34119 145 145 0 38844 0
[pid=1737] vsize: 155956
Current children cumulated CPU time (s) 1148.13
Current children cumulated vsize (Kb) 158080

[startup+1160.1 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 37164 0 0 0 115631 180 0 0 25 0 1 0 1851925442 160305152 34140 4294967295 134512640 135094434 3221224432 3221223088 134557879 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 39137 34140 145 145 0 38992 0
[pid=1737] vsize: 156548
Current children cumulated CPU time (s) 1158.13
Current children cumulated vsize (Kb) 158672

[startup+1170.1 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 37813 0 0 0 116625 183 0 0 25 0 1 0 1851925442 160555008 34195 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 39198 34195 145 145 0 39053 0
[pid=1737] vsize: 156792
Current children cumulated CPU time (s) 1168.1
Current children cumulated vsize (Kb) 158916

[startup+1180.1 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 37816 0 0 0 117626 183 0 0 25 0 1 0 1851925442 160555008 34198 4294967295 134512640 135094434 3221224432 3221223064 134557561 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 39198 34198 145 145 0 39053 0
[pid=1737] vsize: 156792
Current children cumulated CPU time (s) 1178.11
Current children cumulated vsize (Kb) 158916

[startup+1190.1 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 37889 0 0 0 118624 183 0 0 25 0 1 0 1851925442 160825344 34271 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 39264 34271 145 145 0 39119 0
[pid=1737] vsize: 157056
Current children cumulated CPU time (s) 1188.09
Current children cumulated vsize (Kb) 159180

[startup+1200.1 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 37926 0 0 0 119624 183 0 0 25 0 1 0 1851925442 160972800 34308 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 39300 34308 145 145 0 39155 0
[pid=1737] vsize: 157200
Current children cumulated CPU time (s) 1198.09
Current children cumulated vsize (Kb) 159324

[startup+1210.1 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 37995 0 0 0 120624 184 0 0 25 0 1 0 1851925442 161251328 34377 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 39368 34377 145 145 0 39223 0
[pid=1737] vsize: 157472
Current children cumulated CPU time (s) 1208.1
Current children cumulated vsize (Kb) 159596



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.1 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 1737
Raw data (/proc/1733/stat): 1733 (minisat+_script) S 1732 1733 19316 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1851925437 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/1733/statm): 531 226 485 147 0 384 0
[pid=1733] vsize: 2124
Raw data (/proc/1737/stat): 1737 (minisat+_64-bit) R 1733 1733 19316 0 -1 0 37995 0 0 0 120624 184 0 0 25 0 1 0 1851925442 161251328 34377 4294967295 134512640 135094434 3221224432 3221223056 134557650 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/1737/statm): 39368 34377 145 145 0 39223 0
[pid=1737] vsize: 157472
Current children cumulated CPU time (s) 1208.1
Current children cumulated vsize (Kb) 159596

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

Child status: 10
Real time (s): 1210.17
CPU time (s): 1208.15
CPU user time (s): 1206.24
CPU system time (s): 1.90871
CPU usage (%): 99.8329
Max. virtual memory (cumulated for all children) (Kb): 159596

Verifier Data

ERROR: no interpretation found !