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/plato.asu.edu/pub/fctp/normalized-mps-v2-13-7-ran10x10c.opb
MD5SUM	31a8734340f0544712ef974997c104b2
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	2677632
Optimality of the best value was proved	NO
Number of terms in the objective function	2100
Biggest coefficient in the objective function	4718592
Number of bits for the biggest coefficient in the objective function	23
Sum of the numbers in the objective function	515723936
Number of bits of the sum of numbers in the objective function	29
Biggest number in a constraint	4718592
Number of bits of the biggest number in a constraint	23
Biggest sum of numbers in a constraint	515723936
Number of bits of the biggest sum of numbers	29
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.05
Number of variables	2100
Total number of constraints	120
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	120
Minimum length of a constraint	21
Maximum length of a constraint	200
Trace number 31260

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc27 THE 2005-05-25 23:36:57 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=22663 boxname=wulflinc27 idbench=1479 idsolver=15 numberseed=0
MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814  /oldhome/oroussel/solvers/minisat+_script
MD5SUM BENCH:  31a8734340f0544712ef974997c104b2  /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-13-7-ran10x10c.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-13-7-ran10x10c.opb
IDLAUNCH: 22663
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.169
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.169
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:        887116 kB
Buffers:         20728 kB
Cached:         105956 kB
SwapCached:        612 kB
Active:          15928 kB
Inactive:       112844 kB
HighTotal:      131008 kB
HighFree:        29736 kB
LowTotal:       903652 kB
LowFree:        857380 kB
SwapTotal:     2097892 kB
SwapFree:      2096360 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5072 kB
Slab:            13192 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-25 23:57:27 (client local time) WITH STATUS 152 IN 1229.88 SECONDS
stats: 22663 7 1229.88 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 140 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ####################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 138]---> Sorter-cost: 1658     Base: 2 2 2 2 2 2 2 2
c ---[ 136]---> Sorter-cost: 1972     Base: 2 2 2 2 2 2 2 2 2
c ---[ 134]---> Sorter-cost: 2017     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 132]---> Sorter-cost: 1972     Base: 2 2 2 2 2 2 2 2 2
c ---[ 130]---> Sorter-cost: 1972     Base: 2 2 2 2 2 2 2 2 2
c ---[ 128]---> Sorter-cost: 1442     Base: 2 2 2 2 2 2 2
c ---[ 126]---> Sorter-cost: 1972     Base: 2 2 2 2 2 2 2 2 2
c ---[ 124]---> Sorter-cost: 1934     Base: 2 2 2 2 2 2 2 2
c ---[ 122]---> Sorter-cost: 1972     Base: 2 2 2 2 2 2 2 2 2
c ---[ 120]---> Sorter-cost: 2017     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 118]---> Sorter-cost: 1780     Base: 2 2 2 2 2 2 2
c ---[ 116]---> Sorter-cost: 2045     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 114]---> Sorter-cost: 1780     Base: 2 2 2 2 2 2 2
c ---[ 112]---> Sorter-cost: 2045     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 110]---> Adder-cost: 178   maxlim: 8182   bits: 14/13
c ---[ 108]---> Adder-cost: 178   maxlim: 8438   bits: 14/14
c ---[ 106]---> Sorter-cost: 2013     Base: 2 2 2 2 2 2 2 2 2
c ---[ 104]---> Sorter-cost: 2013     Base: 2 2 2 2 2 2 2 2 2
c ---[ 102]---> Sorter-cost: 2045     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 100]---> Sorter-cost: 1780     Base: 2 2 2 2 2 2 2
c ---[  99]---> BDD-cost:   10
c ---[  98]---> BDD-cost:   11
c ---[  97]---> BDD-cost:   10
c ---[  96]---> BDD-cost:   15
c ---[  95]---> BDD-cost:   10
c ---[  94]---> BDD-cost:   15
c ---[  93]---> BDD-cost:   12
c ---[  92]---> BDD-cost:   11
c ---[  91]---> BDD-cost:   15
c ---[  90]---> BDD-cost:   15
c ---[  89]---> BDD-cost:   15
c ---[  88]---> BDD-cost:   10
c ---[  87]---> BDD-cost:   10
c ---[  86]---> BDD-cost:   10
c ---[  85]---> BDD-cost:   13
c ---[  84]---> BDD-cost:   10
c ---[  83]---> BDD-cost:   13
c ---[  82]---> BDD-cost:   12
c ---[  81]---> BDD-cost:   11
c ---[  80]---> BDD-cost:   15
c ---[  79]---> BDD-cost:   13
c ---[  78]---> BDD-cost:   13
c ---[  77]---> BDD-cost:   10
c ---[  76]---> BDD-cost:   11
c ---[  75]---> BDD-cost:   10
c ---[  74]---> BDD-cost:   15
c ---[  73]---> BDD-cost:   10
c ---[  72]---> BDD-cost:   15
c ---[  71]---> BDD-cost:   12
c ---[  70]---> BDD-cost:   11
c ---[  69]---> BDD-cost:   15
c ---[  68]---> BDD-cost:   15
c ---[  67]---> BDD-cost:   15
c ---[  66]---> BDD-cost:   10
c ---[  65]---> BDD-cost:   11
c ---[  64]---> BDD-cost:   10
c ---[  63]---> BDD-cost:   14
c ---[  62]---> BDD-cost:   10
c ---[  61]---> BDD-cost:   14
c ---[  60]---> BDD-cost:   12
c ---[  59]---> BDD-cost:   11
c ---[  58]---> BDD-cost:   14
c ---[  57]---> BDD-cost:   14
c ---[  56]---> BDD-cost:   14
c ---[  55]---> BDD-cost:   10
c ---[  54]---> BDD-cost:   11
c ---[  53]---> BDD-cost:    9
c ---[  52]---> BDD-cost:    9
c ---[  51]---> BDD-cost:    9
c ---[  50]---> BDD-cost:    9
c ---[  49]---> BDD-cost:    9
c ---[  48]---> BDD-cost:    9
c ---[  47]---> BDD-cost:    9
c ---[  46]---> BDD-cost:    9
c ---[  45]---> BDD-cost:    9
c ---[  44]---> BDD-cost:    9
c ---[  43]---> BDD-cost:   11
c ---[  42]---> BDD-cost:   10
c ---[  41]---> BDD-cost:   15
c ---[  40]---> BDD-cost:   10
c ---[  39]---> BDD-cost:   15
c ---[  38]---> BDD-cost:   12
c ---[  37]---> BDD-cost:   11
c ---[  36]---> BDD-cost:   15
c ---[  35]---> BDD-cost:   13
c ---[  34]---> BDD-cost:   15
c ---[  33]---> BDD-cost:   10
c ---[  32]---> BDD-cost:   11
c ---[  31]---> BDD-cost:   10
c ---[  30]---> BDD-cost:   13
c ---[  29]---> BDD-cost:   10
c ---[  28]---> BDD-cost:   13
c ---[  27]---> BDD-cost:   12
c ---[  26]---> BDD-cost:   11
c ---[  25]---> BDD-cost:   13
c ---[  24]---> BDD-cost:   13
c ---[  23]---> BDD-cost:   13
c ---[  22]---> BDD-cost:   10
c ---[  21]---> BDD-cost:   11
c ---[  20]---> BDD-cost:   10
c ---[  19]---> BDD-cost:   15
c ---[  18]---> BDD-cost:   10
c ---[  17]---> BDD-cost:   15
c ---[  16]---> BDD-cost:   12
c ---[  15]---> BDD-cost:   11
c ---[  14]---> BDD-cost:   15
c ---[  13]---> BDD-cost:   15
c ---[  12]---> BDD-cost:   15
c ---[  11]---> BDD-cost:   10
c ---[  10]---> BDD-cost:   10
c ---[   9]---> BDD-cost:   10
c ---[   8]---> BDD-cost:   17
c ---[   7]---> BDD-cost:   10
c ---[   6]---> BDD-cost:   17
c ---[   5]---> BDD-cost:   12
c ---[   4]---> BDD-cost:   11
c ---[   3]---> BDD-cost:   15
c ---[   2]---> BDD-cost:   13
c ---[   1]---> BDD-cost:   17
c ---[   0]---> BDD-cost:   10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   91521   218607 |   30507       0        0     nan |  0.000 % |
c |       101 |   91521   218607 |   33557     101      642     6.4 |  6.867 % |
c |       252 |   91175   217815 |   36913     235     1183     5.0 |  7.174 % |
c |       477 |   91099   217646 |   40604     453     2086     4.6 |  7.238 % |
c |       814 |   90963   217336 |   44665     781     3761     4.8 |  7.358 % |
c |      1320 |   90963   217336 |   49131    1287     6695     5.2 |  7.358 % |
c |      2081 |   90952   217312 |   54045    2046    15341     7.5 |  7.367 % |
c |      3220 |   90899   217192 |   59449    3181    23553     7.4 |  7.416 % |
c ==============================================================================
c [1mFound solution: 10107013[0m
c ---[   0]---> Adder-cost: 4060   maxlim: 2874907   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4823 |  119071   317977 |   39690    4758    65984    13.9 |  7.416 % |
c |      4923 |  119038   317866 |   43659    4854    66482    13.7 |  6.730 % |
c |      5074 |  119022   317831 |   48024    5000    67119    13.4 |  6.744 % |
c |      5300 |  119022   317831 |   52827    5226    68603    13.1 |  6.744 % |
c |      5637 |  119006   317779 |   58110    5561    70687    12.7 |  6.752 % |
c |      6143 |  119006   317779 |   63921    6067    73554    12.1 |  6.752 % |
c |      6902 |  118895   317524 |   70313    6819    78215    11.5 |  6.839 % |
c |      8043 |  118868   317444 |   77344    7957    84971    10.7 |  6.855 % |
c |      9752 |  118826   317342 |   85079    9661   166486    17.2 |  6.888 % |
c |     12314 |  118774   317217 |   93586   12218   198346    16.2 |  6.929 % |
c ==============================================================================
c [1mFound solution: 9973742[0m
c ---[   0]---> Adder-cost: 0   maxlim: 3008178   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12622 |  118807   317467 |   39602   12526   200724    16.0 |  6.929 % |
c |     12722 |  118807   317467 |   43562   12626   201414    16.0 |  6.959 % |
c |     12872 |  118727   317283 |   47918   12775   202250    15.8 |  7.029 % |
c |     13098 |  118727   317283 |   52710   13001   203741    15.7 |  7.029 % |
c |     13435 |  118727   317283 |   57981   13338   206757    15.5 |  7.029 % |
c |     13941 |  118727   317283 |   63779   13844   216461    15.6 |  7.029 % |
c |     14700 |  118579   316932 |   70157   14591   220462    15.1 |  7.157 % |
c |     15839 |  118579   316932 |   77173   15730   251933    16.0 |  7.157 % |
c |     17547 |  118453   316649 |   84890   17430   287900    16.5 |  7.258 % |
c |     20110 |  118445   316623 |   93379   19992   497092    24.9 |  7.261 % |
c ==============================================================================
c [1mFound solution: 3754669[0m
c ---[   0]---> Adder-cost: 2   maxlim: 9227251   bits: 24/24
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     22201 |  118431   316761 |   39477   22082   604335    27.4 |  7.261 % |
c |     22301 |  118380   316647 |   43424   22179   604829    27.3 |  7.364 % |
c |     22452 |  118380   316647 |   47767   22330   605695    27.1 |  7.364 % |
c |     22677 |  118380   316647 |   52543   22555   606999    26.9 |  7.364 % |
c |     23016 |  118380   316647 |   57798   22894   612429    26.8 |  7.364 % |
c |     23522 |  118380   316647 |   63578   23400   627934    26.8 |  7.364 % |
c |     24281 |  118380   316647 |   69935   24159   647058    26.8 |  7.364 % |
c |     25422 |  118337   316552 |   76929   25296   724008    28.6 |  7.397 % |
c |     27130 |  118290   316447 |   84622   26995   832379    30.8 |  7.435 % |
c |     29693 |  118290   316447 |   93084   29558   999206    33.8 |  7.435 % |
c |     33537 |  118067   315927 |  102393   33358  1167125    35.0 |  7.617 % |
c |     39304 |  117853   315435 |  112632   39096  1385920    35.4 |  7.783 % |
c |     47954 |  117382   314355 |  123895   47676  2119946    44.5 |  8.151 % |
c |     60928 |  117349   314282 |  136285   60647  3114519    51.4 |  8.175 % |
c ==============================================================================
c [1mFound solution: 3341769[0m
c ---[   0]---> Adder-cost: 0   maxlim: 9640151   bits: 24/24
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     68046 |  117346   314353 |   39115   67760  4697785    69.3 |  8.175 % |
c |     68146 |  117346   314353 |   43026   19524  1884623    96.5 |  8.203 % |
c |     68296 |  117346   314353 |   47329   19674  1886618    95.9 |  8.203 % |
c |     68521 |  117346   314353 |   52062   19899  1907836    95.9 |  8.203 % |
c |     68858 |  117346   314353 |   57268   20236  1934374    95.6 |  8.203 % |
c |     69364 |  117299   314243 |   62995   20741  1951395    94.1 |  8.244 % |
c |     70124 |  117234   314088 |   69294   21495  1978182    92.0 |  8.293 % |
c |     71264 |  117234   314088 |   76224   22635  2111894    93.3 |  8.293 % |
c |     72975 |  117234   314088 |   83846   24346  2175908    89.4 |  8.293 % |
c |     75537 |  117171   313941 |   92231   26905  2305933    85.7 |  8.347 % |
c |     79383 |  117080   313725 |  101454   30737  2463292    80.1 |  8.415 % |
c |     85150 |  116913   313349 |  111599   36478  2960182    81.1 |  8.554 % |
c |     93799 |  116731   312932 |  122759   45116  3509007    77.8 |  8.701 % |
c |    106774 |  116354   312072 |  135035   58049  5225991    90.0 |  8.995 % |
c |    126235 |  116292   311920 |  148539   77502  6497502    83.8 |  9.044 % |
c |    155427 |  115462   309992 |  163393  106636  8534876    80.0 |  9.751 % |
c |    199217 |  115170   309319 |  179732  150390 18763913   124.8 |  9.999 % |
c |    264901 |  114897   308683 |  197705   46705  2023468    43.3 | 10.211 % |
c ==============================================================================
c [1mFound solution: 3338727[0m
c ---[   0]---> Adder-cost: 0   maxlim: 9643193   bits: 24/24
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    281774 |  114900   308789 |   38300   63575  4054558    63.8 | 10.211 % |
c |    281877 |  114872   308725 |   42130   18625  1713766    92.0 | 10.254 % |
c |    282027 |  114759   308467 |   46343   18770  1714454    91.3 | 10.352 % |
c |    282252 |  114759   308467 |   50977   18995  1715684    90.3 | 10.352 % |
c |    282591 |  114759   308467 |   56075   19334  1720040    89.0 | 10.352 % |
c |    283098 |  114759   308467 |   61682   19841  1776974    89.6 | 10.352 % |
c |    283857 |  114759   308467 |   67850   20600  1790487    86.9 | 10.352 % |
c |    284996 |  114740   308424 |   74635   21738  1854893    85.3 | 10.369 % |
c |    286704 |  114642   308199 |   82099   23433  1893368    80.8 | 10.450 % |
c |    289269 |  114515   307900 |   90309   25990  2036394    78.4 | 10.559 % |
c |    293113 |  114515   307900 |   99340   29834  2704748    90.7 | 10.559 % |
c |    298880 |  114468   307790 |  109274   35600  2976593    83.6 | 10.600 % |
c |    307529 |  114260   307305 |  120201   44230  3855098    87.2 | 10.782 % |
c |    320504 |  114187   307138 |  132221   57182  4619114    80.8 | 10.837 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 22931 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.97 0.99 2/54 22927
Raw data (stat): 22927 (runsolver) R 22926 3394 3393 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 842886630 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0009 s]
Raw data (loadavg): 0.93 0.97 0.99 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.0022 s]
Raw data (loadavg): 0.94 0.97 0.99 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.003 s]
Raw data (loadavg): 0.95 0.97 0.99 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.0031 s]
Raw data (loadavg): 0.95 0.97 0.99 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.0037 s]
Raw data (loadavg): 0.96 0.97 0.99 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.0035 s]
Raw data (loadavg): 0.97 0.97 0.99 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.0047 s]
Raw data (loadavg): 0.97 0.97 0.99 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.0052 s]
Raw data (loadavg): 0.98 0.97 0.99 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.005 s]
Raw data (loadavg): 0.98 0.97 0.99 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.005 s]
Raw data (loadavg): 0.98 0.97 0.99 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.006 s]
Raw data (loadavg): 0.98 0.97 0.99 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.006 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.006 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.006 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.006 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.006 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.006 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.006 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.006 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.007 s]
Raw data (loadavg): 1.15 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.006 s]
Raw data (loadavg): 1.12 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.006 s]
Raw data (loadavg): 1.10 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.007 s]
Raw data (loadavg): 1.09 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.007 s]
Raw data (loadavg): 1.07 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.007 s]
Raw data (loadavg): 1.06 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.008 s]
Raw data (loadavg): 1.05 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.007 s]
Raw data (loadavg): 1.04 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.007 s]
Raw data (loadavg): 1.04 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.007 s]
Raw data (loadavg): 1.03 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.007 s]
Raw data (loadavg): 1.03 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.007 s]
Raw data (loadavg): 1.02 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.007 s]
Raw data (loadavg): 1.02 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.007 s]
Raw data (loadavg): 1.01 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.007 s]
Raw data (loadavg): 1.01 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.008 s]
Raw data (loadavg): 1.01 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.008 s]
Raw data (loadavg): 1.01 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.008 s]
Raw data (loadavg): 1.01 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.009 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.008 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.009 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.009 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.009 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.01 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.01 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.01 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.01 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.01 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.01 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.01 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.011 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.01 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.017 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.026 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.026 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.027 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.028 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.028 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.029 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.028 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.029 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.029 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.029 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.029 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.03 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.03 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.03 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.03 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.03 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.03 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.031 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.031 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.03 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.03 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.031 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.032 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.032 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.031 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.034 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.033 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.034 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.035 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.035 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.036 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.036 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.036 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.037 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.037 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.037 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.037 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.037 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.038 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.038 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.038 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.038 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.039 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.04 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.039 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.04 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.04 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.04 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.04 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.04 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.04 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.04 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.04 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.04 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.04 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.04 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.04 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.04 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.05 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.04 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.05 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.05 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.05 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.05 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.05 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.05 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.05 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.05 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.05 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.05 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.73 s]
Raw data (loadavg): 1.00 1.00 1.00 1/53 22931
Raw data (stat): 22927 (minisat+_script) S 22926 3394 3393 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842886630 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 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.73
CPU time (s): 1229.88
CPU user time (s): 1229.01
CPU system time (s): 0.873867
CPU usage (%): 100.013
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####