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/manquinho/synthesis-ptl-cmos-circuits/normalized-c8.opb
MD5SUM9b291040ec2b77d0bffb739c0db80d53
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 1194
Optimality of the best value was proved YES
Number of terms in the objective function 239
Biggest coefficient in the objective function 61
Number of bits for the biggest coefficient in the objective function 6
Sum of the numbers in the objective function 10012
Number of bits of the sum of numbers in the objective function 14
Biggest number in a constraint 61
Number of bits of the biggest number in a constraint 6
Biggest sum of numbers in a constraint 10012
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 benchmark33.9268
Number of variables239
Total number of constraints524
Number of constraints which are clauses520
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints4
Minimum length of a constraint1
Maximum length of a constraint36

Trace number 2200

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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:        923520 kB
Buffers:         35032 kB
Cached:          49808 kB
SwapCached:        228 kB
Active:          66240 kB
Inactive:        21488 kB
HighTotal:      131008 kB
HighFree:        77476 kB
LowTotal:       903652 kB
LowFree:        846044 kB
SwapTotal:     2097136 kB
SwapFree:      2096756 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6272 kB
Slab:            17780 kB
Committed_AS:    64164 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-18 18:30:39 (client local time) WITH STATUS 10 IN 1209.19 SECONDS
stats: 2593 7 1209.19 10

Solver Data

