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/logic-synthesis/normalized-alu4.b.opb
MD5SUM	db06e7fbd4f70a4af68f8f196fdb3636
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	50
Optimality of the best value was proved	NO
Number of terms in the objective function	808
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	808
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	808
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.03884
Number of variables	807
Total number of constraints	1838
Number of constraints which are clauses	1823
Number of constraints which are cardinality constraints (but not clauses)	15
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	98
Trace number 6163

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc24 THE 2005-04-14 03:36:40 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4573 boxname=wulflinc24 idbench=61 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  db06e7fbd4f70a4af68f8f196fdb3636  /oldhome/oroussel/tmp/wulflinc24/normalized-alu4.b.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc24/normalized-alu4.b.opb /oldhome/oroussel/tmp/wulflinc24/normalized-alu4.b.opb
IDLAUNCH: 4573
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.080
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.080
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:        832740 kB
Buffers:         35260 kB
Cached:         124112 kB
SwapCached:       3828 kB
Active:          55428 kB
Inactive:       110636 kB
HighTotal:      131008 kB
HighFree:         4620 kB
LowTotal:       903652 kB
LowFree:        828120 kB
SwapTotal:     2097892 kB
SwapFree:      2094064 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            30416 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 03:56:42 (client local time) WITH STATUS 10 IN 1200.19 SECONDS
stats: 4573 7 1200.19 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1695 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 |    1694    35961 |     564       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 68[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:36470     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   82462   225006 |   27487       0        0     nan |  0.000 % |
c |       100 |   82462   225006 |   30235     100      743     7.4 |  0.482 % |
c |       250 |   82447   224973 |   33259     249     1749     7.0 |  0.497 % |
c |       477 |   82370   224791 |   36585     473     3950     8.4 |  0.558 % |
c |       814 |   82370   224791 |   40243     810     6685     8.3 |  0.558 % |
c |      1320 |   82133   224244 |   44268    1309    10464     8.0 |  0.790 % |
c |      2079 |   81938   223805 |   48694    1866    22320    12.0 |  0.979 % |
c |      3218 |   81907   223735 |   53564    3000    36696    12.2 |  1.011 % |
c |      4926 |   81545   222920 |   58920    4700    66916    14.2 |  1.392 % |
c |      7488 |   81545   222920 |   64812    7262   259551    35.7 |  1.392 % |
c |     11333 |   81088   221880 |   71294   10926   314340    28.8 |  1.834 % |
c |     17099 |   81088   221880 |   78423   16692   422571    25.3 |  1.834 % |
c ==============================================================================
c [1mFound solution: 67[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20249 |   81123   221969 |   27041   19842   528276    26.6 |  1.834 % |
c |     20351 |   81123   221969 |   29745   19944   529041    26.5 |  1.841 % |
c |     20502 |   81123   221969 |   32719   20095   530525    26.4 |  1.841 % |
c |     20727 |   81123   221969 |   35991   20320   534578    26.3 |  1.841 % |
c |     21064 |   81123   221969 |   39590   20657   545854    26.4 |  1.841 % |
c |     21570 |   81123   221969 |   43549   21163   559365    26.4 |  1.841 % |
c |     22329 |   81123   221969 |   47904   21922   572216    26.1 |  1.841 % |
c ==============================================================================
c [1mFound solution: 66[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     23044 |   81088   221879 |   27029   22637   594694    26.3 |  1.841 % |
c |     23144 |   81088   221879 |   29731   22737   597667    26.3 |  1.888 % |
c |     23296 |   81088   221879 |   32705   22889   599238    26.2 |  1.888 % |
c |     23522 |   81077   221855 |   35975   23113   601662    26.0 |  1.899 % |
c |     23860 |   81077   221855 |   39573   23451   605151    25.8 |  1.899 % |
c |     24368 |   81071   221827 |   43530   23951   610843    25.5 |  1.906 % |
c |     25128 |   81071   221827 |   47883   24711   624841    25.3 |  1.906 % |
c |     26267 |   81071   221827 |   52671   25850   637222    24.7 |  1.906 % |
c |     27975 |   81071   221827 |   57939   27558   659807    23.9 |  1.906 % |
c |     30537 |   81071   221827 |   63732   30120   729368    24.2 |  1.906 % |
c |     34381 |   80927   221504 |   70106   33959   891354    26.2 |  2.047 % |
c |     40147 |   80910   221470 |   77116   39722  1045628    26.3 |  2.051 % |
c ==============================================================================
c [1mFound solution: 58[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     41718 |   80950   221573 |   26983   41249  1151442    27.9 |  2.051 % |
c |     41821 |   80950   221573 |   29681   18389   470446    25.6 |  2.132 % |
c |     41972 |   80950   221573 |   32649   18540   472825    25.5 |  2.132 % |
c |     42201 |   80950   221573 |   35914   18769   474725    25.3 |  2.132 % |
c |     42539 |   80608   220797 |   39505   19048   480461    25.2 |  2.486 % |
c |     43045 |   80608   220797 |   43456   19554   492419    25.2 |  2.486 % |
c ==============================================================================
c [1mFound solution: 57[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     43178 |   80645   220890 |   26881   19687   496624    25.2 |  2.486 % |
c |     43278 |   80645   220890 |   29569   19787   497956    25.2 |  2.492 % |
c |     43428 |   80645   220890 |   32526   19937   498807    25.0 |  2.493 % |
c |     43654 |   80636   220870 |   35778   20159   504287    25.0 |  2.503 % |
c |     43991 |   80636   220870 |   39356   20496   510979    24.9 |  2.503 % |
c |     44498 |   80636   220870 |   43292   21003   518062    24.7 |  2.503 % |
c |     45260 |   80636   220870 |   47621   21765   531044    24.4 |  2.503 % |
c |     46399 |   80636   220870 |   52383   22904   567937    24.8 |  2.503 % |
c |     48107 |   80254   220000 |   57621   24284   622163    25.6 |  2.879 % |
c |     50670 |   80174   219816 |   63383   26845   666782    24.8 |  2.974 % |
c |     54514 |   80120   219693 |   69722   30684   782617    25.5 |  3.035 % |
c ==============================================================================
c [1mFound solution: 56[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     55579 |   72135   201405 |   24045   30743   789054    25.7 |  3.035 % |
c |     55680 |   72078   201276 |   26449   15470   274337    17.7 | 11.781 % |
c |     55831 |   72043   201196 |   29094   15619   275844    17.7 | 11.821 % |
c |     56056 |   72043   201196 |   32003   15844   279304    17.6 | 11.822 % |
c |     56395 |   72043   201196 |   35204   16183   297165    18.4 | 11.821 % |
c |     56903 |   71994   201086 |   38724   16683   306693    18.4 | 11.868 % |
c |     57666 |   71994   201086 |   42597   17446   317630    18.2 | 11.869 % |
c |     58805 |   71941   200962 |   46856   18584   352123    18.9 | 11.926 % |
c |     60515 |   71941   200962 |   51542   20294   428604    21.1 | 11.926 % |
c |     63077 |   71941   200962 |   56696   22856   535845    23.4 | 11.926 % |
c ==============================================================================
c [1mFound solution: 55[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     66130 |   71928   200940 |   23976   25907   809862    31.3 | 11.926 % |
c |     66231 |   71928   200940 |   26373   26008   812309    31.2 | 11.972 % |
c |     66381 |   71928   200940 |   29010   26158   820163    31.4 | 11.972 % |
c |     66607 |   71243   199367 |   31912   26336   821483    31.2 | 12.735 % |
c |     66948 |   71243   199367 |   35103   26677   827225    31.0 | 12.735 % |
c |     67454 |   71243   199367 |   38613   27183   851242    31.3 | 12.735 % |
c |     68213 |   71243   199367 |   42474   27942   879476    31.5 | 12.735 % |
c |     69352 |   71243   199367 |   46722   29081   917602    31.6 | 12.735 % |
c |     71060 |   71209   199289 |   51394   30788  1046936    34.0 | 12.774 % |
c |     73622 |   71209   199289 |   56534   33350  1462629    43.9 | 12.774 % |
c |     77466 |   71209   199289 |   62187   37194  1712638    46.0 | 12.774 % |
c |     83233 |   71209   199289 |   68406   42961  2118332    49.3 | 12.774 % |
c |     91882 |   71143   199136 |   75246   51608  2792090    54.1 | 12.858 % |
c |    104856 |   71068   198966 |   82771   64579  3926836    60.8 | 12.937 % |
c |    124317 |   71068   198966 |   91048   84040  5575743    66.3 | 12.937 % |
c |    153511 |   71068   198966 |  100153  113234  8095781    71.5 | 12.937 % |
c ==============================================================================
c [1mFound solution: 54[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    164612 |   70962   198709 |   23654   31289  2133849    68.2 | 12.937 % |
c |    164713 |   70962   198709 |   26019   15746   584300    37.1 | 13.059 % |
c |    164863 |   70962   198709 |   28621   15896   588313    37.0 | 13.059 % |
c |    165088 |   70962   198709 |   31483   16121   593199    36.8 | 13.059 % |
c |    165427 |   70962   198709 |   34631   16460   616810    37.5 | 13.059 % |
c |    165934 |   70962   198709 |   38095   16967   642740    37.9 | 13.059 % |
c |    166695 |   70962   198709 |   41904   17728   698441    39.4 | 13.059 % |
c |    167835 |   70962   198709 |   46094   18868   755439    40.0 | 13.059 % |
c |    169547 |   70962   198709 |   50704   20580   810845    39.4 | 13.059 % |
c |    172111 |   70962   198709 |   55774   23144   908728    39.3 | 13.059 % |
c |    175955 |   70622   197931 |   61352   26977  1047836    38.8 | 13.435 % |
c |    181721 |   70622   197931 |   67487   32743  1866942    57.0 | 13.435 % |
c |    190375 |   67912   191653 |   74236   41338  2714774    65.7 | 16.595 % |
c ==============================================================================
c [1mFound solution: 53[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    194454 |   67946   191737 |   22648   45417  3132242    69.0 | 16.595 % |
c |    194554 |   67880   191577 |   24912   19923  1271742    63.8 | 16.678 % |
c |    194706 |   67880   191577 |   27404   20075  1283339    63.9 | 16.678 % |
c |    194935 |   67880   191577 |   30144   20304  1292508    63.7 | 16.678 % |
c |    195272 |   67880   191577 |   33158   20641  1306109    63.3 | 16.678 % |
c |    195781 |   67880   191577 |   36474   21150  1340480    63.4 | 16.678 % |
c |    196543 |   67880   191577 |   40122   21912  1364099    62.3 | 16.678 % |
c |    197682 |   67880   191577 |   44134   23051  1402798    60.9 | 16.678 % |
c |    199391 |   67880   191577 |   48547   24760  1484413    60.0 | 16.678 % |
c |    201955 |   67880   191577 |   53402   27324  1590777    58.2 | 16.678 % |
c |    205799 |   67880   191577 |   58743   31168  1908092    61.2 | 16.678 % |
c |    211569 |   67877   191571 |   64617   36937  2373035    64.2 | 16.682 % |
c |    220218 |   67877   191571 |   71079   45586  3013694    66.1 | 16.682 % |
c |    233193 |   67877   191571 |   78187   58561  4634541    79.1 | 16.682 % |
c |    252654 |   67815   191430 |   86005   78015  6039585    77.4 | 16.750 % |
c |    281847 |   67815   191430 |   94606   35602  2496912    70.1 | 16.750 % |
c |    325638 |   66379   188119 |  104066   79277  5577941    70.4 | 18.384 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -x1 -x2 -x3 -x4 -x5 -x6 -x7 -x8 -x9 -x10 -x11 -x12 -x13 -x14 -x15 -x16 -x17 -x18 -x19 -x20 -x21 -x22 -x23 x24 -x25 -x26 -x27 -x28 -x29 x30 -x31 -x32 -x33 -x34 -x35 -x36 -x37 x38 -x39 -x40 -x41 -x42 -x43 -x44 -x45 -x46 -x47 -x48 -x49 -x50 x51 -x52 -x53 -x54 -x55 -x56 -x57 -x58 -x59 -x60 -x61 -x62 -x63 -x64 -x65 -x66 -x67 -x68 -x69 -x70 -x71 -x72 -x73 -x74 -x75 -x76 -x77 -x78 -x79 -x80 -x81 -x82 -x83 -x84 -x85 -x86 -x87 -x88 -x89 x90 -x91 -x92 -x93 -x94 -x95 -x96 -x97 -x98 -x99 -x100 -x101 -x102 -x103 -x104 -x105 -x106 -x107 -x108 -x109 -x110 -x111 -x112 -x113 -x114 -x115 -x116 -x117 -x118 -x119 -x120 -x121 -x122 -x123 -x124 -x125 -x126 -x127 -x128 -x129 -x130 -x131 -x132 -x133 -x134 -x135 x136 -x137 -x138 -x139 -x140 -x141 -x142 -x143 -x144 -x145 -x146 -x147 -x148 -x149 -x150 -x151 -x152 -x153 -x154 -x155 -x156 -x157 -x158 x159 -x160 -x161 -x162 -x163 -x164 -x165 -x166 -x167 -x168 -x169 -x170 -x171 -x172 -x173 -x174 -x175 -x176 -x177 -x178 -x179 -x180 -x181 -x182 -x183 -x184 -x185 -x186 -x187 -x188 -x189 -x190 -x191 -x192 -x193 -x194 -x195 -x196 -x197 -x198 -x199 -x200 -x201 -x202 -x203 -x204 -x205 -x206 -x207 -x208 -x209 -x210 -x211 -x212 -x213 -x214 -x215 -x216 -x217 -x218 -x219 -x220 -x221 -x222 -x223 -x224 -x225 -x226 -x227 x228 -x229 -x230 -x231 -x232 -x233 -x234 -x235 -x236 -x237 -x238 -x239 -x240 x241 -x242 -x243 -x244 -x245 -x246 -x247 -x248 -x249 -x250 x251 -x252 -x253 -x254 -x255 -x256 -x257 -x258 -x259 -x260 -x261 -x262 -x263 -x264 -x265 -x266 -x267 -x268 -x269 -x270 -x271 -x272 -x273 -x274 -x275 -x276 -x277 -x278 -x279 -x280 -x281 -x282 -x283 -x284 -x285 -x286 -x287 -x288 -x289 -x290 -x291 -x292 -x293 -x294 -x295 -x296 -x297 x298 -x299 -x300 -x301 -x302 -x303 -x304 -x305 -x306 -x307 -x308 -x309 -x310 -x311 -x312 -x313 -x314 -x315 -x316 -x317 -x318 -x319 -x320 -x321 -x322 -x323 -x324 -x325 -x326 -x327 -x328 -x329 -x330 -x331 -x332 -x333 -x334 -x335 -x336 -x337 x338 -x339 -x340 -x341 -x342 -x343 -x344 -x345 -x346 -x347 -x348 -x349 -x350 -x351 -x352 -x353 -x354 -x355 -x356 -x357 -x358 -x359 -x360 -x361 -x362 -x363 -x364 -x365 -x366 -x367 -x368 -x369 -x370 -x371 -x372 -x373 -x374 -x375 -x376 -x377 -x378 -x379 -x380 -x381 -x382 -x383 -x384 -x385 -x386 -x387 -x388 -x389 -x390 x391 -x392 -x393 -x394 -x395 -x396 -x397 -x398 -x399 -x400 -x401 -x402 -x403 -x404 -x405 -x406 -x407 -x408 -x409 -x410 -x411 -x412 -x413 -x414 -x415 -x416 -x417 -x418 x419 -x420 -x421 -x422 -x423 -x424 -x425 -x426 -x427 -x428 -x429 -x430 -x431 -x432 -x433 -x434 -x435 -x436 -x437 -x438 -x439 -x440 -x441 -x442 -x443 -x444 -x445 -x446 -x447 x448 -x449 -x450 -x451 -x452 -x453 -x454 -x455 -x456 -x457 -x458 -x459 -x460 -x461 -x462 -x463 -x464 -x465 -x466 -x467 -x468 -x469 -x470 -x471 -x472 -x473 -x474 -x475 x476 -x477 -x478 -x479 -x480 x481 -x482 -x483 -x484 -x485 -x486 -x487 -x488 -x489 -x490 -x491 -x492 -x493 -x494 -x495 -x496 -x497 -x498 -x499 -x500 -x501 -x502 -x503 -x504 -x505 -x506 -x507 -x508 -x509 -x510 -x511 -x512 -x513 -x514 -x515 -x516 -x517 -x518 -x519 -x520 -x521 -x522 -x523 -x524 -x525 -x526 -x527 -x528 -x529 -x530 x531 -x532 -x533 -x534 -x535 -x536 -x537 -x538 -x539 -x540 -x541 -x542 -x543 -x544 -x545 -x546 -x547 -x548 -x549 -x550 -x551 x552 -x553 -x554 -x555 -x556 -x557 -x558 -x559 -x560 -x561 -x562 -x563 -x564 -x565 -x566 -x567 -x568 -x569 -x570 -x571 -x572 -x573 -x574 -x575 -x576 -x577 -x578 -x579 -x580 -x581 -x582 -x583 -x584 -x585 -x586 -x587 -x588 -x589 -x590 -x591 -x592 -x593 x594 -x595 x596 -x597 -x598 -x599 -x600 -x601 -x602 -x603 -x604 -x605 -x606 -x607 -x608 -x609 -x610 -x611 -x612 -x613 -x614 -x615 -x616 -x617 -x618 -x619 x620 -x621 x622 -x623 x624 -x625 -x626 -x627 -x628 x629 -x630 -x631 -x632 -x633 -x634 -x635 -x636 x637 x638 -x639 -x640 -x641 -x642 -x643 -x644 -x645 -x646 -x647 x648 -x649 x650 -x651 -x652 -x653 x654 -x655 -x656 -x657 -x658 -x659 -x660 -x661 x662 -x663 -x664 -x665 -x666 -x667 -x668 -x669 -x670 -x671 -x672 -x673 x674 x675 -x676 -x677 -x678 -x679 -x680 -x681 -x682 -x683 x684 -x685 -x686 -x687 -x688 -x689 -x690 -x691 -x692 -x693 -x694 x695 -x696 -x697 -x698 -x699 -x700#### 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.86 0.90 0.89 2/54 3428
Raw data (stat): 3428 (runsolver) R 3427 28546 28545 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481398142 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0009 s]
Raw data (loadavg): 0.88 0.91 0.89 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 2714 0 0 0 991 7 0 0 25 0 1 0 481398142 13500416 2684 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3296 2684 603 41 0 3255 0
vsize: 13184
[startup+20.0022 s]
Raw data (loadavg): 0.90 0.91 0.89 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 2940 0 0 0 1990 7 0 0 25 0 1 0 481398142 14323712 2910 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3497 2910 603 41 0 3456 0
vsize: 13988
[startup+30.0028 s]
Raw data (loadavg): 0.91 0.91 0.89 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 3079 0 0 0 2990 8 0 0 25 0 1 0 481398142 15007744 3049 4294967295 134512640 134672761 3221224576 3221223744 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3664 3049 603 41 0 3623 0
vsize: 14656
[startup+40.0027 s]
Raw data (loadavg): 0.92 0.91 0.89 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 3233 0 0 0 3989 8 0 0 25 0 1 0 481398142 15716352 3203 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3837 3203 603 41 0 3796 0
vsize: 15348
[startup+50.0033 s]
Raw data (loadavg): 0.94 0.92 0.89 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 3486 0 0 0 4989 8 0 0 25 0 1 0 481398142 16834560 3456 4294967295 134512640 134672761 3221224576 3221223744 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4110 3456 603 41 0 4069 0
vsize: 16440
[startup+60.0027 s]
Raw data (loadavg): 0.95 0.92 0.90 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 3607 0 0 0 5989 9 0 0 25 0 1 0 481398142 17289216 3577 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4221 3577 603 41 0 4180 0
vsize: 16884
[startup+70.0035 s]
Raw data (loadavg): 0.95 0.92 0.90 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 3781 0 0 0 6988 9 0 0 25 0 1 0 481398142 18096128 3751 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4418 3751 603 41 0 4377 0
vsize: 17672
[startup+80.0044 s]
Raw data (loadavg): 0.96 0.92 0.90 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 3950 0 0 0 7986 10 0 0 25 0 1 0 481398142 18890752 3920 4294967295 134512640 134672761 3221224576 3221223700 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4612 3920 603 41 0 4571 0
vsize: 18448
[startup+90.0038 s]
Raw data (loadavg): 0.97 0.92 0.90 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 4103 0 0 0 8986 11 0 0 25 0 1 0 481398142 19423232 4073 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4742 4073 603 41 0 4701 0
vsize: 18968
[startup+100.004 s]
Raw data (loadavg): 0.97 0.93 0.90 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 4261 0 0 0 9986 11 0 0 25 0 1 0 481398142 20070400 4231 4294967295 134512640 134672761 3221224576 3221223744 134560885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4900 4231 603 41 0 4859 0
vsize: 19600
[startup+110.004 s]
Raw data (loadavg): 0.97 0.93 0.90 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 4261 0 0 0 10986 11 0 0 25 0 1 0 481398142 20070400 4231 4294967295 134512640 134672761 3221224576 3221223712 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4900 4231 603 41 0 4859 0
vsize: 19600
[startup+120.004 s]
Raw data (loadavg): 0.98 0.93 0.90 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 4261 0 0 0 11986 11 0 0 25 0 1 0 481398142 20070400 4231 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4900 4231 603 41 0 4859 0
vsize: 19600
[startup+130.004 s]
Raw data (loadavg): 0.98 0.93 0.90 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 4261 0 0 0 12986 11 0 0 25 0 1 0 481398142 20070400 4231 4294967295 134512640 134672761 3221224576 3221223760 134559179 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4900 4231 603 41 0 4859 0
vsize: 19600
[startup+140.004 s]
Raw data (loadavg): 0.98 0.93 0.90 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 4261 0 0 0 13986 11 0 0 25 0 1 0 481398142 20070400 4231 4294967295 134512640 134672761 3221224576 3221223712 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4900 4231 603 41 0 4859 0
vsize: 19600
[startup+150.004 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 4261 0 0 0 14987 11 0 0 25 0 1 0 481398142 20070400 4231 4294967295 134512640 134672761 3221224576 3221223712 134565076 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4900 4231 603 41 0 4859 0
vsize: 19600
[startup+160.004 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 4263 0 0 0 15987 11 0 0 25 0 1 0 481398142 20070400 4233 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4900 4233 603 41 0 4859 0
vsize: 19600
[startup+170.005 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 4379 0 0 0 16987 12 0 0 25 0 1 0 481398142 20602880 4349 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5030 4349 603 41 0 4989 0
vsize: 20120
[startup+180.005 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 4870 0 0 0 17985 13 0 0 25 0 1 0 481398142 22622208 4840 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5523 4840 603 41 0 5482 0
vsize: 22092
[startup+190.005 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 5321 0 0 0 18984 14 0 0 25 0 1 0 481398142 24498176 5291 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5981 5291 603 41 0 5940 0
vsize: 23924
[startup+200.006 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 5539 0 0 0 19983 15 0 0 25 0 1 0 481398142 25309184 5509 4294967295 134512640 134672761 3221224576 3221223744 134561406 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6179 5509 603 41 0 6138 0
vsize: 24716
[startup+210.005 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 5734 0 0 0 20983 16 0 0 25 0 1 0 481398142 26116096 5704 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6376 5704 603 41 0 6335 0
vsize: 25504
[startup+220.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 6036 0 0 0 21983 16 0 0 25 0 1 0 481398142 27324416 6006 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6671 6006 603 41 0 6630 0
vsize: 26684
[startup+230.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 6348 0 0 0 22982 17 0 0 25 0 1 0 481398142 28659712 6318 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6997 6318 603 41 0 6956 0
vsize: 27988
[startup+240.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 6760 0 0 0 23980 19 0 0 25 0 1 0 481398142 30269440 6730 4294967295 134512640 134672761 3221224576 3221223760 134559498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7390 6730 603 41 0 7349 0
vsize: 29560
[startup+250.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 7000 0 0 0 24980 19 0 0 25 0 1 0 481398142 31207424 6970 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7619 6970 603 41 0 7578 0
vsize: 30476
[startup+260.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 7357 0 0 0 25979 21 0 0 25 0 1 0 481398142 32669696 7327 4294967295 134512640 134672761 3221224576 3221223576 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7976 7327 603 41 0 7935 0
vsize: 31904
[startup+270.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 7699 0 0 0 26979 21 0 0 25 0 1 0 481398142 34398208 7669 4294967295 134512640 134672761 3221224576 3221223744 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8398 7669 603 41 0 8357 0
vsize: 33592
[startup+280.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 7933 0 0 0 27978 22 0 0 25 0 1 0 481398142 35328000 7903 4294967295 134512640 134672761 3221224576 3221223744 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8625 7903 603 41 0 8584 0
vsize: 34500
[startup+290.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 8223 0 0 0 28978 23 0 0 25 0 1 0 481398142 36540416 8193 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8921 8193 603 41 0 8880 0
vsize: 35684
[startup+300.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 8539 0 0 0 29977 24 0 0 25 0 1 0 481398142 37744640 8509 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9215 8509 603 41 0 9174 0
vsize: 36860
[startup+310.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 8799 0 0 0 30976 24 0 0 25 0 1 0 481398142 38809600 8769 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9475 8769 603 41 0 9434 0
vsize: 37900
[startup+320.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 9037 0 0 0 31975 25 0 0 25 0 1 0 481398142 39747584 9007 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9704 9007 603 41 0 9663 0
vsize: 38816
[startup+330.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 9189 0 0 0 32976 25 0 0 25 0 1 0 481398142 40415232 9159 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9867 9159 603 41 0 9826 0
vsize: 39468
[startup+340.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 9272 0 0 0 33976 26 0 0 25 0 1 0 481398142 40812544 9242 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9964 9242 603 41 0 9923 0
vsize: 39856
[startup+350.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 9363 0 0 0 34976 26 0 0 25 0 1 0 481398142 41078784 9333 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10029 9333 603 41 0 9988 0
vsize: 40116
[startup+360.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 9456 0 0 0 35976 26 0 0 25 0 1 0 481398142 41476096 9426 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10126 9426 603 41 0 10085 0
vsize: 40504
[startup+370.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 9548 0 0 0 36975 27 0 0 25 0 1 0 481398142 41877504 9518 4294967295 134512640 134672761 3221224576 3221223744 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10224 9518 603 41 0 10183 0
vsize: 40896
[startup+380.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 9643 0 0 0 37975 27 0 0 25 0 1 0 481398142 42299392 9613 4294967295 134512640 134672761 3221224576 3221223680 134560252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10327 9613 603 41 0 10286 0
vsize: 41308
[startup+390.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 9847 0 0 0 38974 28 0 0 25 0 1 0 481398142 43098112 9817 4294967295 134512640 134672761 3221224576 3221223680 134560198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10522 9817 603 41 0 10481 0
vsize: 42088
[startup+400.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 10192 0 0 0 39973 29 0 0 25 0 1 0 481398142 44433408 10162 4294967295 134512640 134672761 3221224576 3221223744 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10848 10162 603 41 0 10807 0
vsize: 43392
[startup+410.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 10532 0 0 0 40972 30 0 0 25 0 1 0 481398142 45887488 10502 4294967295 134512640 134672761 3221224576 3221223744 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11203 10502 603 41 0 11162 0
vsize: 44812
[startup+420.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 10808 0 0 0 41972 31 0 0 25 0 1 0 481398142 46952448 10778 4294967295 134512640 134672761 3221224576 3221223712 134560703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11463 10778 603 41 0 11422 0
vsize: 45852
[startup+430.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 11081 0 0 0 42972 31 0 0 25 0 1 0 481398142 48156672 11051 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11757 11051 603 41 0 11716 0
vsize: 47028
[startup+440.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 11343 0 0 0 43972 31 0 0 25 0 1 0 481398142 49221632 11313 4294967295 134512640 134672761 3221224576 3221223728 134541817 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12017 11313 603 41 0 11976 0
vsize: 48068
[startup+450.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 11570 0 0 0 44971 32 0 0 25 0 1 0 481398142 50171904 11540 4294967295 134512640 134672761 3221224576 3221223680 134559955 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12249 11540 603 41 0 12208 0
vsize: 48996
[startup+460.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 11825 0 0 0 45971 33 0 0 25 0 1 0 481398142 51122176 11795 4294967295 134512640 134672761 3221224576 3221223744 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12481 11795 603 41 0 12440 0
vsize: 49924
[startup+470.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 11992 0 0 0 46970 33 0 0 25 0 1 0 481398142 51920896 11962 4294967295 134512640 134672761 3221224576 3221223776 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12676 11962 603 41 0 12635 0
vsize: 50704
[startup+480.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 11992 0 0 0 47970 33 0 0 25 0 1 0 481398142 51920896 11962 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12676 11962 603 41 0 12635 0
vsize: 50704
[startup+490.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 11992 0 0 0 48970 33 0 0 25 0 1 0 481398142 51920896 11962 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12676 11962 603 41 0 12635 0
vsize: 50704
[startup+500.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 11993 0 0 0 49970 34 0 0 25 0 1 0 481398142 51920896 11963 4294967295 134512640 134672761 3221224576 3221223744 134560813 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12676 11963 603 41 0 12635 0
vsize: 50704
[startup+510.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 11993 0 0 0 50970 34 0 0 25 0 1 0 481398142 51920896 11963 4294967295 134512640 134672761 3221224576 3221223744 134560842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12676 11963 603 41 0 12635 0
vsize: 50704
[startup+520.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 11993 0 0 0 51970 34 0 0 25 0 1 0 481398142 51920896 11963 4294967295 134512640 134672761 3221224576 3221223760 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12676 11963 603 41 0 12635 0
vsize: 50704
[startup+530.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 11993 0 0 0 52971 34 0 0 25 0 1 0 481398142 51920896 11963 4294967295 134512640 134672761 3221224576 3221223760 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12676 11963 603 41 0 12635 0
vsize: 50704
[startup+540.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 11993 0 0 0 53971 34 0 0 25 0 1 0 481398142 51920896 11963 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12676 11963 603 41 0 12635 0
vsize: 50704
[startup+550.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 11993 0 0 0 54971 34 0 0 25 0 1 0 481398142 51920896 11963 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12676 11963 603 41 0 12635 0
vsize: 50704
[startup+560.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 11993 0 0 0 55971 34 0 0 25 0 1 0 481398142 51920896 11963 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12676 11963 603 41 0 12635 0
vsize: 50704
[startup+570.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 11993 0 0 0 56971 34 0 0 25 0 1 0 481398142 51920896 11963 4294967295 134512640 134672761 3221224576 3221223720 134560555 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12676 11963 603 41 0 12635 0
vsize: 50704
[startup+580.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 11993 0 0 0 57971 34 0 0 25 0 1 0 481398142 51920896 11963 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12676 11963 603 41 0 12635 0
vsize: 50704
[startup+590.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 11993 0 0 0 58972 34 0 0 25 0 1 0 481398142 51920896 11963 4294967295 134512640 134672761 3221224576 3221223760 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12676 11963 603 41 0 12635 0
vsize: 50704
[startup+600.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 11993 0 0 0 59972 34 0 0 25 0 1 0 481398142 51920896 11963 4294967295 134512640 134672761 3221224576 3221223712 134560650 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12676 11963 603 41 0 12635 0
vsize: 50704
[startup+610.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 11993 0 0 0 60972 34 0 0 25 0 1 0 481398142 51920896 11963 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12676 11963 603 41 0 12635 0
vsize: 50704
[startup+620.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 11993 0 0 0 61972 34 0 0 25 0 1 0 481398142 51920896 11963 4294967295 134512640 134672761 3221224576 3221223776 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12676 11963 603 41 0 12635 0
vsize: 50704
[startup+630.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 11993 0 0 0 62972 34 0 0 25 0 1 0 481398142 51920896 11963 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12676 11963 603 41 0 12635 0
vsize: 50704
[startup+640.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 11993 0 0 0 63972 34 0 0 25 0 1 0 481398142 51920896 11963 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12676 11963 603 41 0 12635 0
vsize: 50704
[startup+650.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 11993 0 0 0 64972 34 0 0 25 0 1 0 481398142 51920896 11963 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12676 11963 603 41 0 12635 0
vsize: 50704
[startup+660.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 11993 0 0 0 65972 34 0 0 25 0 1 0 481398142 51920896 11963 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12676 11963 603 41 0 12635 0
vsize: 50704
[startup+670.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 11993 0 0 0 66973 34 0 0 25 0 1 0 481398142 51920896 11963 4294967295 134512640 134672761 3221224576 3221223776 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12676 11963 603 41 0 12635 0
vsize: 50704
[startup+680.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 11993 0 0 0 67973 34 0 0 25 0 1 0 481398142 51920896 11963 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12676 11963 603 41 0 12635 0
vsize: 50704
[startup+690.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 11993 0 0 0 68973 34 0 0 25 0 1 0 481398142 51920896 11963 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12676 11963 603 41 0 12635 0
vsize: 50704
[startup+700.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 11993 0 0 0 69973 34 0 0 25 0 1 0 481398142 51920896 11963 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12676 11963 603 41 0 12635 0
vsize: 50704
[startup+710.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 11993 0 0 0 70973 34 0 0 25 0 1 0 481398142 51920896 11963 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12676 11963 603 41 0 12635 0
vsize: 50704
[startup+720.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 11993 0 0 0 71973 34 0 0 25 0 1 0 481398142 51920896 11963 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12676 11963 603 41 0 12635 0
vsize: 50704
[startup+730.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 11993 0 0 0 72973 34 0 0 25 0 1 0 481398142 51920896 11963 4294967295 134512640 134672761 3221224576 3221223740 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12676 11963 603 41 0 12635 0
vsize: 50704
[startup+740.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 11993 0 0 0 73974 34 0 0 25 0 1 0 481398142 51920896 11963 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12676 11963 603 41 0 12635 0
vsize: 50704
[startup+750.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 11993 0 0 0 74974 34 0 0 25 0 1 0 481398142 51920896 11963 4294967295 134512640 134672761 3221224576 3221223712 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12676 11963 603 41 0 12635 0
vsize: 50704
[startup+760.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 11993 0 0 0 75974 34 0 0 25 0 1 0 481398142 51920896 11963 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12676 11963 603 41 0 12635 0
vsize: 50704
[startup+770.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 11993 0 0 0 76974 34 0 0 25 0 1 0 481398142 51920896 11963 4294967295 134512640 134672761 3221224576 3221223744 134560882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12676 11963 603 41 0 12635 0
vsize: 50704
[startup+780.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 11993 0 0 0 77974 34 0 0 25 0 1 0 481398142 51920896 11963 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12676 11963 603 41 0 12635 0
vsize: 50704
[startup+790.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 11994 0 0 0 78975 34 0 0 25 0 1 0 481398142 51920896 11964 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12676 11964 603 41 0 12635 0
vsize: 50704
[startup+800.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 11994 0 0 0 79975 34 0 0 25 0 1 0 481398142 51920896 11964 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12676 11964 603 41 0 12635 0
vsize: 50704
[startup+810.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 11994 0 0 0 80975 34 0 0 25 0 1 0 481398142 51920896 11964 4294967295 134512640 134672761 3221224576 3221223744 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12676 11964 603 41 0 12635 0
vsize: 50704
[startup+820.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 11994 0 0 0 81975 34 0 0 25 0 1 0 481398142 51920896 11964 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12676 11964 603 41 0 12635 0
vsize: 50704
[startup+830.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 11994 0 0 0 82975 34 0 0 25 0 1 0 481398142 51920896 11964 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12676 11964 603 41 0 12635 0
vsize: 50704
[startup+840.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 11994 0 0 0 83976 34 0 0 25 0 1 0 481398142 51920896 11964 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12676 11964 603 41 0 12635 0
vsize: 50704
[startup+850.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 11994 0 0 0 84976 34 0 0 25 0 1 0 481398142 51920896 11964 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12676 11964 603 41 0 12635 0
vsize: 50704
[startup+860.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 11994 0 0 0 85976 34 0 0 25 0 1 0 481398142 51920896 11964 4294967295 134512640 134672761 3221224576 3221223680 134554910 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12676 11964 603 41 0 12635 0
vsize: 50704
[startup+870.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 11994 0 0 0 86976 34 0 0 25 0 1 0 481398142 51920896 11964 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12676 11964 603 41 0 12635 0
vsize: 50704
[startup+880.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 11994 0 0 0 87976 34 0 0 25 0 1 0 481398142 51920896 11964 4294967295 134512640 134672761 3221224576 3221223760 134559356 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12676 11964 603 41 0 12635 0
vsize: 50704
[startup+890.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 11994 0 0 0 88976 34 0 0 25 0 1 0 481398142 51920896 11964 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12676 11964 603 41 0 12635 0
vsize: 50704
[startup+900.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 11994 0 0 0 89977 34 0 0 25 0 1 0 481398142 51920896 11964 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12676 11964 603 41 0 12635 0
vsize: 50704
[startup+910.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 11994 0 0 0 90977 34 0 0 25 0 1 0 481398142 51920896 11964 4294967295 134512640 134672761 3221224576 3221223680 134560169 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12676 11964 603 41 0 12635 0
vsize: 50704
[startup+920.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 11994 0 0 0 91977 34 0 0 25 0 1 0 481398142 51920896 11964 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12676 11964 603 41 0 12635 0
vsize: 50704
[startup+930.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 11994 0 0 0 92977 34 0 0 25 0 1 0 481398142 51920896 11964 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12676 11964 603 41 0 12635 0
vsize: 50704
[startup+940.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 11994 0 0 0 93977 34 0 0 25 0 1 0 481398142 51920896 11964 4294967295 134512640 134672761 3221224576 3221223760 134559031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12676 11964 603 41 0 12635 0
vsize: 50704
[startup+950.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 11994 0 0 0 94977 34 0 0 25 0 1 0 481398142 51920896 11964 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12676 11964 603 41 0 12635 0
vsize: 50704
[startup+960.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 11994 0 0 0 95978 34 0 0 25 0 1 0 481398142 51920896 11964 4294967295 134512640 134672761 3221224576 3221223744 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12676 11964 603 41 0 12635 0
vsize: 50704
[startup+970.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 11994 0 0 0 96978 34 0 0 25 0 1 0 481398142 51920896 11964 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12676 11964 603 41 0 12635 0
vsize: 50704
[startup+980.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 11994 0 0 0 97978 34 0 0 25 0 1 0 481398142 51920896 11964 4294967295 134512640 134672761 3221224576 3221223760 134559498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12676 11964 603 41 0 12635 0
vsize: 50704
[startup+990.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 11994 0 0 0 98978 34 0 0 25 0 1 0 481398142 51920896 11964 4294967295 134512640 134672761 3221224576 3221223744 134560888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12676 11964 603 41 0 12635 0
vsize: 50704
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 11994 0 0 0 99978 35 0 0 25 0 1 0 481398142 51920896 11964 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12676 11964 603 41 0 12635 0
vsize: 50704
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 11994 0 0 0 100978 35 0 0 25 0 1 0 481398142 51920896 11964 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12676 11964 603 41 0 12635 0
vsize: 50704
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 11994 0 0 0 101979 35 0 0 25 0 1 0 481398142 51920896 11964 4294967295 134512640 134672761 3221224576 3221223776 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12676 11964 603 41 0 12635 0
vsize: 50704
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 11994 0 0 0 102979 35 0 0 25 0 1 0 481398142 51920896 11964 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12676 11964 603 41 0 12635 0
vsize: 50704
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 11994 0 0 0 103979 35 0 0 25 0 1 0 481398142 51920896 11964 4294967295 134512640 134672761 3221224576 3221223712 134565137 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12676 11964 603 41 0 12635 0
vsize: 50704
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 11994 0 0 0 104979 35 0 0 25 0 1 0 481398142 51920896 11964 4294967295 134512640 134672761 3221224576 3221223680 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12676 11964 603 41 0 12635 0
vsize: 50704
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 11994 0 0 0 105979 35 0 0 25 0 1 0 481398142 51920896 11964 4294967295 134512640 134672761 3221224576 3221223744 134561406 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12676 11964 603 41 0 12635 0
vsize: 50704
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 11994 0 0 0 106980 35 0 0 25 0 1 0 481398142 51920896 11964 4294967295 134512640 134672761 3221224576 3221223776 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12676 11964 603 41 0 12635 0
vsize: 50704
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 11994 0 0 0 107979 35 0 0 25 0 1 0 481398142 51920896 11964 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12676 11964 603 41 0 12635 0
vsize: 50704
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 11994 0 0 0 108979 35 0 0 25 0 1 0 481398142 51920896 11964 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12676 11964 603 41 0 12635 0
vsize: 50704
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 11994 0 0 0 109979 35 0 0 25 0 1 0 481398142 51920896 11964 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12676 11964 603 41 0 12635 0
vsize: 50704
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 11994 0 0 0 110979 35 0 0 25 0 1 0 481398142 51920896 11964 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12676 11964 603 41 0 12635 0
vsize: 50704
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 11994 0 0 0 111979 35 0 0 25 0 1 0 481398142 51920896 11964 4294967295 134512640 134672761 3221224576 3221223744 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12676 11964 603 41 0 12635 0
vsize: 50704
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 11994 0 0 0 112980 35 0 0 25 0 1 0 481398142 51920896 11964 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12676 11964 603 41 0 12635 0
vsize: 50704
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 11994 0 0 0 113980 35 0 0 25 0 1 0 481398142 51920896 11964 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12676 11964 603 41 0 12635 0
vsize: 50704
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 11994 0 0 0 114980 35 0 0 25 0 1 0 481398142 51920896 11964 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12676 11964 603 41 0 12635 0
vsize: 50704
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 11994 0 0 0 115980 35 0 0 25 0 1 0 481398142 51920896 11964 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12676 11964 603 41 0 12635 0
vsize: 50704
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 11997 0 0 0 116980 35 0 0 25 0 1 0 481398142 51920896 11967 4294967295 134512640 134672761 3221224576 3221223744 134561400 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12676 11967 603 41 0 12635 0
vsize: 50704
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 11997 0 0 0 117980 35 0 0 25 0 1 0 481398142 51920896 11967 4294967295 134512640 134672761 3221224576 3221223744 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12676 11967 603 41 0 12635 0
vsize: 50704
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 12050 0 0 0 118981 35 0 0 25 0 1 0 481398142 52154368 12020 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12733 12020 603 41 0 12692 0
vsize: 50932
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3428
Raw data (stat): 3428 (minisat+) R 3427 28546 28545 0 -1 0 12167 0 0 0 119980 35 0 0 25 0 1 0 481398142 52576256 12137 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12836 12137 603 41 0 12795 0
vsize: 51344
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 3428
Raw data (stat): 3428 (minisat+) Z 3427 28546 28545 0 -1 12 12170 0 0 0 119980 38 0 0 25 0 1 0 481398142 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.05
CPU time (s): 1200.19
CPU user time (s): 1199.81
CPU system time (s): 0.384941
CPU usage (%): 100.012
Max. virtual memory (Kb): 51344
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####