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/mps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-mod013.opb
MD5SUM	b964292d4197638ce79b3f213e8fe89b
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	5130240
Optimality of the best value was proved	NO
Number of terms in the objective function	1008
Biggest coefficient in the objective function	366477312
Number of bits for the biggest coefficient in the objective function	29
Sum of the numbers in the objective function	12643636975
Number of bits of the sum of numbers in the objective function	34
Biggest number in a constraint	366477312
Number of bits of the biggest number in a constraint	29
Biggest sum of numbers in a constraint	12643636975
Number of bits of the biggest sum of numbers	34
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1189.01
Number of variables	1008
Total number of constraints	110
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	48
Number of constraints which are nor clauses,nor cardinality constraints	62
Minimum length of a constraint	1
Maximum length of a constraint	160
Trace number 32287

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc18 THE 2005-05-27 08:50:17 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=23668 boxname=wulflinc18 idbench=1312 idsolver=16 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  b964292d4197638ce79b3f213e8fe89b  /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-13-7-mod013.opb
REAL COMMAND:  minisat+_script -cb -gs /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-13-7-mod013.opb
IDLAUNCH: 23668
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.177
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.177
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:        899452 kB
Buffers:          2984 kB
Cached:         112080 kB
SwapCached:        604 kB
Active:          16224 kB
Inactive:       101076 kB
HighTotal:      131008 kB
HighFree:        15708 kB
LowTotal:       903652 kB
LowFree:        883744 kB
SwapTotal:     2097892 kB
SwapFree:      2096552 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5580 kB
Slab:            12256 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-27 09:10:47 (client local time) WITH STATUS 152 IN 1229.89 SECONDS
stats: 23668 7 1229.89 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 76 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ##############
c   -- Clauses(.)/Splits(s): (none)
c ---[  74]---> BDD-cost:  478
c ---[  72]---> BDD-cost:  468
c ---[  70]---> BDD-cost:  437
c ---[  68]---> BDD-cost:  422
c ---[  66]---> BDD-cost:  422
c ---[  64]---> BDD-cost:  373
c ---[  63]---> BDD-cost:   19
c ---[  62]---> BDD-cost:   16
c ---[  61]---> BDD-cost:   17
c ---[  60]---> BDD-cost:   15
c ---[  58]---> BDD-cost:  880
c ---[  57]---> BDD-cost:   15
c ---[  56]---> BDD-cost:   14
c ---[  55]---> BDD-cost:   14
c ---[  54]---> BDD-cost:   13
c ---[  53]---> BDD-cost:   19
c ---[  52]---> BDD-cost:   16
c ---[  51]---> BDD-cost:   17
c ---[  50]---> BDD-cost:   15
c ---[  49]---> BDD-cost:   15
c ---[  48]---> BDD-cost:   14
c ---[  46]---> BDD-cost:  876
c ---[  45]---> BDD-cost:   14
c ---[  44]---> BDD-cost:   13
c ---[  43]---> BDD-cost:   16
c ---[  42]---> BDD-cost:   16
c ---[  41]---> BDD-cost:   17
c ---[  40]---> BDD-cost:   15
c ---[  39]---> BDD-cost:   15
c ---[  38]---> BDD-cost:   14
c ---[  37]---> BDD-cost:   14
c ---[  36]---> BDD-cost:   13
c ---[  34]---> BDD-cost:  838
c ---[  33]---> BDD-cost:   15
c ---[  32]---> BDD-cost:   15
c ---[  31]---> BDD-cost:   15
c ---[  30]---> BDD-cost:   15
c ---[  29]---> BDD-cost:   15
c ---[  28]---> BDD-cost:   14
c ---[  27]---> BDD-cost:   14
c ---[  26]---> BDD-cost:   13
c ---[  25]---> BDD-cost:   14
c ---[  24]---> BDD-cost:   14
c ---[  22]---> BDD-cost:  805
c ---[  21]---> BDD-cost:   14
c ---[  20]---> BDD-cost:   14
c ---[  19]---> BDD-cost:   14
c ---[  18]---> BDD-cost:   14
c ---[  17]---> BDD-cost:   14
c ---[  16]---> BDD-cost:   13
c ---[  15]---> BDD-cost:   13
c ---[  14]---> BDD-cost:   13
c ---[  13]---> BDD-cost:   13
c ---[  12]---> BDD-cost:   13
c ---[  10]---> BDD-cost:  722
c ---[   9]---> BDD-cost:   13
c ---[   8]---> BDD-cost:   13
c ---[   7]---> BDD-cost:   13
c ---[   6]---> BDD-cost:   13
c ---[   4]---> BDD-cost:  632
c ---[   2]---> BDD-cost:  498
c ---[   0]---> BDD-cost:  482
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   23983    68004 |    7994       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 12019804[0m
c ---[   0]---> Sorter-cost:159959     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        10 |  469647  1108111 |  156549      10      136    13.6 |  0.000 % |
c |       110 |  469627  1108066 |  172203     109     4232    38.8 |  0.305 % |
c |       260 |  469627  1108066 |  189424     259    12140    46.9 |  0.305 % |
c |       485 |  469614  1108038 |  208366     483    13344    27.6 |  0.307 % |
c |       822 |  469176  1107049 |  229203     816    17467    21.4 |  0.378 % |
c |      1329 |  469176  1107049 |  252123    1323    37438    28.3 |  0.378 % |
c ==============================================================================
c [1mFound solution: 11314862[0m
c ---[   0]---> Sorter-cost:   16     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1501 |  469410  1108891 |  156470    1495    42384    28.4 |  0.378 % |
c |      1601 |  469410  1108891 |  172117    1595    42930    26.9 |  0.379 % |
c |      1752 |  469410  1108891 |  189328    1746    46445    26.6 |  0.379 % |
c |      1977 |  469221  1108460 |  208261    1968    53423    27.1 |  0.412 % |
c |      2315 |  469221  1108460 |  229087    2306    64964    28.2 |  0.412 % |
c |      2821 |  469221  1108460 |  251996    2812    72830    25.9 |  0.412 % |
c |      3582 |  469221  1108460 |  277196    3573    82089    23.0 |  0.412 % |
c |      4724 |  469221  1108460 |  304915    4715   118699    25.2 |  0.412 % |
c |      6432 |  469221  1108460 |  335407    6423   434388    67.6 |  0.412 % |
c |      8994 |  469056  1108088 |  368948    8984  1223464   136.2 |  0.440 % |
c |     12838 |  469056  1108088 |  405842   12828  2279093   177.7 |  0.440 % |
c ==============================================================================
c [1mFound solution: 9440856[0m
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     13702 |  469169  1108398 |  156389   13687  2286159   167.0 |  0.440 % |
c |     13802 |  469169  1108398 |  172027   13787  2286856   165.9 |  0.455 % |
c |     13952 |  469169  1108398 |  189230   13937  2288071   164.2 |  0.455 % |
c |     14177 |  468237  1106277 |  208153   14148  2289542   161.8 |  0.620 % |
c |     14514 |  468237  1106277 |  228969   14485  2292415   158.3 |  0.619 % |
c |     15020 |  468237  1106277 |  251866   14991  2297894   153.3 |  0.619 % |
c |     15779 |  468237  1106277 |  277052   15750  2304434   146.3 |  0.619 % |
c |     16918 |  468237  1106277 |  304757   16889  2314098   137.0 |  0.619 % |
c |     18626 |  468237  1106277 |  335233   18597  2349300   126.3 |  0.619 % |
c |     21190 |  468213  1106223 |  368757   21160  2414872   114.1 |  0.623 % |
c |     25035 |  467698  1105048 |  405632   25001  3781442   151.3 |  0.717 % |
c ==============================================================================
c [1mFound solution: 6936352[0m
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     29559 |  468307  1106581 |  156102   29500  3951563   134.0 |  0.717 % |
c |     29659 |  468307  1106581 |  171712   29600  3975408   134.3 |  0.750 % |
c |     29810 |  468303  1106572 |  188883   29750  3976507   133.7 |  0.750 % |
c |     30036 |  468299  1106563 |  207771   29972  3979340   132.8 |  0.751 % |
c |     30373 |  468155  1106231 |  228548   30307  3982134   131.4 |  0.779 % |
c |     30879 |  468155  1106231 |  251403   30813  3990096   129.5 |  0.779 % |
c |     31639 |  467372  1104440 |  276544   31548  4218343   133.7 |  0.923 % |
c |     32779 |  467372  1104440 |  304198   32688  4344352   132.9 |  0.923 % |
c |     34487 |  467372  1104440 |  334618   34396  4400897   127.9 |  0.923 % |
c |     37052 |  467372  1104440 |  368080   36961  4480046   121.2 |  0.923 % |
c |     40896 |  467372  1104440 |  404888   40805  4985112   122.2 |  0.923 % |
c ==============================================================================
c [1mFound solution: 5998915[0m
c ---[   0]---> Sorter-cost:   17     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     42145 |  467344  1104447 |  155781   42053  5161658   122.7 |  0.923 % |
c |     42245 |  467344  1104447 |  171359   42153  5183997   123.0 |  0.953 % |
c |     42395 |  467344  1104447 |  188495   42303  5185645   122.6 |  0.953 % |
c |     42620 |  467252  1104240 |  207344   42522  5191786   122.1 |  0.968 % |
c |     42957 |  467241  1104217 |  228078   42818  5205397   121.6 |  0.972 % |
c |     43463 |  467241  1104217 |  250886   43324  5212231   120.3 |  0.972 % |
c |     44222 |  467241  1104217 |  275975   44083  5224095   118.5 |  0.972 % |
c |     45361 |  467241  1104217 |  303573   45222  5243505   116.0 |  0.972 % |
c ==============================================================================
c [1mFound solution: 5933491[0m
c ---[   0]---> Sorter-cost:   15     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     47060 |  467261  1104269 |  155753   46921  5511609   117.5 |  0.972 % |
c |     47161 |  467261  1104269 |  171328   47022  5517962   117.3 |  0.972 % |
c |     47311 |  467261  1104269 |  188461   47172  5526326   117.2 |  0.972 % |
c |     47536 |  466617  1102787 |  207307   47382  5528015   116.7 |  1.093 % |
c |     47873 |  466012  1101415 |  228037   47700  5530455   115.9 |  1.199 % |
c |     48379 |  465921  1101207 |  250841   48204  5585589   115.9 |  1.215 % |
c |     49138 |  465917  1101199 |  275925   48960  5615925   114.7 |  1.216 % |
c |     50277 |  465917  1101199 |  303518   50099  5991500   119.6 |  1.216 % |
c |     51990 |  465290  1099771 |  333870   51786  6034019   116.5 |  1.325 % |
c |     54555 |  465277  1099743 |  367257   54350  6076631   111.8 |  1.327 % |
c |     58400 |  465087  1099310 |  403983   58192  6698129   115.1 |  1.360 % |
c |     64166 |  464548  1098080 |  444381   63927  9275171   145.1 |  1.460 % |
c |     72816 |  464544  1098071 |  488819   72575 11393116   157.0 |  1.460 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 14727 CPU time limit exceeded $XDIR/minisat+_64-bit_static -try "$@"
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.91 0.95 0.90 2/54 14723
Raw data (stat): 14723 (runsolver) R 14722 24172 24171 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 854839312 1052672 99 4294967295 134512640 135381576 3221224464 3221219672 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.0011 s]
Raw data (loadavg): 0.93 0.95 0.90 2/55 14727
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20.002 s]
Raw data (loadavg): 0.94 0.95 0.91 2/55 14727
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.0025 s]
Raw data (loadavg): 0.95 0.95 0.91 2/55 14727
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.0028 s]
Raw data (loadavg): 0.95 0.95 0.91 2/55 14727
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0048 s]
Raw data (loadavg): 0.96 0.95 0.91 2/55 14727
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.0052 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 14727
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.0056 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 14727
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.0067 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 14727
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.007 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 14727
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.008 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 14727
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.009 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 14727
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 14727
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 14727
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 14727
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 14727
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14727
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14727
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14727
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14727
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14727
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14727
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14727
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14727
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14727
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14727
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14727
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14727
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14727
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14727
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14727
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14727
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14727
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14727
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14727
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+350.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14727
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+360.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14727
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+370.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14727
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14727
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+390.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14727
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+400.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14727
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+410.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14727
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+420.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14727
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+430.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14727
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+440.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14727
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+450.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14727
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+460.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14727
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14727
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14727
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+490.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14727
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+500.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14727
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+510.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14727
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+520.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14727
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+530.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14727
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+540.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14727
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+550.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14727
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+560.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14727
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+570.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14727
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+580.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 14727
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+590.046 s]
Raw data (loadavg): 0.99 0.97 0.91 3/58 14766
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+600.048 s]
Raw data (loadavg): 1.07 0.99 0.91 2/55 14780
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+610.048 s]
Raw data (loadavg): 1.06 0.99 0.91 2/55 14780
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+620.049 s]
Raw data (loadavg): 1.05 0.99 0.91 2/55 14780
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+630.049 s]
Raw data (loadavg): 1.04 0.99 0.91 2/55 14780
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+640.051 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 14780
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+650.053 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 14780
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+660.052 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 14782
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+670.052 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 14782
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+680.053 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 14782
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+690.053 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 14782
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+700.054 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 14782
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+710.055 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 14782
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+720.055 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 14782
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+730.055 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14782
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+740.055 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14782
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+750.056 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14782
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+760.056 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14782
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+770.056 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14782
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+780.056 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14782
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+790.056 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14782
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+800.058 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14782
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+810.058 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14782
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+820.058 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14782
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+830.058 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14782
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+840.058 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14782
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+850.059 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14782
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+860.059 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14782
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+870.059 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14782
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+880.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14782
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+890.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14782
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+900.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14782
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+910.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14782
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+920.061 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14782
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+930.061 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14782
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+940.061 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14782
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+950.061 s]
Raw data (loadavg): 1.00 0.99 0.91 3/57 14784
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+960.061 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14784
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+970.061 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14784
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+980.061 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14784
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+990.062 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14784
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1000.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14784
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1010.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14784
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1020.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14784
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1030.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14784
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1040.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14784
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1050.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14784
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1060.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14784
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1070.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14784
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1080.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14784
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1090.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14784
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1100.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14784
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1110.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14784
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1120.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14784
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1130.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14784
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1140.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14784
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1150.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14784
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1160.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14784
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1170.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14784
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1180.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14784
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1190.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14784
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1200.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14784
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1210.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14784
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1220.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 14784
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1229.78 s]
Raw data (loadavg): 1.00 0.99 0.91 1/53 14784
Raw data (stat): 14723 (minisat+_script) S 14722 24172 24171 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854839312 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

Child status: 152
Real time (s): 1229.78
CPU time (s): 1229.89
CPU user time (s): 1228.82
CPU system time (s): 1.06984
CPU usage (%): 100.009
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####