c Parsing PB file...
c Converting 519 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): .......................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |     519     2283 |     173       0        0     nan |  0.000 % |
c ==============================================================================
c Found solution: 1761
c ---[   0]---> Sorter-cost:29493     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         1 |   71546   168129 |   23848       1       14    14.0 |  0.000 % |
c |       102 |   71012   166938 |   26232      96     5965    62.1 |  0.585 % |
c |       253 |   69760   164083 |   28856     238     9177    38.6 |  2.006 % |
c ==============================================================================
c Found solution: 1663
c ---[   0]---> Sorter-cost:24435     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       420 |  129195   302890 |   43065     404    11865    29.4 |  2.006 % |
c |       523 |  128942   302321 |   47371     505    15464    30.6 |  1.312 % |
c |       674 |  128886   302193 |   52108     650    17491    26.9 |  1.346 % |
c ==============================================================================
c Found solution: 1659
c ---[   0]---> Sorter-cost:22388     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       773 |  183537   429830 |   61179     745    20173    27.1 |  1.346 % |
c ==============================================================================
c Found solution: 1635
c ---[   0]---> Sorter-cost:    4     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       868 |  183802   430480 |   61267     840    22334    26.6 |  1.346 % |
c |       968 |  183802   430480 |   67393     940    25352    27.0 |  1.035 % |
c |      1123 |  183802   430480 |   74133    1095    31539    28.8 |  1.035 % |
c |      1348 |  183802   430480 |   81546    1320    37216    28.2 |  1.035 % |
c |      1686 |  183802   430480 |   89701    1658    45439    27.4 |  1.035 % |
c |      2193 |  183802   430480 |   98671    2165    75257    34.8 |  1.035 % |
c ==============================================================================
c Found solution: 1633
c ---[   0]---> Sorter-cost:    2     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2760 |  183705   430276 |   61235    2731   127537    46.7 |  1.035 % |
c |      2860 |  183705   430276 |   67358    2831   129420    45.7 |  1.086 % |
c |      3010 |  183705   430276 |   74094    2981   150502    50.5 |  1.086 % |
c |      3236 |  183669   430195 |   81503    3206   156140    48.7 |  1.101 % |
c |      3574 |  183669   430195 |   89654    3544   227809    64.3 |  1.101 % |
c |      4081 |  183648   430149 |   98619    4046   242098    59.8 |  1.110 % |
c |      4840 |  183422   429642 |  108481    4803   262574    54.7 |  1.215 % |
c |      5979 |  182959   428603 |  119329    5801   280741    48.4 |  1.410 % |
c |      7688 |  182959   428603 |  131262    7510   354029    47.1 |  1.410 % |
c |     10251 |  182777   428188 |  144388   10064   431174    42.8 |  1.492 % |
c |     14095 |  182777   428188 |  158827   13908   692860    49.8 |  1.492 % |
c ==============================================================================
c Found solution: 1575
c ---[   0]---> Sorter-cost:    3     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14976 |  182784   428207 |   60928   14789   718296    48.6 |  1.492 % |
c |     15076 |  182784   428207 |   67020   14889   720044    48.4 |  1.493 % |
c |     15227 |  182784   428207 |   73722   15040   735483    48.9 |  1.493 % |
c |     15452 |  182784   428207 |   81095   15265   758960    49.7 |  1.493 % |
c |     15789 |  182784   428207 |   89204   15602   762389    48.9 |  1.493 % |
c |     16295 |  182586   427760 |   98125   16054   769845    48.0 |  1.576 % |
c |     17054 |  182478   427511 |  107937   16700   800996    48.0 |  1.627 % |
c |     18193 |  182478   427511 |  118731   17839   927912    52.0 |  1.627 % |
c |     19902 |  182354   427229 |  130604   19524   978241    50.1 |  1.679 % |
c ==============================================================================
c Found solution: 1563
c ---[   0]---> Sorter-cost:    3     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20264 |  182366   427265 |   60788   19882  1006526    50.6 |  1.679 % |
c |     20365 |  182366   427265 |   66866   19983  1008267    50.5 |  1.683 % |
c |     20515 |  182366   427265 |   73553   20133  1011784    50.3 |  1.683 % |
c |     20741 |  182366   427265 |   80908   20359  1018379    50.0 |  1.683 % |
c |     21078 |  182366   427265 |   88999   20696  1024085    49.5 |  1.683 % |
c |     21584 |  182318   427156 |   97899   21199  1064401    50.2 |  1.707 % |
c |     22343 |  182318   427156 |  107689   21958  1161871    52.9 |  1.707 % |
c |     23482 |  182318   427156 |  118458   23097  1182227    51.2 |  1.707 % |
c |     25191 |  182318   427156 |  130304   24806  1221403    49.2 |  1.707 % |
c |     27755 |  182316   427152 |  143334   27369  1542213    56.3 |  1.709 % |
c |     31599 |  182316   427152 |  157668   31213  1746376    56.0 |  1.709 % |
c |     37366 |  182135   426752 |  173435   35849  2046540    57.1 |  1.803 % |
c |     46016 |  182135   426752 |  190778   44499  3422797    76.9 |  1.803 % |
c |     58991 |  182112   426705 |  209856   57471  4480609    78.0 |  1.815 % |
c ==============================================================================
c Found solution: 1562
c ---[   0]---> Sorter-cost:    5     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     64448 |  182442   427528 |   60814   62905  5559278    88.4 |  1.815 % |
c |     64548 |  182442   427528 |   66895   18053  1759157    97.4 |  1.844 % |
c |     64699 |  182442   427528 |   73584   18204  1765019    97.0 |  1.844 % |
c |     64924 |  182442   427528 |   80943   18429  1771117    96.1 |  1.844 % |
c |     65264 |  182426   427491 |   89037   18763  1783613    95.1 |  1.851 % |
c |     65770 |  182426   427491 |   97941   19269  1832793    95.1 |  1.851 % |
c |     66530 |  182338   427290 |  107735   20028  1848421    92.3 |  1.891 % |
c |     67669 |  182338   427290 |  118509   21167  1870338    88.4 |  1.891 % |
c |     69378 |  182338   427290 |  130360   22876  2104457    92.0 |  1.891 % |
c |     71940 |  182338   427290 |  143396   25438  2385384    93.8 |  1.891 % |
c ==============================================================================
c Found solution: 1503
c ---[   0]---> Sorter-cost:    3     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     72011 |  182345   427309 |   60781   25509  2388858    93.6 |  1.891 % |
c |     72111 |  182345   427309 |   66859   25609  2390705    93.4 |  1.893 % |
c |     72263 |  182345   427309 |   73545   25761  2393986    92.9 |  1.893 % |
c |     72488 |  182345   427309 |   80899   25986  2398005    92.3 |  1.893 % |
c |     72825 |  182345   427309 |   88989   26323  2405116    91.4 |  1.893 % |
c |     73335 |  182345   427309 |   97888   26833  2477687    92.3 |  1.893 % |
c |     74094 |  182345   427309 |  107677   27592  2515961    91.2 |  1.893 % |
c |     75233 |  182273   427147 |  118444   28724  2551373    88.8 |  1.924 % |
c |     76941 |  182273   427147 |  130289   30432  2699655    88.7 |  1.924 % |
c |     79503 |  182273   427147 |  143318   32994  2949425    89.4 |  1.924 % |
c |     83348 |  182273   427147 |  157650   36839  3399895    92.3 |  1.924 % |
c ==============================================================================
c Found solution: 1498
c ---[   0]---> Sorter-cost:    6     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     86338 |  182284   427302 |   60761   39829  3484893    87.5 |  1.924 % |
c |     86438 |  182284   427302 |   66837   39929  3486512    87.3 |  1.926 % |
c |     86592 |  182284   427302 |   73520   40083  3488410    87.0 |  1.926 % |
c |     86819 |  182284   427302 |   80872   40310  3491201    86.6 |  1.926 % |
c |     87156 |  182284   427302 |   88960   40647  3497920    86.1 |  1.926 % |
c |     87662 |  182284   427302 |   97856   41153  3552074    86.3 |  1.926 % |
c |     88421 |  182284   427302 |  107641   41912  3633978    86.7 |  1.926 % |
c |     89561 |  182284   427302 |  118405   43052  3689404    85.7 |  1.926 % |
c |     91270 |  182284   427302 |  130246   44761  3736821    83.5 |  1.926 % |
c |     93832 |  182284   427302 |  143271   47323  4129702    87.3 |  1.926 % |
c |     97677 |  182214   427140 |  157598   51158  4540898    88.8 |  1.957 % |
c |    103444 |  182214   427140 |  173358   56925  4829344    84.8 |  1.957 % |
c ==============================================================================
c Found solution: 1496
c ---[   0]---> Sorter-cost:    6     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    103583 |  182222   427158 |   60740   57064  4843242    84.9 |  1.957 % |
c |    103683 |  182222   427158 |   66814   57164  4845319    84.8 |  1.958 % |
c |    103833 |  182222   427158 |   73495   57314  4846534    84.6 |  1.958 % |
c |    104058 |  182222   427158 |   80844   57539  4852492    84.3 |  1.958 % |
c |    104397 |  182222   427158 |   88929   57878  4859319    84.0 |  1.958 % |
c |    104903 |  182222   427158 |   97822   58384  4959658    84.9 |  1.958 % |
c |    105665 |  182222   427158 |  107604   59146  5009406    84.7 |  1.958 % |
c |    106808 |  182222   427158 |  118365   60289  5137477    85.2 |  1.958 % |
c ==============================================================================
c Found solution: 1477
c ---[   0]---> Sorter-cost:    5     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    107692 |  182244   427216 |   60748   61173  5156580    84.3 |  1.958 % |
c ==============================================================================
c Found solution: 1446
c ---[   0]---> Sorter-cost:    4     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    107709 |  182252   427240 |   60750   61190  5159534    84.3 |  1.958 % |
c |    107809 |  182252   427240 |   66825   61290  5161494    84.2 |  1.961 % |
c |    107961 |  182252   427240 |   73507   61442  5165631    84.1 |  1.961 % |
c |    108186 |  182252   427240 |   80858   61667  5170340    83.8 |  1.961 % |
c ==============================================================================
c Found solution: 1394
c ---[   0]---> Sorter-cost:    5     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    108195 |  182275   427300 |   60758   61676  5170450    83.8 |  1.961 % |
c ==============================================================================
c Found solution: 1386
c ---[   0]---> Sorter-cost:    3     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    108245 |  182281   427319 |   60760   61726  5174377    83.8 |  1.961 % |
c |    108345 |  182281   427319 |   66836   61826  5177478    83.7 |  1.963 % |
c |    108498 |  182281   427319 |   73519   61979  5181790    83.6 |  1.963 % |
c |    108725 |  182281   427319 |   80871   62206  5210034    83.8 |  1.963 % |
c |    109062 |  182281   427319 |   88958   62543  5245669    83.9 |  1.963 % |
c |    109569 |  182281   427319 |   97854   63050  5306611    84.2 |  1.963 % |
c |    110328 |  182281   427319 |  107640   63809  5340309    83.7 |  1.963 % |
c |    111468 |  182281   427319 |  118404   64949  5380676    82.8 |  1.963 % |
c |    113176 |  182281   427319 |  130244   66657  5472870    82.1 |  1.963 % |
c |    115739 |  182281   427319 |  143268   69220  5593926    80.8 |  1.963 % |
c ==============================================================================
c Found solution: 1379
c ---[   0]---> Sorter-cost:    2     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    119287 |  182287   427332 |   60762   72768  5923894    81.4 |  1.963 % |
c |    119388 |  182287   427332 |   66838   21679   841947    38.8 |  1.964 % |
c |    119538 |  182287   427332 |   73522   21829   845069    38.7 |  1.965 % |
c |    119763 |  182287   427332 |   80874   22054   851493    38.6 |  1.965 % |
c |    120100 |  182287   427332 |   88961   22391   889109    39.7 |  1.965 % |
c |    120606 |  182287   427332 |   97857   22897   907014    39.6 |  1.965 % |
c |    121365 |  182287   427332 |  107643   23656   939005    39.7 |  1.965 % |
c |    122504 |  182287   427332 |  118407   24795   996962    40.2 |  1.965 % |
c |    124214 |  182287   427332 |  130248   26505  1043747    39.4 |  1.965 % |
c |    126778 |  182287   427332 |  143273   29069  1109598    38.2 |  1.964 % |
c |    130623 |  182287   427332 |  157600   32914  1252928    38.1 |  1.965 % |

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/30738/stat): 30738 (minisat+_script) R 30737 30738 22582 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1785117505 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/30738/statm): 174 3 169 147 0 27 0
[pid=30738] 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=30739
New process pid=30740
New process pid=30741
execve syscall for /bin/sed executable
One traced child (pid=30740) exited with status: 0
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=30741) exited with status: 0
One traced child (pid=30739) exited with status: 0
New process pid=30742
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc10/normalized-c8.opb

