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-ii8d1.opb
MD5SUM	f5ae067eec5cb4736f6ec50c87e4a015
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	343
Optimality of the best value was proved	NO
Number of terms in the objective function	1060
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	1060
Number of bits of the sum of numbers in the objective function	11
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	1060
Number of bits of the biggest sum of numbers	11
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.05184
Number of variables	1060
Total number of constraints	3737
Number of constraints which are clauses	3737
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	10
Trace number 5516

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc30 THE 2005-04-14 00:17:22 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3933 boxname=wulflinc30 idbench=173 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  f5ae067eec5cb4736f6ec50c87e4a015  /oldhome/oroussel/tmp/wulflinc30/normalized-ii8d1.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc30/normalized-ii8d1.opb /oldhome/oroussel/tmp/wulflinc30/normalized-ii8d1.opb
IDLAUNCH: 3933
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        735928 kB
Buffers:         37516 kB
Cached:         220748 kB
SwapCached:          0 kB
Active:          82148 kB
Inactive:       178988 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        735676 kB
SwapTotal:     2097892 kB
SwapFree:      2097892 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            31936 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 00:37:34 (client local time) WITH STATUS 10 IN 1209.97 SECONDS
stats: 3933 7 1209.97 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 3737 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): .........................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |    3727     8470 |    1118       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1040          
c   -- var.elim.:  1040/1040          
c |         0 |    3727     8470 |    1490       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 0.112982 s)
c ==============================================================================
c [1mFound solution: 446[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:57992     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |        19 |   72312   168817 |   21693      19      242    12.7 |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/45890          
c   -- var.elim.:  2000/45890          
c   -- var.elim.:  3000/45890          
c   -- var.elim.:  4000/45890          
c   -- var.elim.:  5000/45890          
c   -- var.elim.:  6000/45890          
c   -- var.elim.:  7000/45890          
c   -- var.elim.:  8000/45890          
c   -- var.elim.:  9000/45890          
c   -- var.elim.:  10000/45890          
c   -- var.elim.:  11000/45890          
c   -- var.elim.:  12000/45890          
c   -- var.elim.:  13000/45890          
c   -- var.elim.:  14000/45890          
c   -- var.elim.:  15000/45890          
c   -- var.elim.:  16000/45890          
c   -- var.elim.:  17000/45890          
c   -- var.elim.:  18000/45890          
c   -- var.elim.:  19000/45890          
c   -- var.elim.:  20000/45890          
c   -- var.elim.:  21000/45890          
c   -- var.elim.:  22000/45890          
c   -- var.elim.:  23000/45890          
c   -- var.elim.:  24000/45890          
c   -- var.elim.:  25000/45890          
c   -- var.elim.:  26000/45890          
c   -- var.elim.:  27000/45890          
c   -- var.elim.:  28000/45890          
c   -- var.elim.:  29000/45890          
c   -- var.elim.:  30000/45890          
c   -- var.elim.:  31000/45890          
c   -- var.elim.:  32000/45890          
c   -- var.elim.:  33000/45890          
c   -- var.elim.:  34000/45890          
c   -- var.elim.:  35000/45890          
c   -- var.elim.:  36000/45890          
c   -- var.elim.:  37000/45890          
c   -- var.elim.:  38000/45890          
c   -- var.elim.:  39000/45890          
c   -- var.elim.:  40000/45890          
c   -- var.elim.:  41000/45890          
c   -- var.elim.:  42000/45890          
c   -- var.elim.:  43000/45890          
c   -- var.elim.:  44000/45890          
c   -- var.elim.:  45000/45890          
c   -- var.elim.:  45890/45890          
c   -- var.elim.:  1000/22766          
c   -- var.elim.:  2000/22766          
c   -- var.elim.:  3000/22766          
c   -- var.elim.:  4000/22766          
c   -- var.elim.:  5000/22766          
c   -- var.elim.:  6000/22766          
c   -- var.elim.:  7000/22766          
c   -- var.elim.:  8000/22766          
c   -- var.elim.:  9000/22766          
c   -- var.elim.:  10000/22766          
c   -- var.elim.:  11000/22766          
c   -- var.elim.:  12000/22766          
c   -- var.elim.:  13000/22766          
c   -- var.elim.:  14000/22766          
c   -- var.elim.:  15000/22766          
c   -- var.elim.:  16000/22766          
c   -- var.elim.:  17000/22766          
c   -- var.elim.:  18000/22766          
c   -- var.elim.:  19000/22766          
c   -- var.elim.:  20000/22766          
c   -- var.elim.:  21000/22766          
c   -- var.elim.:  22000/22766          
c   -- var.elim.:  22766/22766          
c   -- var.elim.:  1000/13892          
c   -- var.elim.:  2000/13892          
c   -- var.elim.:  3000/13892          
c   -- var.elim.:  4000/13892          
c   -- var.elim.:  5000/13892          
c   -- var.elim.:  6000/13892          
c   -- var.elim.:  7000/13892          
c   -- var.elim.:  8000/13892          
c   -- var.elim.:  9000/13892          
c   -- var.elim.:  10000/13892          
c   -- var.elim.:  11000/13892          
c   -- var.elim.:  12000/13892          
c   -- var.elim.:  13000/13892          
c   -- var.elim.:  13892/13892          
c   -- var.elim.:  1000/10323          
c   -- var.elim.:  2000/10323          
c   -- var.elim.:  3000/10323          
c   -- var.elim.:  4000/10323          
c   -- var.elim.:  5000/10323          
c   -- var.elim.:  6000/10323          
c   -- var.elim.:  7000/10323          
c   -- var.elim.:  8000/10323          
c   -- var.elim.:  9000/10323          
c   -- var.elim.:  10000/10323          
c   -- var.elim.:  10323/10323          
c   -- var.elim.:  1000/8558          
c   -- var.elim.:  2000/8558          
c   -- var.elim.:  3000/8558          
c   -- var.elim.:  4000/8558          
c   -- var.elim.:  5000/8558          
c   -- var.elim.:  6000/8558          
c   -- var.elim.:  7000/8558          
c   -- var.elim.:  8000/8558          
c   -- var.elim.:  8558/8558          
c   -- var.elim.:  1000/6422          
c   -- var.elim.:  2000/6422          
c   -- var.elim.:  3000/6422          
c   -- var.elim.:  4000/6422          
c   -- var.elim.:  5000/6422          
c   -- var.elim.:  6000/6422          
c   -- var.elim.:  6422/6422          
c   -- var.elim.:  1000/6544          
c   -- var.elim.:  2000/6544          
c   -- var.elim.:  3000/6544          
c   -- var.elim.:  4000/6544          
c   -- var.elim.:  5000/6544          
c   -- var.elim.:  6000/6544          
c   -- var.elim.:  6544/6544          
c   -- var.elim.:  1000/4190          
c   -- var.elim.:  2000/4190          
c   -- var.elim.:  3000/4190          
c   -- var.elim.:  4000/4190          
c   -- var.elim.:  4190/4190          
c   -- var.elim.:  1000/2704          
c   -- var.elim.:  2000/2704          
c   -- var.elim.:  2704/2704          
c   -- subsuming                       
c   -- var.elim.:  1000/7519          
c   -- var.elim.:  2000/7519          
c   -- var.elim.:  3000/7519          
c   -- var.elim.:  4000/7519          
c   -- var.elim.:  5000/7519          
c   -- var.elim.:  6000/7519          
c   -- var.elim.:  7000/7519          
c   -- var.elim.:  7519/7519          
c   -- var.elim.:  143/143          
c |        19 |   23464   185561 |      --      19       --      -- |     --   | -48838/16774
c |        19 |   23464   185561 |    9385      19      242    12.7 |  0.000 % |
c |       119 |   23281   184022 |   10243     112    12369   110.4 |  0.790 % |
c |       269 |   22974   181152 |   11119     253    52399   207.1 |  2.106 % |
c |       494 |   22549   177327 |   12005     463    87682   189.4 |  3.978 % |
c |       831 |   22452   176464 |   13148     796   125975   158.3 |  4.387 % |
c |      1337 |   22197   174092 |   14299    1292   197981   153.2 |  5.479 % |
c |      2097 |   22084   172921 |   15649    2049   492347   240.3 |  5.967 % |
c |      3236 |   21284   164542 |   16590    3147   689235   219.0 |  9.486 % |
c ==============================================================================
c (current CPU-time: 196.919 s)
c ==============================================================================
c [1mFound solution: 409[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      4426 |   69156   281416 |   20746    4336   963273   222.2 |  9.486 % |
c   -- subsuming                       
c   -- var.elim.:  1000/43188          
c   -- var.elim.:  2000/43188          
c   -- var.elim.:  3000/43188          
c   -- var.elim.:  4000/43188          
c   -- var.elim.:  5000/43188          
c   -- var.elim.:  6000/43188          
c   -- var.elim.:  7000/43188          
c   -- var.elim.:  8000/43188          
c   -- var.elim.:  9000/43188          
c   -- var.elim.:  10000/43188          
c   -- var.elim.:  11000/43188          
c   -- var.elim.:  12000/43188          
c   -- var.elim.:  13000/43188          
c   -- var.elim.:  14000/43188          
c   -- var.elim.:  15000/43188          
c   -- var.elim.:  16000/43188          
c   -- var.elim.:  17000/43188          
c   -- var.elim.:  18000/43188          
c   -- var.elim.:  19000/43188          
c   -- var.elim.:  20000/43188          
c   -- var.elim.:  21000/43188          
c   -- var.elim.:  22000/43188          
c   -- var.elim.:  23000/43188          
c   -- var.elim.:  24000/43188          
c   -- var.elim.:  25000/43188          
c   -- var.elim.:  26000/43188          
c   -- var.elim.:  27000/43188          
c   -- var.elim.:  28000/43188          
c   -- var.elim.:  29000/43188          
c   -- var.elim.:  30000/43188          
c   -- var.elim.:  31000/43188          
c   -- var.elim.:  32000/43188          
c   -- var.elim.:  33000/43188          
c   -- var.elim.:  34000/43188          
c   -- var.elim.:  35000/43188          
c   -- var.elim.:  36000/43188          
c   -- var.elim.:  37000/43188          
c   -- var.elim.:  38000/43188          
c   -- var.elim.:  39000/43188          
c   -- var.elim.:  40000/43188          
c   -- var.elim.:  41000/43188          
c   -- var.elim.:  42000/43188          
c   -- var.elim.:  43000/43188          
c   -- var.elim.:  43188/43188          
c   -- var.elim.:  1000/20744          
c   -- var.elim.:  2000/20744          
c   -- var.elim.:  3000/20744          
c   -- var.elim.:  4000/20744          
c   -- var.elim.:  5000/20744          
c   -- var.elim.:  6000/20744          
c   -- var.elim.:  7000/20744          
c   -- var.elim.:  8000/20744          
c   -- var.elim.:  9000/20744          
c   -- var.elim.:  10000/20744          
c   -- var.elim.:  11000/20744          
c   -- var.elim.:  12000/20744          
c   -- var.elim.:  13000/20744          
c   -- var.elim.:  14000/20744          
c   -- var.elim.:  15000/20744          
c   -- var.elim.:  16000/20744          
c   -- var.elim.:  17000/20744          
c   -- var.elim.:  18000/20744          
c   -- var.elim.:  19000/20744          
c   -- var.elim.:  20000/20744          
c   -- var.elim.:  20744/20744          
c   -- var.elim.:  1000/12021          
c   -- var.elim.:  2000/12021          
c   -- var.elim.:  3000/12021          
c   -- var.elim.:  4000/12021          
c   -- var.elim.:  5000/12021          
c   -- var.elim.:  6000/12021          
c   -- var.elim.:  7000/12021          
c   -- var.elim.:  8000/12021          
c   -- var.elim.:  9000/12021          
c   -- var.elim.:  10000/12021          
c   -- var.elim.:  11000/12021          
c   -- var.elim.:  12000/12021          
c   -- var.elim.:  12021/12021          
c   -- var.elim.:  1000/10000          
c   -- var.elim.:  2000/10000          
c   -- var.elim.:  3000/10000          
c   -- var.elim.:  4000/10000          
c   -- var.elim.:  5000/10000          
c   -- var.elim.:  6000/10000          
c   -- var.elim.:  7000/10000          
c   -- var.elim.:  8000/10000          
c   -- var.elim.:  9000/10000          
c   -- var.elim.:  10000/10000          
c   -- var.elim.:  1000/8314          
c   -- var.elim.:  2000/8314          
c   -- var.elim.:  3000/8314          
c   -- var.elim.:  4000/8314          
c   -- var.elim.:  5000/8314          
c   -- var.elim.:  6000/8314          
c   -- var.elim.:  7000/8314          
c   -- var.elim.:  8000/8314          
c   -- var.elim.:  8314/8314          
c   -- var.elim.:  1000/6979          
c   -- var.elim.:  2000/6979          
c   -- var.elim.:  3000/6979          
c   -- var.elim.:  4000/6979          
c   -- var.elim.:  5000/6979          
c   -- var.elim.:  6000/6979          
c   -- var.elim.:  6979/6979          
c   -- var.elim.:  1000/5819          
c   -- var.elim.:  2000/5819          
c   -- var.elim.:  3000/5819          
c   -- var.elim.:  4000/5819          
c   -- var.elim.:  5000/5819          
c   -- var.elim.:  5819/5819          
c   -- var.elim.:  1000/4088          
c   -- var.elim.:  2000/4088          
c   -- var.elim.:  3000/4088          
c   -- var.elim.:  4000/4088          
c   -- var.elim.:  4088/4088          
c   -- var.elim.:  1000/2794          
c   -- var.elim.:  2000/2794          
c   -- var.elim.:  2794/2794          
c   -- subsuming                       
c   -- var.elim.:  1000/4600          
c   -- var.elim.:  2000/4600          
c   -- var.elim.:  3000/4600          
c   -- var.elim.:  4000/4600          
c   -- var.elim.:  4600/4600          
c   -- var.elim.:  70/70          
c |      4426 |   21842   183470 |      --    4336       --      -- |     --   | -47228/-97773
c |      4426 |   21842   183470 |    8736    2819   191962    68.1 |  9.486 % |
c |      4526 |   21728   182275 |    9560    2914   198295    68.0 | 15.854 % |
c |      4676 |   21633   181304 |   10470    3060   218400    71.4 | 16.229 % |
c |      4902 |   21631   181298 |   11516    3284   243992    74.3 | 16.238 % |
c |      5239 |   21500   179854 |   12591    3616   318340    88.0 | 16.756 % |
c |      5745 |   21462   179450 |   13825    4115   475468   115.5 | 16.890 % |
c |      6504 |   21285   177377 |   15083    4861   615709   126.7 | 17.569 % |
c |      7643 |   21115   175410 |   16458    5986   795611   132.9 | 18.239 % |
c |      9351 |   21014   174224 |   18018    7689   995685   129.5 | 18.641 % |
c |     11914 |   20950   173694 |   19759   10250  1503453   146.7 | 18.909 % |
c |     15758 |   20805   171999 |   21585   14069  2177099   154.7 | 19.498 % |
c |     21526 |   20805   171999 |   23743   19837  4604682   232.1 | 19.498 % |
c |     30175 |   20805   171999 |   26118   28486  9590563   336.7 | 19.498 % |
c |     43150 |   20741   171341 |   28641   25570 11199763   438.0 | 19.748 % |
c |     62614 |   20741   171341 |   31505   25271  9014383   356.7 | 19.748 % |
c |     91807 |   20691   170802 |   34572   27200 13756164   505.7 | 19.954 % |
c |    135596 |   20663   170508 |   37978   14125  6747078   477.7 | 20.079 % |
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 -x701 x702 -x703 x704 -x705 x706 -x707 x708 -x709 x710 x711 -x712 -x713 x714 -x715 x716 -x717 x718 -x719 -x720 -x721 x722 -x723 x724 -x725 x726 -x727 x728 -x729 x730 x731 -x732 -x733 x734 -x735 x736 -x737 x738 -x739 -x740 -x741 x742 -x743 x744 x745 -x746 -x747 x748 -x749 -x750 -x751 x752 -x753 x754 -x755 -x756 -x757 -x758 -x759 -x760 -x761 x762 x763 -x764 -x765 x766 -x767 x768 -x769 x770 -x771 x772 -x773 x774 -x775 x776 -x777 x778 -x779 x780 -x781 x782 -x783 x784 -x785 -x786 -x787 x788 -x789 -x790 x791 -x792 -x793 -x794 -x795 -x796 -x797 -x798 -x799 -x800 -x801 x802 -x803 x804 x805 -x806 -x807 x808 -x809 -x810 -x811 x812 -x813 x814 -x815 -x816 -x817 -x818 -x819 -x820 -x821 x822 -x823 x824 -x825 x826 -x827 x828 -x829 x830 -x831 x832 -x833 x834 -x835 x836 -x837 x838 x839 -x840 -x841 -x842 -x843 -x844 -x845 -x846 -x847 x848 -x849 -x850 -x851 x852 -x853 x854 -x855 -x856 x857 -x858 -x859 -x860 -x861 x862 -x863 x864 -x865 x866 -x867 x868 -x869 x870 x871 -x872 -x873 x874 -x875 x876 -x877 x878 -x879 -x880 -x881 x882 -x883 -x884 -x885 x886 x887 -x888 -x889 x890 -x891 -x892 -x893 x894 -x895 x896 -x897 x898 -x899 -x900 -x901 x902 -x903 x904 -x905 -x906 -x907 x908 x909 -x910 -x911 x912 -x913 -x914 -x915 -x916 -x917 -x918 -x919 x920 -x921 x922 -x923 x924 -x925 -x926 -x927 x928 x929 -x930 -x931 x932 -x933 x934 -x935 -x936 -x937 -x938 -x939 -x940 -x941 x942 -x943 x944 -x945 -x946 -x947 x948 x949 -x950 -x951 x952 -x953 x954 -x955 -x956 -x957 -x958 -x959 x960 -x961 x962 -x963 x964 -x965 x966 -x967 x968 -x969 x970 x971 -x972 -x973 -x974 -x975 x976 -x977 x978 -x979 -x980 -x981 -x982 -x983 x984 -x985 -x986 -x987 x988 x989 -x990 -x991 x992 -x993 x994 -x995 -x996 -x997 -x998 -x999 -x1000 -x1001 x1002 -x1003 x1004 -x1005 -x1006 -x1007 x1008 -x1009 -x1010 -x1011 x1012 -x1013 x1014 -x1015 -x1016 -x1017 -x1018 x1019 -x1020 -x1021 -x1022 -x1023 -x1024 -x1025 -x1026 -x1027 x1028 x1029 -x1030 -x1031 x1032 -x1033 x1034 -x1035 -x1036 -x#### 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.92 0.96 0.91 2/54 16503
Raw data (stat): 16503 (runsolver) R 16502 11931 11930 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 480203191 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.0005 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 7038 0 0 0 975 23 0 0 25 0 1 0 480203191 32169984 6768 4294967295 134512640 134672761 3221224576 3221223024 134643959 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7854 6768 603 41 0 7813 0
vsize: 31416
[startup+20.0009 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 7038 0 0 0 1975 23 0 0 25 0 1 0 480203191 32169984 6768 4294967295 134512640 134672761 3221224576 3221223024 134643984 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7854 6768 603 41 0 7813 0
vsize: 31416
[startup+30.0017 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 7038 0 0 0 2975 23 0 0 25 0 1 0 480203191 32169984 6768 4294967295 134512640 134672761 3221224576 3221223024 134643984 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7854 6768 603 41 0 7813 0
vsize: 31416
[startup+40.0018 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 7040 0 0 0 3975 23 0 0 25 0 1 0 480203191 32169984 6770 4294967295 134512640 134672761 3221224576 3221223024 134643583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7854 6770 603 41 0 7813 0
vsize: 31416
[startup+50.0013 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 7040 0 0 0 4975 23 0 0 25 0 1 0 480203191 32169984 6770 4294967295 134512640 134672761 3221224576 3221223024 134643516 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7854 6770 603 41 0 7813 0
vsize: 31416
[startup+60.0011 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 7040 0 0 0 5975 23 0 0 25 0 1 0 480203191 32169984 6770 4294967295 134512640 134672761 3221224576 3221223024 134643524 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7854 6770 603 41 0 7813 0
vsize: 31416
[startup+70.0015 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 7214 0 0 0 6963 36 0 0 25 0 1 0 480203191 32710656 6889 4294967295 134512640 134672761 3221224576 3221223024 134643612 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7986 6889 603 41 0 7945 0
vsize: 31944
[startup+80.0017 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 7215 0 0 0 7960 38 0 0 25 0 1 0 480203191 32677888 6889 4294967295 134512640 134672761 3221224576 3221223024 134643539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7978 6889 603 41 0 7937 0
vsize: 31912
[startup+90.0015 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 7216 0 0 0 8956 41 0 0 25 0 1 0 480203191 32677888 6890 4294967295 134512640 134672761 3221224576 3221223024 134643951 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7978 6890 603 41 0 7937 0
vsize: 31912
[startup+100.002 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 7216 0 0 0 9955 42 0 0 25 0 1 0 480203191 32673792 6889 4294967295 134512640 134672761 3221224576 3221223024 134643471 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7977 6889 603 41 0 7936 0
vsize: 31908
[startup+110.002 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 7216 0 0 0 10955 43 0 0 25 0 1 0 480203191 32641024 6882 4294967295 134512640 134672761 3221224576 3221223056 134541816 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7969 6882 603 41 0 7928 0
vsize: 31876
[startup+120.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 7216 0 0 0 11955 43 0 0 25 0 1 0 480203191 32641024 6882 4294967295 134512640 134672761 3221224576 3221223032 1075346913 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7969 6882 603 41 0 7928 0
vsize: 31876
[startup+130.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 7216 0 0 0 12955 43 0 0 25 0 1 0 480203191 32641024 6882 4294967295 134512640 134672761 3221224576 3221223024 134643565 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7969 6882 603 41 0 7928 0
vsize: 31876
[startup+140.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 7216 0 0 0 13955 43 0 0 25 0 1 0 480203191 32378880 6837 4294967295 134512640 134672761 3221224576 3221223136 134607998 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7905 6837 603 41 0 7864 0
vsize: 31620
[startup+150.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 7216 0 0 0 14955 44 0 0 25 0 1 0 480203191 32378880 6837 4294967295 134512640 134672761 3221224576 3221223120 134621083 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7905 6837 603 41 0 7864 0
vsize: 31620
[startup+160.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 7216 0 0 0 15955 44 0 0 25 0 1 0 480203191 32378880 6837 4294967295 134512640 134672761 3221224576 3221223120 134621060 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7905 6837 603 41 0 7864 0
vsize: 31620
[startup+170.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 7287 0 0 0 16955 44 0 0 25 0 1 0 480203191 32800768 6908 4294967295 134512640 134672761 3221224576 3221223120 134621062 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8008 6908 603 41 0 7967 0
vsize: 32032
[startup+180.003 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 7287 0 0 0 17955 44 0 0 25 0 1 0 480203191 32378880 6837 4294967295 134512640 134672761 3221224576 3221223024 134644040 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7905 6837 603 41 0 7864 0
vsize: 31620
[startup+190.003 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 7442 0 0 0 18954 44 0 0 25 0 1 0 480203191 33026048 6992 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8063 6992 603 41 0 8022 0
vsize: 32252
[startup+200.003 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 11711 0 0 0 19936 63 0 0 25 0 1 0 480203191 45391872 9282 4294967295 134512640 134672761 3221224576 3221223068 134642759 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11082 9282 603 41 0 11041 0
vsize: 44328
[startup+210.003 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 11782 0 0 0 20935 63 0 0 25 0 1 0 480203191 45912064 9353 4294967295 134512640 134672761 3221224576 3221223120 134621211 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11209 9353 603 41 0 11168 0
vsize: 44836
[startup+220.003 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 12128 0 0 0 21896 77 0 0 25 0 1 0 480203191 46391296 9507 4294967295 134512640 134672761 3221224576 3221223024 134643516 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11326 9507 603 41 0 11285 0
vsize: 45304
[startup+230.004 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 12150 0 0 0 22896 77 0 0 25 0 1 0 480203191 46395392 9486 4294967295 134512640 134672761 3221224576 3221223024 134643516 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11327 9486 603 41 0 11286 0
vsize: 45308
[startup+240.005 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 12150 0 0 0 23896 77 0 0 25 0 1 0 480203191 46395392 9486 4294967295 134512640 134672761 3221224576 3221223024 134643511 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11327 9486 603 41 0 11286 0
vsize: 45308
[startup+250.005 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 12150 0 0 0 24883 85 0 0 24 0 1 0 480203191 46264320 9485 4294967295 134512640 134672761 3221224576 3221222784 1075730206 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11295 9485 603 41 0 11254 0
vsize: 45180
[startup+260.006 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 12150 0 0 0 25878 89 0 0 25 0 1 0 480203191 46264320 9485 4294967295 134512640 134672761 3221224576 3221223024 134643548 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11295 9485 603 41 0 11254 0
vsize: 45180
[startup+270.007 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 12150 0 0 0 26875 92 0 0 25 0 1 0 480203191 46264320 9485 4294967295 134512640 134672761 3221224576 3221223024 134643583 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11295 9485 603 41 0 11254 0
vsize: 45180
[startup+280.007 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 12155 0 0 0 27873 94 0 0 25 0 1 0 480203191 46428160 9490 4294967295 134512640 134672761 3221224576 3221223024 134643570 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11335 9490 603 41 0 11294 0
vsize: 45340
[startup+290.008 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 12155 0 0 0 28872 95 0 0 25 0 1 0 480203191 46428160 9490 4294967295 134512640 134672761 3221224576 3221223024 134643468 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11335 9490 603 41 0 11294 0
vsize: 45340
[startup+300.009 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 12155 0 0 0 29872 95 0 0 25 0 1 0 480203191 46428160 9490 4294967295 134512640 134672761 3221224576 3221223024 134643499 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11335 9490 603 41 0 11294 0
vsize: 45340
[startup+310.01 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 12155 0 0 0 30872 95 0 0 25 0 1 0 480203191 46428160 9490 4294967295 134512640 134672761 3221224576 3221223024 134644014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11335 9490 603 41 0 11294 0
vsize: 45340
[startup+320.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 12155 0 0 0 31872 96 0 0 25 0 1 0 480203191 46166016 9447 4294967295 134512640 134672761 3221224576 3221223184 134553649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11271 9447 603 41 0 11230 0
vsize: 45084
[startup+330.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 12226 0 0 0 32871 96 0 0 25 0 1 0 480203191 46739456 9518 4294967295 134512640 134672761 3221224576 3221223120 134621095 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11411 9518 603 41 0 11370 0
vsize: 45644
[startup+340.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 12226 0 0 0 33871 96 0 0 25 0 1 0 480203191 46166016 9447 4294967295 134512640 134672761 3221224576 3221223104 134566562 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11271 9447 603 41 0 11230 0
vsize: 45084
[startup+350.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 12229 0 0 0 34871 96 0 0 25 0 1 0 480203191 46166016 9450 4294967295 134512640 134672761 3221224576 3221223488 134644251 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11271 9450 603 41 0 11230 0
vsize: 45084
[startup+360.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 12768 0 0 0 35869 98 0 0 25 0 1 0 480203191 48259072 9989 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11782 9989 603 41 0 11741 0
vsize: 47128
[startup+370.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 14012 0 0 0 36864 103 0 0 25 0 1 0 480203191 53395456 11233 4294967295 134512640 134672761 3221224576 3221223408 1075350119 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13036 11233 603 41 0 12995 0
vsize: 52144
[startup+380.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 15817 0 0 0 37859 108 0 0 25 0 1 0 480203191 60862464 13038 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14859 13038 603 41 0 14818 0
vsize: 59436
[startup+390.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 17729 0 0 0 38854 113 0 0 25 0 1 0 480203191 68665344 14950 4294967295 134512640 134672761 3221224576 3221223760 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16764 14950 603 41 0 16723 0
vsize: 67056
[startup+400.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 19635 0 0 0 39851 116 0 0 25 0 1 0 480203191 76447744 16856 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18664 16856 603 41 0 18623 0
vsize: 74656
[startup+410.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 20475 0 0 0 40847 120 0 0 25 0 1 0 480203191 79835136 17696 4294967295 134512640 134672761 3221224576 3221223760 134615794 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19491 17696 603 41 0 19450 0
vsize: 77964
[startup+420.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 20475 0 0 0 41848 120 0 0 25 0 1 0 480203191 79835136 17696 4294967295 134512640 134672761 3221224576 3221223764 134610770 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19491 17696 603 41 0 19450 0
vsize: 77964
[startup+430.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 21197 0 0 0 42846 122 0 0 25 0 1 0 480203191 82870272 18418 4294967295 134512640 134672761 3221224576 3221223616 134612932 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20232 18418 603 41 0 20191 0
vsize: 80928
[startup+440.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 22815 0 0 0 43841 127 0 0 25 0 1 0 480203191 89407488 20036 4294967295 134512640 134672761 3221224576 3221223840 134618040 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21828 20036 603 41 0 21787 0
vsize: 87312
[startup+450.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 24995 0 0 0 44834 134 0 0 25 0 1 0 480203191 98353152 22216 4294967295 134512640 134672761 3221224576 3221223616 134612572 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24012 22216 603 41 0 23971 0
vsize: 96048
[startup+460.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 26927 0 0 0 45828 140 0 0 25 0 1 0 480203191 106360832 24148 4294967295 134512640 134672761 3221224576 3221223616 134612783 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25967 24148 603 41 0 25926 0
vsize: 103868
[startup+470.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 27640 0 0 0 46826 142 0 0 25 0 1 0 480203191 109154304 24860 4294967295 134512640 134672761 3221224576 3221223760 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26649 24860 603 41 0 26608 0
vsize: 106596
[startup+480.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 27640 0 0 0 47826 142 0 0 25 0 1 0 480203191 109154304 24860 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26649 24860 603 41 0 26608 0
vsize: 106596
[startup+490.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 27640 0 0 0 48826 142 0 0 25 0 1 0 480203191 109154304 24860 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26649 24860 603 41 0 26608 0
vsize: 106596
[startup+500.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 27640 0 0 0 49825 143 0 0 25 0 1 0 480203191 109154304 24860 4294967295 134512640 134672761 3221224576 3221223712 134614583 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26649 24860 603 41 0 26608 0
vsize: 106596
[startup+510.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 27640 0 0 0 50825 143 0 0 25 0 1 0 480203191 109154304 24860 4294967295 134512640 134672761 3221224576 3221223616 134614266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26649 24860 603 41 0 26608 0
vsize: 106596
[startup+520.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 27640 0 0 0 51825 143 0 0 25 0 1 0 480203191 109154304 24860 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26649 24860 603 41 0 26608 0
vsize: 106596
[startup+530.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 27640 0 0 0 52825 144 0 0 25 0 1 0 480203191 109154304 24860 4294967295 134512640 134672761 3221224576 3221223760 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26649 24860 603 41 0 26608 0
vsize: 106596
[startup+540.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 28342 0 0 0 53824 145 0 0 25 0 1 0 480203191 112148480 25562 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27380 25562 603 41 0 27339 0
vsize: 109520
[startup+550.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 29005 0 0 0 54822 147 0 0 25 0 1 0 480203191 114581504 26185 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27974 26185 603 41 0 27933 0
vsize: 111896
[startup+560.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 29005 0 0 0 55822 147 0 0 25 0 1 0 480203191 114581504 26185 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27974 26185 603 41 0 27933 0
vsize: 111896
[startup+570.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 29005 0 0 0 56822 147 0 0 25 0 1 0 480203191 114581504 26185 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27974 26185 603 41 0 27933 0
vsize: 111896
[startup+580.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 29005 0 0 0 57823 147 0 0 25 0 1 0 480203191 114581504 26185 4294967295 134512640 134672761 3221224576 3221223760 134615583 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27974 26185 603 41 0 27933 0
vsize: 111896
[startup+590.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 29005 0 0 0 58823 147 0 0 25 0 1 0 480203191 114581504 26185 4294967295 134512640 134672761 3221224576 3221223760 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27974 26185 603 41 0 27933 0
vsize: 111896
[startup+600.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 29005 0 0 0 59823 147 0 0 25 0 1 0 480203191 114581504 26185 4294967295 134512640 134672761 3221224576 3221223760 134615739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27974 26185 603 41 0 27933 0
vsize: 111896
[startup+610.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 29005 0 0 0 60823 147 0 0 25 0 1 0 480203191 114581504 26185 4294967295 134512640 134672761 3221224576 3221223760 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27974 26185 603 41 0 27933 0
vsize: 111896
[startup+620.025 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 29005 0 0 0 61823 147 0 0 25 0 1 0 480203191 114581504 26185 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27974 26185 603 41 0 27933 0
vsize: 111896
[startup+630.025 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 29005 0 0 0 62823 147 0 0 25 0 1 0 480203191 114577408 26184 4294967295 134512640 134672761 3221224576 3221223760 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27973 26184 603 41 0 27932 0
vsize: 111892
[startup+640.025 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 29005 0 0 0 63823 147 0 0 25 0 1 0 480203191 114577408 26184 4294967295 134512640 134672761 3221224576 3221223760 134615758 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27973 26184 603 41 0 27932 0
vsize: 111892
[startup+650.025 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 29005 0 0 0 64824 147 0 0 25 0 1 0 480203191 114577408 26184 4294967295 134512640 134672761 3221224576 3221223616 134614266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27973 26184 603 41 0 27932 0
vsize: 111892
[startup+660.025 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 29005 0 0 0 65824 147 0 0 25 0 1 0 480203191 114577408 26184 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27973 26184 603 41 0 27932 0
vsize: 111892
[startup+670.025 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 29005 0 0 0 66824 147 0 0 25 0 1 0 480203191 114577408 26184 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27973 26184 603 41 0 27932 0
vsize: 111892
[startup+680.026 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 29005 0 0 0 67824 148 0 0 25 0 1 0 480203191 114577408 26184 4294967295 134512640 134672761 3221224576 3221223616 134612684 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27973 26184 603 41 0 27932 0
vsize: 111892
[startup+690.027 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 29005 0 0 0 68824 148 0 0 25 0 1 0 480203191 114577408 26184 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27973 26184 603 41 0 27932 0
vsize: 111892
[startup+700.027 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 29005 0 0 0 69824 148 0 0 25 0 1 0 480203191 114577408 26184 4294967295 134512640 134672761 3221224576 3221223760 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27973 26184 603 41 0 27932 0
vsize: 111892
[startup+710.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 29005 0 0 0 70824 148 0 0 25 0 1 0 480203191 114577408 26184 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27973 26184 603 41 0 27932 0
vsize: 111892
[startup+720.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 29005 0 0 0 71825 148 0 0 25 0 1 0 480203191 114577408 26184 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27973 26184 603 41 0 27932 0
vsize: 111892
[startup+730.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 29005 0 0 0 72825 148 0 0 25 0 1 0 480203191 114577408 26184 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27973 26184 603 41 0 27932 0
vsize: 111892
[startup+740.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 29005 0 0 0 73825 148 0 0 25 0 1 0 480203191 114577408 26184 4294967295 134512640 134672761 3221224576 3221223616 134613818 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27973 26184 603 41 0 27932 0
vsize: 111892
[startup+750.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 29005 0 0 0 74825 148 0 0 25 0 1 0 480203191 114577408 26184 4294967295 134512640 134672761 3221224576 3221223616 134612885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27973 26184 603 41 0 27932 0
vsize: 111892
[startup+760.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 29005 0 0 0 75825 148 0 0 25 0 1 0 480203191 114577408 26184 4294967295 134512640 134672761 3221224576 3221223712 134614683 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27973 26184 603 41 0 27932 0
vsize: 111892
[startup+770.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 29307 0 0 0 76824 149 0 0 25 0 1 0 480203191 115847168 26486 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28283 26486 603 41 0 28242 0
vsize: 113132
[startup+780.031 s]
Raw data (loadavg): 1.00 0.99 0.91 3/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 30549 0 0 0 77822 152 0 0 25 0 1 0 480203191 121028608 27728 4294967295 134512640 134672761 3221224576 3221223448 1075353266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29548 27728 603 41 0 29507 0
vsize: 118192
[startup+790.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 31818 0 0 0 78819 155 0 0 25 0 1 0 480203191 126156800 28997 4294967295 134512640 134672761 3221224576 3221223616 134614266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30800 28997 603 41 0 30759 0
vsize: 123200
[startup+800.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 32916 0 0 0 79817 157 0 0 25 0 1 0 480203191 130662400 30095 4294967295 134512640 134672761 3221224576 3221223760 134615739 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31900 30095 603 41 0 31859 0
vsize: 127600
[startup+810.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 34213 0 0 0 80815 159 0 0 25 0 1 0 480203191 135917568 31392 4294967295 134512640 134672761 3221224576 3221223760 134615635 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33183 31392 603 41 0 33142 0
vsize: 132732
[startup+820.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 35570 0 0 0 81812 163 0 0 25 0 1 0 480203191 141541376 32749 4294967295 134512640 134672761 3221224576 3221223760 134615773 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34556 32749 603 41 0 34515 0
vsize: 138224
[startup+830.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 36526 0 0 0 82810 165 0 0 25 0 1 0 480203191 145534976 33705 4294967295 134512640 134672761 3221224576 3221223616 134614274 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35531 33705 603 41 0 35490 0
vsize: 142124
[startup+840.037 s]
Raw data (loadavg): 1.00 0.99 0.91 3/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 37446 0 0 0 83808 168 0 0 25 0 1 0 480203191 149291008 34625 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36448 34625 603 41 0 36407 0
vsize: 145792
[startup+850.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 38505 0 0 0 84805 170 0 0 25 0 1 0 480203191 153645056 35684 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37511 35684 603 41 0 37470 0
vsize: 150044
[startup+860.038 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 39598 0 0 0 85803 173 0 0 25 0 1 0 480203191 158121984 36777 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38604 36777 603 41 0 38563 0
vsize: 154416
[startup+870.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 39741 0 0 0 86803 173 0 0 25 0 1 0 480203191 158519296 36905 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38701 36905 603 41 0 38660 0
vsize: 154804
[startup+880.038 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 39741 0 0 0 87803 173 0 0 25 0 1 0 480203191 158519296 36905 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38701 36905 603 41 0 38660 0
vsize: 154804
[startup+890.039 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 39741 0 0 0 88803 173 0 0 25 0 1 0 480203191 158519296 36905 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38701 36905 603 41 0 38660 0
vsize: 154804
[startup+900.038 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 39741 0 0 0 89803 173 0 0 25 0 1 0 480203191 158519296 36905 4294967295 134512640 134672761 3221224576 3221223760 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38701 36905 603 41 0 38660 0
vsize: 154804
[startup+910.039 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 39741 0 0 0 90803 173 0 0 25 0 1 0 480203191 158519296 36905 4294967295 134512640 134672761 3221224576 3221223760 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38701 36905 603 41 0 38660 0
vsize: 154804
[startup+920.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 39741 0 0 0 91804 173 0 0 25 0 1 0 480203191 158519296 36905 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38701 36905 603 41 0 38660 0
vsize: 154804
[startup+930.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 39741 0 0 0 92804 173 0 0 25 0 1 0 480203191 158519296 36905 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38701 36905 603 41 0 38660 0
vsize: 154804
[startup+940.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 39741 0 0 0 93804 173 0 0 25 0 1 0 480203191 158519296 36905 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38701 36905 603 41 0 38660 0
vsize: 154804
[startup+950.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 39741 0 0 0 94804 173 0 0 25 0 1 0 480203191 158519296 36905 4294967295 134512640 134672761 3221224576 3221223760 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38701 36905 603 41 0 38660 0
vsize: 154804
[startup+960.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 39741 0 0 0 95804 173 0 0 25 0 1 0 480203191 158519296 36905 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38701 36905 603 41 0 38660 0
vsize: 154804
[startup+970.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 39741 0 0 0 96804 174 0 0 25 0 1 0 480203191 158519296 36905 4294967295 134512640 134672761 3221224576 3221223760 134615767 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38701 36905 603 41 0 38660 0
vsize: 154804
[startup+980.041 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 39741 0 0 0 97804 174 0 0 25 0 1 0 480203191 158519296 36905 4294967295 134512640 134672761 3221224576 3221223760 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38701 36905 603 41 0 38660 0
vsize: 154804
[startup+990.042 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 39741 0 0 0 98805 174 0 0 25 0 1 0 480203191 158519296 36905 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38701 36905 603 41 0 38660 0
vsize: 154804
[startup+1000.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 40033 0 0 0 99804 174 0 0 25 0 1 0 480203191 159805440 37197 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39015 37197 603 41 0 38974 0
vsize: 156060
[startup+1010.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 41090 0 0 0 100802 177 0 0 25 0 1 0 480203191 164130816 38254 4294967295 134512640 134672761 3221224576 3221223760 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40071 38254 603 41 0 40030 0
vsize: 160284
[startup+1020.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 42160 0 0 0 101800 179 0 0 25 0 1 0 480203191 168476672 39324 4294967295 134512640 134672761 3221224576 3221223760 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41132 39324 603 41 0 41091 0
vsize: 164528
[startup+1030.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 43165 0 0 0 102798 181 0 0 25 0 1 0 480203191 172675072 40329 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42157 40329 603 41 0 42116 0
vsize: 168628
[startup+1040.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 44008 0 0 0 103796 183 0 0 25 0 1 0 480203191 176025600 41172 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42975 41172 603 41 0 42934 0
vsize: 171900
[startup+1050.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 44980 0 0 0 104795 184 0 0 25 0 1 0 480203191 179986432 42144 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43942 42144 603 41 0 43901 0
vsize: 175768
[startup+1060.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 45908 0 0 0 105794 186 0 0 25 0 1 0 480203191 183808000 43072 4294967295 134512640 134672761 3221224576 3221223760 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44875 43072 603 41 0 44834 0
vsize: 179500
[startup+1070.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 47212 0 0 0 106790 190 0 0 25 0 1 0 480203191 189136896 44376 4294967295 134512640 134672761 3221224576 3221223760 134616017 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46176 44376 603 41 0 46135 0
vsize: 184704
[startup+1080.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 48070 0 0 0 107788 192 0 0 25 0 1 0 480203191 192778240 45234 4294967295 134512640 134672761 3221224576 3221223616 134612628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47065 45234 603 41 0 47024 0
vsize: 188260
[startup+1090.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 48927 0 0 0 108787 193 0 0 25 0 1 0 480203191 196206592 46091 4294967295 134512640 134672761 3221224576 3221223760 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47902 46091 603 41 0 47861 0
vsize: 191608
[startup+1100.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 49768 0 0 0 109786 194 0 0 25 0 1 0 480203191 199651328 46932 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48743 46932 603 41 0 48702 0
vsize: 194972
[startup+1110.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 50617 0 0 0 110785 196 0 0 25 0 1 0 480203191 203096064 47781 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49584 47781 603 41 0 49543 0
vsize: 198336
[startup+1120.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 51569 0 0 0 111783 198 0 0 25 0 1 0 480203191 207101952 48733 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50562 48733 603 41 0 50521 0
vsize: 202248
[startup+1130.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 52621 0 0 0 112781 200 0 0 25 0 1 0 480203191 211345408 49785 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51598 49785 603 41 0 51557 0
vsize: 206392
[startup+1140.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 53520 0 0 0 113780 201 0 0 25 0 1 0 480203191 215089152 50684 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52512 50684 603 41 0 52471 0
vsize: 210048
[startup+1150.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 54237 0 0 0 114778 203 0 0 25 0 1 0 480203191 217989120 51401 4294967295 134512640 134672761 3221224576 3221223616 134612845 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53220 51401 603 41 0 53179 0
vsize: 212880
[startup+1160.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 55219 0 0 0 115776 205 0 0 25 0 1 0 480203191 222040064 52383 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54209 52383 603 41 0 54168 0
vsize: 216836
[startup+1170.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 56143 0 0 0 116775 206 0 0 25 0 1 0 480203191 225734656 53307 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55111 53307 603 41 0 55070 0
vsize: 220444
[startup+1180.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 57041 0 0 0 117773 209 0 0 25 0 1 0 480203191 229531648 54205 4294967295 134512640 134672761 3221224576 3221223616 134612684 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56038 54205 603 41 0 55997 0
vsize: 224152
[startup+1190.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 58082 0 0 0 118771 211 0 0 25 0 1 0 480203191 233717760 55246 4294967295 134512640 134672761 3221224576 3221223616 134613012 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57060 55246 603 41 0 57019 0
vsize: 228240
[startup+1200.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 58947 0 0 0 119769 213 0 0 25 0 1 0 480203191 237330432 56111 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57942 56111 603 41 0 57901 0
vsize: 231768
[startup+1210.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 16503
Raw data (stat): 16503 (minisat+) R 16502 11931 11930 0 -1 0 59279 0 0 0 120768 214 0 0 25 0 1 0 480203191 238534656 56428 4294967295 134512640 134672761 3221224576 3221223760 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58236 56428 603 41 0 58195 0
vsize: 232944
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1210.19 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 16503
Raw data (stat): 16503 (minisat+) Z 16502 11931 11930 0 -1 12 59280 0 0 0 120769 227 0 0 25 0 1 0 480203191 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): 1210.19
CPU time (s): 1209.97
CPU user time (s): 1207.69
CPU system time (s): 2.27865
CPU usage (%): 99.982
Max. virtual memory (Kb): 232944
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####