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-ii8b1.opb
MD5SUM	812314147c77e28d5e428080c7a2412d
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	672
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	672
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	672
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.03684
Number of variables	672
Total number of constraints	2404
Number of constraints which are clauses	2404
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 31576

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc23 THE 2005-05-27 04:55:15 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=22921 boxname=wulflinc23 idbench=167 idsolver=16 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  812314147c77e28d5e428080c7a2412d  /oldhome/oroussel/tmp/wulflinc23/normalized-ii8b1.opb
REAL COMMAND:  minisat+_script -cb -gs /oldhome/oroussel/tmp/wulflinc23/normalized-ii8b1.opb
IDLAUNCH: 22921
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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:        458252 kB
Buffers:         33824 kB
Cached:         521068 kB
SwapCached:        532 kB
Active:          51796 kB
Inactive:       505444 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        458000 kB
SwapTotal:     2097136 kB
SwapFree:      2096016 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5636 kB
Slab:            13572 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-27 05:15:45 (client local time) WITH STATUS 152 IN 1229.85 SECONDS
stats: 22921 7 1229.85 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 2404 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 |    2404     5328 |     801       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 224[0m
c ---[   0]---> Sorter-cost:30564     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         2 |   39371    91691 |   13123       2       14     7.0 |  0.000 % |
c |       102 |   39094    91112 |   14435      93     3903    42.0 |  0.670 % |
c |       252 |   39002    90914 |   15878     240     6701    27.9 |  0.882 % |
c |       477 |   38987    90884 |   17466     464    15942    34.4 |  0.910 % |
c |       815 |   37805    88284 |   19213     776    24356    31.4 |  3.726 % |
c |      1322 |   37260    87073 |   21134    1269    45788    36.1 |  5.055 % |
c |      2082 |   37129    86792 |   23248    2027    71701    35.4 |  5.354 % |
c |      3223 |   37060    86641 |   25573    3166   105927    33.5 |  5.514 % |
c |      4933 |   36659    85752 |   28130    4825   171835    35.6 |  6.479 % |
c ==============================================================================
c [1mFound solution: 213[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5130 |   36761    86021 |   12253    5022   174707    34.8 |  6.479 % |
c |      5230 |   36692    85868 |   13478    5120   176718    34.5 |  6.749 % |
c |      5381 |   36692    85868 |   14826    5271   182366    34.6 |  6.749 % |
c |      5606 |   36692    85868 |   16308    5496   187885    34.2 |  6.749 % |
c |      5944 |   36590    85644 |   17939    5831   206859    35.5 |  6.987 % |
c |      6450 |   36554    85568 |   19733    6324   229508    36.3 |  7.063 % |
c |      7209 |   36479    85399 |   21706    7081   256581    36.2 |  7.249 % |
c |      8348 |   36479    85399 |   23877    8220   321429    39.1 |  7.249 % |
c ==============================================================================
c [1mFound solution: 212[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8492 |   36455    85340 |   12151    8328   322244    38.7 |  7.249 % |
c |      8592 |   36412    85243 |   13366    8427   325487    38.6 |  7.439 % |
c |      8742 |   36412    85243 |   14702    8577   331063    38.6 |  7.440 % |
c ==============================================================================
c [1mFound solution: 191[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8825 |   36570    85630 |   12190    8660   333479    38.5 |  7.440 % |
c |      8925 |   36570    85630 |   13409    8760   336090    38.4 |  7.604 % |
c |      9075 |   36570    85630 |   14749    8910   343099    38.5 |  7.604 % |
c |      9301 |   36570    85630 |   16224    9136   351679    38.5 |  7.605 % |
c |      9638 |   36570    85630 |   17847    9473   362266    38.2 |  7.604 % |
c |     10144 |   36472    85414 |   19632    9977   379563    38.0 |  7.834 % |
c |     10905 |   36472    85414 |   21595   10738   407634    38.0 |  7.834 % |
c |     12044 |   36472    85414 |   23754   11877   468101    39.4 |  7.834 % |
c |     13754 |   36472    85414 |   26130   13587   522596    38.5 |  7.834 % |
c |     16317 |   36470    85410 |   28743   16149   629422    39.0 |  7.838 % |
c |     20161 |   36426    85316 |   31617   19992   838045    41.9 |  7.936 % |
c |     25927 |   36382    85218 |   34779   25757  1118768    43.4 |  8.043 % |
c |     34576 |   36305    85037 |   38257   34348  1535481    44.7 |  8.244 % |
c |     47550 |   36181    84771 |   42083   21274   996051    46.8 |  8.517 % |
c |     67011 |   36135    84671 |   46291   40732  1888951    46.4 |  8.624 % |
c |     96203 |   36135    84671 |   50920   35083  1330080    37.9 |  8.624 % |
c |    139993 |   36085    84561 |   56012   42013  1861233    44.3 |  8.742 % |
c |    205677 |   36085    84561 |   61613   20830   839310    40.3 |  8.742 % |
c |    304203 |   36085    84561 |   67775   23016   997862    43.4 |  8.742 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 27119 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.88 2/54 27115
Raw data (stat): 27115 (runsolver) R 27114 5562 5561 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 853445635 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.0001 s]
Raw data (loadavg): 0.93 0.95 0.88 2/55 27119
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+19.9995 s]
Raw data (loadavg): 0.94 0.96 0.88 2/55 27119
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.0007 s]
Raw data (loadavg): 0.95 0.96 0.88 2/55 27119
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.0011 s]
Raw data (loadavg): 0.95 0.96 0.88 2/55 27119
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0015 s]
Raw data (loadavg): 0.96 0.96 0.88 2/55 27119
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.0015 s]
Raw data (loadavg): 0.97 0.96 0.88 2/55 27119
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.0012 s]
Raw data (loadavg): 0.97 0.96 0.89 2/55 27119
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.0016 s]
Raw data (loadavg): 0.98 0.96 0.89 2/55 27119
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.0016 s]
Raw data (loadavg): 0.98 0.96 0.89 2/55 27119
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.002 s]
Raw data (loadavg): 0.98 0.96 0.89 2/55 27119
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.003 s]
Raw data (loadavg): 0.98 0.96 0.89 2/55 27119
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.003 s]
Raw data (loadavg): 0.99 0.97 0.89 2/55 27119
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.003 s]
Raw data (loadavg): 0.99 0.97 0.89 2/55 27119
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.003 s]
Raw data (loadavg): 0.99 0.97 0.89 2/55 27119
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.004 s]
Raw data (loadavg): 0.99 0.97 0.89 2/55 27119
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.003 s]
Raw data (loadavg): 0.99 0.97 0.89 2/55 27119
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.003 s]
Raw data (loadavg): 0.99 0.97 0.90 2/55 27119
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.003 s]
Raw data (loadavg): 0.99 0.97 0.90 2/55 27119
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.002 s]
Raw data (loadavg): 0.99 0.97 0.90 2/55 27119
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.003 s]
Raw data (loadavg): 0.99 0.97 0.90 2/55 27119
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.003 s]
Raw data (loadavg): 0.99 0.97 0.90 2/55 27119
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.003 s]
Raw data (loadavg): 0.99 0.97 0.90 2/55 27119
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.003 s]
Raw data (loadavg): 0.99 0.97 0.90 2/55 27119
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.003 s]
Raw data (loadavg): 0.99 0.97 0.90 2/55 27119
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.004 s]
Raw data (loadavg): 0.99 0.97 0.90 2/55 27119
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.004 s]
Raw data (loadavg): 0.99 0.97 0.90 2/55 27119
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27119
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27119
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 27120
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.131 s]
Raw data (loadavg): 1.23 1.02 0.92 2/55 27172
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.13 s]
Raw data (loadavg): 1.19 1.02 0.92 2/55 27172
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.13 s]
Raw data (loadavg): 1.16 1.02 0.92 2/55 27172
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330.132 s]
Raw data (loadavg): 1.14 1.02 0.92 2/55 27172
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340.132 s]
Raw data (loadavg): 1.12 1.02 0.92 2/55 27172
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+350.132 s]
Raw data (loadavg): 1.10 1.02 0.92 2/55 27172
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+360.133 s]
Raw data (loadavg): 1.08 1.01 0.92 2/55 27174
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+370.133 s]
Raw data (loadavg): 1.07 1.01 0.92 2/55 27174
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380.133 s]
Raw data (loadavg): 1.06 1.01 0.92 2/55 27174
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+390.132 s]
Raw data (loadavg): 1.05 1.01 0.92 2/55 27174
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+400.133 s]
Raw data (loadavg): 1.04 1.01 0.92 2/55 27174
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+410.132 s]
Raw data (loadavg): 1.03 1.01 0.92 2/55 27174
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+420.132 s]
Raw data (loadavg): 1.03 1.01 0.92 2/55 27174
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+430.133 s]
Raw data (loadavg): 1.02 1.01 0.92 2/55 27174
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+440.133 s]
Raw data (loadavg): 1.02 1.01 0.92 2/55 27174
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+450.133 s]
Raw data (loadavg): 1.02 1.01 0.92 2/55 27174
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+460.133 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 27174
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.132 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 27174
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.132 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 27174
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+490.132 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 27174
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+500.133 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27174
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+510.132 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27174
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+520.132 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27174
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+530.131 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27174
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+540.131 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27174
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+550.132 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27174
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+560.132 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27174
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+570.131 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27174
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+580.132 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27174
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+590.131 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27174
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+600.132 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27174
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+610.133 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27176
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+620.133 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27176
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+630.134 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27176
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+640.134 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27176
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+650.135 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27176
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+660.134 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27176
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+670.134 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27176
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+680.135 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27176
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+690.135 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27176
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+700.135 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27176
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+710.135 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27176
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+720.135 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27176
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+730.136 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27176
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+740.136 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27176
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+750.136 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27176
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+760.137 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27176
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+770.136 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27176
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+780.137 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27176
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+790.137 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27176
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+800.138 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27176
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+810.137 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27176
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+820.137 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27176
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+830.137 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27176
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+840.137 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27176
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+850.138 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27176
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+860.139 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27176
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+870.138 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27176
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+880.139 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27176
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+890.139 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27176
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+900.14 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27176
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+910.14 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27176
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+920.139 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27176
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+930.14 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27176
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+940.14 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27176
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+950.14 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27176
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+960.14 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27176
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+970.14 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27176
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+980.14 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27176
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+990.141 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27176
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1000.14 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27176
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1010.14 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27176
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1020.14 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27176
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1030.14 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27176
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1040.14 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27176
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1050.14 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27176
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1060.14 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27176
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1070.14 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27176
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1080.14 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27176
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1090.14 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27176
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1100.14 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27176
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1110.14 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27176
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1120.14 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27176
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1130.14 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27176
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1140.14 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27176
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1150.14 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27176
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1160.15 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27176
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1170.14 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27176
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1180.15 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27176
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1190.14 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27176
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1200.14 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27176
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1210.15 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27176
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1220.15 s]
Raw data (loadavg): 1.00 1.00 0.92 2/55 27176
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1229.72 s]
Raw data (loadavg): 1.00 1.00 0.92 1/53 27176
Raw data (stat): 27115 (minisat+_script) S 27114 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853445635 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

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