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 5000

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc19 THE 2005-04-13 21:11:53 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2246 boxname=wulflinc19 idbench=250 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  9b291040ec2b77d0bffb739c0db80d53  /oldhome/oroussel/tmp/wulflinc19/normalized-c8.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc19/normalized-c8.opb
IDLAUNCH: 2246
/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:        893628 kB
Buffers:         33464 kB
Cached:          74056 kB
SwapCached:         56 kB
Active:          45404 kB
Inactive:        65100 kB
HighTotal:      131008 kB
HighFree:        52864 kB
LowTotal:       903652 kB
LowFree:        840764 kB
SwapTotal:     2097892 kB
SwapFree:      2097836 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           7028 kB
Slab:            24948 kB
Committed_AS:    63704 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 21:31:55 (client local time) WITH STATUS 10 IN 1200.24 SECONDS
stats: 2246 7 1200.24 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 % |
c |    130623 |  182287   427332 |  157600   32914  1252928    38.1 |  1.965 % |
#### 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.83 0.95 0.90 2/55 26099
Raw data (stat): 26099 (runsolver) R 26098 22929 22928 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 479087975 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 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.0005 s]
Raw data (loadavg): 0.86 0.95 0.90 2/55 26099
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 5943 0 0 0 984 14 0 0 25 0 1 0 479087975 30404608 5726 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7423 5726 603 41 0 7382 0
vsize: 29692
[startup+20.0006 s]
Raw data (loadavg): 0.88 0.95 0.91 2/55 26099
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 5946 0 0 0 1984 14 0 0 25 0 1 0 479087975 30404608 5729 4294967295 134512640 134672761 3221224640 3221223840 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7423 5729 603 41 0 7382 0
vsize: 29692
[startup+30.0009 s]
Raw data (loadavg): 0.90 0.95 0.91 2/55 26099
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 6081 0 0 0 2983 14 0 0 25 0 1 0 479087975 30765056 5838 4294967295 134512640 134672761 3221224640 3221223840 134557887 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7511 5838 603 41 0 7470 0
vsize: 30044
[startup+40.0009 s]
Raw data (loadavg): 0.91 0.95 0.91 2/55 26099
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 6216 0 0 0 3983 15 0 0 25 0 1 0 479087975 31449088 5973 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7678 5973 603 41 0 7637 0
vsize: 30712
[startup+50.0016 s]
Raw data (loadavg): 0.93 0.96 0.91 2/55 26099
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 6296 0 0 0 4982 15 0 0 25 0 1 0 479087975 31715328 6053 4294967295 134512640 134672761 3221224640 3221223808 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7743 6053 603 41 0 7702 0
vsize: 30972
[startup+60.0012 s]
Raw data (loadavg): 0.94 0.96 0.91 2/55 26099
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 6449 0 0 0 5982 16 0 0 25 0 1 0 479087975 32387072 6206 4294967295 134512640 134672761 3221224640 3221223808 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7907 6206 603 41 0 7866 0
vsize: 31628
[startup+70.0013 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 26099
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 6594 0 0 0 6981 17 0 0 25 0 1 0 479087975 32923648 6351 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8038 6351 603 41 0 7997 0
vsize: 32152
[startup+80.0024 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 26099
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 6694 0 0 0 7981 17 0 0 25 0 1 0 479087975 33325056 6451 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8136 6451 603 41 0 8095 0
vsize: 32544
[startup+90.0016 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 26099
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 6789 0 0 0 8981 17 0 0 25 0 1 0 479087975 33558528 6519 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8193 6519 603 41 0 8152 0
vsize: 32772
[startup+100.003 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 26099
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 6854 0 0 0 9981 17 0 0 25 0 1 0 479087975 34013184 6584 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8304 6584 603 41 0 8263 0
vsize: 33216
[startup+110.004 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 26099
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 6981 0 0 0 10981 18 0 0 25 0 1 0 479087975 34414592 6711 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8402 6711 603 41 0 8361 0
vsize: 33608
[startup+120.003 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 26099
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 7026 0 0 0 11981 18 0 0 25 0 1 0 479087975 34680832 6756 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8467 6756 603 41 0 8426 0
vsize: 33868
[startup+130.003 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 26099
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 7054 0 0 0 12981 18 0 0 25 0 1 0 479087975 34816000 6784 4294967295 134512640 134672761 3221224640 3221223824 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8500 6784 603 41 0 8459 0
vsize: 34000
[startup+140.003 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 26099
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 7150 0 0 0 13980 19 0 0 25 0 1 0 479087975 34967552 6854 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8537 6854 603 41 0 8496 0
vsize: 34148
[startup+150.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 26099
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 7275 0 0 0 14980 20 0 0 25 0 1 0 479087975 35495936 6979 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8666 6979 603 41 0 8625 0
vsize: 34664
[startup+160.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26099
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 7335 0 0 0 15980 20 0 0 25 0 1 0 479087975 35762176 7039 4294967295 134512640 134672761 3221224640 3221223824 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8731 7039 603 41 0 8690 0
vsize: 34924
[startup+170.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26099
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 7394 0 0 0 16980 20 0 0 25 0 1 0 479087975 36024320 7098 4294967295 134512640 134672761 3221224640 3221223808 134560885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8795 7098 603 41 0 8754 0
vsize: 35180
[startup+180.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26099
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 7513 0 0 0 17980 20 0 0 25 0 1 0 479087975 36556800 7217 4294967295 134512640 134672761 3221224640 3221223744 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8925 7217 603 41 0 8884 0
vsize: 35700
[startup+190.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26099
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 7718 0 0 0 18980 20 0 0 25 0 1 0 479087975 37363712 7422 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9122 7422 603 41 0 9081 0
vsize: 36488
[startup+200.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26099
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 7774 0 0 0 19980 21 0 0 25 0 1 0 479087975 37494784 7478 4294967295 134512640 134672761 3221224640 3221223784 134560555 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9154 7478 603 41 0 9113 0
vsize: 36616
[startup+210.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26099
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 7810 0 0 0 20980 21 0 0 25 0 1 0 479087975 37761024 7514 4294967295 134512640 134672761 3221224640 3221223776 134560604 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9219 7514 603 41 0 9178 0
vsize: 36876
[startup+220.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26099
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 7843 0 0 0 21980 21 0 0 25 0 1 0 479087975 37892096 7547 4294967295 134512640 134672761 3221224640 3221223776 134560608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9251 7547 603 41 0 9210 0
vsize: 37004
[startup+230.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26099
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 7864 0 0 0 22980 21 0 0 25 0 1 0 479087975 37892096 7568 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9251 7568 603 41 0 9210 0
vsize: 37004
[startup+240.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26099
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 7911 0 0 0 23980 21 0 0 25 0 1 0 479087975 38162432 7615 4294967295 134512640 134672761 3221224640 3221223744 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9317 7615 603 41 0 9276 0
vsize: 37268
[startup+250.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26099
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 8005 0 0 0 24980 21 0 0 25 0 1 0 479087975 38432768 7709 4294967295 134512640 134672761 3221224640 3221223776 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9383 7709 603 41 0 9342 0
vsize: 37532
[startup+260.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26101
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 8052 0 0 0 25980 21 0 0 25 0 1 0 479087975 38825984 7756 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9479 7756 603 41 0 9438 0
vsize: 37916
[startup+270.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26101
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 8068 0 0 0 26980 22 0 0 25 0 1 0 479087975 38825984 7772 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9479 7772 603 41 0 9438 0
vsize: 37916
[startup+280.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26101
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 8098 0 0 0 27980 22 0 0 25 0 1 0 479087975 38961152 7802 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9512 7802 603 41 0 9471 0
vsize: 38048
[startup+290.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26101
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 8228 0 0 0 28980 22 0 0 25 0 1 0 479087975 39501824 7932 4294967295 134512640 134672761 3221224640 3221223808 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9644 7932 603 41 0 9603 0
vsize: 38576
[startup+300.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26101
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 8415 0 0 0 29980 23 0 0 25 0 1 0 479087975 40308736 8119 4294967295 134512640 134672761 3221224640 3221223776 134560673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9841 8119 603 41 0 9800 0
vsize: 39364
[startup+310.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26101
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 8477 0 0 0 30979 23 0 0 25 0 1 0 479087975 40570880 8181 4294967295 134512640 134672761 3221224640 3221223808 134561400 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9905 8181 603 41 0 9864 0
vsize: 39620
[startup+320.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26101
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 8621 0 0 0 31979 24 0 0 25 0 1 0 479087975 41103360 8325 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10035 8325 603 41 0 9994 0
vsize: 40140
[startup+330.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26101
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 8884 0 0 0 32979 24 0 0 25 0 1 0 479087975 42176512 8588 4294967295 134512640 134672761 3221224640 3221223788 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10297 8588 603 41 0 10256 0
vsize: 41188
[startup+340.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26101
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 9062 0 0 0 33978 25 0 0 25 0 1 0 479087975 42987520 8766 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10495 8766 603 41 0 10454 0
vsize: 41980
[startup+350.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26101
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 9279 0 0 0 34978 26 0 0 25 0 1 0 479087975 43786240 8983 4294967295 134512640 134672761 3221224640 3221223744 134559991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10690 8983 603 41 0 10649 0
vsize: 42760
[startup+360.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26101
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 9450 0 0 0 35977 26 0 0 25 0 1 0 479087975 44462080 9154 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10855 9154 603 41 0 10814 0
vsize: 43420
[startup+370.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26101
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 9632 0 0 0 36977 27 0 0 25 0 1 0 479087975 45268992 9336 4294967295 134512640 134672761 3221224640 3221223808 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11052 9336 603 41 0 11011 0
vsize: 44208
[startup+380.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26101
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 9798 0 0 0 37977 27 0 0 25 0 1 0 479087975 45940736 9502 4294967295 134512640 134672761 3221224640 3221223808 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11216 9502 603 41 0 11175 0
vsize: 44864
[startup+390.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26101
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 9909 0 0 0 38977 27 0 0 25 0 1 0 479087975 46342144 9613 4294967295 134512640 134672761 3221224640 3221223744 134560243 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11314 9613 603 41 0 11273 0
vsize: 45256
[startup+400.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26101
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 10033 0 0 0 39977 27 0 0 25 0 1 0 479087975 46878720 9737 4294967295 134512640 134672761 3221224640 3221223824 134559498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11445 9737 603 41 0 11404 0
vsize: 45780
[startup+410.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26101
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 10101 0 0 0 40977 28 0 0 25 0 1 0 479087975 47144960 9805 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11510 9805 603 41 0 11469 0
vsize: 46040
[startup+420.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26101
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 10185 0 0 0 41977 28 0 0 25 0 1 0 479087975 47546368 9889 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11608 9889 603 41 0 11567 0
vsize: 46432
[startup+430.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26101
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 10286 0 0 0 42977 28 0 0 25 0 1 0 479087975 47947776 9990 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11706 9990 603 41 0 11665 0
vsize: 46824
[startup+440.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26101
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 10478 0 0 0 43977 28 0 0 25 0 1 0 479087975 48754688 10182 4294967295 134512640 134672761 3221224640 3221223808 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11903 10182 603 41 0 11862 0
vsize: 47612
[startup+450.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26101
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 10625 0 0 0 44977 29 0 0 25 0 1 0 479087975 49291264 10329 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12034 10329 603 41 0 11993 0
vsize: 48136
[startup+460.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26101
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 10741 0 0 0 45977 29 0 0 25 0 1 0 479087975 49696768 10445 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12133 10445 603 41 0 12092 0
vsize: 48532
[startup+470.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26101
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 10815 0 0 0 46977 29 0 0 25 0 1 0 479087975 50098176 10519 4294967295 134512640 134672761 3221224640 3221223640 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12231 10519 603 41 0 12190 0
vsize: 48924
[startup+480.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26101
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 10928 0 0 0 47977 30 0 0 25 0 1 0 479087975 50495488 10632 4294967295 134512640 134672761 3221224640 3221223840 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12328 10632 603 41 0 12287 0
vsize: 49312
[startup+490.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26101
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 11112 0 0 0 48976 31 0 0 25 0 1 0 479087975 51298304 10816 4294967295 134512640 134672761 3221224640 3221223808 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12524 10816 603 41 0 12483 0
vsize: 50096
[startup+500.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26101
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 11378 0 0 0 49975 32 0 0 25 0 1 0 479087975 52375552 11082 4294967295 134512640 134672761 3221224640 3221223776 134560632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12787 11082 603 41 0 12746 0
vsize: 51148
[startup+510.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26101
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 11594 0 0 0 50975 32 0 0 25 0 1 0 479087975 53182464 11298 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12984 11298 603 41 0 12943 0
vsize: 51936
[startup+520.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26101
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 11924 0 0 0 51973 34 0 0 25 0 1 0 479087975 54534144 11628 4294967295 134512640 134672761 3221224640 3221223776 134560598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13314 11628 603 41 0 13273 0
vsize: 53256
[startup+530.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26101
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 12097 0 0 0 52973 34 0 0 25 0 1 0 479087975 55095296 11772 4294967295 134512640 134672761 3221224640 3221223824 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13451 11772 603 41 0 13410 0
vsize: 53804
[startup+540.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26101
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 12098 0 0 0 53973 34 0 0 25 0 1 0 479087975 55095296 11773 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13451 11773 603 41 0 13410 0
vsize: 53804
[startup+550.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26101
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 12098 0 0 0 54974 34 0 0 25 0 1 0 479087975 55095296 11773 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13451 11773 603 41 0 13410 0
vsize: 53804
[startup+560.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26103
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 12098 0 0 0 55974 34 0 0 25 0 1 0 479087975 55095296 11773 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13451 11773 603 41 0 13410 0
vsize: 53804
[startup+570.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26103
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 12098 0 0 0 56974 34 0 0 25 0 1 0 479087975 55095296 11773 4294967295 134512640 134672761 3221224640 3221223824 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13451 11773 603 41 0 13410 0
vsize: 53804
[startup+580.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26103
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 12098 0 0 0 57974 34 0 0 25 0 1 0 479087975 55095296 11773 4294967295 134512640 134672761 3221224640 3221223840 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13451 11773 603 41 0 13410 0
vsize: 53804
[startup+590.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26103
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 12098 0 0 0 58975 34 0 0 25 0 1 0 479087975 55095296 11773 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13451 11773 603 41 0 13410 0
vsize: 53804
[startup+600.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26103
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 12098 0 0 0 59975 34 0 0 25 0 1 0 479087975 55095296 11773 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13451 11773 603 41 0 13410 0
vsize: 53804
[startup+610.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26103
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 12098 0 0 0 60975 34 0 0 25 0 1 0 479087975 55095296 11773 4294967295 134512640 134672761 3221224640 3221223744 134560492 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13451 11773 603 41 0 13410 0
vsize: 53804
[startup+620.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26103
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 12098 0 0 0 61975 34 0 0 25 0 1 0 479087975 55095296 11773 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13451 11773 603 41 0 13410 0
vsize: 53804
[startup+630.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26103
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 12098 0 0 0 62975 34 0 0 25 0 1 0 479087975 55095296 11773 4294967295 134512640 134672761 3221224640 3221223776 134560716 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13451 11773 603 41 0 13410 0
vsize: 53804
[startup+640.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26103
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 12098 0 0 0 63975 34 0 0 25 0 1 0 479087975 55095296 11773 4294967295 134512640 134672761 3221224640 3221223744 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13451 11773 603 41 0 13410 0
vsize: 53804
[startup+650.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26103
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 12098 0 0 0 64976 34 0 0 25 0 1 0 479087975 55095296 11773 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13451 11773 603 41 0 13410 0
vsize: 53804
[startup+660.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26103
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 12098 0 0 0 65976 34 0 0 25 0 1 0 479087975 55095296 11773 4294967295 134512640 134672761 3221224640 3221223776 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13451 11773 603 41 0 13410 0
vsize: 53804
[startup+670.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26103
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 12098 0 0 0 66976 34 0 0 25 0 1 0 479087975 55095296 11773 4294967295 134512640 134672761 3221224640 3221223744 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13451 11773 603 41 0 13410 0
vsize: 53804
[startup+680.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26103
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 12098 0 0 0 67976 34 0 0 25 0 1 0 479087975 55095296 11773 4294967295 134512640 134672761 3221224640 3221223776 134560608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13451 11773 603 41 0 13410 0
vsize: 53804
[startup+690.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26103
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 12098 0 0 0 68976 34 0 0 25 0 1 0 479087975 55095296 11773 4294967295 134512640 134672761 3221224640 3221223744 134560399 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13451 11773 603 41 0 13410 0
vsize: 53804
[startup+700.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26103
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 12098 0 0 0 69977 34 0 0 25 0 1 0 479087975 55095296 11773 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13451 11773 603 41 0 13410 0
vsize: 53804
[startup+710.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26103
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 12098 0 0 0 70977 34 0 0 25 0 1 0 479087975 55095296 11773 4294967295 134512640 134672761 3221224640 3221223840 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13451 11773 603 41 0 13410 0
vsize: 53804
[startup+720.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26103
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 12098 0 0 0 71977 34 0 0 25 0 1 0 479087975 55095296 11773 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13451 11773 603 41 0 13410 0
vsize: 53804
[startup+730.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26103
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 12098 0 0 0 72977 34 0 0 25 0 1 0 479087975 55095296 11773 4294967295 134512640 134672761 3221224640 3221223808 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13451 11773 603 41 0 13410 0
vsize: 53804
[startup+740.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26103
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 12098 0 0 0 73977 34 0 0 25 0 1 0 479087975 55095296 11773 4294967295 134512640 134672761 3221224640 3221223776 134565076 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13451 11773 603 41 0 13410 0
vsize: 53804
[startup+750.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26103
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 12098 0 0 0 74977 34 0 0 25 0 1 0 479087975 55095296 11773 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13451 11773 603 41 0 13410 0
vsize: 53804
[startup+760.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26103
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 12098 0 0 0 75978 34 0 0 25 0 1 0 479087975 55095296 11773 4294967295 134512640 134672761 3221224640 3221223776 134560642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13451 11773 603 41 0 13410 0
vsize: 53804
[startup+770.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26103
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 12098 0 0 0 76978 34 0 0 25 0 1 0 479087975 55095296 11773 4294967295 134512640 134672761 3221224640 3221223744 134560477 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13451 11773 603 41 0 13410 0
vsize: 53804
[startup+780.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26103
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 12098 0 0 0 77978 34 0 0 25 0 1 0 479087975 55095296 11773 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13451 11773 603 41 0 13410 0
vsize: 53804
[startup+790.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26103
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 12098 0 0 0 78978 34 0 0 25 0 1 0 479087975 55095296 11773 4294967295 134512640 134672761 3221224640 3221223812 134556680 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13451 11773 603 41 0 13410 0
vsize: 53804
[startup+800.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26103
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 12098 0 0 0 79978 34 0 0 25 0 1 0 479087975 55095296 11773 4294967295 134512640 134672761 3221224640 3221223776 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13451 11773 603 41 0 13410 0
vsize: 53804
[startup+810.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26103
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 12098 0 0 0 80978 34 0 0 25 0 1 0 479087975 55095296 11773 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13451 11773 603 41 0 13410 0
vsize: 53804
[startup+820.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26103
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 12098 0 0 0 81978 35 0 0 25 0 1 0 479087975 55095296 11773 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13451 11773 603 41 0 13410 0
vsize: 53804
[startup+830.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26103
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 12098 0 0 0 82979 35 0 0 25 0 1 0 479087975 55095296 11773 4294967295 134512640 134672761 3221224640 3221223840 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13451 11773 603 41 0 13410 0
vsize: 53804
[startup+840.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26103
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 12098 0 0 0 83979 35 0 0 25 0 1 0 479087975 55095296 11773 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13451 11773 603 41 0 13410 0
vsize: 53804
[startup+850.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26103
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 12098 0 0 0 84979 35 0 0 25 0 1 0 479087975 55095296 11773 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13451 11773 603 41 0 13410 0
vsize: 53804
[startup+860.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26105
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 12098 0 0 0 85979 35 0 0 25 0 1 0 479087975 55095296 11773 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13451 11773 603 41 0 13410 0
vsize: 53804
[startup+870.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26105
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 12098 0 0 0 86979 35 0 0 25 0 1 0 479087975 55095296 11773 4294967295 134512640 134672761 3221224640 3221223776 134560622 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13451 11773 603 41 0 13410 0
vsize: 53804
[startup+880.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26105
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 12098 0 0 0 87979 35 0 0 25 0 1 0 479087975 55095296 11773 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13451 11773 603 41 0 13410 0
vsize: 53804
[startup+890.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26105
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 12098 0 0 0 88979 35 0 0 25 0 1 0 479087975 55095296 11773 4294967295 134512640 134672761 3221224640 3221223776 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13451 11773 603 41 0 13410 0
vsize: 53804
[startup+900.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26105
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 12098 0 0 0 89980 35 0 0 25 0 1 0 479087975 55095296 11773 4294967295 134512640 134672761 3221224640 3221223808 134561261 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13451 11773 603 41 0 13410 0
vsize: 53804
[startup+910.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26105
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 12098 0 0 0 90979 35 0 0 25 0 1 0 479087975 55095296 11773 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13451 11773 603 41 0 13410 0
vsize: 53804
[startup+920.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26105
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 12099 0 0 0 91980 35 0 0 25 0 1 0 479087975 55095296 11774 4294967295 134512640 134672761 3221224640 3221223808 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13451 11774 603 41 0 13410 0
vsize: 53804
[startup+930.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26105
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 12099 0 0 0 92980 35 0 0 25 0 1 0 479087975 55095296 11774 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13451 11774 603 41 0 13410 0
vsize: 53804
[startup+940.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26105
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 12099 0 0 0 93980 35 0 0 25 0 1 0 479087975 55095296 11774 4294967295 134512640 134672761 3221224640 3221223840 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13451 11774 603 41 0 13410 0
vsize: 53804
[startup+950.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26105
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 12100 0 0 0 94980 35 0 0 25 0 1 0 479087975 55095296 11775 4294967295 134512640 134672761 3221224640 3221223776 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13451 11775 603 41 0 13410 0
vsize: 53804
[startup+960.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26105
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 12101 0 0 0 95980 35 0 0 25 0 1 0 479087975 55095296 11776 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13451 11776 603 41 0 13410 0
vsize: 53804
[startup+970.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26105
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 12113 0 0 0 96980 35 0 0 25 0 1 0 479087975 55226368 11788 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13483 11788 603 41 0 13442 0
vsize: 53932
[startup+980.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26105
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 12177 0 0 0 97980 36 0 0 25 0 1 0 479087975 55750656 11852 4294967295 134512640 134672761 3221224640 3221223776 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13611 11852 603 41 0 13570 0
vsize: 54444
[startup+990.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26105
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 12233 0 0 0 98980 36 0 0 25 0 1 0 479087975 56020992 11908 4294967295 134512640 134672761 3221224640 3221223744 134559847 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13677 11908 603 41 0 13636 0
vsize: 54708
[startup+1000.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26105
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 12287 0 0 0 99980 36 0 0 25 0 1 0 479087975 56156160 11962 4294967295 134512640 134672761 3221224640 3221223840 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13710 11962 603 41 0 13669 0
vsize: 54840
[startup+1010.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26105
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 12333 0 0 0 100980 37 0 0 25 0 1 0 479087975 56422400 12008 4294967295 134512640 134672761 3221224640 3221223808 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13775 12008 603 41 0 13734 0
vsize: 55100
[startup+1020.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26105
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 12373 0 0 0 101980 37 0 0 25 0 1 0 479087975 56557568 12048 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13808 12048 603 41 0 13767 0
vsize: 55232
[startup+1030.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26105
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 12398 0 0 0 102980 37 0 0 25 0 1 0 479087975 56557568 12073 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13808 12073 603 41 0 13767 0
vsize: 55232
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26105
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 12509 0 0 0 103979 37 0 0 25 0 1 0 479087975 57090048 12184 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13938 12184 603 41 0 13897 0
vsize: 55752
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26105
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 12674 0 0 0 104979 38 0 0 25 0 1 0 479087975 57761792 12349 4294967295 134512640 134672761 3221224640 3221223840 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14102 12349 603 41 0 14061 0
vsize: 56408
[startup+1060.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26105
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 12766 0 0 0 105979 38 0 0 25 0 1 0 479087975 57933824 12412 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14144 12412 603 41 0 14103 0
vsize: 56576
[startup+1070.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26105
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 12766 0 0 0 106979 38 0 0 25 0 1 0 479087975 57933824 12412 4294967295 134512640 134672761 3221224640 3221223840 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14144 12412 603 41 0 14103 0
vsize: 56576
[startup+1080.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26105
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 12766 0 0 0 107979 38 0 0 25 0 1 0 479087975 57933824 12412 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14144 12412 603 41 0 14103 0
vsize: 56576
[startup+1090.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26105
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 12766 0 0 0 108980 38 0 0 25 0 1 0 479087975 57933824 12412 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14144 12412 603 41 0 14103 0
vsize: 56576
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26105
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 12766 0 0 0 109980 39 0 0 25 0 1 0 479087975 57933824 12412 4294967295 134512640 134672761 3221224640 3221223840 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14144 12412 603 41 0 14103 0
vsize: 56576
[startup+1110.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26105
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 12766 0 0 0 110980 39 0 0 25 0 1 0 479087975 57933824 12412 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14144 12412 603 41 0 14103 0
vsize: 56576
[startup+1120.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26105
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 12766 0 0 0 111980 39 0 0 25 0 1 0 479087975 57933824 12412 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14144 12412 603 41 0 14103 0
vsize: 56576
[startup+1130.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26105
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 12766 0 0 0 112980 39 0 0 25 0 1 0 479087975 57933824 12412 4294967295 134512640 134672761 3221224640 3221223824 134558513 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14144 12412 603 41 0 14103 0
vsize: 56576
[startup+1140.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26105
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 12766 0 0 0 113980 39 0 0 25 0 1 0 479087975 57933824 12412 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14144 12412 603 41 0 14103 0
vsize: 56576
[startup+1150.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26105
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 12766 0 0 0 114981 39 0 0 25 0 1 0 479087975 57933824 12412 4294967295 134512640 134672761 3221224640 3221223808 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14144 12412 603 41 0 14103 0
vsize: 56576
[startup+1160.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26107
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 12766 0 0 0 115981 39 0 0 25 0 1 0 479087975 57933824 12412 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14144 12412 603 41 0 14103 0
vsize: 56576
[startup+1170.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26107
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 12766 0 0 0 116981 39 0 0 25 0 1 0 479087975 57933824 12412 4294967295 134512640 134672761 3221224640 3221223776 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14144 12412 603 41 0 14103 0
vsize: 56576
[startup+1180.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26107
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 12766 0 0 0 117981 39 0 0 25 0 1 0 479087975 57933824 12412 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14144 12412 603 41 0 14103 0
vsize: 56576
[startup+1190.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26107
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 12766 0 0 0 118981 39 0 0 25 0 1 0 479087975 57933824 12412 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14144 12412 603 41 0 14103 0
vsize: 56576
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26107
Raw data (stat): 26099 (minisat+) R 26098 22929 22928 0 -1 0 12766 0 0 0 119981 39 0 0 25 0 1 0 479087975 57933824 12412 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14144 12412 603 41 0 14103 0
vsize: 56576
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 0.99 0.97 0.91 1/55 26107
Raw data (stat): 26099 (minisat+) Z 26098 22929 22928 0 -1 12 12769 0 0 0 119981 41 0 0 25 0 1 0 479087975 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 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.07
CPU time (s): 1200.24
CPU user time (s): 1199.82
CPU system time (s): 0.417936
CPU usage (%): 100.014
Max. virtual memory (Kb): 56576
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####