PB'05 competition: run trace

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:
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.
SOLVER DATA
This is the output of the solver (stdout and stderr).
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.
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

Name	normalized-opb/submitted/manquinho/synthesis-ptl-cmos-circuits/normalized-c8.opb
MD5SUM	9b291040ec2b77d0bffb739c0db80d53
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	1194
Optimality of the best value was proved	NO
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 numbers	14
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	0.941856
Number of variables	239
Total number of constraints	524
Number of constraints which are clauses	520
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	4
Minimum length of a constraint	1
Maximum length of a constraint	36
Trace number 30473

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc12 THE 2005-05-25 16:54:02 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=21832 boxname=wulflinc12 idbench=250 idsolver=15 numberseed=0
MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814  /oldhome/oroussel/solvers/minisat+_script
MD5SUM BENCH:  9b291040ec2b77d0bffb739c0db80d53  /oldhome/oroussel/tmp/wulflinc12/normalized-c8.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc12/normalized-c8.opb
IDLAUNCH: 21832
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.091
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.091
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:        347436 kB
Buffers:         34776 kB
Cached:         631128 kB
SwapCached:        564 kB
Active:          55872 kB
Inactive:       612504 kB
HighTotal:      131008 kB
HighFree:         1904 kB
LowTotal:       903652 kB
LowFree:        345532 kB
SwapTotal:     2097136 kB
SwapFree:      2096076 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5680 kB
Slab:            13248 kB
Committed_AS:    63604 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-25 17:14:32 (client local time) WITH STATUS 152 IN 1229.86 SECONDS
stats: 21832 7 1229.86 152
#### END LAUNCHER DATA ####
#### BEGIN 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 [1mFound solution: 1761[0m
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 [1mFound solution: 1663[0m
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 [1mFound solution: 1659[0m
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 [1mFound solution: 1635[0m
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 [1mFound solution: 1633[0m
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 [1mFound solution: 1575[0m
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 [1mFound solution: 1563[0m
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 [1mFound solution: 1562[0m
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 [1mFound solution: 1503[0m
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 [1mFound solution: 1498[0m
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 [1mFound solution: 1496[0m
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 [1mFound solution: 1477[0m
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 [1mFound solution: 1446[0m
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 [1mFound solution: 1394[0m
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 [1mFound solution: 1386[0m
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 [1mFound solution: 1379[0m
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 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 15145 CPU time limit exceeded $XDIR/minisat+_64-bit_static -try "$@"
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.62 0.85 0.90 2/54 15141
Raw data (stat): 15141 (runsolver) R 15140 32284 32283 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 782246159 1052672 99 4294967295 134512640 135381576 3221224496 3221219704 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0006 s]
Raw data (loadavg): 0.68 0.85 0.90 2/55 15145
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20.001 s]
Raw data (loadavg): 0.73 0.86 0.91 2/55 15145
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.0018 s]
Raw data (loadavg): 0.77 0.86 0.91 2/55 15145
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.0025 s]
Raw data (loadavg): 0.80 0.87 0.91 2/55 15145
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0035 s]
Raw data (loadavg): 0.83 0.87 0.91 2/55 15145
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.0033 s]
Raw data (loadavg): 0.86 0.87 0.91 2/55 15145
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.0046 s]
Raw data (loadavg): 0.88 0.88 0.91 2/55 15145
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.0061 s]
Raw data (loadavg): 0.90 0.88 0.91 2/55 15145
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.0059 s]
Raw data (loadavg): 0.91 0.88 0.91 2/55 15145
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.007 s]
Raw data (loadavg): 0.93 0.89 0.91 2/55 15145
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.008 s]
Raw data (loadavg): 0.94 0.89 0.91 2/55 15145
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.008 s]
Raw data (loadavg): 0.95 0.89 0.91 2/55 15145
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.01 s]
Raw data (loadavg): 0.95 0.90 0.91 2/55 15145
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.01 s]
Raw data (loadavg): 0.96 0.90 0.91 2/55 15145
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.011 s]
Raw data (loadavg): 0.97 0.90 0.91 2/55 15145
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.012 s]
Raw data (loadavg): 0.97 0.91 0.91 2/55 15145
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.012 s]
Raw data (loadavg): 0.97 0.91 0.91 2/55 15145
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.012 s]
Raw data (loadavg): 0.98 0.91 0.91 2/55 15145
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.014 s]
Raw data (loadavg): 0.98 0.91 0.91 2/55 15145
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.014 s]
Raw data (loadavg): 0.98 0.92 0.91 2/55 15145
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.014 s]
Raw data (loadavg): 0.99 0.92 0.91 2/55 15145
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.016 s]
Raw data (loadavg): 0.99 0.92 0.91 2/55 15145
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.016 s]
Raw data (loadavg): 0.99 0.92 0.91 2/55 15145
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.016 s]
Raw data (loadavg): 0.99 0.92 0.91 2/55 15145
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.017 s]
Raw data (loadavg): 0.99 0.93 0.91 2/55 15145
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.017 s]
Raw data (loadavg): 0.99 0.93 0.91 2/55 15145
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.017 s]
Raw data (loadavg): 0.99 0.93 0.91 2/55 15145
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.019 s]
Raw data (loadavg): 0.99 0.93 0.91 2/55 15145
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.019 s]
Raw data (loadavg): 0.99 0.93 0.91 2/55 15145
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.02 s]
Raw data (loadavg): 0.99 0.93 0.91 2/55 15145
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.02 s]
Raw data (loadavg): 0.99 0.94 0.91 2/55 15145
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.019 s]
Raw data (loadavg): 0.99 0.94 0.91 2/55 15145
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330.02 s]
Raw data (loadavg): 0.99 0.94 0.91 2/55 15145
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340.021 s]
Raw data (loadavg): 0.99 0.94 0.91 2/55 15145
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+350.022 s]
Raw data (loadavg): 0.99 0.94 0.91 2/55 15145
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+360.023 s]
Raw data (loadavg): 0.99 0.94 0.91 2/55 15145
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+370.022 s]
Raw data (loadavg): 1.07 0.96 0.91 2/55 15198
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380.022 s]
Raw data (loadavg): 1.06 0.96 0.91 2/55 15198
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+390.022 s]
Raw data (loadavg): 1.05 0.96 0.91 2/55 15198
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+400.028 s]
Raw data (loadavg): 1.04 0.96 0.91 2/55 15198
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+410.029 s]
Raw data (loadavg): 1.03 0.97 0.91 2/55 15198
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+420.029 s]
Raw data (loadavg): 1.03 0.97 0.91 2/55 15198
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+430.029 s]
Raw data (loadavg): 1.02 0.97 0.91 2/55 15198
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+440.029 s]
Raw data (loadavg): 1.02 0.97 0.91 2/55 15200
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+450.03 s]
Raw data (loadavg): 1.02 0.97 0.91 2/55 15200
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+460.03 s]
Raw data (loadavg): 1.01 0.97 0.91 2/55 15200
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.031 s]
Raw data (loadavg): 1.01 0.97 0.91 2/55 15200
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.031 s]
Raw data (loadavg): 1.01 0.97 0.91 2/55 15200
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+490.03 s]
Raw data (loadavg): 1.01 0.97 0.91 2/55 15200
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+500.031 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 15200
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+510.031 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 15200
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+520.035 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 15200
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+530.035 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 15200
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+540.035 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 15200
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+550.035 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 15200
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+560.035 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 15200
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+570.036 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 15200
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+580.036 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 15200
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+590.036 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 15200
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+600.037 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 15200
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+610.038 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 15200
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+620.037 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 15200
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+630.038 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 15200
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+640.038 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 15200
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+650.039 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 15200
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+660.039 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 15200
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+670.039 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 15200
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+680.039 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 15202
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+690.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 15202
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+700.041 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 15202
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+710.041 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 15202
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+720.041 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 15202
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+730.042 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 15202
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+740.042 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 15202
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+750.043 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 15202
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+760.044 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 15202
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+770.043 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 15202
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+780.044 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 15202
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+790.044 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 15202
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+800.045 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 15202
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+810.044 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 15202
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+820.045 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 15202
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+830.045 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 15202
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+840.045 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 15202
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+850.046 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 15202
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+860.046 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 15202
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+870.045 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 15202
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+880.046 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 15202
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+890.046 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 15202
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+900.047 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 15202
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+910.047 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 15202
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+920.047 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 15202
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+930.047 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 15202
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+940.047 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 15202
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+950.046 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 15202
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+960.047 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 15202
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+970.047 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 15202
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+980.047 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 15202
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+990.047 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 15202
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1000.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 15202
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1010.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 15202
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1020.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 15202
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1030.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 15202
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1040.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 15202
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1050.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 15202
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1060.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 15202
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1070.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 15202
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1080.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 15202
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1090.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 15202
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1100.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 15202
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1110.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 15202
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1120.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 15202
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1130.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 15202
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1140.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 15202
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1150.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 15202
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1160.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 15202
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1170.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 15202
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1180.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 15202
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1190.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 15202
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1200.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 15202
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1210.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 15202
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1220.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/55 15202
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1229.73 s]
Raw data (loadavg): 1.00 0.97 0.91 1/53 15202
Raw data (stat): 15141 (minisat+_script) S 15140 32284 32283 0 -1 0 273 239 0 0 0 0 0 0 19 0 1 0 782246159 2174976 226 4294967295 134512640 135087896 3221224560 3221223832 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

Child status: 152
Real time (s): 1229.73
CPU time (s): 1229.86
CPU user time (s): 1229.34
CPU system time (s): 0.511922
CPU usage (%): 100.011
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####