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

Namesubmitted/een/normalized-lseu.opb
MD5SUMa578bf261896413ca78de4dc6db2447f
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 1120
Optimality of the best value was proved YES
Number of terms in the objective function 85
Biggest coefficient in the objective function 517
Number of bits for the biggest coefficient in the objective function 10
Sum of the numbers in the objective function 15494
Number of bits of the sum of numbers in the objective function 14
Biggest number in a constraint 1656
Number of bits of the biggest number in a constraint 11
Biggest sum of numbers in a constraint 15494
Number of bits of the biggest sum of numbers14
Best result obtained on this benchmarkOPTIMUM FOUND
Best CPU time to get the best result obtained on this benchmark526.298
Number of variables89
Total number of constraints28
Number of constraints which are clauses2
Number of constraints which are cardinality constraints (but not clauses)15
Number of constraints which are nor clauses,nor cardinality constraints11
Minimum length of a constraint2
Maximum length of a constraint47

Trace number 2196

Launcher Data

LAUNCH ON wulflinc27 THE 2005-09-18 18:19:16 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2616 boxname=wulflinc27 idbench=272 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  a578bf261896413ca78de4dc6db2447f  /oldhome/oroussel/tmp/wulflinc27/normalized-lseu.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc27/normalized-lseu.opb
IDLAUNCH: 2616
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.169
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.169
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:        911464 kB
Buffers:         35976 kB
Cached:          55264 kB
SwapCached:        764 kB
Active:          66848 kB
Inactive:        26984 kB
HighTotal:      131008 kB
HighFree:        73164 kB
LowTotal:       903652 kB
LowFree:        838300 kB
SwapTotal:     2097892 kB
SwapFree:      2096616 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5724 kB
Slab:            23864 kB
Committed_AS:    64232 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-18 18:28:02 (client local time) WITH STATUS 30 IN 526.298 SECONDS
stats: 2616 0 526.298 30

Solver Data