[startup+10.0046 s]
Raw data (loadavg): 0.93 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 5807 0 0 0 951 22 0 0 25 0 1 0 1785117510 28459008 5576 4294967295 134512640 135094434 3221224448 3221223120 134556266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30742/statm): 6948 5576 145 145 0 6803 0
[pid=30742] vsize: 27792
Current children cumulated CPU time (s) 9.74
Current children cumulated vsize (Kb) 29916

[startup+20.0052 s]
Raw data (loadavg): 0.94 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 5807 0 0 0 1951 22 0 0 25 0 1 0 1785117510 28459008 5576 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30742/statm): 6948 5576 145 145 0 6803 0
[pid=30742] vsize: 27792
Current children cumulated CPU time (s) 19.74
Current children cumulated vsize (Kb) 29916

[startup+30.0078 s]
Raw data (loadavg): 0.95 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 5969 0 0 0 2949 23 0 0 25 0 1 0 1785117510 28856320 5673 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30742/statm): 7045 5673 145 145 0 6900 0
[pid=30742] vsize: 28180
Current children cumulated CPU time (s) 29.73
Current children cumulated vsize (Kb) 30304

[startup+40.0083 s]
Raw data (loadavg): 0.96 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 6095 0 0 0 3946 25 0 0 25 0 1 0 1785117510 29384704 5799 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30742/statm): 7174 5799 145 145 0 7029 0
[pid=30742] vsize: 28696
Current children cumulated CPU time (s) 39.72
Current children cumulated vsize (Kb) 30820

[startup+50.0089 s]
Raw data (loadavg): 0.96 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 6178 0 0 0 4944 26 0 0 25 0 1 0 1785117510 29716480 5882 4294967295 134512640 135094434 3221224448 3221223072 134562068 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30742/statm): 7255 5882 145 145 0 7110 0
[pid=30742] vsize: 29020
Current children cumulated CPU time (s) 49.71
Current children cumulated vsize (Kb) 31144

[startup+60.0104 s]
Raw data (loadavg): 0.97 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 6304 0 0 0 5941 27 0 0 25 0 1 0 1785117510 30248960 6008 4294967295 134512640 135094434 3221224448 3221223072 134557587 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30742/statm): 7385 6008 145 145 0 7240 0
[pid=30742] vsize: 29540
Current children cumulated CPU time (s) 59.69
Current children cumulated vsize (Kb) 31664

[startup+70.011 s]
Raw data (loadavg): 0.97 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 6463 0 0 0 6937 29 0 0 25 0 1 0 1785117510 30892032 6167 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30742/statm): 7542 6167 145 145 0 7397 0
[pid=30742] vsize: 30168
Current children cumulated CPU time (s) 69.67
Current children cumulated vsize (Kb) 32292

[startup+80.0116 s]
Raw data (loadavg): 0.98 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 6580 0 0 0 7935 30 0 0 25 0 1 0 1785117510 31367168 6284 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30742/statm): 7658 6284 145 145 0 7513 0
[pid=30742] vsize: 30632
Current children cumulated CPU time (s) 79.66
Current children cumulated vsize (Kb) 32756

[startup+90.0131 s]
Raw data (loadavg): 0.98 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 6616 0 0 0 8933 31 0 0 25 0 1 0 1785117510 31510528 6320 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30742/statm): 7693 6320 145 145 0 7548 0
[pid=30742] vsize: 30772
Current children cumulated CPU time (s) 89.65
Current children cumulated vsize (Kb) 32896

[startup+100.014 s]
Raw data (loadavg): 0.98 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 6750 0 0 0 9931 33 0 0 25 0 1 0 1785117510 31793152 6390 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30742/statm): 7762 6390 145 145 0 7617 0
[pid=30742] vsize: 31048
Current children cumulated CPU time (s) 99.65
Current children cumulated vsize (Kb) 33172

[startup+110.015 s]
Raw data (loadavg): 0.98 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 6822 0 0 0 10930 33 0 0 25 0 1 0 1785117510 32145408 6462 4294967295 134512640 135094434 3221224448 3221223080 134557638 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30742/statm): 7848 6462 145 145 0 7703 0
[pid=30742] vsize: 31392
Current children cumulated CPU time (s) 109.64
Current children cumulated vsize (Kb) 33516

[startup+120.017 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 6946 0 0 0 11927 35 0 0 25 0 1 0 1785117510 32649216 6586 4294967295 134512640 135094434 3221224448 3221223104 134557903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30742/statm): 7971 6586 145 145 0 7826 0
[pid=30742] vsize: 31884
Current children cumulated CPU time (s) 119.63
Current children cumulated vsize (Kb) 34008

[startup+130.017 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 6973 0 0 0 12927 35 0 0 25 0 1 0 1785117510 32755712 6613 4294967295 134512640 135094434 3221224448 3221223100 134558255 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30742/statm): 7997 6613 145 145 0 7852 0
[pid=30742] vsize: 31988
Current children cumulated CPU time (s) 129.63
Current children cumulated vsize (Kb) 34112

[startup+140.019 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 7095 0 0 0 13924 36 0 0 25 0 1 0 1785117510 32989184 6671 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30742/statm): 8054 6671 145 145 0 7909 0
[pid=30742] vsize: 32216
Current children cumulated CPU time (s) 139.61
Current children cumulated vsize (Kb) 34340

[startup+150.019 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 7157 0 0 0 14922 37 0 0 25 0 1 0 1785117510 33239040 6733 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30742/statm): 8115 6733 145 145 0 7970 0
[pid=30742] vsize: 32460
Current children cumulated CPU time (s) 149.6
Current children cumulated vsize (Kb) 34584

[startup+160.02 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 7283 0 0 0 15920 38 0 0 25 0 1 0 1785117510 33746944 6859 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30742/statm): 8239 6859 145 145 0 8094 0
[pid=30742] vsize: 32956
Current children cumulated CPU time (s) 159.59
Current children cumulated vsize (Kb) 35080

[startup+170.021 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 7334 0 0 0 16918 39 0 0 25 0 1 0 1785117510 33951744 6910 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30742/statm): 8289 6910 145 145 0 8144 0
[pid=30742] vsize: 33156
Current children cumulated CPU time (s) 169.58
Current children cumulated vsize (Kb) 35280

[startup+180.021 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 7383 0 0 0 17917 40 0 0 25 0 1 0 1785117510 34148352 6959 4294967295 134512640 135094434 3221224448 3221223104 134558402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30742/statm): 8337 6959 145 145 0 8192 0
[pid=30742] vsize: 33348
Current children cumulated CPU time (s) 179.58
Current children cumulated vsize (Kb) 35472

[startup+190.022 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 7567 0 0 0 18912 42 0 0 25 0 1 0 1785117510 34897920 7143 4294967295 134512640 135094434 3221224448 3221223040 134557366 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30742/statm): 8520 7143 145 145 0 8375 0
[pid=30742] vsize: 34080
Current children cumulated CPU time (s) 189.55
Current children cumulated vsize (Kb) 36204

[startup+200.022 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 7714 0 0 0 19909 44 0 0 25 0 1 0 1785117510 35491840 7290 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30742/statm): 8665 7290 145 145 0 8520 0
[pid=30742] vsize: 34660
Current children cumulated CPU time (s) 199.54
Current children cumulated vsize (Kb) 36784

