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-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-mod013.opb
MD5SUM	f118194cabf88b58b64a9e7aec087bc0
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	51087398
Optimality of the best value was proved	NO
Number of terms in the objective function	1488
Biggest coefficient in the objective function	375272767488
Number of bits for the biggest coefficient in the objective function	39
Sum of the numbers in the objective function	12937590079727
Number of bits of the sum of numbers in the objective function	44
Biggest number in a constraint	375272767488
Number of bits of the biggest number in a constraint	39
Biggest sum of numbers in a constraint	12937590079727
Number of bits of the biggest sum of numbers	44
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1260.87
Number of variables	1488
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	240
Trace number 30719

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc22 THE 2005-05-25 18:49:43 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=22112 boxname=wulflinc22 idbench=928 idsolver=15 numberseed=0
MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814  /oldhome/oroussel/solvers/minisat+_script
MD5SUM BENCH:  f118194cabf88b58b64a9e7aec087bc0  /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-20-10-mod013.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-20-10-mod013.opb
IDLAUNCH: 22112
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.031
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.031
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:        603408 kB
Buffers:         35296 kB
Cached:         373528 kB
SwapCached:        400 kB
Active:          74476 kB
Inactive:       336564 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        603156 kB
SwapTotal:     2097892 kB
SwapFree:      2096804 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5580 kB
Slab:            14416 kB
Committed_AS:    63604 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-25 19:10:13 (client local time) WITH STATUS 152 IN 1229.88 SECONDS
stats: 22112 7 1229.88 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]---> Sorter-cost: 1234     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  72]---> Sorter-cost: 1234     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  70]---> Sorter-cost: 1176     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  68]---> Sorter-cost: 1176     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  66]---> Sorter-cost: 1176     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  64]---> Sorter-cost: 1042     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  63]---> BDD-cost:   22
c ---[  62]---> BDD-cost:   19
c ---[  61]---> BDD-cost:   20
c ---[  60]---> BDD-cost:   18
c ---[  58]---> Sorter-cost: 1897     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  57]---> BDD-cost:   18
c ---[  56]---> BDD-cost:   17
c ---[  55]---> BDD-cost:   17
c ---[  54]---> BDD-cost:   16
c ---[  53]---> BDD-cost:   22
c ---[  52]---> BDD-cost:   19
c ---[  51]---> BDD-cost:   20
c ---[  50]---> BDD-cost:   18
c ---[  49]---> BDD-cost:   18
c ---[  48]---> BDD-cost:   17
c ---[  46]---> Sorter-cost: 1897     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  45]---> BDD-cost:   17
c ---[  44]---> BDD-cost:   16
c ---[  43]---> BDD-cost:   19
c ---[  42]---> BDD-cost:   19
c ---[  41]---> BDD-cost:   20
c ---[  40]---> BDD-cost:   18
c ---[  39]---> BDD-cost:   18
c ---[  38]---> BDD-cost:   17
c ---[  37]---> BDD-cost:   17
c ---[  36]---> BDD-cost:   16
c ---[  34]---> Sorter-cost: 1843     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  33]---> BDD-cost:   18
c ---[  32]---> BDD-cost:   18
c ---[  31]---> BDD-cost:   18
c ---[  30]---> BDD-cost:   18
c ---[  29]---> BDD-cost:   18
c ---[  28]---> BDD-cost:   17
c ---[  27]---> BDD-cost:   17
c ---[  26]---> BDD-cost:   16
c ---[  25]---> BDD-cost:   17
c ---[  24]---> BDD-cost:   17
c ---[  22]---> Sorter-cost: 1843     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  21]---> BDD-cost:   17
c ---[  20]---> BDD-cost:   17
c ---[  19]---> BDD-cost:   17
c ---[  18]---> BDD-cost:   17
c ---[  17]---> BDD-cost:   17
c ---[  16]---> BDD-cost:   16
c ---[  15]---> BDD-cost:   16
c ---[  14]---> BDD-cost:   16
c ---[  13]---> BDD-cost:   16
c ---[  12]---> BDD-cost:   16
c ---[  10]---> Sorter-cost: 1793     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   9]---> BDD-cost:   16
c ---[   8]---> BDD-cost:   16
c ---[   7]---> BDD-cost:   16
c ---[   6]---> BDD-cost:   16
c ---[   4]---> Sorter-cost: 1589     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   2]---> Sorter-cost: 1219     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   0]---> Sorter-cost: 1234     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   52235   123460 |   17411       0        0     nan |  0.000 % |
c |       100 |   52208   123399 |   19152      99      321     3.2 |  8.091 % |
c |       250 |   52197   123375 |   21067     248      956     3.9 |  8.107 % |
c |       475 |   52169   123313 |   23174     469     2028     4.3 |  8.149 % |
c ==============================================================================
c [1mFound solution: 83322090[0m
c ---[   0]---> Adder-cost: 5416   maxlim: 164477957   bits: 28/28
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       684 |   89762   257873 |   29920     675     3086     4.6 |  8.149 % |
c |       787 |   89607   257520 |   32912     765     3688     4.8 |  6.836 % |
c |       937 |   89607   257520 |   36203     915     4406     4.8 |  6.836 % |
c |      1162 |   89578   257454 |   39823    1139     5432     4.8 |  6.869 % |
c |      1499 |   89445   257150 |   43805    1472    11344     7.7 |  7.032 % |
c |      2005 |   89445   257150 |   48186    1978    29991    15.2 |  7.032 % |
c ==============================================================================
c [1mFound solution: 81983676[0m
c ---[   0]---> Adder-cost: 0   maxlim: 165816371   bits: 28/28
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2474 |   89448   257275 |   29816    2446    37724    15.4 |  7.032 % |
c |      2574 |   89318   256978 |   32797    2541    38267    15.1 |  7.250 % |
c |      2725 |   89318   256978 |   36077    2692    43881    16.3 |  7.250 % |
c |      2950 |   89293   256923 |   39685    2915    45043    15.5 |  7.282 % |
c |      3288 |   89293   256923 |   43653    3253    49459    15.2 |  7.282 % |
c |      3794 |   89293   256923 |   48018    3759    61354    16.3 |  7.282 % |
c |      4553 |   89293   256923 |   52820    4518    84106    18.6 |  7.282 % |
c ==============================================================================
c [1mFound solution: 74364692[0m
c ---[   0]---> Adder-cost: 0   maxlim: 173435355   bits: 28/28
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4699 |   89303   257166 |   29767    4662    92920    19.9 |  7.282 % |
c |      4799 |   89296   257151 |   32743    4761    93439    19.6 |  7.371 % |
c |      4949 |   89267   257083 |   36018    4909    95100    19.4 |  7.404 % |
c |      5174 |   89267   257083 |   39619    5134    96754    18.8 |  7.404 % |
c |      5512 |   89251   257046 |   43581    5468   118879    21.7 |  7.424 % |
c ==============================================================================
c [1mFound solution: 45615645[0m
c ---[   0]---> Adder-cost: 0   maxlim: 202184402   bits: 28/28
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5630 |   89219   256711 |   29739    5578   124868    22.4 |  7.424 % |
c |      5730 |   89219   256711 |   32712    5678   125580    22.1 |  7.500 % |
c |      5880 |   89219   256711 |   35984    5828   126740    21.7 |  7.500 % |
c |      6106 |   89219   256711 |   39582    6054   128379    21.2 |  7.500 % |
c |      6443 |   89203   256659 |   43540    6388   134746    21.1 |  7.513 % |
c |      6953 |   89203   256659 |   47894    6898   191637    27.8 |  7.513 % |
c |      7712 |   89203   256659 |   52684    7657   202078    26.4 |  7.513 % |
c |      8851 |   89203   256659 |   57952    8796   330991    37.6 |  7.513 % |
c |     10559 |   89163   256569 |   63748   10501   631221    60.1 |  7.561 % |
c |     13121 |   89147   256534 |   70123   13061   758387    58.1 |  7.582 % |
c |     16965 |   89147   256534 |   77135   16905  1260176    74.5 |  7.582 % |
c |     22731 |   89057   256330 |   84848   22665  1536060    67.8 |  7.700 % |
c |     31384 |   88979   256153 |   93333   31313  2170685    69.3 |  7.797 % |
c |     44361 |   88979   256153 |  102667   44290  4075055    92.0 |  7.797 % |
c |     63823 |   88975   256144 |  112933   63751  7017820   110.1 |  7.801 % |
c |     93018 |   88929   256038 |  124227   92942  9549585   102.7 |  7.858 % |
c |    136807 |   88909   255994 |  136649   23972  2635704   109.9 |  7.882 % |
c |    202492 |   88742   255609 |  150314   89642  8670166    96.7 |  8.082 % |
c |    301018 |   88539   255148 |  165346   34282  5339795   155.8 |  8.317 % |
/oldhome/oroussel/solvers/minisat+_script: line 9:  6950 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.93 2/54 6946
Raw data (stat): 6946 (runsolver) R 6945 23310 23309 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 841167507 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 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+9.99965 s]
Raw data (loadavg): 0.93 0.95 0.93 2/55 6950
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20.0003 s]
Raw data (loadavg): 0.94 0.96 0.93 2/55 6950
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.0003 s]
Raw data (loadavg): 0.95 0.96 0.93 2/55 6950
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+39.9997 s]
Raw data (loadavg): 0.95 0.96 0.93 2/55 6950
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0004 s]
Raw data (loadavg): 0.96 0.96 0.93 2/55 6950
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.0004 s]
Raw data (loadavg): 0.97 0.96 0.93 2/55 6950
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.0008 s]
Raw data (loadavg): 0.97 0.96 0.93 2/55 6950
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.0015 s]
Raw data (loadavg): 0.98 0.96 0.93 2/55 6950
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.0016 s]
Raw data (loadavg): 0.98 0.96 0.93 2/55 6950
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.002 s]
Raw data (loadavg): 0.98 0.96 0.93 2/55 6950
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.002 s]
Raw data (loadavg): 0.98 0.96 0.93 2/55 6950
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.003 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 6950
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 6950
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 6950
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.003 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 6950
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 6950
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.003 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 6950
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.003 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 6950
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 6950
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 6950
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 6950
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 6950
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 6950
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 6950
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.003 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 6950
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 6950
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 6950
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 6950
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.003 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 6950
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.003 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 6950
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.003 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 6950
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 6950
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 6950
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 6950
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+350.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 6950
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+360.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 6950
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+370.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 6950
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 6950
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+390.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 6950
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+400.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 6950
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+410.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 6950
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+420.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 6950
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+430.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 6950
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+440.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 6950
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+450.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 6950
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+460.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 6950
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 6950
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 6950
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+490.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 6950
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+500.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 6950
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+510.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 6950
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+520.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 6950
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+530.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 6950
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+540.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 6950
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+550.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 6950
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+560.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 6950
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+570.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 6950
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+580.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 6950
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+590.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 6950
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+600.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 6950
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+610.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 6950
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+620.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/56 6951
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+630.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 7003
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+640.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 7003
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+650.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 7003
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+660.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 7003
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+670.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 7003
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+680.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 7003
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+690.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 7003
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+700.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 7005
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+710.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 7005
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+720.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 7005
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+730.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 7005
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+740.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 7005
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+750.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 7005
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+760.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 7005
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+770.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 7005
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+780.019 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 7005
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+790.019 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 7005
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+800.019 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 7005
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+810.019 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 7005
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+820.019 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 7005
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+830.019 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 7005
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+840.018 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 7005
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+850.019 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 7005
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+860.019 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 7005
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+870.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 7005
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+880.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 7005
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+890.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 7005
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+900.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 7005
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+910.019 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 7005
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+920.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 7005
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+930.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 7005
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+940.019 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 7005
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+950.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 7007
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+960.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 7007
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+970.019 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 7007
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+980.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 7007
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+990.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 7007
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 7007
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 7007
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 7007
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 7007
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 7007
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 7007
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 7007
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 7007
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 7007
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 7007
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 7007
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 7007
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 7007
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 7007
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 7007
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 7007
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 7007
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 7007
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 7007
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 7007
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 7007
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1210.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 7007
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1220.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 7007
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1229.72 s]
Raw data (loadavg): 0.99 0.97 0.93 1/53 7007
Raw data (stat): 6946 (minisat+_script) S 6945 23310 23309 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 841167507 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

Child status: 152
Real time (s): 1229.72
CPU time (s): 1229.88
CPU user time (s): 1228.99
CPU system time (s): 0.896863
CPU usage (%): 100.013
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####