c Parsing PB file...
c Converting 28 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #
c   -- Clauses(.)/Splits(s): .....s
c ---[  26]---> BDD-cost:    3
c ---[  25]---> BDD-cost:    3
c ---[  24]---> BDD-cost:    3
c ---[  23]---> BDD-cost:    3
c ---[  22]---> BDD-cost:    3
c ---[  21]---> BDD-cost:    5
c ---[  20]---> BDD-cost:    5
c ---[  19]---> BDD-cost:    5
c ---[  17]---> BDD-cost:    5
c ---[  16]---> BDD-cost:    7
c ---[  15]---> BDD-cost:    7
c ---[  14]---> BDD-cost:    7
c ---[  13]---> BDD-cost:    7
c ---[  12]---> BDD-cost:    7
c ---[   9]---> BDD-cost:   11
c ---[   8]---> BDD-cost:   16
c ---[   7]---> BDD-cost:   28
c ---[   6]---> BDD-cost:  202
c ---[   4]---> Sorter-cost: 1747     Base: 5 2 2 2
c ---[   3]---> Sorter-cost: 1884     Base: 5 2 2 3
c ---[   1]---> Sorter-cost: 3158     Base: 5 2 2 3
c ---[   0]---> BDD-cost:   32
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   16046    38074 |    5348       0        0     nan |  0.000 % |
c |       100 |   15635    37138 |    5882      84      320     3.8 |  2.411 % |
c ==============================================================================
c Found solution: 4214
c ---[   0]---> Sorter-cost:12454     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       165 |   44577   104802 |   14859     126      495     3.9 |  2.411 % |
c |       265 |   44148   103822 |   16344     204     1226     6.0 |  2.633 % |
c |       416 |   42786   100729 |   17979     340     2419     7.1 |  4.977 % |
c ==============================================================================
c Found solution: 4091
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       516 |   43053   101446 |   14351     436     4111     9.4 |  4.977 % |
c |       617 |   42937   101186 |   15786     533     4805     9.0 |  5.472 % |
c ==============================================================================
c Found solution: 2600
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       640 |   43156   101738 |   14385     553     5096     9.2 |  5.472 % |
c ==============================================================================
c Found solution: 2564
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       733 |   43234   101950 |   14411     640     6902    10.8 |  5.472 % |
c |       833 |   42467   100186 |   15852     705     8115    11.5 |  7.152 % |
c |       984 |   42275    99752 |   17437     854    11226    13.1 |  7.490 % |
c |      1209 |   41845    98792 |   19181    1068    14405    13.5 |  8.265 % |
c ==============================================================================
c Found solution: 2366
c ---[   0]---> Sorter-cost:    3     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1405 |   41854    98818 |   13951    1262    19196    15.2 |  8.265 % |
c |      1505 |   41819    98739 |   15346    1359    20565    15.1 |  8.375 % |
c |      1658 |   41819    98739 |   16880    1512    22650    15.0 |  8.375 % |
c |      1886 |   41819    98739 |   18568    1740    26014    15.0 |  8.375 % |
c ==============================================================================
c Found solution: 2325
c ---[   0]---> Sorter-cost:    4     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2148 |   41870    98883 |   13956    2001    37066    18.5 |  8.375 % |
c |      2248 |   41870    98883 |   15351    2101    38353    18.3 |  8.415 % |
c |      2398 |   41718    98530 |   16886    2237    41178    18.4 |  8.688 % |
c ==============================================================================
c Found solution: 2113
c ---[   0]---> Sorter-cost:    6     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2526 |   41859    98891 |   13953    2365    43488    18.4 |  8.688 % |
c |      2626 |   41859    98891 |   15348    2465    45485    18.5 |  8.664 % |
c |      2776 |   40589    95970 |   16883    2550    46881    18.4 | 10.901 % |
c |      3001 |   40500    95764 |   18571    2771    49031    17.7 | 11.062 % |
c ==============================================================================
c Found solution: 2077
c ---[   0]---> Sorter-cost:    4     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3040 |   40584    95973 |   13528    2810    49423    17.6 | 11.062 % |
c |      3140 |   40559    95916 |   14880    2909    50766    17.5 | 11.092 % |
c |      3290 |   40559    95916 |   16368    3059    56749    18.6 | 11.092 % |
c |      3515 |   40515    95820 |   18005    3281    61210    18.7 | 11.184 % |
c |      3852 |   40515    95820 |   19806    3618    65648    18.1 | 11.184 % |
c |      4358 |   40515    95820 |   21786    4124    88847    21.5 | 11.184 % |
c |      5117 |   40196    95082 |   23965    4861   105377    21.7 | 11.755 % |
c ==============================================================================
c Found solution: 2039
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5461 |   40281    95290 |   13427    5205   111999    21.5 | 11.755 % |
c |      5561 |   40281    95290 |   14769    5305   113810    21.5 | 11.737 % |
c |      5713 |   40281    95290 |   16246    5457   119781    21.9 | 11.737 % |
c |      5941 |   40138    94960 |   17871    5682   123620    21.8 | 12.002 % |
c |      6278 |   40056    94769 |   19658    6012   139893    23.3 | 12.145 % |
c |      6785 |   40056    94769 |   21624    6519   154678    23.7 | 12.145 % |
c |      7544 |   40056    94769 |   23786    7278   185023    25.4 | 12.145 % |
c ==============================================================================
c Found solution: 2010
c ---[   0]---> Sorter-cost:    7     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7994 |   40046    94775 |   13348    7727   201707    26.1 | 12.145 % |
c |      8094 |   40046    94775 |   14682    7827   203566    26.0 | 12.180 % |
c |      8247 |   40046    94775 |   16151    7980   207754    26.0 | 12.180 % |
c |      8472 |   40046    94775 |   17766    8205   218952    26.7 | 12.180 % |
c |      8811 |   39869    94368 |   19542    8543   242672    28.4 | 12.478 % |
c |      9317 |   39869    94368 |   21497    9049   265341    29.3 | 12.479 % |
c |     10079 |   39716    94014 |   23646    9808   297070    30.3 | 12.725 % |
c ==============================================================================
c Found solution: 1959
c ---[   0]---> Sorter-cost:    4     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     10263 |   39721    94026 |   13240    9992   307859    30.8 | 12.725 % |
c |     10364 |   39721    94026 |   14564   10093   309197    30.6 | 12.729 % |
c |     10516 |   39721    94026 |   16020   10245   318608    31.1 | 12.729 % |
c |     10741 |   39642    93844 |   17622   10469   325530    31.1 | 12.855 % |
c |     11078 |   39642    93844 |   19384   10806   334232    30.9 | 12.855 % |
c |     11584 |   39642    93844 |   21323   11312   343314    30.3 | 12.855 % |
c |     12343 |   39642    93844 |   23455   12071   395208    32.7 | 12.855 % |
c ==============================================================================
c Found solution: 1886
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     13200 |   39659    93888 |   13219   12928   450474    34.8 | 12.855 % |
c |     13303 |   39659    93888 |   14540   13031   452979    34.8 | 12.853 % |
c |     13454 |   38672    91602 |   15994   13170   458874    34.8 | 14.632 % |
c |     13679 |   38263    90657 |   17594   13381   465007    34.8 | 15.366 % |
c |     14018 |   38263    90657 |   19353   13720   474081    34.6 | 15.366 % |
c |     14524 |   38117    90317 |   21289   14212   486103    34.2 | 15.647 % |
c |     15284 |   38117    90317 |   23418   14972   516201    34.5 | 15.647 % |
c |     16423 |   38096    90271 |   25760   16110   576733    35.8 | 15.688 % |
c |     18132 |   38096    90271 |   28336   17819   637141    35.8 | 15.687 % |
c ==============================================================================
c Found solution: 1856
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19713 |   37961    89969 |   12653   19397   724840    37.4 | 15.687 % |
c |     19814 |   37961    89969 |   13918    9800   342591    35.0 | 15.953 % |
c |     19964 |   37961    89969 |   15310    9950   348722    35.0 | 15.953 % |
c |     20191 |   37961    89969 |   16841   10177   365079    35.9 | 15.953 % |
c |     20528 |   37757    89497 |   18525   10510   372889    35.5 | 16.320 % |
c |     21038 |   37757    89497 |   20377   11020   391939    35.6 | 16.320 % |
c |     21797 |   37757    89497 |   22415   11779   428095    36.3 | 16.320 % |
c |     22936 |   37757    89497 |   24657   12918   478718    37.1 | 16.320 % |
c |     24644 |   37739    89455 |   27122   14624   564886    38.6 | 16.354 % |
c |     27206 |   37739    89455 |   29835   17186   670859    39.0 | 16.356 % |
c ==============================================================================
c Found solution: 1839
c ---[   0]---> Sorter-cost:    4     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     28163 |   37595    89142 |   12531   18140   701282    38.7 | 16.356 % |
c ==============================================================================
c Found solution: 1664
c ---[   0]---> Sorter-cost:    2     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     28226 |   37603    89161 |   12534    9133   312313    34.2 | 16.356 % |
c |     28329 |   37381    88644 |   13787    9234   317012    34.3 | 17.034 % |
c |     28480 |   37342    88554 |   15166    9384   320198    34.1 | 17.108 % |
c |     28706 |   37342    88554 |   16682    9610   330983    34.4 | 17.108 % |
c |     29043 |   37319    88502 |   18351    9946   337229    33.9 | 17.148 % |
c |     29551 |   37253    88349 |   20186   10451   354605    33.9 | 17.263 % |
c |     30310 |   37253    88349 |   22204   11210   376924    33.6 | 17.263 % |
c |     31450 |   37176    88173 |   24425   12348   421282    34.1 | 17.395 % |
c ==============================================================================
c Found solution: 1652
c ---[   0]---> Sorter-cost:    3     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     32430 |   37181    88185 |   12393   13328   478161    35.9 | 17.395 % |
c |     32531 |   37181    88185 |   13632   13429   481643    35.9 | 17.398 % |
c ==============================================================================
c Found solution: 1651
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     32556 |   37188    88201 |   12396   13454   483056    35.9 | 17.398 % |
c |     32657 |   37188    88201 |   13635   13555   488293    36.0 | 17.399 % |
c ==============================================================================
c Found solution: 1645
c ---[   0]---> Sorter-cost:    2     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     32681 |   37193    88212 |   12397   13579   489409    36.0 | 17.399 % |
c ==============================================================================
c Found solution: 1641
c ---[   0]---> Sorter-cost:    4     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     32709 |   37199    88239 |   12399   13607   490510    36.0 | 17.399 % |
c ==============================================================================
c Found solution: 1626
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     32722 |   37206    88255 |   12402   13620   491045    36.1 | 17.399 % |
c ==============================================================================
c Found solution: 1572
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     32812 |   37222    88295 |   12407   13710   495909    36.2 | 17.399 % |
c |     32912 |   37222    88295 |   13647   13810   500499    36.2 | 17.401 % |
c |     33062 |   37222    88295 |   15012   13960   505960    36.2 | 17.401 % |
c |     33288 |   37222    88295 |   16513   14186   515084    36.3 | 17.401 % |
c ==============================================================================
c Found solution: 1569
c ---[   0]---> Sorter-cost:    3     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     33417 |   37227    88310 |   12409   14315   523217    36.6 | 17.401 % |
c |     33523 |   37227    88310 |   13649   14421   526997    36.5 | 17.403 % |
c ==============================================================================
c Found solution: 1561
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     33536 |   37233    88325 |   12411   14434   527364    36.5 | 17.403 % |
c |     33636 |   37233    88325 |   13652   14534   532924    36.7 | 17.405 % |
c |     33786 |   37233    88325 |   15017   14684   542227    36.9 | 17.405 % |
c ==============================================================================
c Found solution: 1553
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     33951 |   37239    88340 |   12413   14849   553272    37.3 | 17.405 % |
c ==============================================================================
c Found solution: 1538
c ---[   0]---> Sorter-cost:    4     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     34010 |   37245    88354 |   12415   14908   556476    37.3 | 17.405 % |
c ==============================================================================
c Found solution: 1472
c ---[   0]---> Sorter-cost:    2     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     34072 |   37250    88365 |   12416   14970   558955    37.3 | 17.405 % |
c ==============================================================================
c Found solution: 1456
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     34088 |   37256    88378 |   12418   14986   559491    37.3 | 17.405 % |
c ==============================================================================
c Found solution: 1452
c ---[   0]---> Sorter-cost:    4     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     34119 |   37263    88397 |   12421   15017   560717    37.3 | 17.405 % |
c |     34223 |   37263    88397 |   13663   15121   564578    37.3 | 17.415 % |
c |     34374 |   37263    88397 |   15029   15272   566776    37.1 | 17.415 % |
c |     34600 |   37212    88281 |   16532   15497   570014    36.8 | 17.507 % |
c |     34937 |   37212    88281 |   18185   15834   579121    36.6 | 17.507 % |
c |     35443 |   37200    88253 |   20004   16339   598956    36.7 | 17.530 % |
c |     36204 |   37200    88253 |   22004   17100   610536    35.7 | 17.530 % |
c |     37345 |   37200    88253 |   24205   18241   664918    36.5 | 17.530 % |
c ==============================================================================
c Found solution: 1447
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     37458 |   37206    88268 |   12402   18354   668483    36.4 | 17.530 % |
c |     37559 |   37206    88268 |   13642    9278   289999    31.3 | 17.531 % |
c |     37710 |   37206    88268 |   15006    9429   292072    31.0 | 17.531 % |
c |     37935 |   37206    88268 |   16507    9654   294931    30.6 | 17.532 % |
c ==============================================================================
c Found solution: 1443
c ---[   0]---> Sorter-cost:    4     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     38158 |   37211    88295 |   12403    9877   303179    30.7 | 17.532 % |
c |     38258 |   37211    88295 |   13643    9977   306001    30.7 | 17.533 % |
c |     38410 |   37211    88295 |   15007   10129   311348    30.7 | 17.533 % |
c |     38635 |   37211    88295 |   16508   10354   318865    30.8 | 17.533 % |
c |     38972 |   37211    88295 |   18159   10691   334629    31.3 | 17.533 % |
c ==============================================================================
c Found solution: 1416
c ---[   0]---> Sorter-cost:    2     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     39137 |   37214    88302 |   12404   10856   341941    31.5 | 17.533 % |
c |     39237 |   37214    88302 |   13644   10956   346578    31.6 | 17.537 % |
c ==============================================================================
c Found solution: 1408
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     39385 |   37222    88321 |   12407   11104   354963    32.0 | 17.537 % |
c |     39486 |   37222    88321 |   13647   11205   359650    32.1 | 17.538 % |
c ==============================================================================
c Found solution: 1402
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     39559 |   37228    88336 |   12409   11278   363189    32.2 | 17.538 % |
c |     39660 |   37228    88336 |   13649   11379   369106    32.4 | 17.539 % |
c |     39810 |   37228    88336 |   15014   11529   374970    32.5 | 17.539 % |
c ==============================================================================
c Found solution: 1394
c ---[   0]---> Sorter-cost:    3     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     39904 |   37232    88346 |   12410   11623   382319    32.9 | 17.539 % |
c ==============================================================================
c Found solution: 1377
c ---[   0]---> Sorter-cost:    2     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     39989 |   37235    88353 |   12411   11708   385879    33.0 | 17.539 % |
c ==============================================================================
c Found solution: 1358
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     40014 |   37242    88369 |   12414   11733   386311    32.9 | 17.539 % |
c ==============================================================================
c Found solution: 1338
c ---[   0]---> Sorter-cost:    3     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     40098 |   37247    88381 |   12415   11817   391980    33.2 | 17.539 % |
c ==============================================================================
c Found solution: 1321
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     40114 |   37254    88397 |   12418   11833   393663    33.3 | 17.539 % |
c |     40215 |   37254    88397 |   13659   11934   398464    33.4 | 17.552 % |
c ==============================================================================
c Found solution: 1315
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     40255 |   37261    88413 |   12420   11974   401118    33.5 | 17.552 % |
c |     40356 |   37261    88413 |   13662   12075   405622    33.6 | 17.553 % |
c ==============================================================================
c Found solution: 1270
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     40457 |   37278    88469 |   12426   12176   409843    33.7 | 17.553 % |
c |     40557 |   37278    88469 |   13668   12276   414230    33.7 | 17.548 % |
c |     40708 |   37278    88469 |   15035   12427   421195    33.9 | 17.548 % |
c |     40935 |   37278    88469 |   16539   12654   429895    34.0 | 17.548 % |
c ==============================================================================
c Found solution: 1260
c ---[   0]---> Sorter-cost:    2     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     41007 |   37282    88481 |   12427   12726   433324    34.1 | 17.548 % |
c |     41108 |   37282    88481 |   13669   12827   435629    34.0 | 17.551 % |
c |     41258 |   37282    88481 |   15036   12977   442812    34.1 | 17.551 % |
c |     41483 |   37282    88481 |   16540   13202   450647    34.1 | 17.551 % |
c |     41820 |   37282    88481 |   18194   13539   465424    34.4 | 17.551 % |
c ==============================================================================
c Found solution: 1251
c ---[   0]---> Sorter-cost:    3     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     41958 |   37286    88491 |   12428   13677   472983    34.6 | 17.551 % |
c |     42058 |   37286    88491 |   13670   13777   475577    34.5 | 17.554 % |
c |     42209 |   37286    88491 |   15037   13928   480858    34.5 | 17.554 % |
c |     42434 |   37286    88491 |   16541   14153   489371    34.6 | 17.554 % |
c |     42771 |   37286    88491 |   18195   14490   504565    34.8 | 17.554 % |
c ==============================================================================
c Found solution: 1236
c ---[   0]---> Sorter-cost:    3     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     43097 |   37290    88501 |   12430   14816   517926    35.0 | 17.554 % |
c |     43201 |   37290    88501 |   13673   14920   520576    34.9 | 17.556 % |
c |     43352 |   37290    88501 |   15040   15071   524544    34.8 | 17.556 % |
c |     43578 |   37290    88501 |   16544   15297   529541    34.6 | 17.556 % |
c |     43915 |   37249    88407 |   18198   15632   546898    35.0 | 17.630 % |
c |     44421 |   37249    88407 |   20018   16138   572561    35.5 | 17.630 % |
c |     45180 |   37249    88407 |   22020   16897   599477    35.5 | 17.630 % |
c |     46319 |   37249    88407 |   24222   18036   663826    36.8 | 17.630 % |
c |     48027 |   37159    88200 |   26644   19742   733345    37.1 | 17.784 % |
c ==============================================================================
c Found solution: 1232
c ---[   0]---> Sorter-cost:    2     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     48159 |   37162    88207 |   12387   19874   739448    37.2 | 17.784 % |
c |     48261 |   37162    88207 |   13625   10039   311227    31.0 | 17.788 % |
c |     48411 |   37162    88207 |   14988   10189   320968    31.5 | 17.788 % |
c |     48636 |   37162    88207 |   16487   10414   330060    31.7 | 17.788 % |
c |     48976 |   37162    88207 |   18135   10754   347428    32.3 | 17.788 % |
c |     49482 |   37162    88207 |   19949   11260   374286    33.2 | 17.788 % |
c ==============================================================================
c Found solution: 1224
c ---[   0]---> Sorter-cost:    4     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     49511 |   37168    88221 |   12389   11289   375722    33.3 | 17.788 % |
c |     49611 |   37168    88221 |   13627   11389   377638    33.2 | 17.790 % |
c |     49762 |   37168    88221 |   14990   11540   379388    32.9 | 17.790 % |
c |     49987 |   37168    88221 |   16489   11765   382453    32.5 | 17.790 % |
c |     50324 |   37168    88221 |   18138   12102   386606    31.9 | 17.790 % |
c |     50830 |   37095    88046 |   19952   12607   411468    32.6 | 17.926 % |
c |     51589 |   37095    88046 |   21947   13366   457483    34.2 | 17.926 % |
c ==============================================================================
c Found solution: 1164
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     51730 |   37102    88062 |   12367   13507   463432    34.3 | 17.926 % |
c ==============================================================================
c Found solution: 1149
c ---[   0]---> Sorter-cost:    3     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     51773 |   37106    88071 |   12368   13550   465084    34.3 | 17.926 % |
c ==============================================================================
c Found solution: 1145
c ---[   0]---> Sorter-cost:    4     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     51800 |   37111    88082 |   12370   13577   466661    34.4 | 17.926 % |
c |     51901 |   37111    88082 |   13607   13678   470120    34.4 | 17.935 % |
c |     52053 |   37050    87942 |   14967   13829   473685    34.3 | 18.043 % |
c |     52280 |   36992    87807 |   16464   14054   482775    34.4 | 18.140 % |
c |     52617 |   36992    87807 |   18110   14391   494648    34.4 | 18.140 % |
c |     53123 |   36932    87669 |   19922   14896   514713    34.6 | 18.248 % |
c |     53883 |   36905    87606 |   21914   15654   548585    35.0 | 18.305 % |
c |     55023 |   36839    87452 |   24105   16790   597435    35.6 | 18.430 % |
c |     56732 |   36839    87452 |   26516   18499   683813    37.0 | 18.430 % |
c |     59294 |   36575    86839 |   29167   21056   779119    37.0 | 18.891 % |
c ==============================================================================
c Found solution: 1143
c ---[   0]---> Sorter-cost:    1     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     62257 |   36529    86733 |   12176   24018   940108    39.1 | 18.891 % |
c |     62357 |   36529    86733 |   13393   12109   411396    34.0 | 18.968 % |
c |     62507 |   36529    86733 |   14732   12259   416196    34.0 | 18.968 % |
c |     62736 |   36529    86733 |   16206   12488   424299    34.0 | 18.968 % |
c |     63074 |   36525    86724 |   17826   12824   435716    34.0 | 18.973 % |
c |     63580 |   36525    86724 |   19609   13330   453755    34.0 | 18.973 % |
c |     64340 |   36525    86724 |   21570   14090   483252    34.3 | 18.973 % |
c |     65480 |   36525    86724 |   23727   15230   531010    34.9 | 18.973 % |
c ==============================================================================
c Found solution: 1136
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     66364 |   36531    86739 |   12177   16114   566145    35.1 | 18.973 % |
c |     66465 |   36531    86739 |   13394    8158   210937    25.9 | 18.975 % |
c |     66617 |   36531    86739 |   14734    8310   214915    25.9 | 18.975 % |
c |     66845 |   36531    86739 |   16207    8538   226913    26.6 | 18.975 % |
c |     67185 |   36531    86739 |   17828    8878   240121    27.0 | 18.975 % |
c |     67691 |   36531    86739 |   19611    9384   254470    27.1 | 18.975 % |
c |     68450 |   36531    86739 |   21572   10143   285357    28.1 | 18.975 % |
c |     69589 |   36531    86739 |   23729   11282   325499    28.9 | 18.975 % |
c |     71298 |   36531    86739 |   26102   12991   388992    29.9 | 18.975 % |
c |     73862 |   36531    86739 |   28712   15555   499400    32.1 | 18.975 % |
c |     77706 |   36531    86739 |   31584   19399   641893    33.1 | 18.975 % |
c |     83473 |   36531    86739 |   34742   25166   851867    33.8 | 18.975 % |
c ==============================================================================
c Found solution: 1128
c ---[   0]---> Sorter-cost:10819     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     83855 |   48846   115593 |   16282    9881   252889    25.6 | 18.975 % |
c |     83955 |   48846   115593 |   17910    9981   256387    25.7 | 13.426 % |
c |     84108 |   48846   115593 |   19701   10134   262174    25.9 | 13.426 % |
c |     84335 |   48846   115593 |   21671   10361   273735    26.4 | 13.426 % |
c |     84674 |   48846   115593 |   23838   10700   287638    26.9 | 13.426 % |
c |     85180 |   48846   115593 |   26222   11206   302850    27.0 | 13.426 % |
c |     85939 |   48846   115593 |   28844   11965   328037    27.4 | 13.426 % |
c |     87080 |   48846   115593 |   31729   13106   363663    27.7 | 13.426 % |
c |     88789 |   48846   115593 |   34901   14815   448569    30.3 | 13.426 % |
c |     91351 |   48842   115584 |   38392   17376   574966    33.1 | 13.430 % |
c |     95195 |   48842   115584 |   42231   21220   715548    33.7 | 13.430 % |
c |    100962 |   48832   115561 |   46454   26986   948975    35.2 | 13.441 % |
c ==============================================================================
c Found solution: 1120
c ---[   0]---> Sorter-cost:    6     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    102576 |   58954   139062 |   19651   28600   999476    34.9 | 13.441 % |
c |    102676 |   58954   139062 |   21616   14400   427455    29.7 | 16.672 % |
c |    102826 |   58954   139062 |   23777   14550   429765    29.5 | 16.672 % |
c |    103052 |   58954   139062 |   26155   14776   433516    29.3 | 16.672 % |
c |    103390 |   58314   137610 |   28771   14316   428116    29.9 | 17.465 % |
c |    103898 |   58250   137467 |   31648   14819   442265    29.8 | 17.541 % |
c |    104661 |   58250   137467 |   34812   15582   470141    30.2 | 17.541 % |
c |    105802 |   58250   137467 |   38294   16723   498243    29.8 | 17.541 % |
c |    107510 |   58250   137467 |   42123   18431   562484    30.5 | 17.541 % |
c |    110076 |   58250   137467 |   46336   20997   665926    31.7 | 17.541 % |
c |    113921 |   58250   137467 |   50969   24842   808229    32.5 | 17.541 % |
c ==============================================================================
c Optimal solution: 1120
s OPTIMUM FOUND
v x0 x1 -x2 -x3 -x4 -x5 -x6 -x7 -x8 x9 -x10 -x11 -x12 -x13 -x14 -x15 -x16 -x17 -x18 -x19 -x20 -x21 x22 -x23 -x24 -x25 -x26 -x27 -x28 -x29 x30 -x31 -x32 -x33 x34 -x35 -x36 -x37 x38 -x39 -x40 -x41 -x42 -x43 -x44 -x45 x46 -x47 x48 -x49 -x50 -x51 -x52 -x53 -x54 -x55 -x56 -x57 -x58 x59 -x60 x61 -x62 -x63 -x64 -x65 -x66 -x67 -x68 -x69 -x70 -x71 -x72 -x73 -x74 -x75 -x76 -x77 -x78 -x79 -x80 x81 -x82 -x83 -x84 -x85 x86 -x87 -x88
c _______________________________________________________________________________
c 
c restarts              : 222
c conflicts             : 114741         (218 /sec)
c decisions             : 222002         (422 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 525.999 s
c _______________________________________________________________________________

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/9468/stat): 9468 (minisat+_script) R 9467 9468 28974 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1843345786 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/9468/statm): 174 3 169 147 0 27 0
[pid=9468] 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=9469
New process pid=9470
New process pid=9471
execve syscall for /bin/sed executable
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
One traced child (pid=9470) exited with status: 0
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=9471) exited with status: 0
One traced child (pid=9469) exited with status: 0
New process pid=9472
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc27/normalized-lseu.opb

