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 5964

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc23 THE 2005-04-14 02:31:31 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4386 boxname=wulflinc23 idbench=250 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  9b291040ec2b77d0bffb739c0db80d53  /oldhome/oroussel/tmp/wulflinc23/normalized-c8.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc23/normalized-c8.opb /oldhome/oroussel/tmp/wulflinc23/normalized-c8.opb
IDLAUNCH: 4386
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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	: 3
cpu MHz		: 451.037
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:        893612 kB
Buffers:         34896 kB
Cached:          63308 kB
SwapCached:        192 kB
Active:          53144 kB
Inactive:        48120 kB
HighTotal:      131008 kB
HighFree:        63896 kB
LowTotal:       903652 kB
LowFree:        829716 kB
SwapTotal:     2097136 kB
SwapFree:      2096944 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6908 kB
Slab:            34132 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 02:51:34 (client local time) WITH STATUS 10 IN 1200.22 SECONDS
stats: 4386 7 1200.22 10
#### 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   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
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 % |
#### 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.84 0.94 0.90 2/54 7560
Raw data (stat): 7560 (runsolver) R 7559 3260 3259 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481009741 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0004 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 5840 0 0 0 984 14 0 0 25 0 1 0 481009741 30285824 5681 4294967295 134512640 134672761 3221224576 3221223776 134557900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7394 5681 603 41 0 7353 0
vsize: 29576
[startup+20.0016 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 5863 0 0 0 1983 14 0 0 25 0 1 0 481009741 30285824 5704 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7394 5704 603 41 0 7353 0
vsize: 29576
[startup+30.0022 s]
Raw data (loadavg): 0.90 0.94 0.90 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 5974 0 0 0 2981 15 0 0 25 0 1 0 481009741 30822400 5815 4294967295 134512640 134672761 3221224576 3221223776 134557885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7525 5815 603 41 0 7484 0
vsize: 30100
[startup+40.0012 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 6100 0 0 0 3980 16 0 0 25 0 1 0 481009741 31363072 5941 4294967295 134512640 134672761 3221224576 3221223680 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7657 5941 603 41 0 7616 0
vsize: 30628
[startup+50.0022 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 6183 0 0 0 4980 16 0 0 25 0 1 0 481009741 31633408 6024 4294967295 134512640 134672761 3221224576 3221223744 134560979 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7723 6024 603 41 0 7682 0
vsize: 30892
[startup+60.0022 s]
Raw data (loadavg): 0.94 0.95 0.90 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 6313 0 0 0 5979 16 0 0 25 0 1 0 481009741 32182272 6154 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7857 6154 603 41 0 7816 0
vsize: 31428
[startup+70.0022 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 6468 0 0 0 6978 17 0 0 25 0 1 0 481009741 32854016 6309 4294967295 134512640 134672761 3221224576 3221223712 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8021 6309 603 41 0 7980 0
vsize: 32084
[startup+80.0031 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 6586 0 0 0 7978 17 0 0 25 0 1 0 481009741 33255424 6427 4294967295 134512640 134672761 3221224576 3221223776 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8119 6427 603 41 0 8078 0
vsize: 32476
[startup+90.0028 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 6621 0 0 0 8978 18 0 0 25 0 1 0 481009741 33386496 6462 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8151 6462 603 41 0 8110 0
vsize: 32604
[startup+100.003 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 6692 0 0 0 9978 18 0 0 25 0 1 0 481009741 33648640 6533 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8215 6533 603 41 0 8174 0
vsize: 32860
[startup+110.003 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 6760 0 0 0 10977 19 0 0 25 0 1 0 481009741 34099200 6601 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8325 6601 603 41 0 8284 0
vsize: 33300
[startup+120.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 6888 0 0 0 11977 19 0 0 25 0 1 0 481009741 34500608 6729 4294967295 134512640 134672761 3221224576 3221223760 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8423 6729 603 41 0 8382 0
vsize: 33692
[startup+130.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 6915 0 0 0 12977 19 0 0 25 0 1 0 481009741 34631680 6756 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8455 6756 603 41 0 8414 0
vsize: 33820
[startup+140.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 6971 0 0 0 13977 19 0 0 25 0 1 0 481009741 34897920 6812 4294967295 134512640 134672761 3221224576 3221223776 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8520 6812 603 41 0 8479 0
vsize: 34080
[startup+150.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 7034 0 0 0 14977 19 0 0 25 0 1 0 481009741 35168256 6875 4294967295 134512640 134672761 3221224576 3221223776 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8586 6875 603 41 0 8545 0
vsize: 34344
[startup+160.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 7159 0 0 0 15977 20 0 0 25 0 1 0 481009741 35708928 7000 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8718 7000 603 41 0 8677 0
vsize: 34872
[startup+170.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 7208 0 0 0 16978 20 0 0 25 0 1 0 481009741 35844096 7049 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8751 7049 603 41 0 8710 0
vsize: 35004
[startup+180.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 7258 0 0 0 17978 20 0 0 25 0 1 0 481009741 35979264 7099 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8784 7099 603 41 0 8743 0
vsize: 35136
[startup+190.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 7435 0 0 0 18977 20 0 0 25 0 1 0 481009741 36782080 7276 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8980 7276 603 41 0 8939 0
vsize: 35920
[startup+200.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 7586 0 0 0 19977 20 0 0 25 0 1 0 481009741 37318656 7427 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9111 7427 603 41 0 9070 0
vsize: 36444
[startup+210.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 7633 0 0 0 20977 21 0 0 25 0 1 0 481009741 37584896 7474 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9176 7474 603 41 0 9135 0
vsize: 36704
[startup+220.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 7668 0 0 0 21977 21 0 0 25 0 1 0 481009741 37715968 7509 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9208 7509 603 41 0 9167 0
vsize: 36832
[startup+230.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 7693 0 0 0 22978 21 0 0 25 0 1 0 481009741 37847040 7534 4294967295 134512640 134672761 3221224576 3221223712 134560703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9240 7534 603 41 0 9199 0
vsize: 36960
[startup+240.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 7718 0 0 0 23977 21 0 0 25 0 1 0 481009741 37847040 7559 4294967295 134512640 134672761 3221224576 3221223712 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9240 7559 603 41 0 9199 0
vsize: 36960
[startup+250.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 7795 0 0 0 24977 22 0 0 25 0 1 0 481009741 38252544 7636 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9339 7636 603 41 0 9298 0
vsize: 37356
[startup+260.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 7860 0 0 0 25977 22 0 0 25 0 1 0 481009741 38522880 7701 4294967295 134512640 134672761 3221224576 3221223776 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9405 7701 603 41 0 9364 0
vsize: 37620
[startup+270.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 7898 0 0 0 26977 22 0 0 25 0 1 0 481009741 38785024 7739 4294967295 134512640 134672761 3221224576 3221223712 134560613 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9469 7739 603 41 0 9428 0
vsize: 37876
[startup+280.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 7919 0 0 0 27977 22 0 0 25 0 1 0 481009741 38785024 7760 4294967295 134512640 134672761 3221224576 3221223776 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9469 7760 603 41 0 9428 0
vsize: 37876
[startup+290.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 7945 0 0 0 28977 22 0 0 25 0 1 0 481009741 38916096 7786 4294967295 134512640 134672761 3221224576 3221223760 134558648 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9501 7786 603 41 0 9460 0
vsize: 38004
[startup+300.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 8079 0 0 0 29977 23 0 0 25 0 1 0 481009741 39456768 7920 4294967295 134512640 134672761 3221224576 3221223680 134559877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9633 7920 603 41 0 9592 0
vsize: 38532
[startup+310.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 8261 0 0 0 30976 23 0 0 25 0 1 0 481009741 40259584 8102 4294967295 134512640 134672761 3221224576 3221223744 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9829 8102 603 41 0 9788 0
vsize: 39316
[startup+320.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 8322 0 0 0 31976 24 0 0 25 0 1 0 481009741 40525824 8163 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9894 8163 603 41 0 9853 0
vsize: 39576
[startup+330.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 8444 0 0 0 32976 24 0 0 25 0 1 0 481009741 40927232 8285 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9992 8285 603 41 0 9951 0
vsize: 39968
[startup+340.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 8712 0 0 0 33975 25 0 0 25 0 1 0 481009741 42135552 8553 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10287 8553 603 41 0 10246 0
vsize: 41148
[startup+350.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 8894 0 0 0 34975 26 0 0 25 0 1 0 481009741 42807296 8735 4294967295 134512640 134672761 3221224576 3221223712 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10451 8735 603 41 0 10410 0
vsize: 41804
[startup+360.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 9093 0 0 0 35974 27 0 0 25 0 1 0 481009741 43618304 8934 4294967295 134512640 134672761 3221224576 3221223576 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10649 8934 603 41 0 10608 0
vsize: 42596
[startup+370.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 9257 0 0 0 36974 27 0 0 25 0 1 0 481009741 44277760 9098 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10810 9098 603 41 0 10769 0
vsize: 43240
[startup+380.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 9437 0 0 0 37974 28 0 0 25 0 1 0 481009741 45064192 9278 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11002 9278 603 41 0 10961 0
vsize: 44008
[startup+390.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 9626 0 0 0 38973 29 0 0 25 0 1 0 481009741 45867008 9467 4294967295 134512640 134672761 3221224576 3221223776 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11198 9467 603 41 0 11157 0
vsize: 44792
[startup+400.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 9721 0 0 0 39973 29 0 0 25 0 1 0 481009741 46264320 9562 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11295 9562 603 41 0 11254 0
vsize: 45180
[startup+410.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 9830 0 0 0 40972 30 0 0 25 0 1 0 481009741 46665728 9671 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11393 9671 603 41 0 11352 0
vsize: 45572
[startup+420.007 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 9932 0 0 0 41972 30 0 0 25 0 1 0 481009741 47067136 9773 4294967295 134512640 134672761 3221224576 3221223744 134560885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11491 9773 603 41 0 11450 0
vsize: 45964
[startup+430.006 s]
Raw data (loadavg): 1.14 1.00 0.92 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 9999 0 0 0 42972 30 0 0 25 0 1 0 481009741 47337472 9840 4294967295 134512640 134672761 3221224576 3221223776 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11557 9840 603 41 0 11516 0
vsize: 46228
[startup+440.006 s]
Raw data (loadavg): 1.11 1.00 0.92 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 10067 0 0 0 43972 30 0 0 25 0 1 0 481009741 47607808 9908 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11623 9908 603 41 0 11582 0
vsize: 46492
[startup+450.006 s]
Raw data (loadavg): 1.10 1.00 0.92 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 10241 0 0 0 44972 31 0 0 25 0 1 0 481009741 48279552 10082 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11787 10082 603 41 0 11746 0
vsize: 47148
[startup+460.006 s]
Raw data (loadavg): 1.08 1.00 0.92 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 10430 0 0 0 45971 31 0 0 25 0 1 0 481009741 49078272 10271 4294967295 134512640 134672761 3221224576 3221223532 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11982 10271 603 41 0 11941 0
vsize: 47928
[startup+470.007 s]
Raw data (loadavg): 1.07 1.00 0.92 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 10511 0 0 0 46971 32 0 0 25 0 1 0 481009741 49348608 10352 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12048 10352 603 41 0 12007 0
vsize: 48192
[startup+480.007 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 10631 0 0 0 47971 32 0 0 25 0 1 0 481009741 49885184 10472 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12179 10472 603 41 0 12138 0
vsize: 48716
[startup+490.006 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 10702 0 0 0 48971 32 0 0 25 0 1 0 481009741 50155520 10543 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12245 10543 603 41 0 12204 0
vsize: 48980
[startup+500.006 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 10801 0 0 0 49971 33 0 0 25 0 1 0 481009741 50561024 10642 4294967295 134512640 134672761 3221224576 3221223744 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12344 10642 603 41 0 12303 0
vsize: 49376
[startup+510.006 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 11082 0 0 0 50970 33 0 0 25 0 1 0 481009741 51777536 10923 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12641 10923 603 41 0 12600 0
vsize: 50564
[startup+520.006 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 11296 0 0 0 51970 34 0 0 25 0 1 0 481009741 52572160 11137 4294967295 134512640 134672761 3221224576 3221223744 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12835 11137 603 41 0 12794 0
vsize: 51340
[startup+530.007 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 11522 0 0 0 52969 35 0 0 25 0 1 0 481009741 53506048 11363 4294967295 134512640 134672761 3221224576 3221223744 134561266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13063 11363 603 41 0 13022 0
vsize: 52252
[startup+540.007 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 11853 0 0 0 53968 36 0 0 25 0 1 0 481009741 54845440 11694 4294967295 134512640 134672761 3221224576 3221223680 134560335 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13390 11694 603 41 0 13349 0
vsize: 53560
[startup+550.007 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 11891 0 0 0 54968 36 0 0 25 0 1 0 481009741 54980608 11732 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13423 11732 603 41 0 13382 0
vsize: 53692
[startup+560.015 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 11892 0 0 0 55969 36 0 0 25 0 1 0 481009741 54980608 11733 4294967295 134512640 134672761 3221224576 3221223720 134560630 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13423 11733 603 41 0 13382 0
vsize: 53692
[startup+570.016 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 11892 0 0 0 56969 36 0 0 25 0 1 0 481009741 54980608 11733 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13423 11733 603 41 0 13382 0
vsize: 53692
[startup+580.016 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 11892 0 0 0 57969 36 0 0 25 0 1 0 481009741 54980608 11733 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13423 11733 603 41 0 13382 0
vsize: 53692
[startup+590.016 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 11892 0 0 0 58970 36 0 0 25 0 1 0 481009741 54980608 11733 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13423 11733 603 41 0 13382 0
vsize: 53692
[startup+600.017 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 11892 0 0 0 59970 36 0 0 25 0 1 0 481009741 54980608 11733 4294967295 134512640 134672761 3221224576 3221223776 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13423 11733 603 41 0 13382 0
vsize: 53692
[startup+610.016 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 11892 0 0 0 60970 36 0 0 25 0 1 0 481009741 54980608 11733 4294967295 134512640 134672761 3221224576 3221223680 134560410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13423 11733 603 41 0 13382 0
vsize: 53692
[startup+620.017 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 11892 0 0 0 61970 36 0 0 25 0 1 0 481009741 54980608 11733 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13423 11733 603 41 0 13382 0
vsize: 53692
[startup+630.018 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 11892 0 0 0 62970 36 0 0 25 0 1 0 481009741 54980608 11733 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13423 11733 603 41 0 13382 0
vsize: 53692
[startup+640.017 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 11892 0 0 0 63970 36 0 0 25 0 1 0 481009741 54980608 11733 4294967295 134512640 134672761 3221224576 3221223760 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13423 11733 603 41 0 13382 0
vsize: 53692
[startup+650.018 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 11892 0 0 0 64971 36 0 0 25 0 1 0 481009741 54980608 11733 4294967295 134512640 134672761 3221224576 3221223744 134560994 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13423 11733 603 41 0 13382 0
vsize: 53692
[startup+660.018 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 11892 0 0 0 65971 36 0 0 25 0 1 0 481009741 54980608 11733 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13423 11733 603 41 0 13382 0
vsize: 53692
[startup+670.018 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 11892 0 0 0 66971 36 0 0 25 0 1 0 481009741 54980608 11733 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13423 11733 603 41 0 13382 0
vsize: 53692
[startup+680.018 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 11892 0 0 0 67971 36 0 0 25 0 1 0 481009741 54980608 11733 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13423 11733 603 41 0 13382 0
vsize: 53692
[startup+690.018 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 11892 0 0 0 68971 36 0 0 25 0 1 0 481009741 54980608 11733 4294967295 134512640 134672761 3221224576 3221223712 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13423 11733 603 41 0 13382 0
vsize: 53692
[startup+700.018 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 11892 0 0 0 69972 36 0 0 25 0 1 0 481009741 54980608 11733 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13423 11733 603 41 0 13382 0
vsize: 53692
[startup+710.018 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 11892 0 0 0 70972 36 0 0 25 0 1 0 481009741 54980608 11733 4294967295 134512640 134672761 3221224576 3221223680 134560418 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13423 11733 603 41 0 13382 0
vsize: 53692
[startup+720.018 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 11892 0 0 0 71972 36 0 0 25 0 1 0 481009741 54980608 11733 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13423 11733 603 41 0 13382 0
vsize: 53692
[startup+730.018 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 11892 0 0 0 72972 36 0 0 25 0 1 0 481009741 54980608 11733 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13423 11733 603 41 0 13382 0
vsize: 53692
[startup+740.018 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 11892 0 0 0 73972 36 0 0 25 0 1 0 481009741 54980608 11733 4294967295 134512640 134672761 3221224576 3221223776 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13423 11733 603 41 0 13382 0
vsize: 53692
[startup+750.019 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 11892 0 0 0 74972 36 0 0 25 0 1 0 481009741 54980608 11733 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13423 11733 603 41 0 13382 0
vsize: 53692
[startup+760.019 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 11892 0 0 0 75973 37 0 0 25 0 1 0 481009741 54980608 11733 4294967295 134512640 134672761 3221224576 3221223680 134559847 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13423 11733 603 41 0 13382 0
vsize: 53692
[startup+770.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 11892 0 0 0 76973 37 0 0 25 0 1 0 481009741 54980608 11733 4294967295 134512640 134672761 3221224576 3221223744 134560833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13423 11733 603 41 0 13382 0
vsize: 53692
[startup+780.019 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 11892 0 0 0 77973 37 0 0 25 0 1 0 481009741 54980608 11733 4294967295 134512640 134672761 3221224576 3221223680 134555175 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13423 11733 603 41 0 13382 0
vsize: 53692
[startup+790.019 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 11892 0 0 0 78973 37 0 0 25 0 1 0 481009741 54980608 11733 4294967295 134512640 134672761 3221224576 3221223712 134560697 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13423 11733 603 41 0 13382 0
vsize: 53692
[startup+800.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 11892 0 0 0 79973 37 0 0 25 0 1 0 481009741 54980608 11733 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13423 11733 603 41 0 13382 0
vsize: 53692
[startup+810.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 11892 0 0 0 80973 37 0 0 25 0 1 0 481009741 54980608 11733 4294967295 134512640 134672761 3221224576 3221223712 134560557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13423 11733 603 41 0 13382 0
vsize: 53692
[startup+820.021 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 11892 0 0 0 81974 37 0 0 25 0 1 0 481009741 54980608 11733 4294967295 134512640 134672761 3221224576 3221223776 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13423 11733 603 41 0 13382 0
vsize: 53692
[startup+830.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 11892 0 0 0 82974 37 0 0 25 0 1 0 481009741 54980608 11733 4294967295 134512640 134672761 3221224576 3221223680 134560191 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13423 11733 603 41 0 13382 0
vsize: 53692
[startup+840.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 11892 0 0 0 83974 37 0 0 25 0 1 0 481009741 54980608 11733 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13423 11733 603 41 0 13382 0
vsize: 53692
[startup+850.021 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 11892 0 0 0 84974 37 0 0 25 0 1 0 481009741 54980608 11733 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13423 11733 603 41 0 13382 0
vsize: 53692
[startup+860.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 11892 0 0 0 85974 37 0 0 25 0 1 0 481009741 54980608 11733 4294967295 134512640 134672761 3221224576 3221223760 134558656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13423 11733 603 41 0 13382 0
vsize: 53692
[startup+870.021 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 11892 0 0 0 86975 37 0 0 25 0 1 0 481009741 54980608 11733 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13423 11733 603 41 0 13382 0
vsize: 53692
[startup+880.022 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 11892 0 0 0 87975 37 0 0 25 0 1 0 481009741 54980608 11733 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13423 11733 603 41 0 13382 0
vsize: 53692
[startup+890.021 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 11892 0 0 0 88975 37 0 0 25 0 1 0 481009741 54980608 11733 4294967295 134512640 134672761 3221224576 3221223744 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13423 11733 603 41 0 13382 0
vsize: 53692
[startup+900.022 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 11892 0 0 0 89975 37 0 0 25 0 1 0 481009741 54980608 11733 4294967295 134512640 134672761 3221224576 3221223760 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13423 11733 603 41 0 13382 0
vsize: 53692
[startup+910.023 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 11892 0 0 0 90975 37 0 0 25 0 1 0 481009741 54980608 11733 4294967295 134512640 134672761 3221224576 3221223744 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13423 11733 603 41 0 13382 0
vsize: 53692
[startup+920.023 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 11892 0 0 0 91976 37 0 0 25 0 1 0 481009741 54980608 11733 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13423 11733 603 41 0 13382 0
vsize: 53692
[startup+930.024 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 11892 0 0 0 92976 37 0 0 25 0 1 0 481009741 54980608 11733 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13423 11733 603 41 0 13382 0
vsize: 53692
[startup+940.025 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 11892 0 0 0 93976 37 0 0 25 0 1 0 481009741 54980608 11733 4294967295 134512640 134672761 3221224576 3221223680 134560158 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13423 11733 603 41 0 13382 0
vsize: 53692
[startup+950.025 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 11892 0 0 0 94976 37 0 0 25 0 1 0 481009741 54980608 11733 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13423 11733 603 41 0 13382 0
vsize: 53692
[startup+960.025 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 11892 0 0 0 95977 37 0 0 25 0 1 0 481009741 54980608 11733 4294967295 134512640 134672761 3221224576 3221223744 134561139 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13423 11733 603 41 0 13382 0
vsize: 53692
[startup+970.025 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 11892 0 0 0 96977 37 0 0 25 0 1 0 481009741 54980608 11733 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13423 11733 603 41 0 13382 0
vsize: 53692
[startup+980.026 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 11893 0 0 0 97977 37 0 0 25 0 1 0 481009741 54980608 11734 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13423 11734 603 41 0 13382 0
vsize: 53692
[startup+990.026 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 11893 0 0 0 98977 37 0 0 25 0 1 0 481009741 54980608 11734 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13423 11734 603 41 0 13382 0
vsize: 53692
[startup+1000.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 11919 0 0 0 99977 37 0 0 25 0 1 0 481009741 55115776 11760 4294967295 134512640 134672761 3221224576 3221223744 134560797 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13456 11760 603 41 0 13415 0
vsize: 53824
[startup+1010.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 11983 0 0 0 100977 37 0 0 25 0 1 0 481009741 55644160 11824 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13585 11824 603 41 0 13544 0
vsize: 54340
[startup+1020.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 12029 0 0 0 101977 37 0 0 25 0 1 0 481009741 55779328 11870 4294967295 134512640 134672761 3221224576 3221223712 134560557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13618 11870 603 41 0 13577 0
vsize: 54472
[startup+1030.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 12089 0 0 0 102977 37 0 0 25 0 1 0 481009741 56049664 11930 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13684 11930 603 41 0 13643 0
vsize: 54736
[startup+1040.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 12140 0 0 0 103977 38 0 0 25 0 1 0 481009741 56311808 11981 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13748 11981 603 41 0 13707 0
vsize: 54992
[startup+1050.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 12180 0 0 0 104977 38 0 0 25 0 1 0 481009741 56446976 12021 4294967295 134512640 134672761 3221224576 3221223744 134561025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13781 12021 603 41 0 13740 0
vsize: 55124
[startup+1060.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 12204 0 0 0 105977 38 0 0 25 0 1 0 481009741 56578048 12045 4294967295 134512640 134672761 3221224576 3221223732 134561241 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13813 12045 603 41 0 13772 0
vsize: 55252
[startup+1070.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 12246 0 0 0 106977 38 0 0 25 0 1 0 481009741 56709120 12087 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13845 12087 603 41 0 13804 0
vsize: 55380
[startup+1080.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 12413 0 0 0 107977 39 0 0 25 0 1 0 481009741 57380864 12254 4294967295 134512640 134672761 3221224576 3221223712 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14009 12255 603 41 0 13968 0
vsize: 56036
[startup+1090.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 12531 0 0 0 108977 39 0 0 25 0 1 0 481009741 57892864 12372 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14134 12372 603 41 0 14093 0
vsize: 56536
[startup+1100.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 12531 0 0 0 109977 39 0 0 25 0 1 0 481009741 57892864 12372 4294967295 134512640 134672761 3221224576 3221223744 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14134 12372 603 41 0 14093 0
vsize: 56536
[startup+1110.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 12531 0 0 0 110977 39 0 0 25 0 1 0 481009741 57892864 12372 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14134 12372 603 41 0 14093 0
vsize: 56536
[startup+1120.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 12531 0 0 0 111977 39 0 0 25 0 1 0 481009741 57892864 12372 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14134 12372 603 41 0 14093 0
vsize: 56536
[startup+1130.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 12531 0 0 0 112978 39 0 0 25 0 1 0 481009741 57892864 12372 4294967295 134512640 134672761 3221224576 3221223744 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14134 12372 603 41 0 14093 0
vsize: 56536
[startup+1140.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 12531 0 0 0 113978 39 0 0 25 0 1 0 481009741 57892864 12372 4294967295 134512640 134672761 3221224576 3221223744 134561406 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14134 12372 603 41 0 14093 0
vsize: 56536
[startup+1150.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 12531 0 0 0 114978 39 0 0 25 0 1 0 481009741 57892864 12372 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14134 12372 603 41 0 14093 0
vsize: 56536
[startup+1160.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 12531 0 0 0 115978 39 0 0 25 0 1 0 481009741 57892864 12372 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14134 12372 603 41 0 14093 0
vsize: 56536
[startup+1170.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 12531 0 0 0 116979 39 0 0 25 0 1 0 481009741 57892864 12372 4294967295 134512640 134672761 3221224576 3221223776 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14134 12372 603 41 0 14093 0
vsize: 56536
[startup+1180.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 12531 0 0 0 117979 39 0 0 25 0 1 0 481009741 57892864 12372 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14134 12372 603 41 0 14093 0
vsize: 56536
[startup+1190.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 12531 0 0 0 118979 39 0 0 25 0 1 0 481009741 57892864 12372 4294967295 134512640 134672761 3221224576 3221223728 134561249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14134 12372 603 41 0 14093 0
vsize: 56536
[startup+1200.03 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 7560
Raw data (stat): 7560 (minisat+) R 7559 3260 3259 0 -1 0 12531 0 0 0 119979 39 0 0 25 0 1 0 481009741 57892864 12372 4294967295 134512640 134672761 3221224576 3221223744 134561234 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14134 12372 603 41 0 14093 0
vsize: 56536
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 1.00 1.00 0.92 1/54 7560
Raw data (stat): 7560 (minisat+) Z 7559 3260 3259 0 -1 12 12534 0 0 0 119979 42 0 0 25 0 1 0 481009741 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.06
CPU time (s): 1200.22
CPU user time (s): 1199.8
CPU system time (s): 0.420936
CPU usage (%): 100.013
Max. virtual memory (Kb): 56536
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####