[startup+210.024 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 7756 0 0 0 20908 44 0 0 25 0 1 0 1785117510 35663872 7332 4294967295 134512640 135094434 3221224448 3221223104 134558135 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30742/statm): 8707 7332 145 145 0 8562 0
[pid=30742] vsize: 34828
Current children cumulated CPU time (s) 209.53
Current children cumulated vsize (Kb) 36952

[startup+220.024 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 7792 0 0 0 21907 45 0 0 25 0 1 0 1785117510 35807232 7368 4294967295 134512640 135094434 3221224448 3221223136 134554739 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30742/statm): 8742 7368 145 145 0 8597 0
[pid=30742] vsize: 34968
Current children cumulated CPU time (s) 219.53
Current children cumulated vsize (Kb) 37092

[startup+230.025 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 7816 0 0 0 22906 45 0 0 25 0 1 0 1785117510 35905536 7392 4294967295 134512640 135094434 3221224448 3221223104 134557937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30742/statm): 8766 7392 145 145 0 8621 0
[pid=30742] vsize: 35064
Current children cumulated CPU time (s) 229.52
Current children cumulated vsize (Kb) 37188

[startup+240.027 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 7842 0 0 0 23905 46 0 0 25 0 1 0 1785117510 36007936 7418 4294967295 134512640 135094434 3221224448 3221223104 134558210 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30742/statm): 8791 7418 145 145 0 8646 0
[pid=30742] vsize: 35164
Current children cumulated CPU time (s) 239.52
Current children cumulated vsize (Kb) 37288

[startup+250.027 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 7933 0 0 0 24903 47 0 0 25 0 1 0 1785117510 36376576 7509 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30742/statm): 8881 7509 145 145 0 8736 0
[pid=30742] vsize: 35524
Current children cumulated CPU time (s) 249.51
Current children cumulated vsize (Kb) 37648

[startup+260.028 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 8020 0 0 0 25903 47 0 0 25 0 1 0 1785117510 36859904 7596 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30742/statm): 8999 7596 145 145 0 8854 0
[pid=30742] vsize: 35996
Current children cumulated CPU time (s) 259.51
Current children cumulated vsize (Kb) 38120

[startup+270.028 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 8020 0 0 0 26903 47 0 0 25 0 1 0 1785117510 36859904 7596 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30742/statm): 8999 7596 145 145 0 8854 0
[pid=30742] vsize: 35996
Current children cumulated CPU time (s) 269.51
Current children cumulated vsize (Kb) 38120

[startup+280.029 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 8044 0 0 0 27903 47 0 0 25 0 1 0 1785117510 36954112 7620 4294967295 134512640 135094434 3221224448 3221223104 134557846 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30742/statm): 9022 7620 145 145 0 8877 0
[pid=30742] vsize: 36088
Current children cumulated CPU time (s) 279.51
Current children cumulated vsize (Kb) 38212

[startup+290.029 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 8073 0 0 0 28902 48 0 0 25 0 1 0 1785117510 37068800 7649 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30742/statm): 9050 7649 145 145 0 8905 0
[pid=30742] vsize: 36200
Current children cumulated CPU time (s) 289.51
Current children cumulated vsize (Kb) 38324

[startup+300.03 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 8267 0 0 0 29898 50 0 0 25 0 1 0 1785117510 37863424 7843 4294967295 134512640 135094434 3221224448 3221223120 134555802 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30742/statm): 9244 7843 145 145 0 9099 0
[pid=30742] vsize: 36976
Current children cumulated CPU time (s) 299.49
Current children cumulated vsize (Kb) 39100

[startup+310.031 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 8407 0 0 0 30896 51 0 0 25 0 1 0 1785117510 38428672 7983 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30742/statm): 9382 7983 145 145 0 9237 0
[pid=30742] vsize: 37528
Current children cumulated CPU time (s) 309.48
Current children cumulated vsize (Kb) 39652

[startup+320.032 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 8457 0 0 0 31895 51 0 0 25 0 1 0 1785117510 38629376 8033 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30742/statm): 9431 8033 145 145 0 9286 0
[pid=30742] vsize: 37724
Current children cumulated CPU time (s) 319.47
Current children cumulated vsize (Kb) 39848

[startup+330.033 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 8636 0 0 0 32892 53 0 0 25 0 1 0 1785117510 39358464 8212 4294967295 134512640 135094434 3221224448 3221223136 134554739 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30742/statm): 9609 8212 145 145 0 9464 0
[pid=30742] vsize: 38436
Current children cumulated CPU time (s) 329.46
Current children cumulated vsize (Kb) 40560

[startup+340.033 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 8877 0 0 0 33887 55 0 0 25 0 1 0 1785117510 40341504 8453 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30742/statm): 9849 8453 145 145 0 9704 0
[pid=30742] vsize: 39396
Current children cumulated CPU time (s) 339.43
Current children cumulated vsize (Kb) 41520

[startup+350.034 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 9053 0 0 0 34883 58 0 0 25 0 1 0 1785117510 41086976 8629 4294967295 134512640 135094434 3221224448 3221223104 134557860 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30742/statm): 10031 8629 145 145 0 9886 0
[pid=30742] vsize: 40124
Current children cumulated CPU time (s) 349.42
Current children cumulated vsize (Kb) 42248

[startup+360.035 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 9273 0 0 0 35879 60 0 0 25 0 1 0 1785117510 41984000 8849 4294967295 134512640 135094434 3221224448 3221223104 134557846 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30742/statm): 10250 8849 145 145 0 10105 0
[pid=30742] vsize: 41000
Current children cumulated CPU time (s) 359.4
Current children cumulated vsize (Kb) 43124

[startup+370.036 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 9431 0 0 0 36875 62 0 0 25 0 1 0 1785117510 42618880 9007 4294967295 134512640 135094434 3221224448 3221223040 134557273 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30742/statm): 10405 9007 145 145 0 10260 0
[pid=30742] vsize: 41620
Current children cumulated CPU time (s) 369.38
Current children cumulated vsize (Kb) 43744

[startup+380.036 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 9613 0 0 0 37872 64 0 0 25 0 1 0 1785117510 43360256 9189 4294967295 134512640 135094434 3221224448 3221223120 134555568 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30742/statm): 10586 9189 145 145 0 10441 0
[pid=30742] vsize: 42344
Current children cumulated CPU time (s) 379.37
Current children cumulated vsize (Kb) 44468

[startup+390.037 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 9769 0 0 0 38868 65 0 0 25 0 1 0 1785117510 43995136 9345 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30742/statm): 10741 9345 145 145 0 10596 0
[pid=30742] vsize: 42964
Current children cumulated CPU time (s) 389.34
Current children cumulated vsize (Kb) 45088

[startup+400.037 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 9881 0 0 0 39868 66 0 0 25 0 1 0 1785117510 44449792 9457 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30742/statm): 10852 9457 145 145 0 10707 0
[pid=30742] vsize: 43408
Current children cumulated CPU time (s) 399.35
Current children cumulated vsize (Kb) 45532