[startup+10.0035 s]
Raw data (loadavg): 0.93 0.96 0.92 2/57 9472
Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9468/statm): 531 226 485 147 0 384 0
[pid=9468] vsize: 2124
Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 1621 0 0 0 984 5 0 0 25 0 1 0 1843345791 7946240 1597 4294967295 134512640 135094434 3221224448 3221223104 134557882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9472/statm): 1940 1597 145 145 0 1795 0
[pid=9472] vsize: 7760
Current children cumulated CPU time (s) 9.89
Current children cumulated vsize (Kb) 9884

[startup+20.0053 s]
Raw data (loadavg): 0.94 0.96 0.92 2/57 9472
Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9468/statm): 531 226 485 147 0 384 0
[pid=9468] vsize: 2124
Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 1777 0 0 0 1981 6 0 0 25 0 1 0 1843345791 8585216 1753 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9472/statm): 2096 1753 145 145 0 1951 0
[pid=9472] vsize: 8384
Current children cumulated CPU time (s) 19.87
Current children cumulated vsize (Kb) 10508

[startup+30.0071 s]
Raw data (loadavg): 0.95 0.96 0.92 2/57 9472
Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9468/statm): 531 226 485 147 0 384 0
[pid=9468] vsize: 2124
Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 1959 0 0 0 2977 8 0 0 25 0 1 0 1843345791 9355264 1935 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9472/statm): 2284 1935 145 145 0 2139 0
[pid=9472] vsize: 9136
Current children cumulated CPU time (s) 29.85
Current children cumulated vsize (Kb) 11260

