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/submitted/manquinho/primes-dimacs-cnf/normalized-ii8a3.opb
MD5SUM	a430664a9b4f203a5896b33ca2b0e0e5
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	191
Optimality of the best value was proved	NO
Number of terms in the objective function	528
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	528
Number of bits of the sum of numbers in the objective function	10
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	528
Number of bits of the biggest sum of numbers	10
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.02384
Number of variables	528
Total number of constraints	1816
Number of constraints which are clauses	1816
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	2
Maximum length of a constraint	8
Trace number 31574

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc10 THE 2005-05-27 04:54:59 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=22919 boxname=wulflinc10 idbench=165 idsolver=16 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  a430664a9b4f203a5896b33ca2b0e0e5  /oldhome/oroussel/tmp/wulflinc10/normalized-ii8a3.opb
REAL COMMAND:  minisat+_script -cb -gs /oldhome/oroussel/tmp/wulflinc10/normalized-ii8a3.opb
IDLAUNCH: 22919
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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	: 2
cpu MHz		: 450.999
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:        612148 kB
Buffers:         35372 kB
Cached:         364988 kB
SwapCached:         92 kB
Active:          66156 kB
Inactive:       336888 kB
HighTotal:      131008 kB
HighFree:         9296 kB
LowTotal:       903652 kB
LowFree:        602852 kB
SwapTotal:     2097136 kB
SwapFree:      2096752 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6396 kB
Slab:            13704 kB
Committed_AS:    63604 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-27 05:15:29 (client local time) WITH STATUS 152 IN 1229.84 SECONDS
stats: 22919 7 1229.84 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1816 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ........................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    1816     4536 |     605       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 232[0m
c ---[   0]---> Sorter-cost:23592     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         3 |   29165    68520 |    9721       3       16     5.3 |  0.000 % |
c ==============================================================================
c [1mFound solution: 210[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        59 |   29396    69141 |    9798      58      792    13.7 |  0.000 % |
c |       159 |   29373    69094 |   10777     157     5757    36.7 |  0.383 % |
c |       309 |   29326    68997 |   11855     305    12018    39.4 |  0.516 % |
c |       534 |   28837    67952 |   13041     517    17976    34.8 |  1.995 % |
c ==============================================================================
c [1mFound solution: 204[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       621 |   28880    68089 |    9626     588    18176    30.9 |  1.995 % |
c |       721 |   28880    68089 |   10588     688    22308    32.4 |  2.200 % |
c |       871 |   28524    67303 |   11647     827    25164    30.4 |  3.340 % |
c |      1097 |   28524    67303 |   12812    1053    42619    40.5 |  3.340 % |
c |      1435 |   28524    67303 |   14093    1391    53572    38.5 |  3.340 % |
c ==============================================================================
c [1mFound solution: 199[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1910 |   28602    67526 |    9534    1866    63598    34.1 |  3.340 % |
c |      2010 |   28318    66912 |   10487    1959    66161    33.8 |  4.209 % |
c |      2161 |   28233    66721 |   11536    2108    68666    32.6 |  4.489 % |
c |      2387 |   28233    66721 |   12689    2334    80278    34.4 |  4.489 % |
c |      2726 |   28092    66412 |   13958    2670    97944    36.7 |  4.933 % |
c |      3232 |   27650    65426 |   15354    3164   139189    44.0 |  6.371 % |
c |      3992 |   27650    65426 |   16890    3924   180674    46.0 |  6.371 % |
c |      5136 |   27551    65211 |   18579    5065   211969    41.8 |  6.673 % |
c ==============================================================================
c [1mFound solution: 192[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6518 |   27558    65253 |    9186    6436   265899    41.3 |  6.673 % |
c |      6619 |   27519    65166 |   10104    6536   269336    41.2 |  7.104 % |
c |      6769 |   27415    64938 |   11115    6684   274644    41.1 |  7.431 % |
c |      6994 |   27379    64854 |   12226    6897   277613    40.3 |  7.557 % |
c |      7331 |   27379    64854 |   13449    7234   295109    40.8 |  7.557 % |
c |      7838 |   27325    64734 |   14794    7535   302474    40.1 |  7.721 % |
c |      8597 |   27274    64621 |   16273    8293   341703    41.2 |  7.884 % |
c |      9736 |   27274    64621 |   17900    9432   369370    39.2 |  7.884 % |
c |     11444 |   27232    64533 |   19691   11138   486622    43.7 |  8.005 % |
c |     14007 |   27151    64356 |   21660   13694   628930    45.9 |  8.253 % |
c |     17851 |   27151    64356 |   23826   17538   912902    52.1 |  8.253 % |
c |     23619 |   27118    64281 |   26208   23271  1310002    56.3 |  8.364 % |
c |     32268 |   27118    64281 |   28829   16325   870814    53.3 |  8.364 % |
c |     45244 |   27118    64281 |   31712   29301  1724772    58.9 |  8.364 % |
c |     64705 |   27024    64061 |   34883   29562  1535665    51.9 |  8.696 % |
c |     93897 |   27024    64061 |   38372   36552  1736312    47.5 |  8.696 % |
c |    137686 |   27024    64061 |   42209   32006  1723902    53.9 |  8.696 % |
c |    203370 |   26915    63818 |   46430   41295  2182791    52.9 |  9.043 % |
c |    301896 |   26810    63575 |   51073   47594  2455983    51.6 |  9.407 % |
/oldhome/oroussel/solvers/minisat+_script: line 9:  8830 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.83 2/54 8826
Raw data (stat): 8826 (runsolver) R 8825 15547 15546 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 795233923 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0005 s]
Raw data (loadavg): 0.93 0.95 0.83 2/55 8830
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.0008 s]
Raw data (loadavg): 0.94 0.96 0.83 2/55 8830
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.001 s]
Raw data (loadavg): 0.95 0.96 0.83 2/55 8830
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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+40.001 s]
Raw data (loadavg): 0.95 0.96 0.83 2/55 8830
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.0014 s]
Raw data (loadavg): 0.96 0.96 0.83 2/55 8830
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.001 s]
Raw data (loadavg): 0.97 0.96 0.83 2/55 8830
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.0006 s]
Raw data (loadavg): 0.97 0.96 0.84 2/55 8830
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.0011 s]
Raw data (loadavg): 0.98 0.96 0.84 2/55 8830
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.0004 s]
Raw data (loadavg): 0.98 0.96 0.84 2/55 8830
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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 s]
Raw data (loadavg): 0.98 0.96 0.84 2/55 8830
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.001 s]
Raw data (loadavg): 0.98 0.96 0.84 2/55 8830
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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 s]
Raw data (loadavg): 0.99 0.97 0.84 2/55 8830
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.001 s]
Raw data (loadavg): 0.99 0.97 0.84 2/55 8830
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.001 s]
Raw data (loadavg): 0.99 0.97 0.84 2/55 8830
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.001 s]
Raw data (loadavg): 0.99 0.97 0.84 2/55 8830
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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 s]
Raw data (loadavg): 0.99 0.97 0.84 2/55 8830
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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 s]
Raw data (loadavg): 0.99 0.97 0.85 2/55 8830
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.001 s]
Raw data (loadavg): 0.99 0.97 0.85 2/55 8830
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.001 s]
Raw data (loadavg): 0.99 0.97 0.85 2/55 8830
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.001 s]
Raw data (loadavg): 0.99 0.97 0.85 2/55 8830
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.001 s]
Raw data (loadavg): 0.99 0.97 0.85 2/55 8830
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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 s]
Raw data (loadavg): 0.99 0.97 0.85 2/55 8830
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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 s]
Raw data (loadavg): 0.99 0.97 0.85 2/55 8830
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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 s]
Raw data (loadavg): 0.99 0.97 0.85 2/55 8830
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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 s]
Raw data (loadavg): 0.99 0.97 0.85 2/55 8830
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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+259.999 s]
Raw data (loadavg): 0.99 0.97 0.85 2/55 8830
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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+269.999 s]
Raw data (loadavg): 0.99 0.97 0.86 2/55 8830
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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+279.999 s]
Raw data (loadavg): 0.99 0.97 0.86 2/55 8830
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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+289.999 s]
Raw data (loadavg): 0.99 0.97 0.86 2/55 8830
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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 s]
Raw data (loadavg): 0.99 0.97 0.86 2/55 8830
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.131 s]
Raw data (loadavg): 0.99 0.97 0.86 3/58 8866
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.156 s]
Raw data (loadavg): 1.07 0.99 0.87 2/57 8878
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.157 s]
Raw data (loadavg): 1.20 1.02 0.88 2/55 8883
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.156 s]
Raw data (loadavg): 1.17 1.02 0.88 2/55 8883
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.155 s]
Raw data (loadavg): 1.15 1.02 0.88 2/55 8883
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.156 s]
Raw data (loadavg): 1.12 1.02 0.88 2/55 8883
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.155 s]
Raw data (loadavg): 1.10 1.02 0.88 2/55 8883
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.154 s]
Raw data (loadavg): 1.09 1.02 0.88 2/55 8883
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.154 s]
Raw data (loadavg): 1.07 1.01 0.88 2/55 8883
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.154 s]
Raw data (loadavg): 1.06 1.01 0.88 2/55 8885
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.154 s]
Raw data (loadavg): 1.05 1.01 0.89 2/55 8885
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.154 s]
Raw data (loadavg): 1.04 1.01 0.89 2/55 8885
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.154 s]
Raw data (loadavg): 1.04 1.01 0.89 2/55 8885
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.154 s]
Raw data (loadavg): 1.03 1.01 0.89 2/55 8885
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.154 s]
Raw data (loadavg): 1.02 1.01 0.89 2/55 8885
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.153 s]
Raw data (loadavg): 1.02 1.01 0.89 2/55 8885
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.152 s]
Raw data (loadavg): 1.02 1.01 0.89 2/55 8885
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.153 s]
Raw data (loadavg): 1.01 1.01 0.89 2/55 8885
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.153 s]
Raw data (loadavg): 1.01 1.00 0.89 2/55 8885
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.153 s]
Raw data (loadavg): 1.01 1.00 0.89 2/55 8885
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.153 s]
Raw data (loadavg): 1.01 1.00 0.89 2/55 8885
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.152 s]
Raw data (loadavg): 1.01 1.00 0.90 2/55 8885
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.152 s]
Raw data (loadavg): 1.00 1.00 0.90 2/55 8885
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.152 s]
Raw data (loadavg): 1.00 1.00 0.90 2/55 8885
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.152 s]
Raw data (loadavg): 1.00 1.00 0.90 2/55 8885
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.152 s]
Raw data (loadavg): 1.00 1.00 0.90 2/55 8885
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.152 s]
Raw data (loadavg): 1.00 1.00 0.90 2/55 8885
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.152 s]
Raw data (loadavg): 1.00 1.00 0.90 2/55 8885
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.151 s]
Raw data (loadavg): 1.00 1.00 0.90 2/55 8885
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.153 s]
Raw data (loadavg): 1.00 1.00 0.90 2/55 8885
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.153 s]
Raw data (loadavg): 1.00 1.00 0.90 2/55 8885
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.152 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 8885
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.152 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 8885
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.152 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 8887
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.153 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 8887
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.153 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 8887
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.152 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 8887
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.153 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 8887
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.153 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 8887
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.153 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 8887
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.153 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 8887
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.154 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 8887
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.154 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 8887
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.154 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 8887
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.154 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 8887
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.154 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 8887
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.153 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 8887
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.154 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 8887
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.154 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 8887
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.154 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 8887
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.153 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 8887
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.153 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 8887
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.154 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 8887
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.154 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 8887
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.154 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 8887
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.155 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 8887
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.154 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 8887
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.154 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 8887
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.154 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 8887
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.155 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 8887
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.155 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 8887
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.154 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 8887
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.154 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 8887
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.154 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 8887
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.155 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 8887
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.156 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 8887
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.155 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 8887
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.156 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 8887
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.156 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 8887
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.16 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 8887
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.16 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 8887
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.16 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 8887
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.16 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 8887
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.16 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 8887
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.16 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 8887
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.16 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 8887
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.16 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 8887
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.16 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 8887
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.16 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 8887
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.16 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 8887
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.16 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 8887
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.16 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 8887
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.16 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 8887
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.16 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 8887
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.16 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 8887
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.16 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 8887
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.16 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 8887
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.16 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 8887
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.16 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 8887
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.16 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 8887
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.16 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 8887
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.16 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 8887
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.67 s]
Raw data (loadavg): 1.00 1.00 0.91 1/53 8887
Raw data (stat): 8826 (minisat+_script) S 8825 15547 15546 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795233923 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.67
CPU time (s): 1229.84
CPU user time (s): 1229.63
CPU system time (s): 0.216967
CPU usage (%): 100.014
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####