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/web/www.ps.uni-sb.de/~walser/benchmarks/radar/normalized-10:10:4.5:0.95:100.opb
MD5SUM	b2c6bc03457d15976fdaf81252d9cdae
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	3
Optimality of the best value was proved	NO
Number of terms in the objective function	435
Biggest coefficient in the objective function	282
Number of bits for the biggest coefficient in the objective function	9
Sum of the numbers in the objective function	1168
Number of bits of the sum of numbers in the objective function	11
Biggest number in a constraint	282
Number of bits of the biggest number in a constraint	9
Biggest sum of numbers in a constraint	1168
Number of bits of the biggest sum of numbers	11
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.02284
Number of variables	435
Total number of constraints	935
Number of constraints which are clauses	403
Number of constraints which are cardinality constraints (but not clauses)	532
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	16
Trace number 5661

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc20 THE 2005-04-14 01:21:31 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4125 boxname=wulflinc20 idbench=365 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  b2c6bc03457d15976fdaf81252d9cdae  /oldhome/oroussel/tmp/wulflinc20/normalized-10:10:4.5:0.95:100.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc20/normalized-10:10:4.5:0.95:100.opb /oldhome/oroussel/tmp/wulflinc20/normalized-10:10:4.5:0.95:100.opb
IDLAUNCH: 4125
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.215
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.215
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        887236 kB
Buffers:         34592 kB
Cached:          77284 kB
SwapCached:       2636 kB
Active:          48884 kB
Inactive:        68440 kB
HighTotal:      131008 kB
HighFree:        49952 kB
LowTotal:       903652 kB
LowFree:        837284 kB
SwapTotal:     2097892 kB
SwapFree:      2095256 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            24408 kB
Committed_AS:    63448 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 01:41:43 (client local time) WITH STATUS 10 IN 1209.68 SECONDS
stats: 4125 7 1209.68 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 500 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ...................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[  97]---> BDD-cost:    5
c ---[  96]---> BDD-cost:    5
c ---[  95]---> BDD-cost:    8
c ---[  94]---> BDD-cost:    8
c ---[  93]---> BDD-cost:   11
c ---[  92]---> BDD-cost:   11
c ---[  91]---> BDD-cost:    7
c ---[  90]---> BDD-cost:    3
c ---[  89]---> BDD-cost:    8
c ---[  88]---> BDD-cost:   11
c ---[  87]---> BDD-cost:   17
c ---[  86]---> BDD-cost:    8
c ---[  85]---> BDD-cost:   14
c ---[  84]---> BDD-cost:   14
c ---[  83]---> BDD-cost:    7
c ---[  82]---> BDD-cost:    3
c ---[  81]---> BDD-cost:    7
c ---[  79]---> BDD-cost:   14
c ---[  78]---> BDD-cost:   17
c ---[  77]---> BDD-cost:   20
c ---[  76]---> BDD-cost:   20
c ---[  75]---> BDD-cost:   26
c ---[  74]---> BDD-cost:    7
c ---[  73]---> BDD-cost:   23
c ---[  72]---> BDD-cost:    7
c ---[  71]---> BDD-cost:    9
c ---[  70]---> BDD-cost:    7
c ---[  69]---> BDD-cost:   17
c ---[  68]---> BDD-cost:   20
c ---[  67]---> BDD-cost:   26
c ---[  66]---> BDD-cost:   29
c ---[  65]---> BDD-cost:   38
c ---[  64]---> BDD-cost:   32
c ---[  63]---> BDD-cost:   29
c ---[  62]---> BDD-cost:   20
c ---[  61]---> BDD-cost:   15
c ---[  60]---> BDD-cost:    9
c ---[  59]---> BDD-cost:   20
c ---[  58]---> BDD-cost:   26
c ---[  57]---> BDD-cost:   32
c ---[  56]---> BDD-cost:   35
c ---[  55]---> BDD-cost:   38
c ---[  54]---> BDD-cost:   38
c ---[  53]---> BDD-cost:   27
c ---[  52]---> BDD-cost:   20
c ---[  51]---> BDD-cost:   17
c ---[  50]---> BDD-cost:   17
c ---[  49]---> BDD-cost:   17
c ---[  48]---> BDD-cost:   26
c ---[  47]---> BDD-cost:   26
c ---[  46]---> BDD-cost:   32
c ---[  45]---> BDD-cost:   41
c ---[  44]---> BDD-cost:   38
c ---[  43]---> BDD-cost:   26
c ---[  42]---> BDD-cost:   20
c ---[  41]---> BDD-cost:   17
c ---[  40]---> BDD-cost:   11
c ---[  39]---> BDD-cost:   14
c ---[  38]---> BDD-cost:   20
c ---[  37]---> BDD-cost:   29
c ---[  36]---> BDD-cost:   32
c ---[  35]---> BDD-cost:   35
c ---[  34]---> BDD-cost:   38
c ---[  33]---> BDD-cost:   29
c ---[  32]---> BDD-cost:   23
c ---[  31]---> BDD-cost:   20
c ---[  30]---> BDD-cost:   14
c ---[  29]---> BDD-cost:   17
c ---[  28]---> BDD-cost:   23
c ---[  27]---> BDD-cost:   26
c ---[  26]---> BDD-cost:   26
c ---[  25]---> BDD-cost:   32
c ---[  24]---> BDD-cost:   38
c ---[  23]---> BDD-cost:   29
c ---[  22]---> BDD-cost:   26
c ---[  21]---> BDD-cost:   23
c ---[  20]---> BDD-cost:   17
c ---[  19]---> BDD-cost:   15
c ---[  18]---> BDD-cost:   23
c ---[  17]---> BDD-cost:   23
c ---[  16]---> BDD-cost:   23
c ---[  15]---> BDD-cost:   26
c ---[  14]---> BDD-cost:   29
c ---[  13]---> BDD-cost:   20
c ---[  12]---> BDD-cost:   26
c ---[  11]---> BDD-cost:   20
c ---[  10]---> BDD-cost:   14
c ---[   9]---> BDD-cost:    8
c ---[   8]---> BDD-cost:   17
c ---[   7]---> BDD-cost:   14
c ---[   6]---> BDD-cost:   20
c ---[   5]---> BDD-cost:   17
c ---[   4]---> BDD-cost:   20
c ---[   3]---> BDD-cost:   17
c ---[   2]---> BDD-cost:   20
c ---[   1]---> BDD-cost:   14
c ---[   0]---> BDD-cost:   11
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |    4866    13838 |    1459       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/2278          
c   -- var.elim.:  2000/2278          
c   -- var.elim.:  2278/2278          
c   -- var.elim.:  1000/1139          
c   -- var.elim.:  1139/1139          
c   -- subsuming                       
c   -- var.elim.:  1000/1046          
c   -- var.elim.:  1046/1046          
c   -- var.elim.:  602/602          
c   -- subsuming                       
c   -- var.elim.:  8/8          
c   -- var.elim.:  6/6          
c |         0 |    3637    12728 |      --       0       --      -- |     --   | -1229/-819
c |         0 |    3637    12728 |    1454       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 0.243962 s)
c ==============================================================================
c [1mFound solution: 391[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:24586     Base: 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   33773    83452 |   10131       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/20453          
c   -- var.elim.:  2000/20453          
c   -- var.elim.:  3000/20453          
c   -- var.elim.:  4000/20453          
c   -- var.elim.:  5000/20453          
c   -- var.elim.:  6000/20453          
c   -- var.elim.:  7000/20453          
c   -- var.elim.:  8000/20453          
c   -- var.elim.:  9000/20453          
c   -- var.elim.:  10000/20453          
c   -- var.elim.:  11000/20453          
c   -- var.elim.:  12000/20453          
c   -- var.elim.:  13000/20453          
c   -- var.elim.:  14000/20453          
c   -- var.elim.:  15000/20453          
c   -- var.elim.:  16000/20453          
c   -- var.elim.:  17000/20453          
c   -- var.elim.:  18000/20453          
c   -- var.elim.:  19000/20453          
c   -- var.elim.:  20000/20453          
c   -- var.elim.:  20453/20453          
c   -- var.elim.:  1000/10317          
c   -- var.elim.:  2000/10317          
c   -- var.elim.:  3000/10317          
c   -- var.elim.:  4000/10317          
c   -- var.elim.:  5000/10317          
c   -- var.elim.:  6000/10317          
c   -- var.elim.:  7000/10317          
c   -- var.elim.:  8000/10317          
c   -- var.elim.:  9000/10317          
c   -- var.elim.:  10000/10317          
c   -- var.elim.:  10317/10317          
c   -- subsuming                       
c   -- var.elim.:  1000/10059          
c   -- var.elim.:  2000/10059          
c   -- var.elim.:  3000/10059          
c   -- var.elim.:  4000/10059          
c   -- var.elim.:  5000/10059          
c   -- var.elim.:  6000/10059          
c   -- var.elim.:  7000/10059          
c   -- var.elim.:  8000/10059          
c   -- var.elim.:  9000/10059          
c   -- var.elim.:  10000/10059          
c   -- var.elim.:  10059/10059          
c   -- var.elim.:  1000/2940          
c   -- var.elim.:  2000/2940          
c   -- var.elim.:  2940/2940          
c   -- subsuming                       
c   -- var.elim.:  1000/3277          
c   -- var.elim.:  2000/3277          
c   -- var.elim.:  3000/3277          
c   -- var.elim.:  3277/3277          
c   -- var.elim.:  770/770          
c |         0 |   23614   171662 |      --       0       --      -- |     --   | -10159/88211
c |         0 |   23614   171662 |    9445       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 126.163 s)
c ==============================================================================
c [1mFound solution: 59[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |        29 |   28445   185159 |    8533      29      658    22.7 |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/9333          
c   -- var.elim.:  2000/9333          
c   -- var.elim.:  3000/9333          
c   -- var.elim.:  4000/9333          
c   -- var.elim.:  5000/9333          
c   -- var.elim.:  6000/9333          
c   -- var.elim.:  7000/9333          
c   -- var.elim.:  8000/9333          
c   -- var.elim.:  9000/9333          
c   -- var.elim.:  9333/9333          
c   -- var.elim.:  1000/3950          
c   -- var.elim.:  2000/3950          
c   -- var.elim.:  3000/3950          
c   -- var.elim.:  3950/3950          
c   -- subsuming                       
c   -- var.elim.:  1000/3065          
c   -- var.elim.:  2000/3065          
c   -- var.elim.:  3000/3065          
c   -- var.elim.:  3065/3065          
c   -- var.elim.:  31/31          
c |        29 |   24591   180766 |      --      29       --      -- |     --   | -3854/-4392
c |        29 |   24591   180766 |    9836      29      658    22.7 |  0.000 % |
c |       129 |   24591   180766 |   10820     129     9669    75.0 |  1.256 % |
c |       279 |   24591   180766 |   11902     279    17314    62.1 |  1.256 % |
c |       506 |   24591   180766 |   13092     506    61974   122.5 |  1.256 % |
c |       845 |   24591   180766 |   14401     845   122762   145.3 |  1.256 % |
c |      1353 |   24591   180766 |   15841    1353   186407   137.8 |  1.256 % |
c |      2113 |   24591   180766 |   17425    2113   341848   161.8 |  1.256 % |
c ==============================================================================
c (current CPU-time: 140.812 s)
c ==============================================================================
c [1mFound solution: 30[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      2273 |   40653   220201 |   12195    2271   355817   156.7 |  1.256 % |
c   -- subsuming                       
c   -- var.elim.:  1000/10707          
c   -- var.elim.:  2000/10707          
c   -- var.elim.:  3000/10707          
c   -- var.elim.:  4000/10707          
c   -- var.elim.:  5000/10707          
c   -- var.elim.:  6000/10707          
c   -- var.elim.:  7000/10707          
c   -- var.elim.:  8000/10707          
c   -- var.elim.:  9000/10707          
c   -- var.elim.:  10000/10707          
c   -- var.elim.:  10707/10707          
c   -- var.elim.:  1000/5880          
c   -- var.elim.:  2000/5880          
c   -- var.elim.:  3000/5880          
c   -- var.elim.:  4000/5880          
c   -- var.elim.:  5000/5880          
c   -- var.elim.:  5880/5880          
c   -- subsuming                       
c   -- var.elim.:  1000/2723          
c   -- var.elim.:  2000/2723          
c   -- var.elim.:  2723/2723          
c |      2273 |   38355   219843 |      --    2271       --      -- |     --   | -2285/-331
c |      2273 |   38355   219843 |   15342    1726   162306    94.0 |  1.256 % |
c |      2373 |   38355   219843 |   16876    1826   189501   103.8 |  1.460 % |
c |      2523 |   38265   219198 |   18520    1975   207492   105.1 |  1.679 % |
c |      2748 |   38227   218836 |   20352    2197   256837   116.9 |  1.814 % |
c |      3086 |   38201   218633 |   22372    2533   302403   119.4 |  1.904 % |
c |      3593 |   38155   218208 |   24579    3035   369022   121.6 |  2.070 % |
c |      4352 |   38019   217219 |   26941    3782   436015   115.3 |  2.394 % |
c |      5491 |   37995   217000 |   29616    4915   557361   113.4 |  2.484 % |
c |      7199 |   37898   216297 |   32495    6613   744992   112.7 |  2.740 % |
c |      9762 |   37858   215940 |   35706    9164  1093129   119.3 |  2.883 % |
c |     13606 |   37663   214753 |   39075   12995  1585844   122.0 |  3.289 % |
c |     19372 |   37663   214753 |   42982   18761  3558305   189.7 |  3.289 % |
c |     28023 |   37342   212831 |   46878   27397  5376303   196.2 |  3.967 % |
c |     40998 |   37267   212397 |   51462   40357  8793074   217.9 |  4.087 % |
c |     60459 |   37006   210786 |   56212   23272  3126280   134.3 |  4.659 % |
c |     89651 |   36968   210520 |   61769   52462 15412074   293.8 |  4.765 % |
c |    133440 |   36968   210520 |   67946   45191 14009768   310.0 |  4.765 % |
c |    199125 |   36964   210488 |   74733   51628 19734846   382.3 |  4.772 % |
c ==============================================================================
c (current CPU-time: 888.843 s)
c ==============================================================================
c [1mFound solution: 14[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    220274 |   37393   211756 |   11217   72777 23185365   318.6 |  4.772 % |
c   -- subsuming                       
c   -- var.elim.:  1000/9028          
c   -- var.elim.:  2000/9028          
c   -- var.elim.:  3000/9028          
c   -- var.elim.:  4000/9028          
c   -- var.elim.:  5000/9028          
c   -- var.elim.:  6000/9028          
c   -- var.elim.:  7000/9028          
c   -- var.elim.:  8000/9028          
c   -- var.elim.:  9000/9028          
c   -- var.elim.:  9028/9028          
c   -- var.elim.:  788/788          
c   -- subsuming                       
c |    220274 |   37011   212050 |      --   72777       --      -- |     --   | -381/297
c |    220274 |   37011   212050 |   14804   72709 23164876   318.6 |  4.772 % |
c |    220374 |   37011   212050 |   16284   14810  2528010   170.7 |  4.880 % |
c |    220525 |   37011   212050 |   17913   14961  2535001   169.4 |  4.880 % |
c |    220750 |   37011   212050 |   19704   15186  2552846   168.1 |  4.880 % |
c |    221088 |   37011   212050 |   21675   15524  2590730   166.9 |  4.880 % |
c |    221595 |   36955   211725 |   23806   16029  2630277   164.1 |  4.962 % |
c |    222356 |   36955   211725 |   26187   16790  2709476   161.4 |  4.962 % |
c |    223495 |   36955   211725 |   28805   17929  2797898   156.1 |  4.962 % |
c |    225203 |   36955   211725 |   31686   19637  3254194   165.7 |  4.962 % |
c |    227766 |   36955   211725 |   34855   22200  3916270   176.4 |  4.962 % |
c |    231610 |   36955   211725 |   38340   26044  4456416   171.1 |  4.962 % |
c |    237377 |   36955   211725 |   42174   31811  5436439   170.9 |  4.962 % |
c |    246027 |   36955   211725 |   46392   40461  7703958   190.4 |  4.962 % |
c |    259001 |   36862   211111 |   50903   19065  2828347   148.4 |  5.181 % |
c |    278463 |   36862   211111 |   55993   38527 10344610   268.5 |  5.181 % |
c |    307655 |   36821   210888 |   61524   22938  3121334   136.1 |  5.256 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v v358 v234 -v62 v5 v340 -v235 -v399 v362 v339 -v239 v6 v398 -v360 -v238 v7 v400 v341 -v236 v143 -v10 v433 -v361 v343 -v237 v142 -v8 -v416 -v365 v144 -v9 -v420 v344 v434 v357 v233 v182 -v61 -v2 v336 v232 -v186 v4 v363 v335 -v320 -v243 v3 -v11 -v366 v342 v401 -v364 v345 -v415 v409 v419 -v405 v145 -v404 -v386 v153 -v26 v149 -v30 -v355 -v316 v251 v246 v181 -v63 v359 -v255 v247 -v185 -v1 v356 -v319 -v242 v19 -v367 v337 v15 -v406 v338 -v240 -v160 -v67 #### 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.95 0.99 0.92 2/54 32458
Raw data (stat): 32458 (runsolver) R 32457 27565 27564 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 480589982 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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.0008 s]
Raw data (loadavg): 0.96 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 3479 0 0 0 881 57 0 0 25 0 1 0 480589982 16510976 3319 4294967295 134512640 134672761 3221224544 3221222992 134644016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4031 3319 603 41 0 3990 0
vsize: 16124
[startup+20.0009 s]
Raw data (loadavg): 0.97 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 3482 0 0 0 1881 57 0 0 25 0 1 0 480589982 16510976 3322 4294967295 134512640 134672761 3221224544 3221222992 134643580 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4031 3322 603 41 0 3990 0
vsize: 16124
[startup+30.0009 s]
Raw data (loadavg): 0.97 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 3514 0 0 0 2881 57 0 0 25 0 1 0 480589982 16646144 3354 4294967295 134512640 134672761 3221224544 3221222992 134643987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4064 3354 603 41 0 4023 0
vsize: 16256
[startup+40.0006 s]
Raw data (loadavg): 0.97 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 3514 0 0 0 3881 57 0 0 25 0 1 0 480589982 16646144 3354 4294967295 134512640 134672761 3221224544 3221222992 134643516 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4064 3354 603 41 0 4023 0
vsize: 16256
[startup+50.001 s]
Raw data (loadavg): 0.98 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 3584 0 0 0 4881 57 0 0 25 0 1 0 480589982 17260544 3424 4294967295 134512640 134672761 3221224544 3221222320 134566554 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4214 3424 603 41 0 4173 0
vsize: 16856
[startup+60.0011 s]
Raw data (loadavg): 0.98 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 3584 0 0 0 5881 57 0 0 25 0 1 0 480589982 17260544 3424 4294967295 134512640 134672761 3221224544 3221222944 134605448 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4214 3424 603 41 0 4173 0
vsize: 16856
[startup+70.0018 s]
Raw data (loadavg): 0.98 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 3584 0 0 0 6881 58 0 0 25 0 1 0 480589982 17260544 3424 4294967295 134512640 134672761 3221224544 3221222944 134605433 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4214 3424 603 41 0 4173 0
vsize: 16856
[startup+80.0012 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 3584 0 0 0 7881 58 0 0 25 0 1 0 480589982 17260544 3424 4294967295 134512640 134672761 3221224544 3221223088 134621173 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4214 3424 603 41 0 4173 0
vsize: 16856
[startup+90.0012 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 3584 0 0 0 8881 58 0 0 25 0 1 0 480589982 16683008 3378 4294967295 134512640 134672761 3221224544 3221222992 134643548 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4073 3378 603 41 0 4032 0
vsize: 16292
[startup+100.001 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 3584 0 0 0 9881 58 0 0 25 0 1 0 480589982 16683008 3378 4294967295 134512640 134672761 3221224544 3221222992 134643539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4073 3378 603 41 0 4032 0
vsize: 16292
[startup+110.001 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 3640 0 0 0 10881 58 0 0 25 0 1 0 480589982 17055744 3434 4294967295 134512640 134672761 3221224544 3221222768 134621194 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4164 3434 603 41 0 4123 0
vsize: 16656
[startup+120.001 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 3640 0 0 0 11881 58 0 0 25 0 1 0 480589982 17055744 3434 4294967295 134512640 134672761 3221224544 3221223088 134621207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4164 3434 603 41 0 4123 0
vsize: 16656
[startup+130.001 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 4497 0 0 0 12864 76 0 0 25 0 1 0 480589982 17707008 3702 4294967295 134512640 134672761 3221224544 3221223056 134637092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4323 3702 603 41 0 4282 0
vsize: 17292
[startup+140.002 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 4537 0 0 0 13863 76 0 0 25 0 1 0 480589982 17707008 3709 4294967295 134512640 134672761 3221224544 3221223584 134612987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4323 3709 603 41 0 4282 0
vsize: 17292
[startup+150.002 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 5799 0 0 0 14846 93 0 0 25 0 1 0 480589982 20672512 4489 4294967295 134512640 134672761 3221224544 3221223088 134621046 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5047 4489 603 41 0 5006 0
vsize: 20188
[startup+160.003 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 5801 0 0 0 15846 93 0 0 25 0 1 0 480589982 20189184 4411 4294967295 134512640 134672761 3221224544 3221223680 134614739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4929 4411 603 41 0 4888 0
vsize: 19716
[startup+170.003 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 6393 0 0 0 16844 95 0 0 25 0 1 0 480589982 22679552 5003 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5537 5003 603 41 0 5496 0
vsize: 22148
[startup+180.003 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 7340 0 0 0 17841 98 0 0 25 0 1 0 480589982 26488832 5950 4294967295 134512640 134672761 3221224544 3221223728 134615945 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6467 5950 603 41 0 6426 0
vsize: 25868
[startup+190.003 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 8633 0 0 0 18838 102 0 0 25 0 1 0 480589982 31789056 7243 4294967295 134512640 134672761 3221224544 3221223744 134610646 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7761 7243 603 41 0 7720 0
vsize: 31044
[startup+200.003 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 9405 0 0 0 19835 104 0 0 25 0 1 0 480589982 34947072 8015 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8532 8015 603 41 0 8491 0
vsize: 34128
[startup+210.003 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 10439 0 0 0 20833 107 0 0 25 0 1 0 480589982 39239680 9049 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9580 9049 603 41 0 9539 0
vsize: 38320
[startup+220.004 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 11019 0 0 0 21831 109 0 0 25 0 1 0 480589982 41594880 9629 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10155 9629 603 41 0 10114 0
vsize: 40620
[startup+230.003 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 11915 0 0 0 22829 112 0 0 25 0 1 0 480589982 45420544 10525 4294967295 134512640 134672761 3221224544 3221223584 134612478 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11089 10525 603 41 0 11048 0
vsize: 44356
[startup+240.003 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 12911 0 0 0 23826 115 0 0 25 0 1 0 480589982 49467392 11521 4294967295 134512640 134672761 3221224544 3221223584 134612614 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12077 11521 603 41 0 12036 0
vsize: 48308
[startup+250.004 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 13934 0 0 0 24824 117 0 0 25 0 1 0 480589982 53538816 12544 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13071 12544 603 41 0 13030 0
vsize: 52284
[startup+260.004 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 14690 0 0 0 25821 120 0 0 25 0 1 0 480589982 56696832 13300 4294967295 134512640 134672761 3221224544 3221223680 134614724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13842 13300 603 41 0 13801 0
vsize: 55368
[startup+270.004 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 15383 0 0 0 26819 122 0 0 25 0 1 0 480589982 59572224 13993 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14544 13993 603 41 0 14503 0
vsize: 58176
[startup+280.004 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 15987 0 0 0 27817 124 0 0 25 0 1 0 480589982 61943808 14597 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15123 14597 603 41 0 15082 0
vsize: 60492
[startup+290.004 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 16808 0 0 0 28816 126 0 0 25 0 1 0 480589982 65150976 15365 4294967295 134512640 134672761 3221224544 3221223584 134612628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15906 15365 603 41 0 15865 0
vsize: 63624
[startup+300.004 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 16808 0 0 0 29816 126 0 0 25 0 1 0 480589982 65150976 15365 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15906 15365 603 41 0 15865 0
vsize: 63624
[startup+310.005 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 16808 0 0 0 30816 126 0 0 25 0 1 0 480589982 65150976 15365 4294967295 134512640 134672761 3221224544 3221223648 134604307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15906 15365 603 41 0 15865 0
vsize: 63624
[startup+320.006 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 16808 0 0 0 31816 126 0 0 25 0 1 0 480589982 65150976 15365 4294967295 134512640 134672761 3221224544 3221223584 134612892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15906 15365 603 41 0 15865 0
vsize: 63624
[startup+330.006 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 16808 0 0 0 32816 126 0 0 25 0 1 0 480589982 65150976 15365 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15906 15365 603 41 0 15865 0
vsize: 63624
[startup+340.006 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 16808 0 0 0 33816 126 0 0 25 0 1 0 480589982 65150976 15365 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15906 15365 603 41 0 15865 0
vsize: 63624
[startup+350.006 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 16808 0 0 0 34817 126 0 0 25 0 1 0 480589982 65150976 15365 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15906 15365 603 41 0 15865 0
vsize: 63624
[startup+360.006 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 16808 0 0 0 35817 126 0 0 25 0 1 0 480589982 65150976 15365 4294967295 134512640 134672761 3221224544 3221223584 134612987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15906 15365 603 41 0 15865 0
vsize: 63624
[startup+370.007 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 17446 0 0 0 36815 129 0 0 25 0 1 0 480589982 67887104 16003 4294967295 134512640 134672761 3221224544 3221223728 134615571 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16574 16003 603 41 0 16533 0
vsize: 66296
[startup+380.006 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 18624 0 0 0 37812 131 0 0 25 0 1 0 480589982 72634368 17181 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17733 17181 603 41 0 17692 0
vsize: 70932
[startup+390.006 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 19612 0 0 0 38810 134 0 0 25 0 1 0 480589982 76681216 18169 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18721 18169 603 41 0 18680 0
vsize: 74884
[startup+400.007 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 20553 0 0 0 39808 135 0 0 25 0 1 0 480589982 80502784 19110 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19654 19110 603 41 0 19613 0
vsize: 78616
[startup+410.007 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 21473 0 0 0 40806 138 0 0 25 0 1 0 480589982 84291584 20030 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20579 20030 603 41 0 20538 0
vsize: 82316
[startup+420.007 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 22069 0 0 0 41805 139 0 0 25 0 1 0 480589982 86802432 20626 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21192 20626 603 41 0 21151 0
vsize: 84768
[startup+430.007 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 22622 0 0 0 42804 140 0 0 25 0 1 0 480589982 89038848 21179 4294967295 134512640 134672761 3221224544 3221223584 134612572 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21738 21179 603 41 0 21697 0
vsize: 86952
[startup+440.007 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 23435 0 0 0 43802 143 0 0 25 0 1 0 480589982 92303360 21992 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22535 21992 603 41 0 22494 0
vsize: 90140
[startup+450.007 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 24366 0 0 0 44799 145 0 0 25 0 1 0 480589982 96382976 22923 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23531 22923 603 41 0 23490 0
vsize: 94124
[startup+460.008 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 24569 0 0 0 45799 146 0 0 25 0 1 0 480589982 96690176 23028 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23606 23028 603 41 0 23565 0
vsize: 94424
[startup+470.007 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 24569 0 0 0 46799 146 0 0 25 0 1 0 480589982 96690176 23028 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23606 23028 603 41 0 23565 0
vsize: 94424
[startup+480.007 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 24569 0 0 0 47799 146 0 0 25 0 1 0 480589982 96690176 23028 4294967295 134512640 134672761 3221224544 3221223584 134612614 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23606 23028 603 41 0 23565 0
vsize: 94424
[startup+490.008 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 24569 0 0 0 48800 146 0 0 25 0 1 0 480589982 96690176 23028 4294967295 134512640 134672761 3221224544 3221223584 134613743 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23606 23028 603 41 0 23565 0
vsize: 94424
[startup+500.009 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 24569 0 0 0 49800 146 0 0 25 0 1 0 480589982 96690176 23028 4294967295 134512640 134672761 3221224544 3221223584 134612783 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23606 23028 603 41 0 23565 0
vsize: 94424
[startup+510.009 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 24569 0 0 0 50800 146 0 0 25 0 1 0 480589982 96690176 23028 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23606 23028 603 41 0 23565 0
vsize: 94424
[startup+520.008 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 24569 0 0 0 51800 146 0 0 25 0 1 0 480589982 96690176 23028 4294967295 134512640 134672761 3221224544 3221223584 134612684 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23606 23028 603 41 0 23565 0
vsize: 94424
[startup+530.008 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 24569 0 0 0 52800 146 0 0 25 0 1 0 480589982 96690176 23028 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23606 23028 603 41 0 23565 0
vsize: 94424
[startup+540.008 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 24569 0 0 0 53801 146 0 0 25 0 1 0 480589982 96690176 23028 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23606 23028 603 41 0 23565 0
vsize: 94424
[startup+550.008 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 24569 0 0 0 54801 146 0 0 25 0 1 0 480589982 96690176 23028 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23606 23028 603 41 0 23565 0
vsize: 94424
[startup+560.008 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 24569 0 0 0 55801 146 0 0 25 0 1 0 480589982 96690176 23028 4294967295 134512640 134672761 3221224544 3221223584 134612739 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23606 23028 603 41 0 23565 0
vsize: 94424
[startup+570.009 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 24569 0 0 0 56801 146 0 0 25 0 1 0 480589982 96690176 23028 4294967295 134512640 134672761 3221224544 3221223584 134613118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23606 23028 603 41 0 23565 0
vsize: 94424
[startup+580.008 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 24569 0 0 0 57801 146 0 0 25 0 1 0 480589982 96690176 23028 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23606 23028 603 41 0 23565 0
vsize: 94424
[startup+590.008 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 24569 0 0 0 58801 146 0 0 25 0 1 0 480589982 96690176 23028 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23606 23028 603 41 0 23565 0
vsize: 94424
[startup+600.009 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 24569 0 0 0 59802 146 0 0 25 0 1 0 480589982 96690176 23028 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23606 23028 603 41 0 23565 0
vsize: 94424
[startup+610.01 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 25624 0 0 0 60799 148 0 0 25 0 1 0 480589982 101113856 24083 4294967295 134512640 134672761 3221224544 3221223376 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24686 24083 603 41 0 24645 0
vsize: 98744
[startup+620.01 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 26635 0 0 0 61796 152 0 0 25 0 1 0 480589982 105238528 25094 4294967295 134512640 134672761 3221224544 3221223728 134615571 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25693 25094 603 41 0 25652 0
vsize: 102772
[startup+630.009 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 27520 0 0 0 62794 154 0 0 25 0 1 0 480589982 108785664 25979 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26559 25979 603 41 0 26518 0
vsize: 106236
[startup+640.01 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 28545 0 0 0 63791 157 0 0 25 0 1 0 480589982 113082368 27004 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27608 27004 603 41 0 27567 0
vsize: 110432
[startup+650.01 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 29222 0 0 0 64789 160 0 0 25 0 1 0 480589982 115888128 27681 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28293 27681 603 41 0 28252 0
vsize: 113172
[startup+660.01 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 30047 0 0 0 65786 162 0 0 25 0 1 0 480589982 119185408 28506 4294967295 134512640 134672761 3221224544 3221223680 134614677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29098 28506 603 41 0 29057 0
vsize: 116392
[startup+670.011 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 30809 0 0 0 66784 165 0 0 25 0 1 0 480589982 121909248 29195 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29763 29195 603 41 0 29722 0
vsize: 119052
[startup+680.011 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 30809 0 0 0 67784 165 0 0 25 0 1 0 480589982 121909248 29195 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29763 29195 603 41 0 29722 0
vsize: 119052
[startup+690.012 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 30809 0 0 0 68785 165 0 0 25 0 1 0 480589982 121909248 29195 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29763 29195 603 41 0 29722 0
vsize: 119052
[startup+700.012 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 30809 0 0 0 69785 165 0 0 25 0 1 0 480589982 121909248 29195 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29763 29195 603 41 0 29722 0
vsize: 119052
[startup+710.013 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 30809 0 0 0 70785 165 0 0 25 0 1 0 480589982 121909248 29195 4294967295 134512640 134672761 3221224544 3221223584 134612628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29763 29195 603 41 0 29722 0
vsize: 119052
[startup+720.013 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 30809 0 0 0 71785 165 0 0 25 0 1 0 480589982 121909248 29195 4294967295 134512640 134672761 3221224544 3221223728 134615665 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29763 29195 603 41 0 29722 0
vsize: 119052
[startup+730.013 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 30809 0 0 0 72785 165 0 0 25 0 1 0 480589982 121909248 29195 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29763 29195 603 41 0 29722 0
vsize: 119052
[startup+740.013 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 30809 0 0 0 73785 165 0 0 25 0 1 0 480589982 121909248 29195 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29763 29195 603 41 0 29722 0
vsize: 119052
[startup+750.013 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 30809 0 0 0 74785 165 0 0 25 0 1 0 480589982 121909248 29195 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29763 29195 603 41 0 29722 0
vsize: 119052
[startup+760.013 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 30809 0 0 0 75785 165 0 0 25 0 1 0 480589982 121909248 29195 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29763 29195 603 41 0 29722 0
vsize: 119052
[startup+770.013 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 30809 0 0 0 76785 165 0 0 25 0 1 0 480589982 121909248 29195 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29763 29195 603 41 0 29722 0
vsize: 119052
[startup+780.013 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 30809 0 0 0 77785 166 0 0 25 0 1 0 480589982 121909248 29195 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29763 29195 603 41 0 29722 0
vsize: 119052
[startup+790.014 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 30809 0 0 0 78786 166 0 0 25 0 1 0 480589982 121909248 29195 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29763 29195 603 41 0 29722 0
vsize: 119052
[startup+800.015 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 30809 0 0 0 79786 166 0 0 25 0 1 0 480589982 121909248 29195 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29763 29195 603 41 0 29722 0
vsize: 119052
[startup+810.015 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 30809 0 0 0 80786 166 0 0 25 0 1 0 480589982 121909248 29195 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29763 29195 603 41 0 29722 0
vsize: 119052
[startup+820.015 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 30809 0 0 0 81786 166 0 0 25 0 1 0 480589982 121909248 29195 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29763 29195 603 41 0 29722 0
vsize: 119052
[startup+830.015 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 30809 0 0 0 82786 166 0 0 25 0 1 0 480589982 121909248 29195 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29763 29195 603 41 0 29722 0
vsize: 119052
[startup+840.015 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 30809 0 0 0 83786 166 0 0 25 0 1 0 480589982 121909248 29195 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29763 29195 603 41 0 29722 0
vsize: 119052
[startup+850.015 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 30809 0 0 0 84786 166 0 0 25 0 1 0 480589982 121909248 29195 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29763 29195 603 41 0 29722 0
vsize: 119052
[startup+860.016 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 30809 0 0 0 85786 166 0 0 25 0 1 0 480589982 121909248 29195 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29763 29195 603 41 0 29722 0
vsize: 119052
[startup+870.017 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 30809 0 0 0 86787 166 0 0 25 0 1 0 480589982 121909248 29195 4294967295 134512640 134672761 3221224544 3221223712 134564772 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29763 29195 603 41 0 29722 0
vsize: 119052
[startup+880.016 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 30809 0 0 0 87787 166 0 0 25 0 1 0 480589982 121909248 29195 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29763 29195 603 41 0 29722 0
vsize: 119052
[startup+890.016 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 30809 0 0 0 88787 166 0 0 25 0 1 0 480589982 121909248 29195 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29763 29195 603 41 0 29722 0
vsize: 119052
[startup+900.016 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 31337 0 0 0 89776 177 0 0 25 0 1 0 480589982 121909248 29204 4294967295 134512640 134672761 3221224544 3221222992 134643565 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29763 29204 603 41 0 29722 0
vsize: 119052
[startup+910.017 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 31490 0 0 0 90775 177 0 0 25 0 1 0 480589982 121876480 29197 4294967295 134512640 134672761 3221224544 3221223728 134615948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29755 29197 603 41 0 29714 0
vsize: 119020
[startup+920.016 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 31490 0 0 0 91775 177 0 0 25 0 1 0 480589982 121876480 29197 4294967295 134512640 134672761 3221224544 3221223584 134614348 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29755 29197 603 41 0 29714 0
vsize: 119020
[startup+930.016 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 31490 0 0 0 92775 178 0 0 25 0 1 0 480589982 121876480 29197 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29755 29197 603 41 0 29714 0
vsize: 119020
[startup+940.016 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 31490 0 0 0 93775 178 0 0 25 0 1 0 480589982 121876480 29197 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29755 29197 603 41 0 29714 0
vsize: 119020
[startup+950.016 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 31490 0 0 0 94775 178 0 0 25 0 1 0 480589982 121876480 29197 4294967295 134512640 134672761 3221224544 3221223728 134615948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29755 29197 603 41 0 29714 0
vsize: 119020
[startup+960.017 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 31490 0 0 0 95776 178 0 0 25 0 1 0 480589982 121876480 29197 4294967295 134512640 134672761 3221224544 3221223744 134610661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29755 29197 603 41 0 29714 0
vsize: 119020
[startup+970.017 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 31490 0 0 0 96776 178 0 0 25 0 1 0 480589982 121876480 29197 4294967295 134512640 134672761 3221224544 3221223584 134613012 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29755 29197 603 41 0 29714 0
vsize: 119020
[startup+980.017 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 31490 0 0 0 97776 178 0 0 25 0 1 0 480589982 121876480 29197 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29755 29197 603 41 0 29714 0
vsize: 119020
[startup+990.017 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 31490 0 0 0 98776 178 0 0 25 0 1 0 480589982 121876480 29197 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29755 29197 603 41 0 29714 0
vsize: 119020
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 31490 0 0 0 99776 178 0 0 25 0 1 0 480589982 121876480 29197 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29755 29197 603 41 0 29714 0
vsize: 119020
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 31490 0 0 0 100776 178 0 0 25 0 1 0 480589982 121876480 29197 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29755 29197 603 41 0 29714 0
vsize: 119020
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 31490 0 0 0 101777 178 0 0 25 0 1 0 480589982 121876480 29197 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29755 29197 603 41 0 29714 0
vsize: 119020
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 31490 0 0 0 102777 178 0 0 25 0 1 0 480589982 121876480 29197 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29755 29197 603 41 0 29714 0
vsize: 119020
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 31490 0 0 0 103777 178 0 0 25 0 1 0 480589982 121876480 29197 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29755 29197 603 41 0 29714 0
vsize: 119020
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 31490 0 0 0 104777 178 0 0 25 0 1 0 480589982 121876480 29197 4294967295 134512640 134672761 3221224544 3221223680 134614690 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29755 29197 603 41 0 29714 0
vsize: 119020
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 31490 0 0 0 105777 178 0 0 25 0 1 0 480589982 121876480 29197 4294967295 134512640 134672761 3221224544 3221223416 1075353072 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29755 29197 603 41 0 29714 0
vsize: 119020
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 31490 0 0 0 106777 178 0 0 25 0 1 0 480589982 121876480 29197 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29755 29197 603 41 0 29714 0
vsize: 119020
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 31490 0 0 0 107778 178 0 0 25 0 1 0 480589982 121876480 29197 4294967295 134512640 134672761 3221224544 3221223728 134615838 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29755 29197 603 41 0 29714 0
vsize: 119020
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 31490 0 0 0 108778 178 0 0 25 0 1 0 480589982 121876480 29197 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29755 29197 603 41 0 29714 0
vsize: 119020
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 31490 0 0 0 109778 178 0 0 25 0 1 0 480589982 121876480 29197 4294967295 134512640 134672761 3221224544 3221223728 134615681 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29755 29197 603 41 0 29714 0
vsize: 119020
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 31490 0 0 0 110778 178 0 0 25 0 1 0 480589982 121876480 29197 4294967295 134512640 134672761 3221224544 3221223584 134612478 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29755 29197 603 41 0 29714 0
vsize: 119020
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 31490 0 0 0 111778 178 0 0 25 0 1 0 480589982 121876480 29197 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29755 29197 603 41 0 29714 0
vsize: 119020
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 31490 0 0 0 112778 178 0 0 25 0 1 0 480589982 121876480 29197 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29755 29197 603 41 0 29714 0
vsize: 119020
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 31490 0 0 0 113779 178 0 0 25 0 1 0 480589982 121876480 29197 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29755 29197 603 41 0 29714 0
vsize: 119020
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 31490 0 0 0 114779 178 0 0 25 0 1 0 480589982 121876480 29197 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29755 29197 603 41 0 29714 0
vsize: 119020
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 31490 0 0 0 115779 178 0 0 25 0 1 0 480589982 121876480 29197 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29755 29197 603 41 0 29714 0
vsize: 119020
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 31490 0 0 0 116779 178 0 0 25 0 1 0 480589982 121876480 29197 4294967295 134512640 134672761 3221224544 3221223584 134612783 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29755 29197 603 41 0 29714 0
vsize: 119020
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 31490 0 0 0 117779 178 0 0 25 0 1 0 480589982 121876480 29197 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29755 29197 603 41 0 29714 0
vsize: 119020
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 31490 0 0 0 118780 178 0 0 25 0 1 0 480589982 121876480 29197 4294967295 134512640 134672761 3221224544 3221223584 134612783 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29755 29197 603 41 0 29714 0
vsize: 119020
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 31490 0 0 0 119780 178 0 0 25 0 1 0 480589982 121876480 29197 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29755 29197 603 41 0 29714 0
vsize: 119020
[startup+1210.02 s]
Raw data (loadavg): 0.99 0.99 0.92 2/54 32458
Raw data (stat): 32458 (minisat+) R 32457 27565 27564 0 -1 0 31490 0 0 0 120780 178 0 0 25 0 1 0 480589982 121876480 29197 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29755 29197 603 41 0 29714 0
vsize: 119020
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1210.11 s]
Raw data (loadavg): 0.99 0.99 0.92 1/54 32458
Raw data (stat): 32458 (minisat+) Z 32457 27565 27564 0 -1 12 31491 0 0 0 120780 187 0 0 25 0 1 0 480589982 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): 1210.11
CPU time (s): 1209.68
CPU user time (s): 1207.81
CPU system time (s): 1.87271
CPU usage (%): 99.9643
Max. virtual memory (Kb): 119052
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####