[startup+40.0079 s]
Raw data (loadavg): 0.96 0.96 0.92 2/57 9472
Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9468/statm): 531 226 485 147 0 384 0
[pid=9468] vsize: 2124
Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) T 9468 9468 28974 0 -1 0 2118 0 0 0 3975 9 0 0 25 0 1 0 1843345791 9986048 2094 4294967295 134512640 135094434 3221224448 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/9472/statm): 2438 2094 145 145 0 2293 0
[pid=9472] vsize: 9752
Current children cumulated CPU time (s) 39.84
Current children cumulated vsize (Kb) 11876

[startup+50.0088 s]
Raw data (loadavg): 0.96 0.96 0.92 2/57 9472
Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9468/statm): 531 226 485 147 0 384 0
[pid=9468] vsize: 2124
Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 2263 0 0 0 4972 10 0 0 25 0 1 0 1843345791 10571776 2239 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9472/statm): 2581 2239 145 145 0 2436 0
[pid=9472] vsize: 10324
Current children cumulated CPU time (s) 49.82
Current children cumulated vsize (Kb) 12448

[startup+60.0096 s]
Raw data (loadavg): 0.97 0.96 0.92 2/57 9472
Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9468/statm): 531 226 485 147 0 384 0
[pid=9468] vsize: 2124
Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 2389 0 0 0 5971 11 0 0 25 0 1 0 1843345791 11141120 2365 4294967295 134512640 135094434 3221224448 3221223136 134554687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/9472/statm): 2720 2365 145 145 0 2575 0
[pid=9472] vsize: 10880
Current children cumulated CPU time (s) 59.82
Current children cumulated vsize (Kb) 13004