[startup+410.037 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 10001 0 0 0 40865 67 0 0 25 0 1 0 1785117510 44937216 9577 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30742/statm): 10971 9577 145 145 0 10826 0
[pid=30742] vsize: 43884
Current children cumulated CPU time (s) 409.33
Current children cumulated vsize (Kb) 46008

[startup+420.038 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 10069 0 0 0 41864 67 0 0 25 0 1 0 1785117510 45211648 9645 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30742/statm): 11038 9645 145 145 0 10893 0
[pid=30742] vsize: 44152
Current children cumulated CPU time (s) 419.32
Current children cumulated vsize (Kb) 46276

[startup+430.038 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 10153 0 0 0 42862 68 0 0 25 0 1 0 1785117510 45547520 9729 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30742/statm): 11120 9729 145 145 0 10975 0
[pid=30742] vsize: 44480
Current children cumulated CPU time (s) 429.31
Current children cumulated vsize (Kb) 46604

[startup+440.039 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 10251 0 0 0 43859 70 0 0 25 0 1 0 1785117510 45944832 9827 4294967295 134512640 135094434 3221224448 3221223104 134557813 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30742/statm): 11217 9827 145 145 0 11072 0
[pid=30742] vsize: 44868
Current children cumulated CPU time (s) 439.3
Current children cumulated vsize (Kb) 46992

[startup+450.039 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 10439 0 0 0 44855 72 0 0 25 0 1 0 1785117510 46710784 10015 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30742/statm): 11404 10015 145 145 0 11259 0
[pid=30742] vsize: 45616
Current children cumulated CPU time (s) 449.28
Current children cumulated vsize (Kb) 47740

[startup+460.04 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 10589 0 0 0 45852 73 0 0 25 0 1 0 1785117510 47321088 10165 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30742/statm): 11553 10165 145 145 0 11408 0
[pid=30742] vsize: 46212
Current children cumulated CPU time (s) 459.26
Current children cumulated vsize (Kb) 48336

[startup+470.04 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 10704 0 0 0 46850 74 0 0 25 0 1 0 1785117510 47788032 10280 4294967295 134512640 135094434 3221224448 3221223104 134557884 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30742/statm): 11667 10280 145 145 0 11522 0
[pid=30742] vsize: 46668
Current children cumulated CPU time (s) 469.25
Current children cumulated vsize (Kb) 48792

[startup+480.04 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 10779 0 0 0 47848 75 0 0 25 0 1 0 1785117510 48091136 10355 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30742/statm): 11741 10355 145 145 0 11596 0
[pid=30742] vsize: 46964
Current children cumulated CPU time (s) 479.24
Current children cumulated vsize (Kb) 49088

[startup+490.041 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 10890 0 0 0 48846 76 0 0 25 0 1 0 1785117510 48537600 10466 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30742/statm): 11850 10466 145 145 0 11705 0
[pid=30742] vsize: 47400
Current children cumulated CPU time (s) 489.23
Current children cumulated vsize (Kb) 49524

[startup+500.041 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 11051 0 0 0 49842 77 0 0 25 0 1 0 1785117510 49192960 10627 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30742/statm): 12010 10627 145 145 0 11865 0
[pid=30742] vsize: 48040
Current children cumulated CPU time (s) 499.2
Current children cumulated vsize (Kb) 50164

[startup+510.042 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 11335 0 0 0 50837 80 0 0 25 0 1 0 1785117510 50352128 10911 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30742/statm): 12293 10911 145 145 0 12148 0
[pid=30742] vsize: 49172
Current children cumulated CPU time (s) 509.18
Current children cumulated vsize (Kb) 51296

[startup+520.042 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 11538 0 0 0 51832 81 0 0 25 0 1 0 1785117510 51175424 11114 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30742/statm): 12494 11114 145 145 0 12349 0
[pid=30742] vsize: 49976
Current children cumulated CPU time (s) 519.14
Current children cumulated vsize (Kb) 52100

[startup+530.043 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 11838 0 0 0 52828 83 0 0 25 0 1 0 1785117510 52404224 11414 4294967295 134512640 135094434 3221224448 3221223040 134557389 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30742/statm): 12794 11414 145 145 0 12649 0
[pid=30742] vsize: 51176
Current children cumulated CPU time (s) 529.12
Current children cumulated vsize (Kb) 53300

[startup+540.043 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 12081 0 0 0 53825 84 0 0 25 0 1 0 1785117510 53116928 11590 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30742/statm): 12968 11590 145 145 0 12823 0
[pid=30742] vsize: 51872
Current children cumulated CPU time (s) 539.1
Current children cumulated vsize (Kb) 53996

[startup+550.044 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 12082 0 0 0 54825 84 0 0 25 0 1 0 1785117510 53116928 11591 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30742/statm): 12968 11591 145 145 0 12823 0
[pid=30742] vsize: 51872
Current children cumulated CPU time (s) 549.1
Current children cumulated vsize (Kb) 53996

[startup+560.045 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 12082 0 0 0 55825 84 0 0 25 0 1 0 1785117510 53116928 11591 4294967295 134512640 135094434 3221224448 3221223072 134557565 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30742/statm): 12968 11591 145 145 0 12823 0
[pid=30742] vsize: 51872
Current children cumulated CPU time (s) 559.1
Current children cumulated vsize (Kb) 53996

[startup+570.046 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 12082 0 0 0 56825 84 0 0 25 0 1 0 1785117510 53116928 11591 4294967295 134512640 135094434 3221224448 3221223040 134557375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30742/statm): 12968 11591 145 145 0 12823 0
[pid=30742] vsize: 51872
Current children cumulated CPU time (s) 569.1
Current children cumulated vsize (Kb) 53996

[startup+580.046 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 12082 0 0 0 57825 84 0 0 25 0 1 0 1785117510 53116928 11591 4294967295 134512640 135094434 3221224448 3221223104 134558398 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30742/statm): 12968 11591 145 145 0 12823 0
[pid=30742] vsize: 51872
Current children cumulated CPU time (s) 579.1
Current children cumulated vsize (Kb) 53996

[startup+590.046 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 12082 0 0 0 58825 84 0 0 25 0 1 0 1785117510 53116928 11591 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30742/statm): 12968 11591 145 145 0 12823 0
[pid=30742] vsize: 51872
Current children cumulated CPU time (s) 589.1
Current children cumulated vsize (Kb) 53996

[startup+600.047 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 12082 0 0 0 59826 84 0 0 25 0 1 0 1785117510 53116928 11591 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30742/statm): 12968 11591 145 145 0 12823 0
[pid=30742] vsize: 51872
Current children cumulated CPU time (s) 599.11
Current children cumulated vsize (Kb) 53996

[startup+610.047 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 12099 0 0 0 60826 85 0 0 25 0 1 0 1785117510 53186560 11608 4294967295 134512640 135094434 3221224448 3221223136 134554723 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30742/statm): 12985 11608 145 145 0 12840 0
[pid=30742] vsize: 51940
Current children cumulated CPU time (s) 609.12
Current children cumulated vsize (Kb) 54064

[startup+620.048 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 12099 0 0 0 61824 86 0 0 25 0 1 0 1785117510 53186560 11608 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30742/statm): 12985 11608 145 145 0 12840 0
[pid=30742] vsize: 51940
Current children cumulated CPU time (s) 619.11
Current children cumulated vsize (Kb) 54064

