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-gr4x6.opb
MD5SUM	c1c7537cd9b3e10215a81ec1ca3be5cb
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	2605440
Optimality of the best value was proved	NO
Number of terms in the objective function	504
Biggest coefficient in the objective function	148373504
Number of bits for the biggest coefficient in the objective function	28
Sum of the numbers in the objective function	3393589600
Number of bits of the sum of numbers in the objective function	32
Biggest number in a constraint	148373504
Number of bits of the biggest number in a constraint	28
Biggest sum of numbers in a constraint	3393589600
Number of bits of the biggest sum of numbers	32
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1189.01
Number of variables	504
Total number of constraints	34
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	34
Minimum length of a constraint	21
Maximum length of a constraint	120
Trace number 32433

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc1 THE 2005-05-27 09:53:09 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=23817 boxname=wulflinc1 idbench=1461 idsolver=16 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  c1c7537cd9b3e10215a81ec1ca3be5cb  /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-13-7-gr4x6.opb
REAL COMMAND:  minisat+_script -cb -gs /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-13-7-gr4x6.opb
IDLAUNCH: 23817
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.053
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	: 2
cpu MHz		: 451.053
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:        913356 kB
Buffers:           152 kB
Cached:          97944 kB
SwapCached:        708 kB
Active:          16348 kB
Inactive:        83924 kB
HighTotal:      131008 kB
HighFree:        29260 kB
LowTotal:       903652 kB
LowFree:        884096 kB
SwapTotal:     2097136 kB
SwapFree:      2095336 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5684 kB
Slab:            15120 kB
Committed_AS:    92712 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-27 10:13:39 (client local time) WITH STATUS 152 IN 1229.86 SECONDS
stats: 23817 7 1229.86 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 44 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ##########
c   -- Clauses(.)/Splits(s): (none)
c ---[  42]---> BDD-cost:  495
c ---[  40]---> BDD-cost:  488
c ---[  38]---> BDD-cost:  463
c ---[  36]---> BDD-cost:  435
c ---[  34]---> BDD-cost:  234
c ---[  32]---> BDD-cost:  224
c ---[  30]---> BDD-cost:  224
c ---[  28]---> BDD-cost:  204
c ---[  26]---> BDD-cost:  177
c ---[  24]---> BDD-cost:  177
c ---[  23]---> BDD-cost:   19
c ---[  22]---> BDD-cost:   16
c ---[  21]---> BDD-cost:   13
c ---[  20]---> BDD-cost:   13
c ---[  19]---> BDD-cost:   15
c ---[  18]---> BDD-cost:   15
c ---[  17]---> BDD-cost:   15
c ---[  16]---> BDD-cost:   15
c ---[  15]---> BDD-cost:   13
c ---[  14]---> BDD-cost:   13
c ---[  13]---> BDD-cost:   15
c ---[  12]---> BDD-cost:   15
c ---[  11]---> BDD-cost:   17
c ---[  10]---> BDD-cost:   15
c ---[   9]---> BDD-cost:   15
c ---[   8]---> BDD-cost:   13
c ---[   7]---> BDD-cost:   13
c ---[   6]---> BDD-cost:   15
c ---[   5]---> BDD-cost:   13
c ---[   4]---> BDD-cost:   13
c ---[   3]---> BDD-cost:   19
c ---[   2]---> BDD-cost:   16
c ---[   1]---> BDD-cost:   17
c ---[   0]---> BDD-cost:   15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    8809    24521 |    2936       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 6085600[0m
c ---[   0]---> Sorter-cost:63811     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         7 |  185634   437451 |   61878       7       28     4.0 |  0.000 % |
c |       109 |  185634   437451 |   68065     109    10829    99.3 |  0.389 % |
c |       259 |  185634   437451 |   74872     259    12339    47.6 |  0.389 % |
c |       484 |  185634   437451 |   82359     484    17455    36.1 |  0.389 % |
c ==============================================================================
c [1mFound solution: 6054672[0m
c ---[   0]---> Sorter-cost:   12     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       543 |  185656   438008 |   61885     543    19291    35.5 |  0.389 % |
c |       645 |  185656   438008 |   68073     645    20191    31.3 |  0.391 % |
c |       796 |  185644   437981 |   74880     795    20911    26.3 |  0.395 % |
c |      1022 |  185620   437927 |   82368    1019    23599    23.2 |  0.405 % |
c |      1359 |  185620   437927 |   90605    1356    26746    19.7 |  0.405 % |
c |      1865 |  185620   437927 |   99666    1862    30127    16.2 |  0.405 % |
c |      2626 |  185620   437927 |  109633    2623    39710    15.1 |  0.405 % |
c |      3767 |  185620   437927 |  120596    3764    54884    14.6 |  0.405 % |
c ==============================================================================
c [1mFound solution: 5902515[0m
c ---[   0]---> Sorter-cost:   16     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3832 |  186071   439121 |   62023    3829    56124    14.7 |  0.405 % |
c |      3932 |  186071   439121 |   68225    3929    56740    14.4 |  0.405 % |
c ==============================================================================
c [1mFound solution: 5604192[0m
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3990 |  186595   440382 |   62198    3987    57332    14.4 |  0.405 % |
c |      4090 |  186595   440382 |   68417    4087    58977    14.4 |  0.404 % |
c |      4240 |  186595   440382 |   75259    4237    60735    14.3 |  0.404 % |
c |      4465 |  186595   440382 |   82785    4462    72438    16.2 |  0.404 % |
c |      4803 |  186316   439754 |   91064    4784    80147    16.8 |  0.521 % |
c |      5313 |  186316   439754 |  100170    5294    85822    16.2 |  0.521 % |
c |      6074 |  186297   439712 |  110187    6054   117578    19.4 |  0.529 % |
c ==============================================================================
c [1mFound solution: 5516752[0m
c ---[   0]---> Sorter-cost:   11     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6108 |  186757   440811 |   62252    6088   118170    19.4 |  0.529 % |
c |      6210 |  186757   440811 |   68477    6190   121479    19.6 |  0.528 % |
c |      6362 |  186757   440811 |   75324    6342   127324    20.1 |  0.528 % |
c ==============================================================================
c [1mFound solution: 5488590[0m
c ---[   0]---> Sorter-cost:   16     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6492 |  186992   441414 |   62330    6469   131533    20.3 |  0.528 % |
c |      6592 |  186992   441414 |   68563    6569   132394    20.2 |  0.572 % |
c |      6742 |  186992   441414 |   75419    6719   133154    19.8 |  0.572 % |
c |      6967 |  186992   441414 |   82961    6944   136111    19.6 |  0.572 % |
c |      7304 |  186992   441414 |   91257    7281   141916    19.5 |  0.572 % |
c |      7810 |  186949   441314 |  100383    7784   175720    22.6 |  0.589 % |
c ==============================================================================
c [1mFound solution: 5338603[0m
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7917 |  186973   441372 |   62324    7891   177945    22.6 |  0.589 % |
c |      8020 |  186973   441372 |   68556    7994   199887    25.0 |  0.590 % |
c |      8170 |  186973   441372 |   75412    8144   202174    24.8 |  0.590 % |
c |      8396 |  186801   440984 |   82953    8363   203607    24.3 |  0.663 % |
c |      8733 |  186801   440984 |   91248    8700   205751    23.6 |  0.663 % |
c |      9239 |  186801   440984 |  100373    9206   211248    22.9 |  0.663 % |
c |      9998 |  186801   440984 |  110410    9965   218736    22.0 |  0.663 % |
c |     11137 |  186801   440984 |  121451   11104   228027    20.5 |  0.663 % |
c |     12845 |  186801   440984 |  133597   12812   368304    28.7 |  0.663 % |
c |     15407 |  186801   440984 |  146956   15374   979575    63.7 |  0.663 % |
c ==============================================================================
c [1mFound solution: 5180312[0m
c ---[   0]---> Sorter-cost:   15     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     17753 |  186644   440653 |   62214   17709  1203958    68.0 |  0.663 % |
c |     17854 |  186515   440368 |   68435   17807  1204705    67.7 |  0.806 % |
c |     18005 |  186200   439656 |   75278   17951  1205614    67.2 |  0.943 % |
c |     18230 |  186200   439656 |   82806   18176  1222002    67.2 |  0.943 % |
c |     18568 |  186200   439656 |   91087   18514  1226151    66.2 |  0.943 % |
c |     19074 |  186200   439656 |  100196   19020  1231480    64.7 |  0.943 % |
c |     19833 |  186200   439656 |  110215   19779  1243008    62.8 |  0.943 % |
c ==============================================================================
c [1mFound solution: 4770772[0m
c ---[   0]---> Sorter-cost:   15     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20202 |  186253   439796 |   62084   20148  1336483    66.3 |  0.943 % |
c |     20303 |  186253   439796 |   68292   20249  1337769    66.1 |  0.944 % |
c ==============================================================================
c [1mFound solution: 4664369[0m
c ---[   0]---> Sorter-cost:   12     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20452 |  186286   439884 |   62095   20398  1353419    66.4 |  0.944 % |
c ==============================================================================
c [1mFound solution: 3772369[0m
c ---[   0]---> Sorter-cost:   12     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20500 |  186337   440021 |   62112   20443  1353834    66.2 |  0.944 % |
c ==============================================================================
c [1mFound solution: 3694603[0m
c ---[   0]---> Sorter-cost:   13     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20503 |  186361   440080 |   62120   20446  1353863    66.2 |  0.944 % |
c ==============================================================================
c [1mFound solution: 3515403[0m
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20508 |  186391   440157 |   62130   20451  1354519    66.2 |  0.944 % |
c |     20608 |  186391   440157 |   68343   20551  1356510    66.0 |  0.963 % |
c |     20758 |  186391   440157 |   75177   20701  1357754    65.6 |  0.963 % |
c |     20983 |  186391   440157 |   82695   20926  1375834    65.7 |  0.963 % |
c |     21322 |  186391   440157 |   90964   21265  1422802    66.9 |  0.963 % |
c |     21830 |  186391   440157 |  100060   21773  1500138    68.9 |  0.963 % |
c |     22591 |  186387   440149 |  110067   22532  1589109    70.5 |  0.966 % |
c ==============================================================================
c [1mFound solution: 3439232[0m
c ---[   0]---> Sorter-cost:   13     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     22783 |  186423   440244 |   62141   22724  1598461    70.3 |  0.966 % |
c |     22883 |  186423   440244 |   68355   22824  1601441    70.2 |  0.967 % |
c |     23034 |  186423   440244 |   75190   22975  1604453    69.8 |  0.967 % |
c |     23259 |  186423   440244 |   82709   23200  1620505    69.8 |  0.967 % |
c ==============================================================================
c [1mFound solution: 3298528[0m
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     23385 |  186440   440289 |   62146   23326  1638607    70.2 |  0.967 % |
c |     23486 |  186339   440062 |   68360   23424  1639187    70.0 |  1.012 % |
c |     23636 |  186339   440062 |   75196   23574  1640902    69.6 |  1.012 % |
c |     23861 |  186339   440062 |   82716   23799  1653029    69.5 |  1.012 % |
c |     24198 |  186284   439937 |   90987   24134  1683585    69.8 |  1.036 % |
c |     24705 |  186284   439937 |  100086   24641  1723776    70.0 |  1.036 % |
c |     25464 |  186284   439937 |  110095   25400  1841069    72.5 |  1.036 % |
c |     26603 |  186284   439937 |  121104   26539  1867145    70.4 |  1.036 % |
c ==============================================================================
c [1mFound solution: 2806400[0m
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26960 |  186328   440045 |   62109   26896  1875438    69.7 |  1.036 % |
c |     27060 |  186328   440045 |   68319   26996  1877658    69.6 |  1.040 % |
c |     27210 |  186328   440045 |   75151   27146  1880790    69.3 |  1.040 % |
c |     27436 |  186328   440045 |   82667   27372  1885651    68.9 |  1.040 % |
c |     27774 |  186328   440045 |   90933   27710  1905488    68.8 |  1.040 % |
c |     28282 |  186328   440045 |  100027   28218  1949296    69.1 |  1.040 % |
c |     29044 |  186328   440045 |  110029   28980  1990282    68.7 |  1.040 % |
c |     30184 |  186283   439944 |  121032   30114  2026792    67.3 |  1.062 % |
c |     31893 |  186283   439944 |  133136   31823  2201134    69.2 |  1.062 % |
c |     34456 |  186283   439944 |  146449   34386  2355851    68.5 |  1.062 % |
c |     38301 |  186283   439944 |  161094   38231  2596501    67.9 |  1.062 % |
c |     44069 |  186283   439944 |  177204   43999  2861641    65.0 |  1.062 % |
c |     52719 |  186283   439944 |  194924   52649  3331230    63.3 |  1.062 % |
c |     65694 |  186283   439944 |  214417   65624  4071595    62.0 |  1.062 % |
c |     85157 |  186283   439944 |  235858   85087  5112278    60.1 |  1.062 % |
c |    114349 |  186283   439944 |  259444  114279  7244007    63.4 |  1.062 % |
/oldhome/oroussel/solvers/minisat+_script: line 9:  4122 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.97 0.97 0.91 2/55 4118
Raw data (stat): 4118 (runsolver) R 4117 8378 8377 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 740153094 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+10.0008 s]
Raw data (loadavg): 0.97 0.97 0.91 2/56 4122
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.0017 s]
Raw data (loadavg): 0.98 0.97 0.91 2/56 4122
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.0026 s]
Raw data (loadavg): 0.98 0.97 0.91 2/56 4122
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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+40.0024 s]
Raw data (loadavg): 0.98 0.97 0.91 2/56 4122
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.0032 s]
Raw data (loadavg): 0.98 0.97 0.91 2/56 4122
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4122
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.0045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4122
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.0047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4122
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.0045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4122
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4122
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4122
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4122
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4122
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4122
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4122
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4122
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4122
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4122
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4122
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4122
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4122
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4122
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4122
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4122
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4122
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4122
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4122
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4122
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4122
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4122
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4122
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4122
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4122
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4122
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4122
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4122
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4122
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4122
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4122
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4122
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4122
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4175
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4175
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4175
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4175
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4175
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4175
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4179
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4179
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4179
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4179
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4179
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4179
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4179
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4179
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4179
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4179
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4179
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4179
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4179
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4179
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4179
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4179
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4179
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4179
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4179
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4179
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4179
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4179
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4179
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4179
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4179
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4181
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4181
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4181
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4181
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4181
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4181
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4181
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4181
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4181
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4181
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4181
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4181
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4181
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4181
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4181
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4181
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4181
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4181
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4181
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4181
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4181
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4181
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4181
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4181
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4181
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4181
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4181
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4181
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4181
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.91 2/56 4181
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4181
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4181
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4181
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4181
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4181
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4181
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4181
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4181
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4181
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4181
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4181
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4181
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4181
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4181
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4181
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4181
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4181
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4181
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4181
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 4181
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.75 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 4181
Raw data (stat): 4118 (minisat+_script) S 4117 8378 8377 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 740153094 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.75
CPU time (s): 1229.86
CPU user time (s): 1229.33
CPU system time (s): 0.530919
CPU usage (%): 100.009
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####