[startup+70.0104 s]
Raw data (loadavg): 0.97 0.96 0.92 2/57 9472
Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9468/statm): 531 226 485 147 0 384 0
[pid=9468] vsize: 2124
Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 2452 0 0 0 6969 11 0 0 25 0 1 0 1843345791 11395072 2428 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9472/statm): 2782 2428 145 145 0 2637 0
[pid=9472] vsize: 11128
Current children cumulated CPU time (s) 69.8
Current children cumulated vsize (Kb) 13252

[startup+80.0122 s]
Raw data (loadavg): 0.98 0.96 0.92 2/57 9472
Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9468/statm): 531 226 485 147 0 384 0
[pid=9468] vsize: 2124
Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 2452 0 0 0 7969 12 0 0 25 0 1 0 1843345791 11395072 2428 4294967295 134512640 135094434 3221224448 3221223072 134557630 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9472/statm): 2782 2428 145 145 0 2637 0
[pid=9472] vsize: 11128
Current children cumulated CPU time (s) 79.81
Current children cumulated vsize (Kb) 13252

[startup+90.013 s]
Raw data (loadavg): 0.98 0.96 0.92 2/57 9472
Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9468/statm): 531 226 485 147 0 384 0
[pid=9468] vsize: 2124
Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 2460 0 0 0 8970 12 0 0 25 0 1 0 1843345791 11431936 2436 4294967295 134512640 135094434 3221224448 3221223136 134554687 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9472/statm): 2791 2436 145 145 0 2646 0
[pid=9472] vsize: 11164
Current children cumulated CPU time (s) 89.82
Current children cumulated vsize (Kb) 13288

