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-ii32d2.opb
MD5SUM	a483fc3761bb4050329265bf3a3a7ca5
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	372
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.04284
Number of variables	808
Total number of constraints	5557
Number of constraints which are clauses	5557
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	32
Trace number 6253

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc21 THE 2005-04-14 03:58:33 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4668 boxname=wulflinc21 idbench=156 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  a483fc3761bb4050329265bf3a3a7ca5  /oldhome/oroussel/tmp/wulflinc21/normalized-ii32d2.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc21/normalized-ii32d2.opb /oldhome/oroussel/tmp/wulflinc21/normalized-ii32d2.opb
IDLAUNCH: 4668
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.161
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.161
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:        873460 kB
Buffers:         28600 kB
Cached:         112636 kB
SwapCached:          0 kB
Active:          37572 kB
Inactive:       106580 kB
HighTotal:      131008 kB
HighFree:        14728 kB
LowTotal:       903652 kB
LowFree:        858732 kB
SwapTotal:     2097892 kB
SwapFree:      2097804 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            11472 kB
Committed_AS:    63788 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 04:18:35 (client local time) WITH STATUS 10 IN 1200.14 SECONDS
stats: 4668 7 1200.14 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 5557 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 |    5557    18748 |    1852       0        0     nan |  0.000 % |
c |       100 |    5557    18748 |    2037     100     8211    82.1 |  0.006 % |
c |       252 |    5557    18748 |    2240     252    19966    79.2 |  0.000 % |
c |       477 |    5557    18748 |    2465     477    34035    71.4 |  0.000 % |
c |       816 |    5557    18748 |    2711     816    61162    75.0 |  0.000 % |
c |      1322 |    5557    18748 |    2982    1322   101974    77.1 |  0.000 % |
c |      2082 |    5557    18748 |    3280    2082   175391    84.2 |  0.000 % |
c |      3222 |    5557    18748 |    3609    3222   287281    89.2 |  0.000 % |
c |      4930 |    5557    18748 |    3969    3034   259982    85.7 |  0.000 % |
c |      7492 |    5557    18748 |    4366    3524   289629    82.2 |  0.000 % |
c ==============================================================================
c [1mFound solution: 386[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:37286     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8400 |   96057   230397 |   32019    4432   356590    80.5 |  0.000 % |
c |      8500 |   96057   230397 |   35220    4532   364865    80.5 |  0.033 % |
c |      8650 |   96057   230397 |   38742    4682   378388    80.8 |  0.033 % |
c |      8875 |   96057   230397 |   42617    4907   396581    80.8 |  0.033 % |
c |      9212 |   95957   230173 |   46879    5242   426881    81.4 |  0.117 % |
c |      9718 |   95957   230173 |   51566    5748   473258    82.3 |  0.117 % |
c |     10477 |   95693   229576 |   56723    6503   525068    80.7 |  0.354 % |
c |     11617 |   95557   229270 |   62395    7641   618601    81.0 |  0.471 % |
c |     13328 |   95043   228109 |   68635    9344   748898    80.1 |  0.930 % |
c ==============================================================================
c [1mFound solution: 385[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 |     14785 |   94953   227945 |   31651   10798   846694    78.4 |  0.930 % |
c |     14885 |   94821   227646 |   34816   10896   852362    78.2 |  1.250 % |
c |     15036 |   94631   227213 |   38297   11045   858525    77.7 |  1.429 % |
c |     15262 |   94522   226966 |   42127   11270   868709    77.1 |  1.526 % |
c |     15600 |   94381   226649 |   46340   11605   886187    76.4 |  1.650 % |
c |     16106 |   94381   226649 |   50974   12111   910884    75.2 |  1.650 % |
c |     16868 |   94296   226455 |   56071   12872   948129    73.7 |  1.731 % |
c |     18007 |   87327   210467 |   61678   13827  1002603    72.5 |  8.755 % |
c |     19715 |   70420   171508 |   67846   15155  1063112    70.1 | 25.707 % |
c |     22279 |   70145   170875 |   74631   17716  1260992    71.2 | 25.986 % |
c |     26123 |   69308   168944 |   82094   21549  1536795    71.3 | 26.844 % |
c |     31890 |   67591   164984 |   90303   27286  2013047    73.8 | 28.601 % |
c ==============================================================================
c [1mFound solution: 384[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 |     31964 |   67409   164557 |   22469   27357  2019680    73.8 | 28.601 % |
c ==============================================================================
c [1mFound solution: 383[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 |     32015 |   67254   164217 |   22418   27404  2022484    73.8 | 28.601 % |
c |     32116 |   67254   164217 |   24659   27505  2030536    73.8 | 28.997 % |
c |     32268 |   67254   164217 |   27125   27657  2042348    73.8 | 28.997 % |
c |     32495 |   67254   164217 |   29838   27884  2060099    73.9 | 28.997 % |
c |     32835 |   67254   164217 |   32822   28224  2090744    74.1 | 28.997 % |
c |     33341 |   67254   164217 |   36104   28730  2133402    74.3 | 28.997 % |
c |     34102 |   67163   164004 |   39714   29490  2192525    74.3 | 29.100 % |
c |     35241 |   66961   163537 |   43686   30617  2284942    74.6 | 29.311 % |
c ==============================================================================
c [1mFound solution: 382[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 |     35748 |   66910   163412 |   22303   31123  2329362    74.8 | 29.311 % |
c |     35848 |   65370   159898 |   24533   31148  2330020    74.8 | 30.818 % |
c |     35998 |   65370   159898 |   26986   31298  2335984    74.6 | 30.818 % |
c |     36226 |   65370   159898 |   29685   31526  2346743    74.4 | 30.818 % |
c |     36564 |   65267   159660 |   32653   31856  2372411    74.5 | 30.925 % |
c |     37070 |   65039   159134 |   35919   32357  2403597    74.3 | 31.159 % |
c |     37830 |   64928   158877 |   39511   33116  2472010    74.6 | 31.276 % |
c |     38971 |   64928   158877 |   43462   34257  2562081    74.8 | 31.276 % |
c ==============================================================================
c [1mFound solution: 380[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 |     39869 |   64955   158952 |   21651   35146  2636718    75.0 | 31.276 % |
c |     39970 |   64955   158952 |   23816   14544  1014169    69.7 | 31.315 % |
c |     40120 |   64955   158952 |   26197   14694  1028395    70.0 | 31.315 % |
c ==============================================================================
c [1mFound solution: 379[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 |     40300 |   64902   158853 |   21634   14869  1044700    70.3 | 31.315 % |
c |     40400 |   64777   158567 |   23797   14968  1052721    70.3 | 31.532 % |
c |     40551 |   64668   158314 |   26177   15117  1061468    70.2 | 31.649 % |
c |     40778 |   64668   158314 |   28794   15344  1080194    70.4 | 31.649 % |
c |     41118 |   64668   158314 |   31674   15684  1109723    70.8 | 31.649 % |
c |     41625 |   64533   158003 |   34841   16190  1147836    70.9 | 31.785 % |
c |     42384 |   64533   158003 |   38325   16949  1202940    71.0 | 31.785 % |
c |     43524 |   64317   157505 |   42158   18081  1287085    71.2 | 32.005 % |
c |     45236 |   63762   156220 |   46374   19784  1423217    71.9 | 32.588 % |
c ==============================================================================
c [1mFound solution: 378[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 |     45622 |   63379   155326 |   21126   20158  1453671    72.1 | 32.588 % |
c ==============================================================================
c [1mFound solution: 377[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 |     45625 |   63453   155517 |   21151   20161  1453797    72.1 | 32.588 % |
c |     45725 |   63358   155300 |   23266   20260  1461293    72.1 | 33.061 % |
c ==============================================================================
c [1mFound solution: 376[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 |     45735 |   63308   155173 |   21102   20262  1461545    72.1 | 33.061 % |
c ==============================================================================
c [1mFound solution: 375[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 |     45735 |   63372   155340 |   21124   20262  1461545    72.1 | 33.061 % |
c ==============================================================================
c [1mFound solution: 374[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 |     45736 |   63189   154907 |   21063   20251  1460032    72.1 | 33.061 % |
c ==============================================================================
c [1mFound solution: 373[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 |     45746 |   63158   154857 |   21052   20260  1460544    72.1 | 33.061 % |
c |     45846 |   63158   154857 |   23157   20360  1470626    72.2 | 33.371 % |
c |     45996 |   58865   144937 |   25472   20435  1471976    72.0 | 37.801 % |
c |     46222 |   58865   144937 |   28020   20661  1487864    72.0 | 37.801 % |
c |     46559 |   58865   144937 |   30822   20998  1512778    72.0 | 37.801 % |
c |     47066 |   58865   144937 |   33904   21505  1552817    72.2 | 37.801 % |
c |     47828 |   58522   144146 |   37294   22264  1617261    72.6 | 38.150 % |
c |     48969 |   57781   142450 |   41024   23369  1702329    72.8 | 38.864 % |
c |     50677 |   56140   138667 |   45126   24997  1822654    72.9 | 40.531 % |
c |     53239 |   55922   138163 |   49639   27557  1983234    72.0 | 40.757 % |
c |     57087 |   54889   135769 |   54603   31393  2311740    73.6 | 41.833 % |
c |     62856 |   54782   135520 |   60063   37160  2719970    73.2 | 41.950 % |
c |     71506 |   54055   133843 |   66070   45794  3364428    73.5 | 42.680 % |
c |     84483 |   46854   117148 |   72677   58522  4268403    72.9 | 50.147 % |
c |    103944 |   45910   114952 |   79944   77960  5637159    72.3 | 51.142 % |
c ==============================================================================
c [1mFound solution: 372[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 |    117336 |   42704   107475 |   14234   91075  6417950    70.5 | 51.142 % |
c |    117436 |   41696   105119 |   15657   18381   819075    44.6 | 55.617 % |
c |    117587 |   40811   103051 |   17223   18516   823401    44.5 | 56.577 % |
c |    117812 |   40811   103051 |   18945   18741   836104    44.6 | 56.577 % |
c |    118150 |   40811   103051 |   20839   19079   854302    44.8 | 56.577 % |
c |    118656 |   40692   102776 |   22923   19583   891767    45.5 | 56.699 % |
c |    119416 |   40561   102471 |   25216   20341   919948    45.2 | 56.838 % |
c |    120555 |   40561   102471 |   27738   21480  1016179    47.3 | 56.838 % |
c |    122263 |   40427   102159 |   30511   23187  1156486    49.9 | 56.977 % |
c |    124825 |   40314   101897 |   33563   25747  1340605    52.1 | 57.097 % |
c |    128670 |   40314   101897 |   36919   29592  1611670    54.5 | 57.097 % |
c |    134438 |   39736   100553 |   40611   35325  1996089    56.5 | 57.707 % |
c |    143087 |   38846    98482 |   44672   43949  2768642    63.0 | 58.641 % |
c |    156061 |   36613    93292 |   49139   56871  3565266    62.7 | 61.013 % |
c |    175523 |   34834    89140 |   54053   26570  1870663    70.4 | 62.925 % |
c |    204716 |   34711    88848 |   59458   55761  6245503   112.0 | 63.067 % |
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 x7#### 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.85 0.91 0.90 2/55 4781
Raw data (stat): 4781 (runsolver) D 4780 30927 30926 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 358796380 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 3225161850 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0002 s]
Raw data (loadavg): 0.88 0.92 0.90 2/55 4781
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 3493 0 0 0 992 7 0 0 25 0 1 0 358796380 16248832 3414 4294967295 134512640 134672761 3221224576 3221223744 134560828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3967 3414 603 41 0 3926 0
vsize: 15868
[startup+19.9999 s]
Raw data (loadavg): 0.89 0.92 0.90 2/55 4781
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 3772 0 0 0 1991 8 0 0 25 0 1 0 358796380 17457152 3693 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4262 3693 603 41 0 4221 0
vsize: 17048
[startup+30.0006 s]
Raw data (loadavg): 0.91 0.92 0.90 2/55 4781
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 3973 0 0 0 2989 9 0 0 25 0 1 0 358796380 18276352 3894 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4462 3894 603 41 0 4421 0
vsize: 17848
[startup+40.0003 s]
Raw data (loadavg): 0.92 0.92 0.90 2/55 4781
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 4173 0 0 0 3988 10 0 0 25 0 1 0 358796380 19193856 4094 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4686 4094 603 41 0 4645 0
vsize: 18744
[startup+50.0008 s]
Raw data (loadavg): 0.93 0.92 0.90 2/55 4781
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 4276 0 0 0 4988 10 0 0 25 0 1 0 358796380 19595264 4197 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4784 4197 603 41 0 4743 0
vsize: 19136
[startup+60.0008 s]
Raw data (loadavg): 0.94 0.93 0.90 2/55 4781
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 4329 0 0 0 5988 11 0 0 25 0 1 0 358796380 19865600 4250 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4850 4250 603 41 0 4809 0
vsize: 19400
[startup+70.0003 s]
Raw data (loadavg): 0.95 0.93 0.90 2/55 4781
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 4424 0 0 0 6987 11 0 0 25 0 1 0 358796380 20267008 4345 4294967295 134512640 134672761 3221224576 3221223712 134560716 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4948 4345 603 41 0 4907 0
vsize: 19792
[startup+80.0009 s]
Raw data (loadavg): 0.96 0.93 0.90 2/55 4781
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 4668 0 0 0 7987 12 0 0 25 0 1 0 358796380 21372928 4589 4294967295 134512640 134672761 3221224576 3221223712 134560697 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5218 4589 603 41 0 5177 0
vsize: 20872
[startup+90.0005 s]
Raw data (loadavg): 0.96 0.93 0.90 2/55 4781
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 4886 0 0 0 8986 13 0 0 25 0 1 0 358796380 22196224 4807 4294967295 134512640 134672761 3221224576 3221223744 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5419 4807 603 41 0 5378 0
vsize: 21676
[startup+100.001 s]
Raw data (loadavg): 1.04 0.95 0.91 2/55 4834
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 5086 0 0 0 9985 13 0 0 25 0 1 0 358796380 23007232 5007 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5617 5007 603 41 0 5576 0
vsize: 22468
[startup+110.002 s]
Raw data (loadavg): 1.04 0.95 0.91 2/55 4834
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 5285 0 0 0 10985 14 0 0 25 0 1 0 358796380 23875584 5206 4294967295 134512640 134672761 3221224576 3221223712 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5829 5206 603 41 0 5788 0
vsize: 23316
[startup+120.002 s]
Raw data (loadavg): 1.03 0.95 0.91 2/55 4834
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 5428 0 0 0 11985 14 0 0 25 0 1 0 358796380 24416256 5349 4294967295 134512640 134672761 3221224576 3221223744 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5961 5349 603 41 0 5920 0
vsize: 23844
[startup+130.002 s]
Raw data (loadavg): 1.03 0.95 0.91 2/55 4834
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 5605 0 0 0 12984 15 0 0 25 0 1 0 358796380 25219072 5526 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6157 5526 603 41 0 6116 0
vsize: 24628
[startup+140.002 s]
Raw data (loadavg): 1.02 0.95 0.91 2/55 4834
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 5804 0 0 0 13983 16 0 0 25 0 1 0 358796380 26038272 5725 4294967295 134512640 134672761 3221224576 3221223744 134560968 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6357 5725 603 41 0 6316 0
vsize: 25428
[startup+150.003 s]
Raw data (loadavg): 1.02 0.95 0.91 2/55 4836
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 5966 0 0 0 14983 17 0 0 25 0 1 0 358796380 26701824 5887 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6519 5887 603 41 0 6478 0
vsize: 26076
[startup+160.002 s]
Raw data (loadavg): 1.01 0.96 0.91 2/55 4836
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 6110 0 0 0 15982 17 0 0 25 0 1 0 358796380 27443200 6031 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6700 6031 603 41 0 6659 0
vsize: 26800
[startup+170.002 s]
Raw data (loadavg): 1.01 0.96 0.91 2/55 4838
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 6256 0 0 0 16982 18 0 0 25 0 1 0 358796380 28106752 6177 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6862 6177 603 41 0 6821 0
vsize: 27448
[startup+180.002 s]
Raw data (loadavg): 1.01 0.96 0.91 2/55 4838
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 6388 0 0 0 17982 18 0 0 25 0 1 0 358796380 28635136 6309 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6991 6309 603 41 0 6950 0
vsize: 27964
[startup+190.002 s]
Raw data (loadavg): 1.01 0.96 0.91 2/55 4838
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 6402 0 0 0 18982 18 0 0 25 0 1 0 358796380 28770304 6323 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7024 6323 603 41 0 6983 0
vsize: 28096
[startup+200.003 s]
Raw data (loadavg): 1.01 0.96 0.91 2/55 4838
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 6420 0 0 0 19983 18 0 0 25 0 1 0 358796380 28770304 6341 4294967295 134512640 134672761 3221224576 3221223744 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7024 6341 603 41 0 6983 0
vsize: 28096
[startup+210.007 s]
Raw data (loadavg): 1.00 0.96 0.91 3/69 4855
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 6439 0 0 0 20982 18 0 0 25 0 1 0 358796380 28934144 6360 4294967295 134512640 134672761 3221224576 3221223876 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7064 6360 603 41 0 7023 0
vsize: 28256
[startup+220.018 s]
Raw data (loadavg): 1.23 1.01 0.93 4/62 4869
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 6446 0 0 0 21979 18 0 0 25 0 1 0 358796380 28934144 6367 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7064 6367 603 41 0 7023 0
vsize: 28256
[startup+230.019 s]
Raw data (loadavg): 1.35 1.04 0.94 3/61 5114
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 6454 0 0 0 22975 19 0 0 25 0 1 0 358796380 28934144 6375 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7064 6375 603 41 0 7023 0
vsize: 28256
[startup+240.047 s]
Raw data (loadavg): 1.37 1.06 0.94 2/55 5157
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 6454 0 0 0 23978 19 0 0 25 0 1 0 358796380 28934144 6375 4294967295 134512640 134672761 3221224576 3221223744 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7064 6375 603 41 0 7023 0
vsize: 28256
[startup+250.047 s]
Raw data (loadavg): 1.31 1.06 0.94 2/55 5157
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 6461 0 0 0 24978 19 0 0 25 0 1 0 358796380 29097984 6382 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7104 6382 603 41 0 7063 0
vsize: 28416
[startup+260.048 s]
Raw data (loadavg): 1.26 1.05 0.94 2/55 5157
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 6474 0 0 0 25978 19 0 0 25 0 1 0 358796380 29097984 6395 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7104 6395 603 41 0 7063 0
vsize: 28416
[startup+270.048 s]
Raw data (loadavg): 1.22 1.05 0.94 2/55 5157
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 6474 0 0 0 26978 19 0 0 25 0 1 0 358796380 29097984 6395 4294967295 134512640 134672761 3221224576 3221223740 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7104 6395 603 41 0 7063 0
vsize: 28416
[startup+280.047 s]
Raw data (loadavg): 1.19 1.05 0.94 2/55 5157
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 6477 0 0 0 27979 19 0 0 25 0 1 0 358796380 29097984 6398 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7104 6398 603 41 0 7063 0
vsize: 28416
[startup+290.047 s]
Raw data (loadavg): 1.16 1.05 0.94 2/55 5157
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 6488 0 0 0 28979 19 0 0 25 0 1 0 358796380 29097984 6409 4294967295 134512640 134672761 3221224576 3221223712 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7104 6409 603 41 0 7063 0
vsize: 28416
[startup+300.048 s]
Raw data (loadavg): 1.13 1.05 0.94 2/55 5157
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 6555 0 0 0 29979 19 0 0 25 0 1 0 358796380 29429760 6476 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7185 6476 603 41 0 7144 0
vsize: 28740
[startup+310.048 s]
Raw data (loadavg): 1.11 1.04 0.94 2/55 5157
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 6687 0 0 0 30978 20 0 0 25 0 1 0 358796380 29966336 6608 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7316 6608 603 41 0 7275 0
vsize: 29264
[startup+320.048 s]
Raw data (loadavg): 1.10 1.04 0.94 2/55 5157
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 6817 0 0 0 31978 21 0 0 25 0 1 0 358796380 30494720 6738 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7445 6738 603 41 0 7404 0
vsize: 29780
[startup+330.049 s]
Raw data (loadavg): 1.08 1.04 0.94 2/55 5157
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 6960 0 0 0 32977 21 0 0 25 0 1 0 358796380 31027200 6881 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7575 6881 603 41 0 7534 0
vsize: 30300
[startup+340.049 s]
Raw data (loadavg): 1.07 1.04 0.94 2/55 5157
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 7108 0 0 0 33977 22 0 0 25 0 1 0 358796380 31698944 7029 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7739 7029 603 41 0 7698 0
vsize: 30956
[startup+350.05 s]
Raw data (loadavg): 1.06 1.04 0.94 2/55 5157
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 7245 0 0 0 34977 22 0 0 25 0 1 0 358796380 32231424 7166 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7869 7166 603 41 0 7828 0
vsize: 31476
[startup+360.05 s]
Raw data (loadavg): 1.05 1.03 0.94 2/55 5157
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 7380 0 0 0 35976 23 0 0 25 0 1 0 358796380 32817152 7301 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8012 7301 603 41 0 7971 0
vsize: 32048
[startup+370.05 s]
Raw data (loadavg): 1.04 1.03 0.94 2/55 5157
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 7514 0 0 0 36976 23 0 0 25 0 1 0 358796380 33353728 7435 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8143 7435 603 41 0 8102 0
vsize: 32572
[startup+380.049 s]
Raw data (loadavg): 1.03 1.03 0.94 2/55 5157
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 7638 0 0 0 37976 23 0 0 25 0 1 0 358796380 33886208 7559 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8273 7559 603 41 0 8232 0
vsize: 33092
[startup+390.049 s]
Raw data (loadavg): 1.03 1.03 0.94 2/55 5157
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 7784 0 0 0 38976 24 0 0 25 0 1 0 358796380 34553856 7705 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8436 7705 603 41 0 8395 0
vsize: 33744
[startup+400.05 s]
Raw data (loadavg): 1.02 1.03 0.94 2/55 5157
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 7882 0 0 0 39976 24 0 0 25 0 1 0 358796380 34959360 7803 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8535 7803 603 41 0 8494 0
vsize: 34140
[startup+410.05 s]
Raw data (loadavg): 1.02 1.03 0.94 2/55 5157
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 7973 0 0 0 40975 25 0 0 25 0 1 0 358796380 35299328 7894 4294967295 134512640 134672761 3221224576 3221223744 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8618 7894 603 41 0 8577 0
vsize: 34472
[startup+420.05 s]
Raw data (loadavg): 1.02 1.03 0.94 2/55 5157
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 8058 0 0 0 41975 25 0 0 25 0 1 0 358796380 35700736 7979 4294967295 134512640 134672761 3221224576 3221223744 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8716 7979 603 41 0 8675 0
vsize: 34864
[startup+430.05 s]
Raw data (loadavg): 1.01 1.02 0.94 2/55 5157
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 8177 0 0 0 42975 25 0 0 25 0 1 0 358796380 36098048 8098 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8813 8098 603 41 0 8772 0
vsize: 35252
[startup+440.049 s]
Raw data (loadavg): 1.01 1.02 0.94 2/55 5157
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 8271 0 0 0 43975 26 0 0 25 0 1 0 358796380 36503552 8192 4294967295 134512640 134672761 3221224576 3221223744 134561400 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8912 8192 603 41 0 8871 0
vsize: 35648
[startup+450.05 s]
Raw data (loadavg): 1.01 1.02 0.94 2/55 5157
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 8398 0 0 0 44975 26 0 0 25 0 1 0 358796380 37076992 8319 4294967295 134512640 134672761 3221224576 3221223744 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9052 8319 603 41 0 9011 0
vsize: 36208
[startup+460.05 s]
Raw data (loadavg): 1.01 1.02 0.94 2/55 5157
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 8507 0 0 0 45975 27 0 0 25 0 1 0 358796380 37478400 8428 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9150 8428 603 41 0 9109 0
vsize: 36600
[startup+470.051 s]
Raw data (loadavg): 1.00 1.02 0.94 2/55 5157
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 8620 0 0 0 46974 27 0 0 25 0 1 0 358796380 38006784 8541 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9279 8541 603 41 0 9238 0
vsize: 37116
[startup+480.052 s]
Raw data (loadavg): 1.00 1.02 0.94 2/55 5157
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 8743 0 0 0 47973 28 0 0 25 0 1 0 358796380 38404096 8664 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9376 8664 603 41 0 9335 0
vsize: 37504
[startup+490.052 s]
Raw data (loadavg): 1.00 1.02 0.94 2/55 5157
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 8866 0 0 0 48973 29 0 0 25 0 1 0 358796380 38944768 8787 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9508 8787 603 41 0 9467 0
vsize: 38032
[startup+500.053 s]
Raw data (loadavg): 1.00 1.02 0.94 2/55 5157
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 8979 0 0 0 49972 29 0 0 25 0 1 0 358796380 39477248 8900 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9638 8900 603 41 0 9597 0
vsize: 38552
[startup+510.052 s]
Raw data (loadavg): 1.00 1.02 0.94 2/55 5157
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 9092 0 0 0 50972 30 0 0 25 0 1 0 358796380 40148992 9013 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9802 9013 603 41 0 9761 0
vsize: 39208
[startup+520.052 s]
Raw data (loadavg): 1.00 1.02 0.94 2/55 5157
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 9235 0 0 0 51971 30 0 0 25 0 1 0 358796380 40701952 9156 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9937 9156 603 41 0 9896 0
vsize: 39748
[startup+530.053 s]
Raw data (loadavg): 1.00 1.02 0.94 2/55 5157
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 9335 0 0 0 52972 31 0 0 25 0 1 0 358796380 41107456 9256 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10036 9256 603 41 0 9995 0
vsize: 40144
[startup+540.054 s]
Raw data (loadavg): 1.00 1.01 0.94 2/55 5157
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 9411 0 0 0 53971 31 0 0 25 0 1 0 358796380 41508864 9332 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10134 9332 603 41 0 10093 0
vsize: 40536
[startup+550.054 s]
Raw data (loadavg): 1.00 1.01 0.94 2/55 5157
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 9492 0 0 0 54971 31 0 0 25 0 1 0 358796380 41910272 9413 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10232 9413 603 41 0 10191 0
vsize: 40928
[startup+560.054 s]
Raw data (loadavg): 1.00 1.01 0.94 2/55 5157
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 9556 0 0 0 55969 32 0 0 25 0 1 0 358796380 42045440 9477 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10265 9477 603 41 0 10224 0
vsize: 41060
[startup+570.054 s]
Raw data (loadavg): 1.00 1.01 0.94 2/55 5159
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 9641 0 0 0 56969 33 0 0 25 0 1 0 358796380 42446848 9562 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10363 9562 603 41 0 10322 0
vsize: 41452
[startup+580.055 s]
Raw data (loadavg): 1.00 1.01 0.94 2/55 5159
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 9715 0 0 0 57969 33 0 0 25 0 1 0 358796380 42713088 9636 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10428 9636 603 41 0 10387 0
vsize: 41712
[startup+590.055 s]
Raw data (loadavg): 1.00 1.01 0.94 2/55 5159
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 9806 0 0 0 58969 33 0 0 25 0 1 0 358796380 43118592 9727 4294967295 134512640 134672761 3221224576 3221223744 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10527 9727 603 41 0 10486 0
vsize: 42108
[startup+600.056 s]
Raw data (loadavg): 1.00 1.01 0.94 2/55 5159
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 9890 0 0 0 59968 34 0 0 25 0 1 0 358796380 43528192 9811 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10627 9811 603 41 0 10586 0
vsize: 42508
[startup+610.056 s]
Raw data (loadavg): 1.00 1.01 0.94 2/55 5159
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 9970 0 0 0 60968 35 0 0 25 0 1 0 358796380 43798528 9891 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10693 9891 603 41 0 10652 0
vsize: 42772
[startup+620.056 s]
Raw data (loadavg): 1.00 1.01 0.94 2/55 5159
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 10058 0 0 0 61967 35 0 0 25 0 1 0 358796380 44204032 9979 4294967295 134512640 134672761 3221224576 3221223744 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10792 9979 603 41 0 10751 0
vsize: 43168
[startup+630.057 s]
Raw data (loadavg): 1.00 1.01 0.94 2/55 5159
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 10138 0 0 0 62967 36 0 0 25 0 1 0 358796380 44531712 10059 4294967295 134512640 134672761 3221224576 3221223744 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10872 10059 603 41 0 10831 0
vsize: 43488
[startup+640.057 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 5159
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 10269 0 0 0 63967 36 0 0 25 0 1 0 358796380 45068288 10190 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11003 10190 603 41 0 10962 0
vsize: 44012
[startup+650.057 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 5159
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 10301 0 0 0 64967 36 0 0 25 0 1 0 358796380 45244416 10222 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11046 10222 603 41 0 11005 0
vsize: 44184
[startup+660.058 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 5159
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 10350 0 0 0 65967 37 0 0 25 0 1 0 358796380 45379584 10271 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11079 10271 603 41 0 11038 0
vsize: 44316
[startup+670.057 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 5159
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 10407 0 0 0 66966 37 0 0 25 0 1 0 358796380 45682688 10328 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11153 10328 603 41 0 11112 0
vsize: 44612
[startup+680.058 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 5159
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 10473 0 0 0 67966 38 0 0 25 0 1 0 358796380 45944832 10394 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11217 10394 603 41 0 11176 0
vsize: 44868
[startup+690.058 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 5159
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 10537 0 0 0 68966 38 0 0 25 0 1 0 358796380 46211072 10458 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11282 10458 603 41 0 11241 0
vsize: 45128
[startup+700.057 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 5159
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 10601 0 0 0 69966 38 0 0 25 0 1 0 358796380 46481408 10522 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11348 10522 603 41 0 11307 0
vsize: 45392
[startup+710.058 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 5159
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 10664 0 0 0 70966 38 0 0 25 0 1 0 358796380 46759936 10585 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11416 10585 603 41 0 11375 0
vsize: 45664
[startup+720.058 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 5159
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 10731 0 0 0 71965 39 0 0 25 0 1 0 358796380 47034368 10652 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11483 10652 603 41 0 11442 0
vsize: 45932
[startup+730.058 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 5159
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 10795 0 0 0 72965 39 0 0 25 0 1 0 358796380 47202304 10716 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11524 10716 603 41 0 11483 0
vsize: 46096
[startup+740.058 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 5159
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 10850 0 0 0 73965 40 0 0 25 0 1 0 358796380 47464448 10771 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11588 10771 603 41 0 11547 0
vsize: 46352
[startup+750.058 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 5159
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 10903 0 0 0 74965 40 0 0 25 0 1 0 358796380 47599616 10824 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11621 10824 603 41 0 11580 0
vsize: 46484
[startup+760.057 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 5159
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 10987 0 0 0 75965 40 0 0 25 0 1 0 358796380 48037888 10908 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11728 10908 603 41 0 11687 0
vsize: 46912
[startup+770.058 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 5159
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 11048 0 0 0 76964 41 0 0 25 0 1 0 358796380 48259072 10969 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11782 10969 603 41 0 11741 0
vsize: 47128
[startup+780.058 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 5159
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 11048 0 0 0 77964 41 0 0 25 0 1 0 358796380 48259072 10969 4294967295 134512640 134672761 3221224576 3221223728 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11782 10969 603 41 0 11741 0
vsize: 47128
[startup+790.058 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 5159
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 11048 0 0 0 78964 41 0 0 25 0 1 0 358796380 48259072 10969 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11782 10969 603 41 0 11741 0
vsize: 47128
[startup+800.058 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 5159
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 11048 0 0 0 79964 41 0 0 25 0 1 0 358796380 48259072 10969 4294967295 134512640 134672761 3221224576 3221223744 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11782 10969 603 41 0 11741 0
vsize: 47128
[startup+810.058 s]
Raw data (loadavg): 1.00 1.00 0.94 3/55 5159
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 11048 0 0 0 80964 41 0 0 25 0 1 0 358796380 48259072 10969 4294967295 134512640 134672761 3221224576 3221223744 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11782 10969 603 41 0 11741 0
vsize: 47128
[startup+820.058 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 5159
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 11048 0 0 0 81964 41 0 0 25 0 1 0 358796380 48259072 10969 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11782 10969 603 41 0 11741 0
vsize: 47128
[startup+830.06 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 5159
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 11048 0 0 0 82964 41 0 0 25 0 1 0 358796380 48259072 10969 4294967295 134512640 134672761 3221224576 3221223744 134559068 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11782 10969 603 41 0 11741 0
vsize: 47128
[startup+840.06 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 5159
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 11048 0 0 0 83965 41 0 0 25 0 1 0 358796380 48259072 10969 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11782 10969 603 41 0 11741 0
vsize: 47128
[startup+850.061 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 5159
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 11048 0 0 0 84965 41 0 0 25 0 1 0 358796380 48259072 10969 4294967295 134512640 134672761 3221224576 3221223776 134557887 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11782 10969 603 41 0 11741 0
vsize: 47128
[startup+860.06 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 5159
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 11048 0 0 0 85965 42 0 0 25 0 1 0 358796380 48259072 10969 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11782 10969 603 41 0 11741 0
vsize: 47128
[startup+870.06 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 5159
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 11048 0 0 0 86964 42 0 0 25 0 1 0 358796380 48259072 10969 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11782 10969 603 41 0 11741 0
vsize: 47128
[startup+880.061 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 5159
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 11048 0 0 0 87964 42 0 0 25 0 1 0 358796380 48259072 10969 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11782 10969 603 41 0 11741 0
vsize: 47128
[startup+890.062 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 5159
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 11048 0 0 0 88964 42 0 0 25 0 1 0 358796380 48259072 10969 4294967295 134512640 134672761 3221224576 3221223748 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11782 10969 603 41 0 11741 0
vsize: 47128
[startup+900.061 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 5159
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 11048 0 0 0 89964 42 0 0 25 0 1 0 358796380 48259072 10969 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11782 10969 603 41 0 11741 0
vsize: 47128
[startup+910.062 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 5159
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 11048 0 0 0 90964 42 0 0 25 0 1 0 358796380 48259072 10969 4294967295 134512640 134672761 3221224576 3221223744 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11782 10969 603 41 0 11741 0
vsize: 47128
[startup+920.061 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 5159
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 11048 0 0 0 91964 43 0 0 25 0 1 0 358796380 48259072 10969 4294967295 134512640 134672761 3221224576 3221223744 134560964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11782 10969 603 41 0 11741 0
vsize: 47128
[startup+930.062 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 5159
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 11048 0 0 0 92964 43 0 0 25 0 1 0 358796380 48259072 10969 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11782 10969 603 41 0 11741 0
vsize: 47128
[startup+940.062 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 5159
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 11048 0 0 0 93964 43 0 0 25 0 1 0 358796380 48259072 10969 4294967295 134512640 134672761 3221224576 3221223760 134559330 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11782 10969 603 41 0 11741 0
vsize: 47128
[startup+950.062 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 5159
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 11048 0 0 0 94964 43 0 0 25 0 1 0 358796380 48259072 10969 4294967295 134512640 134672761 3221224576 3221223712 134560604 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11782 10969 603 41 0 11741 0
vsize: 47128
[startup+960.062 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 5159
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 11049 0 0 0 95964 43 0 0 25 0 1 0 358796380 48259072 10970 4294967295 134512640 134672761 3221224576 3221223680 134554926 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11782 10970 603 41 0 11741 0
vsize: 47128
[startup+970.062 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 5159
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 11049 0 0 0 96964 44 0 0 25 0 1 0 358796380 48259072 10970 4294967295 134512640 134672761 3221224576 3221223680 134560326 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11782 10970 603 41 0 11741 0
vsize: 47128
[startup+980.062 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 5159
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 11049 0 0 0 97964 44 0 0 25 0 1 0 358796380 48259072 10970 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11782 10970 603 41 0 11741 0
vsize: 47128
[startup+990.063 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 5159
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 11049 0 0 0 98964 44 0 0 25 0 1 0 358796380 48259072 10970 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11782 10970 603 41 0 11741 0
vsize: 47128
[startup+1000.06 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 5159
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 11049 0 0 0 99964 44 0 0 25 0 1 0 358796380 48259072 10970 4294967295 134512640 134672761 3221224576 3221223776 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11782 10970 603 41 0 11741 0
vsize: 47128
[startup+1010.06 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 5159
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 11049 0 0 0 100964 44 0 0 25 0 1 0 358796380 48259072 10970 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11782 10970 603 41 0 11741 0
vsize: 47128
[startup+1020.06 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 5159
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 11049 0 0 0 101964 44 0 0 25 0 1 0 358796380 48259072 10970 4294967295 134512640 134672761 3221224576 3221223744 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11782 10970 603 41 0 11741 0
vsize: 47128
[startup+1030.06 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 5159
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 11049 0 0 0 102964 44 0 0 25 0 1 0 358796380 48254976 10970 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11781 10970 603 41 0 11740 0
vsize: 47124
[startup+1040.06 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 5159
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 11049 0 0 0 103964 45 0 0 25 0 1 0 358796380 48254976 10970 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11781 10970 603 41 0 11740 0
vsize: 47124
[startup+1050.06 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 5159
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 11049 0 0 0 104964 45 0 0 25 0 1 0 358796380 48254976 10970 4294967295 134512640 134672761 3221224576 3221223776 134557800 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11781 10970 603 41 0 11740 0
vsize: 47124
[startup+1060.06 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 5159
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 11049 0 0 0 105964 45 0 0 25 0 1 0 358796380 48254976 10970 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11781 10970 603 41 0 11740 0
vsize: 47124
[startup+1070.06 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 5159
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 11050 0 0 0 106964 45 0 0 25 0 1 0 358796380 48254976 10971 4294967295 134512640 134672761 3221224576 3221223744 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11781 10971 603 41 0 11740 0
vsize: 47124
[startup+1080.06 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 5159
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 11050 0 0 0 107964 45 0 0 25 0 1 0 358796380 48254976 10971 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11781 10971 603 41 0 11740 0
vsize: 47124
[startup+1090.06 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 5159
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 11052 0 0 0 108964 45 0 0 25 0 1 0 358796380 48254976 10973 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11781 10973 603 41 0 11740 0
vsize: 47124
[startup+1100.06 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 5159
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 11052 0 0 0 109964 45 0 0 25 0 1 0 358796380 48254976 10973 4294967295 134512640 134672761 3221224576 3221223680 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11781 10973 603 41 0 11740 0
vsize: 47124
[startup+1110.06 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 5159
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 11052 0 0 0 110964 46 0 0 25 0 1 0 358796380 48254976 10973 4294967295 134512640 134672761 3221224576 3221223680 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11781 10973 603 41 0 11740 0
vsize: 47124
[startup+1120.06 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 5159
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 11052 0 0 0 111964 46 0 0 25 0 1 0 358796380 48254976 10973 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11781 10973 603 41 0 11740 0
vsize: 47124
[startup+1130.06 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 5159
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 11052 0 0 0 112964 46 0 0 25 0 1 0 358796380 48254976 10973 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11781 10973 603 41 0 11740 0
vsize: 47124
[startup+1140.06 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 5159
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 11052 0 0 0 113964 46 0 0 25 0 1 0 358796380 48254976 10973 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11781 10973 603 41 0 11740 0
vsize: 47124
[startup+1150.06 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 5159
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 11052 0 0 0 114964 46 0 0 25 0 1 0 358796380 48254976 10973 4294967295 134512640 134672761 3221224576 3221223760 134558883 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11781 10973 603 41 0 11740 0
vsize: 47124
[startup+1160.06 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 5159
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 11052 0 0 0 115964 46 0 0 25 0 1 0 358796380 48254976 10973 4294967295 134512640 134672761 3221224576 3221223712 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11781 10973 603 41 0 11740 0
vsize: 47124
[startup+1170.06 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 5159
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 11052 0 0 0 116964 46 0 0 25 0 1 0 358796380 48254976 10973 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11781 10973 603 41 0 11740 0
vsize: 47124
[startup+1180.07 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 5159
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 11052 0 0 0 117964 46 0 0 25 0 1 0 358796380 48254976 10973 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11781 10973 603 41 0 11740 0
vsize: 47124
[startup+1190.06 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 5159
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 11052 0 0 0 118964 46 0 0 25 0 1 0 358796380 48254976 10973 4294967295 134512640 134672761 3221224576 3221223680 134560194 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11781 10973 603 41 0 11740 0
vsize: 47124
[startup+1200.06 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 5159
Raw data (stat): 4781 (minisat+) R 4780 30927 30926 0 -1 0 11052 0 0 0 119964 47 0 0 25 0 1 0 358796380 48254976 10973 4294967295 134512640 134672761 3221224576 3221223712 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11781 10973 603 41 0 11740 0
vsize: 47124
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.09 s]
Raw data (loadavg): 1.00 1.00 0.94 1/55 5159
Raw data (stat): 4781 (minisat+) Z 4780 30927 30926 0 -1 12 11055 0 0 0 119964 49 0 0 25 0 1 0 358796380 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 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.09
CPU time (s): 1200.14
CPU user time (s): 1199.65
CPU system time (s): 0.491925
CPU usage (%): 100.004
Max. virtual memory (Kb): 47128
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####