[startup+630.048 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 12099 0 0 0 62824 86 0 0 25 0 1 0 1785117510 53186560 11608 4294967295 134512640 135094434 3221224448 3221223072 134557565 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30742/statm): 12985 11608 145 145 0 12840 0
[pid=30742] vsize: 51940
Current children cumulated CPU time (s) 629.11
Current children cumulated vsize (Kb) 54064

[startup+640.049 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 12099 0 0 0 63824 86 0 0 25 0 1 0 1785117510 53186560 11608 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30742/statm): 12985 11608 145 145 0 12840 0
[pid=30742] vsize: 51940
Current children cumulated CPU time (s) 639.11
Current children cumulated vsize (Kb) 54064

[startup+650.05 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 12099 0 0 0 64824 87 0 0 25 0 1 0 1785117510 53186560 11608 4294967295 134512640 135094434 3221224448 3221223104 134557843 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30742/statm): 12985 11608 145 145 0 12840 0
[pid=30742] vsize: 51940
Current children cumulated CPU time (s) 649.12
Current children cumulated vsize (Kb) 54064

[startup+660.051 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 12099 0 0 0 65824 87 0 0 25 0 1 0 1785117510 53186560 11608 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30742/statm): 12985 11608 145 145 0 12840 0
[pid=30742] vsize: 51940
Current children cumulated CPU time (s) 659.12
Current children cumulated vsize (Kb) 54064

[startup+670.052 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 12099 0 0 0 66825 87 0 0 25 0 1 0 1785117510 53186560 11608 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30742/statm): 12985 11608 145 145 0 12840 0
[pid=30742] vsize: 51940
Current children cumulated CPU time (s) 669.13
Current children cumulated vsize (Kb) 54064

[startup+680.052 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 12099 0 0 0 67824 87 0 0 25 0 1 0 1785117510 53186560 11608 4294967295 134512640 135094434 3221224448 3221223104 134558035 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30742/statm): 12985 11608 145 145 0 12840 0
[pid=30742] vsize: 51940
Current children cumulated CPU time (s) 679.12
Current children cumulated vsize (Kb) 54064

[startup+690.053 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 12099 0 0 0 68825 87 0 0 25 0 1 0 1785117510 53186560 11608 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30742/statm): 12985 11608 145 145 0 12840 0
[pid=30742] vsize: 51940
Current children cumulated CPU time (s) 689.13
Current children cumulated vsize (Kb) 54064

[startup+700.053 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 12099 0 0 0 69825 88 0 0 25 0 1 0 1785117510 53186560 11608 4294967295 134512640 135094434 3221224448 3221223040 134556862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30742/statm): 12985 11608 145 145 0 12840 0
[pid=30742] vsize: 51940
Current children cumulated CPU time (s) 699.14
Current children cumulated vsize (Kb) 54064

[startup+710.054 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 12099 0 0 0 70825 88 0 0 25 0 1 0 1785117510 53186560 11608 4294967295 134512640 135094434 3221224448 3221223120 134556073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30742/statm): 12985 11608 145 145 0 12840 0
[pid=30742] vsize: 51940
Current children cumulated CPU time (s) 709.14
Current children cumulated vsize (Kb) 54064

[startup+720.054 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 12099 0 0 0 71825 88 0 0 25 0 1 0 1785117510 53186560 11608 4294967295 134512640 135094434 3221224448 3221223072 134557565 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30742/statm): 12985 11608 145 145 0 12840 0
[pid=30742] vsize: 51940
Current children cumulated CPU time (s) 719.14
Current children cumulated vsize (Kb) 54064

[startup+730.055 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 12099 0 0 0 72825 88 0 0 25 0 1 0 1785117510 53186560 11608 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30742/statm): 12985 11608 145 145 0 12840 0
[pid=30742] vsize: 51940
Current children cumulated CPU time (s) 729.14
Current children cumulated vsize (Kb) 54064

[startup+740.056 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 12099 0 0 0 73825 88 0 0 25 0 1 0 1785117510 53186560 11608 4294967295 134512640 135094434 3221224448 3221223080 134557561 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30742/statm): 12985 11608 145 145 0 12840 0
[pid=30742] vsize: 51940
Current children cumulated CPU time (s) 739.14
Current children cumulated vsize (Kb) 54064

[startup+750.056 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 12099 0 0 0 74825 88 0 0 25 0 1 0 1785117510 53186560 11608 4294967295 134512640 135094434 3221224448 3221223040 134556791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30742/statm): 12985 11608 145 145 0 12840 0
[pid=30742] vsize: 51940
Current children cumulated CPU time (s) 749.14
Current children cumulated vsize (Kb) 54064

[startup+760.057 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 12099 0 0 0 75825 88 0 0 25 0 1 0 1785117510 53186560 11608 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30742/statm): 12985 11608 145 145 0 12840 0
[pid=30742] vsize: 51940
Current children cumulated CPU time (s) 759.14
Current children cumulated vsize (Kb) 54064

[startup+770.057 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 12099 0 0 0 76825 88 0 0 25 0 1 0 1785117510 53186560 11608 4294967295 134512640 135094434 3221224448 3221223104 134557823 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30742/statm): 12985 11608 145 145 0 12840 0
[pid=30742] vsize: 51940
Current children cumulated CPU time (s) 769.14
Current children cumulated vsize (Kb) 54064

[startup+780.058 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 12099 0 0 0 77826 88 0 0 25 0 1 0 1785117510 53186560 11608 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30742/statm): 12985 11608 145 145 0 12840 0
[pid=30742] vsize: 51940
Current children cumulated CPU time (s) 779.15
Current children cumulated vsize (Kb) 54064

[startup+790.059 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 12099 0 0 0 78826 88 0 0 25 0 1 0 1785117510 53186560 11608 4294967295 134512640 135094434 3221224448 3221223008 134550326 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30742/statm): 12985 11608 145 145 0 12840 0
[pid=30742] vsize: 51940
Current children cumulated CPU time (s) 789.15
Current children cumulated vsize (Kb) 54064

[startup+800.059 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 12099 0 0 0 79826 89 0 0 25 0 1 0 1785117510 53186560 11608 4294967295 134512640 135094434 3221224448 3221223096 134558258 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30742/statm): 12985 11608 145 145 0 12840 0
[pid=30742] vsize: 51940
Current children cumulated CPU time (s) 799.16
Current children cumulated vsize (Kb) 54064

[startup+810.06 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 12099 0 0 0 80826 89 0 0 25 0 1 0 1785117510 53186560 11608 4294967295 134512640 135094434 3221224448 3221223104 134558225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30742/statm): 12985 11608 145 145 0 12840 0
[pid=30742] vsize: 51940
Current children cumulated CPU time (s) 809.16
Current children cumulated vsize (Kb) 54064

[startup+820.06 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 12099 0 0 0 81826 89 0 0 25 0 1 0 1785117510 53186560 11608 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30742/statm): 12985 11608 145 145 0 12840 0
[pid=30742] vsize: 51940
Current children cumulated CPU time (s) 819.16
Current children cumulated vsize (Kb) 54064