[startup+100.014 s]
Raw data (loadavg): 0.98 0.96 0.92 2/57 9472
Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9468/statm): 531 226 485 147 0 384 0
[pid=9468] vsize: 2124
Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 2486 0 0 0 9969 12 0 0 25 0 1 0 1843345791 11534336 2462 4294967295 134512640 135094434 3221224448 3221223136 134554717 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9472/statm): 2816 2462 145 145 0 2671 0
[pid=9472] vsize: 11264
Current children cumulated CPU time (s) 99.81
Current children cumulated vsize (Kb) 13388

[startup+110.016 s]
Raw data (loadavg): 0.98 0.97 0.92 2/57 9472
Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9468/statm): 531 226 485 147 0 384 0
[pid=9468] vsize: 2124
Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 2486 0 0 0 10969 12 0 0 25 0 1 0 1843345791 11534336 2462 4294967295 134512640 135094434 3221224448 3221223104 134558208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9472/statm): 2816 2462 145 145 0 2671 0
[pid=9472] vsize: 11264
Current children cumulated CPU time (s) 109.81
Current children cumulated vsize (Kb) 13388

[startup+120.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 9472
Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9468/statm): 531 226 485 147 0 384 0
[pid=9468] vsize: 2124
Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 2486 0 0 0 11969 12 0 0 25 0 1 0 1843345791 11534336 2462 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9472/statm): 2816 2462 145 145 0 2671 0
[pid=9472] vsize: 11264
Current children cumulated CPU time (s) 119.81
Current children cumulated vsize (Kb) 13388

[startup+130.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 9472
Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9468/statm): 531 226 485 147 0 384 0
[pid=9468] vsize: 2124
Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 2486 0 0 0 12969 12 0 0 25 0 1 0 1843345791 11534336 2462 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9472/statm): 2816 2462 145 145 0 2671 0
[pid=9472] vsize: 11264
Current children cumulated CPU time (s) 129.81
Current children cumulated vsize (Kb) 13388

[startup+140.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 9472
Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9468/statm): 531 226 485 147 0 384 0
[pid=9468] vsize: 2124
Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 2486 0 0 0 13969 13 0 0 25 0 1 0 1843345791 11534336 2462 4294967295 134512640 135094434 3221224448 3221223088 134562224 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9472/statm): 2816 2462 145 145 0 2671 0
[pid=9472] vsize: 11264
Current children cumulated CPU time (s) 139.82
Current children cumulated vsize (Kb) 13388

[startup+150.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 9472
Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9468/statm): 531 226 485 147 0 384 0
[pid=9468] vsize: 2124
Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 2487 0 0 0 14969 13 0 0 25 0 1 0 1843345791 11534336 2463 4294967295 134512640 135094434 3221224448 3221221488 134519148 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9472/statm): 2816 2463 145 145 0 2671 0
[pid=9472] vsize: 11264
Current children cumulated CPU time (s) 149.82
Current children cumulated vsize (Kb) 13388

[startup+160.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 9472
Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9468/statm): 531 226 485 147 0 384 0
[pid=9468] vsize: 2124
Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 2487 0 0 0 15970 13 0 0 25 0 1 0 1843345791 11534336 2463 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9472/statm): 2816 2463 145 145 0 2671 0
[pid=9472] vsize: 11264
Current children cumulated CPU time (s) 159.83
Current children cumulated vsize (Kb) 13388

[startup+170.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 9472
Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9468/statm): 531 226 485 147 0 384 0
[pid=9468] vsize: 2124
Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 2490 0 0 0 16970 13 0 0 25 0 1 0 1843345791 11546624 2466 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9472/statm): 2819 2466 145 145 0 2674 0
[pid=9472] vsize: 11276
Current children cumulated CPU time (s) 169.83
Current children cumulated vsize (Kb) 13400

[startup+180.022 s]
Raw data (loadavg): 0.99 0.97 0.92 1/57 9472
Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9468/statm): 531 226 485 147 0 384 0
[pid=9468] vsize: 2124
Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) T 9468 9468 28974 0 -1 0 2591 0 0 0 17967 14 0 0 25 0 1 0 1843345791 11968512 2567 4294967295 134512640 135094434 3221224448 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/9472/statm): 2922 2567 145 145 0 2777 0
[pid=9472] vsize: 11688
Current children cumulated CPU time (s) 179.81
Current children cumulated vsize (Kb) 13812

[startup+190.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 9472
Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9468/statm): 531 226 485 147 0 384 0
[pid=9468] vsize: 2124
Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 2616 0 0 0 18967 14 0 0 25 0 1 0 1843345791 12070912 2592 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9472/statm): 2947 2592 145 145 0 2802 0
[pid=9472] vsize: 11788
Current children cumulated CPU time (s) 189.81
Current children cumulated vsize (Kb) 13912

[startup+200.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 9472
Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9468/statm): 531 226 485 147 0 384 0
[pid=9468] vsize: 2124
Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 2616 0 0 0 19967 14 0 0 25 0 1 0 1843345791 12070912 2592 4294967295 134512640 135094434 3221224448 3221223040 134556812 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9472/statm): 2947 2592 145 145 0 2802 0
[pid=9472] vsize: 11788
Current children cumulated CPU time (s) 199.81
Current children cumulated vsize (Kb) 13912

[startup+210.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 9472
Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9468/statm): 531 226 485 147 0 384 0
[pid=9468] vsize: 2124
Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 2616 0 0 0 20967 14 0 0 25 0 1 0 1843345791 12070912 2592 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9472/statm): 2947 2592 145 145 0 2802 0
[pid=9472] vsize: 11788
Current children cumulated CPU time (s) 209.81
Current children cumulated vsize (Kb) 13912

[startup+220.026 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 9472
Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9468/statm): 531 226 485 147 0 384 0
[pid=9468] vsize: 2124
Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 2616 0 0 0 21968 14 0 0 25 0 1 0 1843345791 12070912 2592 4294967295 134512640 135094434 3221224448 3221223136 134554685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9472/statm): 2947 2592 145 145 0 2802 0
[pid=9472] vsize: 11788
Current children cumulated CPU time (s) 219.82
Current children cumulated vsize (Kb) 13912

[startup+230.028 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 9472
Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9468/statm): 531 226 485 147 0 384 0
[pid=9468] vsize: 2124
Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 2628 0 0 0 22968 14 0 0 25 0 1 0 1843345791 12115968 2604 4294967295 134512640 135094434 3221224448 3221223040 134557227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9472/statm): 2958 2604 145 145 0 2813 0
[pid=9472] vsize: 11832
Current children cumulated CPU time (s) 229.82
Current children cumulated vsize (Kb) 13956

[startup+240.028 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 9472
Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9468/statm): 531 226 485 147 0 384 0
[pid=9468] vsize: 2124
Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 2734 0 0 0 23965 15 0 0 25 0 1 0 1843345791 12541952 2710 4294967295 134512640 135094434 3221224448 3221223072 134557737 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9472/statm): 3062 2710 145 145 0 2917 0
[pid=9472] vsize: 12248
Current children cumulated CPU time (s) 239.8
Current children cumulated vsize (Kb) 14372

[startup+250.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 9472
Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9468/statm): 531 226 485 147 0 384 0
[pid=9468] vsize: 2124
Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 2853 0 0 0 24963 17 0 0 25 0 1 0 1843345791 13033472 2829 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9472/statm): 3182 2829 145 145 0 3037 0
[pid=9472] vsize: 12728
Current children cumulated CPU time (s) 249.8
Current children cumulated vsize (Kb) 14852

[startup+260.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 9472
Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9468/statm): 531 226 485 147 0 384 0
[pid=9468] vsize: 2124
Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 2870 0 0 0 25963 17 0 0 25 0 1 0 1843345791 13103104 2846 4294967295 134512640 135094434 3221224448 3221223040 134557004 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9472/statm): 3199 2846 145 145 0 3054 0
[pid=9472] vsize: 12796
Current children cumulated CPU time (s) 259.8
Current children cumulated vsize (Kb) 14920

[startup+270.031 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 9472
Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9468/statm): 531 226 485 147 0 384 0
[pid=9468] vsize: 2124
Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 2876 0 0 0 26963 17 0 0 25 0 1 0 1843345791 13127680 2852 4294967295 134512640 135094434 3221224448 3221223120 134555568 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9472/statm): 3205 2852 145 145 0 3060 0
[pid=9472] vsize: 12820
Current children cumulated CPU time (s) 269.8
Current children cumulated vsize (Kb) 14944

[startup+280.032 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 9472
Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9468/statm): 531 226 485 147 0 384 0
[pid=9468] vsize: 2124
Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 2876 0 0 0 27963 17 0 0 25 0 1 0 1843345791 13127680 2852 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9472/statm): 3205 2852 145 145 0 3060 0
[pid=9472] vsize: 12820
Current children cumulated CPU time (s) 279.8
Current children cumulated vsize (Kb) 14944

[startup+290.032 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 9472
Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9468/statm): 531 226 485 147 0 384 0
[pid=9468] vsize: 2124
Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 2876 0 0 0 28963 17 0 0 25 0 1 0 1843345791 13127680 2852 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9472/statm): 3205 2852 145 145 0 3060 0
[pid=9472] vsize: 12820
Current children cumulated CPU time (s) 289.8
Current children cumulated vsize (Kb) 14944

[startup+300.033 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 9472
Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9468/statm): 531 226 485 147 0 384 0
[pid=9468] vsize: 2124
Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 2876 0 0 0 29964 17 0 0 25 0 1 0 1843345791 13127680 2852 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9472/statm): 3205 2852 145 145 0 3060 0
[pid=9472] vsize: 12820
Current children cumulated CPU time (s) 299.81
Current children cumulated vsize (Kb) 14944

[startup+310.034 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 9472
Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9468/statm): 531 226 485 147 0 384 0
[pid=9468] vsize: 2124
Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 2876 0 0 0 30964 17 0 0 25 0 1 0 1843345791 13127680 2852 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9472/statm): 3205 2852 145 145 0 3060 0
[pid=9472] vsize: 12820
Current children cumulated CPU time (s) 309.81
Current children cumulated vsize (Kb) 14944

[startup+320.035 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 9472
Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9468/statm): 531 226 485 147 0 384 0
[pid=9468] vsize: 2124
Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 2876 0 0 0 31964 17 0 0 25 0 1 0 1843345791 13127680 2852 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9472/statm): 3205 2852 145 145 0 3060 0
[pid=9472] vsize: 12820
Current children cumulated CPU time (s) 319.81
Current children cumulated vsize (Kb) 14944

[startup+330.036 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 9472
Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9468/statm): 531 226 485 147 0 384 0
[pid=9468] vsize: 2124
Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 2879 0 0 0 32964 17 0 0 25 0 1 0 1843345791 13144064 2855 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9472/statm): 3209 2855 145 145 0 3064 0
[pid=9472] vsize: 12836
Current children cumulated CPU time (s) 329.81
Current children cumulated vsize (Kb) 14960

[startup+340.037 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 9472
Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9468/statm): 531 226 485 147 0 384 0
[pid=9468] vsize: 2124
Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 2891 0 0 0 33965 17 0 0 25 0 1 0 1843345791 13209600 2867 4294967295 134512640 135094434 3221224448 3221223040 134556765 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9472/statm): 3225 2867 145 145 0 3080 0
[pid=9472] vsize: 12900
Current children cumulated CPU time (s) 339.82
Current children cumulated vsize (Kb) 15024

[startup+350.037 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 9472
Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9468/statm): 531 226 485 147 0 384 0
[pid=9468] vsize: 2124
Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 2904 0 0 0 34965 17 0 0 25 0 1 0 1843345791 13307904 2880 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9472/statm): 3249 2880 145 145 0 3104 0
[pid=9472] vsize: 12996
Current children cumulated CPU time (s) 349.82
Current children cumulated vsize (Kb) 15120

[startup+360.039 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 9472
Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9468/statm): 531 226 485 147 0 384 0
[pid=9468] vsize: 2124
Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 3163 0 0 0 35964 18 0 0 25 0 1 0 1843345791 13574144 3097 4294967295 134512640 135094434 3221224448 3221223072 134557726 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9472/statm): 3314 3097 145 145 0 3169 0
[pid=9472] vsize: 13256
Current children cumulated CPU time (s) 359.82
Current children cumulated vsize (Kb) 15380

[startup+370.039 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 9472
Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9468/statm): 531 226 485 147 0 384 0
[pid=9468] vsize: 2124
Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 3163 0 0 0 36964 18 0 0 25 0 1 0 1843345791 13574144 3097 4294967295 134512640 135094434 3221224448 3221223072 134562085 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9472/statm): 3314 3097 145 145 0 3169 0
[pid=9472] vsize: 13256
Current children cumulated CPU time (s) 369.82
Current children cumulated vsize (Kb) 15380

[startup+380.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 9472
Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9468/statm): 531 226 485 147 0 384 0
[pid=9468] vsize: 2124
Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 3163 0 0 0 37964 18 0 0 25 0 1 0 1843345791 13574144 3097 4294967295 134512640 135094434 3221224448 3221223040 134557389 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9472/statm): 3314 3097 145 145 0 3169 0
[pid=9472] vsize: 13256
Current children cumulated CPU time (s) 379.82
Current children cumulated vsize (Kb) 15380

[startup+390.041 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 9472
Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9468/statm): 531 226 485 147 0 384 0
[pid=9468] vsize: 2124
Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 3167 0 0 0 38964 19 0 0 25 0 1 0 1843345791 13590528 3101 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9472/statm): 3318 3101 145 145 0 3173 0
[pid=9472] vsize: 13272
Current children cumulated CPU time (s) 389.83
Current children cumulated vsize (Kb) 15396