[startup+830.06 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 12099 0 0 0 82827 89 0 0 25 0 1 0 1785117510 53186560 11608 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30742/statm): 12985 11608 145 145 0 12840 0
[pid=30742] vsize: 51940
Current children cumulated CPU time (s) 829.17
Current children cumulated vsize (Kb) 54064

[startup+840.06 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 12099 0 0 0 83827 89 0 0 25 0 1 0 1785117510 53186560 11608 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30742/statm): 12985 11608 145 145 0 12840 0
[pid=30742] vsize: 51940
Current children cumulated CPU time (s) 839.17
Current children cumulated vsize (Kb) 54064

[startup+850.061 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 12099 0 0 0 84827 89 0 0 25 0 1 0 1785117510 53186560 11608 4294967295 134512640 135094434 3221224448 3221223060 134563069 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30742/statm): 12985 11608 145 145 0 12840 0
[pid=30742] vsize: 51940
Current children cumulated CPU time (s) 849.17
Current children cumulated vsize (Kb) 54064

[startup+860.061 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 12099 0 0 0 85827 89 0 0 25 0 1 0 1785117510 53186560 11608 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30742/statm): 12985 11608 145 145 0 12840 0
[pid=30742] vsize: 51940
Current children cumulated CPU time (s) 859.17
Current children cumulated vsize (Kb) 54064

[startup+870.062 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 12099 0 0 0 86827 89 0 0 25 0 1 0 1785117510 53186560 11608 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30742/statm): 12985 11608 145 145 0 12840 0
[pid=30742] vsize: 51940
Current children cumulated CPU time (s) 869.17
Current children cumulated vsize (Kb) 54064

[startup+880.062 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 12099 0 0 0 87827 89 0 0 25 0 1 0 1785117510 53186560 11608 4294967295 134512640 135094434 3221224448 3221223104 134558405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30742/statm): 12985 11608 145 145 0 12840 0
[pid=30742] vsize: 51940
Current children cumulated CPU time (s) 879.17
Current children cumulated vsize (Kb) 54064

[startup+890.062 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 12099 0 0 0 88827 89 0 0 25 0 1 0 1785117510 53186560 11608 4294967295 134512640 135094434 3221224448 3221223084 134557560 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30742/statm): 12985 11608 145 145 0 12840 0
[pid=30742] vsize: 51940
Current children cumulated CPU time (s) 889.17
Current children cumulated vsize (Kb) 54064

[startup+900.063 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 12099 0 0 0 89827 89 0 0 25 0 1 0 1785117510 53186560 11608 4294967295 134512640 135094434 3221224448 3221223104 134557884 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30742/statm): 12985 11608 145 145 0 12840 0
[pid=30742] vsize: 51940
Current children cumulated CPU time (s) 899.17
Current children cumulated vsize (Kb) 54064

[startup+910.063 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 12099 0 0 0 90828 89 0 0 25 0 1 0 1785117510 53186560 11608 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30742/statm): 12985 11608 145 145 0 12840 0
[pid=30742] vsize: 51940
Current children cumulated CPU time (s) 909.18
Current children cumulated vsize (Kb) 54064

[startup+920.064 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 12099 0 0 0 91828 89 0 0 25 0 1 0 1785117510 53186560 11608 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30742/statm): 12985 11608 145 145 0 12840 0
[pid=30742] vsize: 51940
Current children cumulated CPU time (s) 919.18
Current children cumulated vsize (Kb) 54064

[startup+930.064 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 12099 0 0 0 92828 90 0 0 25 0 1 0 1785117510 53186560 11608 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30742/statm): 12985 11608 145 145 0 12840 0
[pid=30742] vsize: 51940
Current children cumulated CPU time (s) 929.19
Current children cumulated vsize (Kb) 54064

[startup+940.065 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 12100 0 0 0 93827 90 0 0 25 0 1 0 1785117510 53186560 11609 4294967295 134512640 135094434 3221224448 3221223236 134553497 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30742/statm): 12985 11609 145 145 0 12840 0
[pid=30742] vsize: 51940
Current children cumulated CPU time (s) 939.18
Current children cumulated vsize (Kb) 54064

[startup+950.064 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 12100 0 0 0 94827 90 0 0 25 0 1 0 1785117510 53186560 11609 4294967295 134512640 135094434 3221224448 3221223104 134557813 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30742/statm): 12985 11609 145 145 0 12840 0
[pid=30742] vsize: 51940
Current children cumulated CPU time (s) 949.18
Current children cumulated vsize (Kb) 54064

[startup+960.066 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 12101 0 0 0 95827 90 0 0 25 0 1 0 1785117510 53186560 11610 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30742/statm): 12985 11610 145 145 0 12840 0
[pid=30742] vsize: 51940
Current children cumulated CPU time (s) 959.18
Current children cumulated vsize (Kb) 54064

[startup+970.067 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 12101 0 0 0 96827 90 0 0 25 0 1 0 1785117510 53186560 11610 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30742/statm): 12985 11610 145 145 0 12840 0
[pid=30742] vsize: 51940
Current children cumulated CPU time (s) 969.18
Current children cumulated vsize (Kb) 54064

[startup+980.066 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 12102 0 0 0 97827 90 0 0 25 0 1 0 1785117510 53186560 11611 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30742/statm): 12985 11611 145 145 0 12840 0
[pid=30742] vsize: 51940
Current children cumulated CPU time (s) 979.18
Current children cumulated vsize (Kb) 54064

[startup+990.067 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 12134 0 0 0 98827 91 0 0 25 0 1 0 1785117510 53575680 11643 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30742/statm): 13080 11643 145 145 0 12935 0
[pid=30742] vsize: 52320
Current children cumulated CPU time (s) 989.19
Current children cumulated vsize (Kb) 54444

[startup+1000.07 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 12199 0 0 0 99826 91 0 0 25 0 1 0 1785117510 53841920 11708 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30742/statm): 13145 11708 145 145 0 13000 0
[pid=30742] vsize: 52580
Current children cumulated CPU time (s) 999.18
Current children cumulated vsize (Kb) 54704

[startup+1010.07 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 12259 0 0 0 100825 92 0 0 25 0 1 0 1785117510 54083584 11768 4294967295 134512640 135094434 3221224448 3221223040 134557157 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30742/statm): 13204 11768 145 145 0 13059 0
[pid=30742] vsize: 52816
Current children cumulated CPU time (s) 1009.18
Current children cumulated vsize (Kb) 54940

[startup+1020.07 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 12309 0 0 0 101824 92 0 0 25 0 1 0 1785117510 54284288 11818 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30742/statm): 13253 11818 145 145 0 13108 0
[pid=30742] vsize: 53012
Current children cumulated CPU time (s) 1019.17
Current children cumulated vsize (Kb) 55136

[startup+1030.07 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 12357 0 0 0 102823 93 0 0 25 0 1 0 1785117510 54476800 11866 4294967295 134512640 135094434 3221224448 3221223072 134557696 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30742/statm): 13300 11866 145 145 0 13155 0
[pid=30742] vsize: 53200
Current children cumulated CPU time (s) 1029.17
Current children cumulated vsize (Kb) 55324