[startup+400.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 9472
Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9468/statm): 531 226 485 147 0 384 0
[pid=9468] vsize: 2124
Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 3252 0 0 0 39963 19 0 0 25 0 1 0 1843345791 13934592 3186 4294967295 134512640 135094434 3221224448 3221223120 134555568 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9472/statm): 3402 3186 145 145 0 3257 0
[pid=9472] vsize: 13608
Current children cumulated CPU time (s) 399.82
Current children cumulated vsize (Kb) 15732

[startup+410.041 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 9472
Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9468/statm): 531 226 485 147 0 384 0
[pid=9468] vsize: 2124
Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 3341 0 0 0 40961 20 0 0 25 0 1 0 1843345791 14299136 3275 4294967295 134512640 135094434 3221224448 3221223040 134557182 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9472/statm): 3491 3275 145 145 0 3346 0
[pid=9472] vsize: 13964
Current children cumulated CPU time (s) 409.81
Current children cumulated vsize (Kb) 16088

[startup+420.042 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 9472
Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9468/statm): 531 226 485 147 0 384 0
[pid=9468] vsize: 2124
Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 3423 0 0 0 41960 21 0 0 25 0 1 0 1843345791 14639104 3357 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9472/statm): 3574 3357 145 145 0 3429 0
[pid=9472] vsize: 14296
Current children cumulated CPU time (s) 419.81
Current children cumulated vsize (Kb) 16420

[startup+430.043 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 9472
Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9468/statm): 531 226 485 147 0 384 0
[pid=9468] vsize: 2124
Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 3516 0 0 0 42958 22 0 0 25 0 1 0 1843345791 15015936 3450 4294967295 134512640 135094434 3221224448 3221223072 134562057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9472/statm): 3666 3450 145 145 0 3521 0
[pid=9472] vsize: 14664
Current children cumulated CPU time (s) 429.8
Current children cumulated vsize (Kb) 16788

[startup+440.044 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 9472
Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9468/statm): 531 226 485 147 0 384 0
[pid=9468] vsize: 2124
Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 3601 0 0 0 43957 22 0 0 25 0 1 0 1843345791 15380480 3535 4294967295 134512640 135094434 3221224448 3221223040 134557230 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9472/statm): 3755 3535 145 145 0 3610 0
[pid=9472] vsize: 15020
Current children cumulated CPU time (s) 439.79
Current children cumulated vsize (Kb) 17144

[startup+450.045 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 9472
Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9468/statm): 531 226 485 147 0 384 0
[pid=9468] vsize: 2124
Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 3761 0 0 0 44955 24 0 0 25 0 1 0 1843345791 15998976 3695 4294967295 134512640 135094434 3221224448 3221223072 134557612 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9472/statm): 3906 3695 145 145 0 3761 0
[pid=9472] vsize: 15624
Current children cumulated CPU time (s) 449.79
Current children cumulated vsize (Kb) 17748

[startup+460.045 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 9472
Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9468/statm): 531 226 485 147 0 384 0
[pid=9468] vsize: 2124
Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 3766 0 0 0 45955 24 0 0 25 0 1 0 1843345791 16031744 3700 4294967295 134512640 135094434 3221224448 3221223104 134557882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9472/statm): 3914 3700 145 145 0 3769 0
[pid=9472] vsize: 15656
Current children cumulated CPU time (s) 459.79
Current children cumulated vsize (Kb) 17780

[startup+470.046 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 9472
Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9468/statm): 531 226 485 147 0 384 0
[pid=9468] vsize: 2124
Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 3767 0 0 0 46956 24 0 0 25 0 1 0 1843345791 16031744 3701 4294967295 134512640 135094434 3221224448 3221223104 134557890 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9472/statm): 3914 3701 145 145 0 3769 0
[pid=9472] vsize: 15656
Current children cumulated CPU time (s) 469.8
Current children cumulated vsize (Kb) 17780

[startup+480.047 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 9472
Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9468/statm): 531 226 485 147 0 384 0
[pid=9468] vsize: 2124
Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 3779 0 0 0 47956 24 0 0 25 0 1 0 1843345791 16105472 3713 4294967295 134512640 135094434 3221224448 3221223040 134557404 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9472/statm): 3932 3713 145 145 0 3787 0
[pid=9472] vsize: 15728
Current children cumulated CPU time (s) 479.8
Current children cumulated vsize (Kb) 17852

[startup+490.048 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 9472
Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9468/statm): 531 226 485 147 0 384 0
[pid=9468] vsize: 2124
Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 3779 0 0 0 48956 24 0 0 25 0 1 0 1843345791 16105472 3713 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9472/statm): 3932 3713 145 145 0 3787 0
[pid=9472] vsize: 15728
Current children cumulated CPU time (s) 489.8
Current children cumulated vsize (Kb) 17852

[startup+500.049 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 9472
Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9468/statm): 531 226 485 147 0 384 0
[pid=9468] vsize: 2124
Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 3779 0 0 0 49956 24 0 0 25 0 1 0 1843345791 16105472 3713 4294967295 134512640 135094434 3221224448 3221223040 134556843 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9472/statm): 3932 3713 145 145 0 3787 0
[pid=9472] vsize: 15728
Current children cumulated CPU time (s) 499.8
Current children cumulated vsize (Kb) 17852

[startup+510.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 9472
Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9468/statm): 531 226 485 147 0 384 0
[pid=9468] vsize: 2124
Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 3779 0 0 0 50956 24 0 0 25 0 1 0 1843345791 16105472 3713 4294967295 134512640 135094434 3221224448 3221223040 134557416 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9472/statm): 3932 3713 145 145 0 3787 0
[pid=9472] vsize: 15728
Current children cumulated CPU time (s) 509.8
Current children cumulated vsize (Kb) 17852

[startup+520.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 9472
Raw data (/proc/9468/stat): 9468 (minisat+_script) S 9467 9468 28974 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843345786 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/9468/statm): 531 226 485 147 0 384 0
[pid=9468] vsize: 2124
Raw data (/proc/9472/stat): 9472 (minisat+_64-bit) R 9468 9468 28974 0 -1 0 3812 0 0 0 51956 24 0 0 25 0 1 0 1843345791 16261120 3746 4294967295 134512640 135094434 3221224448 3221223072 134557726 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/9472/statm): 3970 3746 145 145 0 3825 0
[pid=9472] vsize: 15880
Current children cumulated CPU time (s) 519.8
Current children cumulated vsize (Kb) 18004
One traced child (pid=9472) exited with status: 30
One traced child (pid=9468) exited with status: 30
All traced children have exited ! Game is over.

Child status: 30
Real time (s): 526.512
CPU time (s): 526.298
CPU user time (s): 526.025
CPU system time (s): 0.272958
CPU usage (%): 99.9594
Max. virtual memory (cumulated for all children) (Kb): 18004

Verifier Data

Verifier:	OK	1120