[startup+1040.07 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 12385 0 0 0 103823 93 0 0 25 0 1 0 1785117510 54587392 11894 4294967295 134512640 135094434 3221224448 3221223072 134557714 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30742/statm): 13327 11894 145 145 0 13182 0
[pid=30742] vsize: 53308
Current children cumulated CPU time (s) 1039.17
Current children cumulated vsize (Kb) 55432

[startup+1050.07 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 12409 0 0 0 104823 93 0 0 25 0 1 0 1785117510 54689792 11918 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30742/statm): 13352 11918 145 145 0 13207 0
[pid=30742] vsize: 53408
Current children cumulated CPU time (s) 1049.17
Current children cumulated vsize (Kb) 55532

[startup+1060.07 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 12549 0 0 0 105821 95 0 0 22 0 1 0 1785117510 55259136 12058 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30742/statm): 13491 12058 145 145 0 13346 0
[pid=30742] vsize: 53964
Current children cumulated CPU time (s) 1059.17
Current children cumulated vsize (Kb) 56088

[startup+1070.07 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 12713 0 0 0 106817 96 0 0 25 0 1 0 1785117510 55922688 12222 4294967295 134512640 135094434 3221224448 3221223060 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30742/statm): 13653 12222 145 145 0 13508 0
[pid=30742] vsize: 54612
Current children cumulated CPU time (s) 1069.14
Current children cumulated vsize (Kb) 56736

[startup+1080.07 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 12788 0 0 0 107817 97 0 0 25 0 1 0 1785117510 55959552 12231 4294967295 134512640 135094434 3221224448 3221223136 134554723 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30742/statm): 13662 12231 145 145 0 13517 0
[pid=30742] vsize: 54648
Current children cumulated CPU time (s) 1079.15
Current children cumulated vsize (Kb) 56772

[startup+1090.07 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 12788 0 0 0 108817 97 0 0 25 0 1 0 1785117510 55959552 12231 4294967295 134512640 135094434 3221224448 3221223104 134558398 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30742/statm): 13662 12231 145 145 0 13517 0
[pid=30742] vsize: 54648
Current children cumulated CPU time (s) 1089.15
Current children cumulated vsize (Kb) 56772

[startup+1100.07 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 12788 0 0 0 109816 98 0 0 25 0 1 0 1785117510 55959552 12231 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30742/statm): 13662 12231 145 145 0 13517 0
[pid=30742] vsize: 54648
Current children cumulated CPU time (s) 1099.15
Current children cumulated vsize (Kb) 56772

[startup+1110.07 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 12788 0 0 0 110816 98 0 0 25 0 1 0 1785117510 55959552 12231 4294967295 134512640 135094434 3221224448 3221223104 134558276 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30742/statm): 13662 12231 145 145 0 13517 0
[pid=30742] vsize: 54648
Current children cumulated CPU time (s) 1109.15
Current children cumulated vsize (Kb) 56772

[startup+1120.08 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 12788 0 0 0 111816 98 0 0 25 0 1 0 1785117510 55959552 12231 4294967295 134512640 135094434 3221224448 3221223112 134562037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30742/statm): 13662 12231 145 145 0 13517 0
[pid=30742] vsize: 54648
Current children cumulated CPU time (s) 1119.15
Current children cumulated vsize (Kb) 56772

[startup+1130.08 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 12788 0 0 0 112815 99 0 0 25 0 1 0 1785117510 55959552 12231 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30742/statm): 13662 12231 145 145 0 13517 0
[pid=30742] vsize: 54648
Current children cumulated CPU time (s) 1129.15
Current children cumulated vsize (Kb) 56772

[startup+1140.08 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 12788 0 0 0 113815 99 0 0 25 0 1 0 1785117510 55959552 12231 4294967295 134512640 135094434 3221224448 3221223072 134557737 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/30742/statm): 13662 12231 145 145 0 13517 0
[pid=30742] vsize: 54648
Current children cumulated CPU time (s) 1139.15
Current children cumulated vsize (Kb) 56772

[startup+1150.08 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 12788 0 0 0 114815 99 0 0 25 0 1 0 1785117510 55959552 12231 4294967295 134512640 135094434 3221224448 3221223072 134557655 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30742/statm): 13662 12231 145 145 0 13517 0
[pid=30742] vsize: 54648
Current children cumulated CPU time (s) 1149.15
Current children cumulated vsize (Kb) 56772

[startup+1160.08 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 12788 0 0 0 115815 99 0 0 25 0 1 0 1785117510 55959552 12231 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30742/statm): 13662 12231 145 145 0 13517 0
[pid=30742] vsize: 54648
Current children cumulated CPU time (s) 1159.15
Current children cumulated vsize (Kb) 56772

[startup+1170.08 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 12788 0 0 0 116815 99 0 0 25 0 1 0 1785117510 55959552 12231 4294967295 134512640 135094434 3221224448 3221223088 134558043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30742/statm): 13662 12231 145 145 0 13517 0
[pid=30742] vsize: 54648
Current children cumulated CPU time (s) 1169.15
Current children cumulated vsize (Kb) 56772

[startup+1180.08 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 12788 0 0 0 117816 99 0 0 25 0 1 0 1785117510 55959552 12231 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30742/statm): 13662 12231 145 145 0 13517 0
[pid=30742] vsize: 54648
Current children cumulated CPU time (s) 1179.16
Current children cumulated vsize (Kb) 56772

[startup+1190.08 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 12788 0 0 0 118816 100 0 0 25 0 1 0 1785117510 55959552 12231 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30742/statm): 13662 12231 145 145 0 13517 0
[pid=30742] vsize: 54648
Current children cumulated CPU time (s) 1189.17
Current children cumulated vsize (Kb) 56772

[startup+1200.08 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 12788 0 0 0 119816 100 0 0 25 0 1 0 1785117510 55959552 12231 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30742/statm): 13662 12231 145 145 0 13517 0
[pid=30742] vsize: 54648
Current children cumulated CPU time (s) 1199.17
Current children cumulated vsize (Kb) 56772

[startup+1210.08 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 12788 0 0 0 120816 100 0 0 25 0 1 0 1785117510 55959552 12231 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30742/statm): 13662 12231 145 145 0 13517 0
[pid=30742] vsize: 54648
Current children cumulated CPU time (s) 1209.17
Current children cumulated vsize (Kb) 56772



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.08 s]
Raw data (loadavg): 0.99 0.98 0.99 2/57 30742
Raw data (/proc/30738/stat): 30738 (minisat+_script) S 30737 30738 22582 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785117505 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/30738/statm): 531 226 485 147 0 384 0
[pid=30738] vsize: 2124
Raw data (/proc/30742/stat): 30742 (minisat+_64-bit) R 30738 30738 22582 0 -1 0 12788 0 0 0 120816 100 0 0 25 0 1 0 1785117510 55959552 12231 4294967295 134512640 135094434 3221224448 3221223072 134557711 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/30742/statm): 13662 12231 145 145 0 13517 0
[pid=30742] vsize: 54648
Current children cumulated CPU time (s) 1209.17
Current children cumulated vsize (Kb) 56772

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

Child status: 10
Real time (s): 1210.11
CPU time (s): 1209.19
CPU user time (s): 1208.17
CPU system time (s): 1.02584
CPU usage (%): 99.9243
Max. virtual memory (cumulated for all children) (Kb): 56772

Verifier Data

ERROR: no interpretation found !