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/mps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-p0291.opb
MD5SUM	1d9168a9335e29df835d07b0bdf2adea
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	10447498
Optimality of the best value was proved	NO
Number of terms in the objective function	289
Biggest coefficient in the objective function	80000000
Number of bits for the biggest coefficient in the objective function	27
Sum of the numbers in the objective function	686518451
Number of bits of the sum of numbers in the objective function	30
Biggest number in a constraint	80000000
Number of bits of the biggest number in a constraint	27
Biggest sum of numbers in a constraint	686518451
Number of bits of the biggest sum of numbers	30
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	0.333948
Number of variables	291
Total number of constraints	543
Number of constraints which are clauses	189
Number of constraints which are cardinality constraints (but not clauses)	295
Number of constraints which are nor clauses,nor cardinality constraints	59
Minimum length of a constraint	1
Maximum length of a constraint	53
Trace number 15600

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc22 THE 2005-04-21 05:08:49 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=17144 boxname=wulflinc22 idbench=1319 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  1d9168a9335e29df835d07b0bdf2adea  /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-13-7-p0291.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-13-7-p0291.opb /oldhome/oroussel/tmp/wulflinc22/normalized-mps-v2-13-7-p0291.opb
IDLAUNCH: 17144
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.031
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.031
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:        728964 kB
Buffers:         26992 kB
Cached:         248588 kB
SwapCached:         24 kB
Active:          28668 kB
Inactive:       249560 kB
HighTotal:      131008 kB
HighFree:        18592 kB
LowTotal:       903652 kB
LowFree:        710372 kB
SwapTotal:     2097892 kB
SwapFree:      2097660 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           6640 kB
Slab:            21852 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 05:28:51 (client local time) WITH STATUS 10 IN 1200.22 SECONDS
stats: 17144 7 1200.22 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 205 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): .............................................................................................................................................................................................sssss
c ---[ 144]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 139]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  14]---> Adder-cost: 147   maxlim: 485   bits: 10/9
c ---[  13]---> Adder-cost: 117   maxlim: 539   bits: 11/10
c ---[  11]---> Adder-cost: 104   maxlim: 51   bits: 7/6
c ---[  10]---> Adder-cost: 104   maxlim: 51   bits: 7/6
c ---[   9]---> Adder-cost: 104   maxlim: 51   bits: 7/6
c ---[   8]---> Adder-cost: 24   maxlim: 11   bits: 5/4
c ---[   7]---> Adder-cost: 15   maxlim: 7   bits: 4/3
c ---[   6]---> Adder-cost: 31   maxlim: 15   bits: 5/4
c ---[   5]---> Adder-cost: 56   maxlim: 27   bits: 6/5
c ---[   4]---> Adder-cost: 24   maxlim: 19   bits: 6/5
c ---[   3]---> Adder-cost: 59   maxlim: 55   bits: 7/6
c ---[   2]---> Adder-cost: 81   maxlim: 87   bits: 8/7
c ---[   1]---> Adder-cost: 91   maxlim: 159   bits: 9/8
c ---[   0]---> Adder-cost: 18   maxlim: 19   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    6296    22114 |    2098       0        0     nan |  0.000 % |
c |       100 |    6296    22114 |    2307     100      557     5.6 |  3.157 % |
c |       251 |    6296    22114 |    2538     251     1772     7.1 |  3.157 % |
c ==============================================================================
c [1mFound solution: 52128157[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 4008   maxlim: 424299904   bits: 29/29
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       471 |   34009   121116 |   11336     470     3736     7.9 |  3.157 % |
c |       571 |   34009   121116 |   12469     570     4461     7.8 |  1.154 % |
c |       721 |   33984   121033 |   13716     715     5649     7.9 |  1.230 % |
c |       946 |   33926   120831 |   15088     925     7236     7.8 |  1.381 % |
c |      1284 |   33918   120805 |   16597    1261    11375     9.0 |  1.419 % |
c |      1793 |   33918   120805 |   18256    1770    16948     9.6 |  1.419 % |
c |      2552 |   33918   120805 |   20082    2529    30167    11.9 |  1.419 % |
c |      3691 |   33918   120805 |   22090    3668    54647    14.9 |  1.419 % |
c |      5400 |   33909   120774 |   24299    5376    90480    16.8 |  1.438 % |
c |      7966 |   33909   120774 |   26729    7942   166044    20.9 |  1.438 % |
c |     11810 |   33909   120774 |   29402   11786   328844    27.9 |  1.438 % |
c |     17576 |   33909   120774 |   32342   17552   587265    33.5 |  1.438 % |
c |     26226 |   33882   120677 |   35577   26200   991686    37.9 |  1.457 % |
c |     39200 |   33882   120677 |   39134   39174  2081877    53.1 |  1.457 % |
c |     58662 |   33861   120602 |   43048   32882  2757349    83.9 |  1.476 % |
c |     87854 |   33861   120602 |   47353   31925  2294066    71.9 |  1.476 % |
c ==============================================================================
c [1mFound solution: 51953164[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 2666   maxlim: 386959717   bits: 29/29
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     95344 |   52322   186563 |   17440   39413  2669923    67.7 |  1.476 % |
c |     95446 |   52322   186563 |   19184   15184   805936    53.1 |  1.155 % |
c |     95596 |   52322   186563 |   21102   15334   806853    52.6 |  1.155 % |
c |     95821 |   52322   186563 |   23212   15559   812645    52.2 |  1.155 % |
c |     96161 |   52322   186563 |   25533   15899   821655    51.7 |  1.156 % |
c |     96668 |   52322   186563 |   28087   16406   833043    50.8 |  1.155 % |
c |     97427 |   52322   186563 |   30896   17165   870249    50.7 |  1.155 % |
c |     98566 |   52322   186563 |   33985   18304   919224    50.2 |  1.155 % |
c |    100275 |   52322   186563 |   37384   20013   969974    48.5 |  1.155 % |
c |    102837 |   52322   186563 |   41122   22575  1128408    50.0 |  1.155 % |
c |    106681 |   52322   186563 |   45234   26419  1344605    50.9 |  1.155 % |
c |    112449 |   52322   186563 |   49758   32187  1751316    54.4 |  1.155 % |
c |    121098 |   52322   186563 |   54734   40836  2149541    52.6 |  1.155 % |
c ==============================================================================
c [1mFound solution: 48598200[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 390314681   bits: 29/29
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    127352 |   52359   186889 |   17453   47090  2617772    55.6 |  1.155 % |
c |    127452 |   52359   186889 |   19198   15669   758136    48.4 |  1.316 % |
c |    127603 |   52359   186889 |   21118   15820   760395    48.1 |  1.316 % |
c |    127830 |   52359   186889 |   23229   16047   769122    47.9 |  1.316 % |
c |    128167 |   52359   186889 |   25552   16384   778109    47.5 |  1.316 % |
c |    128674 |   52359   186889 |   28108   16891   790756    46.8 |  1.316 % |
c |    129433 |   52359   186889 |   30919   17650   813409    46.1 |  1.316 % |
c |    130572 |   52359   186889 |   34010   18789   865561    46.1 |  1.316 % |
c |    132282 |   52359   186889 |   37412   20499   938830    45.8 |  1.316 % |
c |    134845 |   52359   186889 |   41153   23062  1064072    46.1 |  1.316 % |
c |    138691 |   52359   186889 |   45268   26908  1247411    46.4 |  1.316 % |
c |    144457 |   52359   186889 |   49795   32674  1629064    49.9 |  1.316 % |
c |    153106 |   52359   186889 |   54774   41323  1964251    47.5 |  1.316 % |
c |    166082 |   52359   186889 |   60252   54299  4087971    75.3 |  1.316 % |
c |    185543 |   52359   186889 |   66277   26698  1814676    68.0 |  1.316 % |
c |    214736 |   52359   186889 |   72905   55891  5612823   100.4 |  1.316 % |
c |    258526 |   52359   186889 |   80196   35150  5426643   154.4 |  1.316 % |
c ==============================================================================
c [1mFound solution: 44547717[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 1378   maxlim: 346365164   bits: 29/29
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    321806 |   61657   220229 |   20552   29509  4096249   138.8 |  1.316 % |
c |    321906 |   61642   220180 |   22607   13297  1753350   131.9 |  1.430 % |
c |    322056 |   61642   220180 |   24867   13447  1754299   130.5 |  1.430 % |
c |    322281 |   61642   220180 |   27354   13672  1755821   128.4 |  1.430 % |
c |    322618 |   61642   220180 |   30090   14009  1758564   125.5 |  1.430 % |
c |    323124 |   61642   220180 |   33099   14515  1765135   121.6 |  1.430 % |
c |    323883 |   61642   220180 |   36409   15274  1786015   116.9 |  1.430 % |
c |    325022 |   61642   220180 |   40050   16413  1802314   109.8 |  1.430 % |
c |    326731 |   61642   220180 |   44055   18122  1840433   101.6 |  1.430 % |
c |    329293 |   61550   219852 |   48460   20678  1908909    92.3 |  1.494 % |
c |    333137 |   61550   219852 |   53306   24522  2028673    82.7 |  1.494 % |
c |    338904 |   61550   219852 |   58637   30289  2315549    76.4 |  1.494 % |
c |    347553 |   61541   219825 |   64500   38937  2744062    70.5 |  1.516 % |
c |    360527 |   61505   219697 |   70951   51908  3464505    66.7 |  1.537 % |
c ==============================================================================
c [1mFound solution: 44546226[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 2190   maxlim: 345462755   bits: 29/29
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    368761 |   76650   273861 |   25550   60142  4051496    67.4 |  1.537 % |
c |    368862 |   76650   273861 |   28105   15623  1014216    64.9 |  1.417 % |
c |    369012 |   76650   273861 |   30915   15773  1016609    64.5 |  1.417 % |
c |    369239 |   76650   273861 |   34007   16000  1020990    63.8 |  1.417 % |
c |    369576 |   76650   273861 |   37407   16337  1028496    63.0 |  1.417 % |
c |    370082 |   76650   273861 |   41148   16843  1047728    62.2 |  1.417 % |
c |    370843 |   76650   273861 |   45263   17604  1071639    60.9 |  1.417 % |
c |    371984 |   76650   273861 |   49789   18745  1104286    58.9 |  1.417 % |
c |    373692 |   76650   273861 |   54768   20453  1205464    58.9 |  1.417 % |
c |    376255 |   76650   273861 |   60245   23016  1298019    56.4 |  1.417 % |
c ==============================================================================
c [1mFound solution: 15518352[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 1246   maxlim: 130490629   bits: 28/27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    379374 |   69349   248002 |   23116   21198  1073718    50.7 |  1.417 % |
c |    379474 |   69349   248002 |   25427   21298  1074346    50.4 | 10.544 % |
c |    379624 |   69349   248002 |   27970   21448  1092902    51.0 | 10.544 % |
c |    379849 |   69349   248002 |   30767   21673  1094831    50.5 | 10.544 % |
c |    380188 |   69349   248002 |   33844   22012  1101495    50.0 | 10.544 % |
c |    380696 |   69343   247985 |   37228   22519  1109501    49.3 | 10.552 % |
c |    381455 |   69304   247856 |   40951   23263  1123898    48.3 | 10.591 % |
c |    382595 |   69304   247856 |   45046   24403  1162832    47.7 | 10.591 % |
c |    384303 |   69296   247830 |   49551   26052  1181253    45.3 | 10.606 % |
c ==============================================================================
c [1mFound solution: 15514737[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 2072   maxlim: 64733882   bits: 27/26
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    386574 |   83675   299278 |   27891   28323  1246825    44.0 | 10.606 % |
c |    386674 |   83675   299278 |   30680   28423  1247441    43.9 |  9.235 % |
c |    386827 |   83675   299278 |   33748   28576  1249740    43.7 |  9.235 % |
c |    387054 |   83675   299278 |   37122   28803  1254983    43.6 |  9.235 % |
c |    387392 |   83675   299278 |   40835   29141  1264445    43.4 |  9.235 % |
c |    387900 |   83675   299278 |   44918   29649  1274378    43.0 |  9.235 % |
c |    388660 |   83675   299278 |   49410   30409  1297331    42.7 |  9.235 % |
c |    389799 |   83675   299278 |   54351   31548  1340124    42.5 |  9.235 % |
c |    391508 |   83675   299278 |   59786   33257  1414471    42.5 |  9.235 % |
c |    394071 |   83675   299278 |   65765   35820  1491616    41.6 |  9.235 % |
c |    397915 |   83675   299278 |   72342   39664  1978678    49.9 |  9.235 % |
c |    403682 |   83675   299278 |   79576   45431  2241219    49.3 |  9.235 % |
c ==============================================================================
c [1mFound solution: 15510588[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 64738031   bits: 27/26
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    407778 |   83689   299429 |   27896   49527  2491096    50.3 |  9.235 % |
c |    407878 |   83689   299429 |   30685   15595   809103    51.9 |  9.271 % |
c |    408028 |   83689   299429 |   33754   15745   810840    51.5 |  9.271 % |
c |    408255 |   83689   299429 |   37129   15972   817040    51.2 |  9.271 % |
c |    408592 |   83689   299429 |   40842   16309   827614    50.7 |  9.271 % |
c |    409099 |   83689   299429 |   44926   16816   841455    50.0 |  9.271 % |
c |    409860 |   83689   299429 |   49419   17577   861305    49.0 |  9.271 % |
c |    411000 |   83689   299429 |   54361   18717   904651    48.3 |  9.271 % |
c |    412708 |   83689   299429 |   59797   20425   939443    46.0 |  9.271 % |
c |    415270 |   83689   299429 |   65777   22987  1173211    51.0 |  9.271 % |
c |    419114 |   83689   299429 |   72355   26831  1277488    47.6 |  9.271 % |
c ==============================================================================
c [1mFound solution: 14953888[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 65294731   bits: 27/26
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    421687 |   83704   299588 |   27901   29404  1414926    48.1 |  9.271 % |
c |    421788 |   83704   299588 |   30691   14803   537064    36.3 |  9.319 % |
c |    421938 |   83704   299588 |   33760   14953   538987    36.0 |  9.319 % |
c |    422163 |   83704   299588 |   37136   15178   544374    35.9 |  9.319 % |
c |    422501 |   83704   299588 |   40849   15516   551368    35.5 |  9.319 % |
c |    423007 |   83704   299588 |   44934   16022   565299    35.3 |  9.319 % |
c |    423766 |   83704   299588 |   49428   16781   590362    35.2 |  9.319 % |
c |    424906 |   83704   299588 |   54371   17921   673819    37.6 |  9.319 % |
c |    426615 |   83704   299588 |   59808   19630   719672    36.7 |  9.319 % |
c |    429178 |   83696   299563 |   65789   22192   824706    37.2 |  9.332 % |
c |    433023 |   83696   299563 |   72368   26037   969772    37.2 |  9.332 % |
c |    438790 |   83690   299543 |   79604   31799  1432035    45.0 |  9.339 % |
c |    447439 |   83690   299543 |   87565   40448  2079617    51.4 |  9.339 % |
c |    460413 |   83690   299543 |   96321   53422  2806992    52.5 |  9.339 % |
c |    479874 |   83637   299352 |  105954   72660  4728639    65.1 |  9.352 % |
c |    509070 |   83637   299352 |  116549  101856  7699095    75.6 |  9.352 % |
c |    552860 |   83630   299329 |  128204   38162  2810779    73.7 |  9.359 % |
c ==============================================================================
c [1mFound solution: 14953718[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 908   maxlim: 65294901   bits: 27/26
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    557043 |   89912   321845 |   29970   42345  2992631    70.7 |  9.359 % |
c |    557143 |   89912   321845 |   32967   13928   588100    42.2 |  8.897 % |
c |    557294 |   89912   321845 |   36263   14079   590343    41.9 |  8.897 % |
c |    557521 |   89912   321845 |   39890   14306   602706    42.1 |  8.897 % |
c |    557862 |   89912   321845 |   43879   14647   607107    41.4 |  8.897 % |
c |    558368 |   89912   321845 |   48266   15153   614334    40.5 |  8.897 % |
c |    559127 |   89912   321845 |   53093   15912   630584    39.6 |  8.897 % |
c |    560267 |   89912   321845 |   58403   17052   654924    38.4 |  8.897 % |
c |    561975 |   89912   321845 |   64243   18760   730341    38.9 |  8.897 % |
c |    564537 |   89912   321845 |   70667   21322   887333    41.6 |  8.897 % |
c |    568381 |   89912   321845 |   77734   25166  1043652    41.5 |  8.897 % |
c |    574147 |   89912   321845 |   85507   30932  1527411    49.4 |  8.897 % |
c |    582796 |   89912   321845 |   94058   39581  1964291    49.6 |  8.897 % |
c |    595770 |   89912   321845 |  103464   52555  3318199    63.1 |  8.897 % |
c |    615231 |   89912   321845 |  113811   72016  5901878    82.0 |  8.897 % |
c |    644424 |   89912   321845 |  125192  101209  8957059    88.5 |  8.897 % |
c |    688214 |   89912   321845 |  137711   28474  2865984   100.7 |  8.897 % |
#### 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.98 0.96 2/54 27269
Raw data (stat): 27269 (runsolver) R 27268 26298 26297 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 542441316 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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.0003 s]
Raw data (loadavg): 0.93 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 1791 0 0 0 993 5 0 0 25 0 1 0 542441316 9207808 1767 4294967295 134512640 134672761 3221224544 3221223648 134560243 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2248 1767 603 41 0 2207 0
vsize: 8992
[startup+20.0009 s]
Raw data (loadavg): 0.94 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 2668 0 0 0 1990 7 0 0 25 0 1 0 542441316 12820480 2644 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3130 2644 603 41 0 3089 0
vsize: 12520
[startup+30.001 s]
Raw data (loadavg): 0.95 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 3379 0 0 0 2987 9 0 0 25 0 1 0 542441316 15769600 3355 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3850 3355 603 41 0 3809 0
vsize: 15400
[startup+40.0014 s]
Raw data (loadavg): 0.96 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 3516 0 0 0 3987 10 0 0 25 0 1 0 542441316 16302080 3492 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3980 3492 603 41 0 3939 0
vsize: 15920
[startup+50.0014 s]
Raw data (loadavg): 0.96 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 4341 0 0 0 4985 12 0 0 25 0 1 0 542441316 19656704 4317 4294967295 134512640 134672761 3221224544 3221223712 134561156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4799 4317 603 41 0 4758 0
vsize: 19196
[startup+60.0022 s]
Raw data (loadavg): 0.97 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 4970 0 0 0 5983 14 0 0 25 0 1 0 542441316 22200320 4946 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5420 4946 603 41 0 5379 0
vsize: 21680
[startup+70.0025 s]
Raw data (loadavg): 0.97 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 4970 0 0 0 6983 14 0 0 25 0 1 0 542441316 22200320 4946 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5420 4946 603 41 0 5379 0
vsize: 21680
[startup+80.0028 s]
Raw data (loadavg): 0.98 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 5069 0 0 0 7983 15 0 0 25 0 1 0 542441316 22638592 5041 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5527 5041 603 41 0 5486 0
vsize: 22108
[startup+90.0033 s]
Raw data (loadavg): 0.98 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 5071 0 0 0 8983 15 0 0 25 0 1 0 542441316 22638592 5043 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5527 5043 603 41 0 5486 0
vsize: 22108
[startup+100.003 s]
Raw data (loadavg): 0.98 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 5071 0 0 0 9983 15 0 0 25 0 1 0 542441316 22638592 5043 4294967295 134512640 134672761 3221224544 3221223648 134560207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5527 5043 603 41 0 5486 0
vsize: 22108
[startup+110.004 s]
Raw data (loadavg): 0.98 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 5073 0 0 0 10984 15 0 0 25 0 1 0 542441316 22638592 5045 4294967295 134512640 134672761 3221224544 3221223728 134559388 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5527 5045 603 41 0 5486 0
vsize: 22108
[startup+120.003 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 5075 0 0 0 11984 15 0 0 25 0 1 0 542441316 22638592 5047 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5527 5047 603 41 0 5486 0
vsize: 22108
[startup+130.003 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 5075 0 0 0 12984 15 0 0 25 0 1 0 542441316 22638592 5047 4294967295 134512640 134672761 3221224544 3221223712 134560806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5527 5047 603 41 0 5486 0
vsize: 22108
[startup+140.004 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 5075 0 0 0 13984 15 0 0 25 0 1 0 542441316 22638592 5047 4294967295 134512640 134672761 3221224544 3221223728 134559161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5527 5047 603 41 0 5486 0
vsize: 22108
[startup+150.005 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 5075 0 0 0 14984 15 0 0 25 0 1 0 542441316 22638592 5047 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5527 5047 603 41 0 5486 0
vsize: 22108
[startup+160.005 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 5786 0 0 0 15982 17 0 0 25 0 1 0 542441316 25464832 5758 4294967295 134512640 134672761 3221224544 3221223744 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6217 5758 603 41 0 6176 0
vsize: 24868
[startup+170.005 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 6363 0 0 0 16981 18 0 0 25 0 1 0 542441316 27738112 6335 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6772 6335 603 41 0 6731 0
vsize: 27088
[startup+180.005 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 6717 0 0 0 17980 19 0 0 25 0 1 0 542441316 29220864 6689 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7134 6689 603 41 0 7093 0
vsize: 28536
[startup+190.005 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 6717 0 0 0 18980 19 0 0 25 0 1 0 542441316 29220864 6689 4294967295 134512640 134672761 3221224544 3221223648 134555116 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7134 6689 603 41 0 7093 0
vsize: 28536
[startup+200.005 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 6717 0 0 0 19980 19 0 0 25 0 1 0 542441316 29220864 6689 4294967295 134512640 134672761 3221224544 3221223648 134555128 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7134 6689 603 41 0 7093 0
vsize: 28536
[startup+210.006 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 6717 0 0 0 20980 20 0 0 25 0 1 0 542441316 29220864 6689 4294967295 134512640 134672761 3221224544 3221223728 134558638 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7134 6689 603 41 0 7093 0
vsize: 28536
[startup+220.007 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 6717 0 0 0 21980 20 0 0 25 0 1 0 542441316 29220864 6689 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7134 6689 603 41 0 7093 0
vsize: 28536
[startup+230.006 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 6990 0 0 0 22980 20 0 0 25 0 1 0 542441316 30289920 6962 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7395 6962 603 41 0 7354 0
vsize: 29580
[startup+240.006 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 7774 0 0 0 23979 22 0 0 25 0 1 0 542441316 33513472 7746 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8182 7746 603 41 0 8141 0
vsize: 32728
[startup+250.007 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 8457 0 0 0 24977 24 0 0 25 0 1 0 542441316 36327424 8429 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8869 8429 603 41 0 8828 0
vsize: 35476
[startup+260.007 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 9349 0 0 0 25975 26 0 0 25 0 1 0 542441316 40222720 9321 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9820 9321 603 41 0 9779 0
vsize: 39280
[startup+270.007 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 10194 0 0 0 26973 28 0 0 25 0 1 0 542441316 43728896 10166 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10676 10166 603 41 0 10635 0
vsize: 42704
[startup+280.007 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 10882 0 0 0 27972 29 0 0 25 0 1 0 542441316 46419968 10854 4294967295 134512640 134672761 3221224544 3221223536 134565856 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11333 10854 603 41 0 11292 0
vsize: 45332
[startup+290.007 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 10882 0 0 0 28972 30 0 0 25 0 1 0 542441316 46419968 10854 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11333 10854 603 41 0 11292 0
vsize: 45332
[startup+300.007 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 10882 0 0 0 29972 30 0 0 25 0 1 0 542441316 46419968 10854 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11333 10854 603 41 0 11292 0
vsize: 45332
[startup+310.008 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 10882 0 0 0 30972 30 0 0 25 0 1 0 542441316 46419968 10854 4294967295 134512640 134672761 3221224544 3221223728 134559293 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11333 10854 603 41 0 11292 0
vsize: 45332
[startup+320.009 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 10882 0 0 0 31972 30 0 0 25 0 1 0 542441316 46419968 10854 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11333 10854 603 41 0 11292 0
vsize: 45332
[startup+330.008 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 10882 0 0 0 32972 30 0 0 25 0 1 0 542441316 46419968 10854 4294967295 134512640 134672761 3221224544 3221223712 134560906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11333 10854 603 41 0 11292 0
vsize: 45332
[startup+340.009 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 10882 0 0 0 33972 30 0 0 25 0 1 0 542441316 46419968 10854 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11333 10854 603 41 0 11292 0
vsize: 45332
[startup+350.009 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 10882 0 0 0 34973 30 0 0 25 0 1 0 542441316 46419968 10854 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11333 10854 603 41 0 11292 0
vsize: 45332
[startup+360.01 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 10882 0 0 0 35973 30 0 0 25 0 1 0 542441316 46419968 10854 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11333 10854 603 41 0 11292 0
vsize: 45332
[startup+370.01 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 10882 0 0 0 36973 30 0 0 25 0 1 0 542441316 46419968 10854 4294967295 134512640 134672761 3221224544 3221223648 134560154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11333 10854 603 41 0 11292 0
vsize: 45332
[startup+380.01 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 11506 0 0 0 37971 32 0 0 25 0 1 0 542441316 48971776 11478 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11956 11478 603 41 0 11915 0
vsize: 47824
[startup+390.011 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 12158 0 0 0 38970 34 0 0 25 0 1 0 542441316 51675136 12130 4294967295 134512640 134672761 3221224544 3221223648 134560215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12616 12130 603 41 0 12575 0
vsize: 50464
[startup+400.01 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 12815 0 0 0 39968 36 0 0 25 0 1 0 542441316 54366208 12787 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13273 12787 603 41 0 13232 0
vsize: 53092
[startup+410.011 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 13358 0 0 0 40966 38 0 0 25 0 1 0 542441316 56651776 13330 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13831 13330 603 41 0 13790 0
vsize: 55324
[startup+420.012 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 13942 0 0 0 41965 39 0 0 25 0 1 0 542441316 58933248 13914 4294967295 134512640 134672761 3221224544 3221223552 134565782 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14388 13914 603 41 0 14347 0
vsize: 57552
[startup+430.011 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 13942 0 0 0 42965 39 0 0 25 0 1 0 542441316 58933248 13914 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14388 13914 603 41 0 14347 0
vsize: 57552
[startup+440.012 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 13942 0 0 0 43965 39 0 0 25 0 1 0 542441316 58933248 13914 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14388 13914 603 41 0 14347 0
vsize: 57552
[startup+450.013 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 13967 0 0 0 44965 40 0 0 25 0 1 0 542441316 59129856 13939 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14436 13939 603 41 0 14395 0
vsize: 57744
[startup+460.014 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 13967 0 0 0 45965 40 0 0 25 0 1 0 542441316 59129856 13939 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14436 13939 603 41 0 14395 0
vsize: 57744
[startup+470.013 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 13967 0 0 0 46965 40 0 0 25 0 1 0 542441316 59129856 13939 4294967295 134512640 134672761 3221224544 3221223728 134559663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14436 13939 603 41 0 14395 0
vsize: 57744
[startup+480.013 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 13967 0 0 0 47965 40 0 0 25 0 1 0 542441316 59129856 13939 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14436 13939 603 41 0 14395 0
vsize: 57744
[startup+490.014 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 14007 0 0 0 48965 40 0 0 25 0 1 0 542441316 59392000 13979 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14500 13979 603 41 0 14459 0
vsize: 58000
[startup+500.013 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 14007 0 0 0 49965 40 0 0 25 0 1 0 542441316 59392000 13979 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14500 13979 603 41 0 14459 0
vsize: 58000
[startup+510.014 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 14088 0 0 0 50965 40 0 0 25 0 1 0 542441316 59850752 14058 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14612 14058 603 41 0 14571 0
vsize: 58448
[startup+520.015 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 14088 0 0 0 51965 40 0 0 25 0 1 0 542441316 59850752 14058 4294967295 134512640 134672761 3221224544 3221223712 134560874 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14612 14058 603 41 0 14571 0
vsize: 58448
[startup+530.014 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 14088 0 0 0 52965 40 0 0 25 0 1 0 542441316 59850752 14058 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14612 14058 603 41 0 14571 0
vsize: 58448
[startup+540.014 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 14088 0 0 0 53965 40 0 0 25 0 1 0 542441316 59850752 14058 4294967295 134512640 134672761 3221224544 3221223648 134559841 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14612 14058 603 41 0 14571 0
vsize: 58448
[startup+550.014 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 14088 0 0 0 54966 40 0 0 25 0 1 0 542441316 59850752 14058 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14612 14058 603 41 0 14571 0
vsize: 58448
[startup+560.015 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 14088 0 0 0 55966 40 0 0 25 0 1 0 542441316 59850752 14058 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14612 14058 603 41 0 14571 0
vsize: 58448
[startup+570.014 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 14090 0 0 0 56966 40 0 0 25 0 1 0 542441316 59850752 14060 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14612 14060 603 41 0 14571 0
vsize: 58448
[startup+580.014 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 14090 0 0 0 57966 41 0 0 25 0 1 0 542441316 59850752 14060 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14612 14060 603 41 0 14571 0
vsize: 58448
[startup+590.014 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 14090 0 0 0 58966 41 0 0 25 0 1 0 542441316 59850752 14060 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14612 14060 603 41 0 14571 0
vsize: 58448
[startup+600.014 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 14090 0 0 0 59966 41 0 0 25 0 1 0 542441316 59850752 14060 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14612 14060 603 41 0 14571 0
vsize: 58448
[startup+610.015 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 14090 0 0 0 60966 41 0 0 25 0 1 0 542441316 59850752 14060 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14612 14060 603 41 0 14571 0
vsize: 58448
[startup+620.016 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 14090 0 0 0 61967 41 0 0 25 0 1 0 542441316 59850752 14060 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14612 14060 603 41 0 14571 0
vsize: 58448
[startup+630.016 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 14090 0 0 0 62967 41 0 0 25 0 1 0 542441316 59850752 14060 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14612 14060 603 41 0 14571 0
vsize: 58448
[startup+640.016 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 14090 0 0 0 63967 41 0 0 25 0 1 0 542441316 59850752 14060 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14612 14060 603 41 0 14571 0
vsize: 58448
[startup+650.016 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 14090 0 0 0 64967 41 0 0 25 0 1 0 542441316 59850752 14060 4294967295 134512640 134672761 3221224544 3221223648 134560248 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14612 14060 603 41 0 14571 0
vsize: 58448
[startup+660.017 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 14090 0 0 0 65967 41 0 0 25 0 1 0 542441316 59850752 14060 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14612 14060 603 41 0 14571 0
vsize: 58448
[startup+670.016 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 14090 0 0 0 66967 41 0 0 25 0 1 0 542441316 59850752 14060 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14612 14060 603 41 0 14571 0
vsize: 58448
[startup+680.016 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 14090 0 0 0 67967 41 0 0 25 0 1 0 542441316 59850752 14060 4294967295 134512640 134672761 3221224544 3221223668 134566077 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14612 14060 603 41 0 14571 0
vsize: 58448
[startup+690.017 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 14090 0 0 0 68968 41 0 0 25 0 1 0 542441316 59850752 14060 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14612 14060 603 41 0 14571 0
vsize: 58448
[startup+700.018 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 14091 0 0 0 69968 41 0 0 25 0 1 0 542441316 59850752 14061 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14612 14061 603 41 0 14571 0
vsize: 58448
[startup+710.018 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 14094 0 0 0 70968 41 0 0 25 0 1 0 542441316 59850752 14064 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14612 14064 603 41 0 14571 0
vsize: 58448
[startup+720.018 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 14097 0 0 0 71968 41 0 0 25 0 1 0 542441316 59850752 14067 4294967295 134512640 134672761 3221224544 3221223728 134559293 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14612 14067 603 41 0 14571 0
vsize: 58448
[startup+730.018 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 14100 0 0 0 72968 41 0 0 25 0 1 0 542441316 59850752 14070 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14612 14070 603 41 0 14571 0
vsize: 58448
[startup+740.018 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 14102 0 0 0 73968 41 0 0 25 0 1 0 542441316 59850752 14072 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14612 14072 603 41 0 14571 0
vsize: 58448
[startup+750.018 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 14105 0 0 0 74968 41 0 0 25 0 1 0 542441316 59850752 14075 4294967295 134512640 134672761 3221224544 3221223648 134560379 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14612 14075 603 41 0 14571 0
vsize: 58448
[startup+760.019 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 14109 0 0 0 75969 41 0 0 25 0 1 0 542441316 59850752 14079 4294967295 134512640 134672761 3221224544 3221223712 134560874 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14612 14079 603 41 0 14571 0
vsize: 58448
[startup+770.02 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 14112 0 0 0 76969 42 0 0 25 0 1 0 542441316 59850752 14082 4294967295 134512640 134672761 3221224544 3221223648 134560254 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14612 14082 603 41 0 14571 0
vsize: 58448
[startup+780.019 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 14117 0 0 0 77969 42 0 0 25 0 1 0 542441316 59850752 14087 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14612 14087 603 41 0 14571 0
vsize: 58448
[startup+790.02 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 14122 0 0 0 78969 42 0 0 25 0 1 0 542441316 59850752 14092 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14612 14092 603 41 0 14571 0
vsize: 58448
[startup+800.02 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 14192 0 0 0 79969 42 0 0 25 0 1 0 542441316 60121088 14162 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14678 14163 603 41 0 14637 0
vsize: 58712
[startup+810.02 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 14605 0 0 0 80968 43 0 0 25 0 1 0 542441316 61853696 14575 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15101 14575 603 41 0 15060 0
vsize: 60404
[startup+820.02 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 14605 0 0 0 81968 43 0 0 25 0 1 0 542441316 61853696 14575 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15101 14575 603 41 0 15060 0
vsize: 60404
[startup+830.02 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 14605 0 0 0 82968 43 0 0 25 0 1 0 542441316 61853696 14575 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15101 14575 603 41 0 15060 0
vsize: 60404
[startup+840.02 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 14605 0 0 0 83968 43 0 0 25 0 1 0 542441316 61853696 14575 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15101 14575 603 41 0 15060 0
vsize: 60404
[startup+850.02 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 14620 0 0 0 84968 44 0 0 25 0 1 0 542441316 61853696 14590 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15101 14590 603 41 0 15060 0
vsize: 60404
[startup+860.021 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 14620 0 0 0 85968 44 0 0 25 0 1 0 542441316 61853696 14590 4294967295 134512640 134672761 3221224544 3221223728 134559330 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15101 14590 603 41 0 15060 0
vsize: 60404
[startup+870.022 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 14620 0 0 0 86968 44 0 0 25 0 1 0 542441316 61853696 14590 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15101 14590 603 41 0 15060 0
vsize: 60404
[startup+880.021 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 14620 0 0 0 87968 44 0 0 25 0 1 0 542441316 61853696 14590 4294967295 134512640 134672761 3221224544 3221223680 134560697 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15101 14590 603 41 0 15060 0
vsize: 60404
[startup+890.021 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 14620 0 0 0 88968 44 0 0 25 0 1 0 542441316 61853696 14590 4294967295 134512640 134672761 3221224544 3221223712 134561212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15101 14590 603 41 0 15060 0
vsize: 60404
[startup+900.021 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 14620 0 0 0 89968 44 0 0 25 0 1 0 542441316 61853696 14590 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15101 14590 603 41 0 15060 0
vsize: 60404
[startup+910.021 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 14620 0 0 0 90968 45 0 0 25 0 1 0 542441316 61853696 14590 4294967295 134512640 134672761 3221224544 3221223668 134566049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15101 14590 603 41 0 15060 0
vsize: 60404
[startup+920.021 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 14620 0 0 0 91968 45 0 0 25 0 1 0 542441316 61853696 14590 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15101 14590 603 41 0 15060 0
vsize: 60404
[startup+930.021 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 14620 0 0 0 92968 45 0 0 25 0 1 0 542441316 61853696 14590 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15101 14590 603 41 0 15060 0
vsize: 60404
[startup+940.021 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 14620 0 0 0 93969 45 0 0 25 0 1 0 542441316 61853696 14590 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15101 14590 603 41 0 15060 0
vsize: 60404
[startup+950.021 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 14620 0 0 0 94969 45 0 0 25 0 1 0 542441316 61853696 14590 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15101 14590 603 41 0 15060 0
vsize: 60404
[startup+960.022 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 14620 0 0 0 95969 45 0 0 25 0 1 0 542441316 61853696 14590 4294967295 134512640 134672761 3221224544 3221223728 134559392 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15101 14590 603 41 0 15060 0
vsize: 60404
[startup+970.021 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 14620 0 0 0 96969 45 0 0 25 0 1 0 542441316 61853696 14590 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15101 14590 603 41 0 15060 0
vsize: 60404
[startup+980.022 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 14620 0 0 0 97969 45 0 0 25 0 1 0 542441316 61853696 14590 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15101 14590 603 41 0 15060 0
vsize: 60404
[startup+990.022 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 14620 0 0 0 98969 45 0 0 25 0 1 0 542441316 61853696 14590 4294967295 134512640 134672761 3221224544 3221223712 134561400 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15101 14590 603 41 0 15060 0
vsize: 60404
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 14620 0 0 0 99969 45 0 0 25 0 1 0 542441316 61853696 14590 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15101 14590 603 41 0 15060 0
vsize: 60404
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 14620 0 0 0 100969 45 0 0 25 0 1 0 542441316 61853696 14590 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15101 14590 603 41 0 15060 0
vsize: 60404
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 14620 0 0 0 101969 46 0 0 25 0 1 0 542441316 61853696 14590 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15101 14590 603 41 0 15060 0
vsize: 60404
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 14620 0 0 0 102970 46 0 0 25 0 1 0 542441316 61853696 14590 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15101 14590 603 41 0 15060 0
vsize: 60404
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.98 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 14620 0 0 0 103970 46 0 0 25 0 1 0 542441316 61853696 14590 4294967295 134512640 134672761 3221224544 3221223712 134560874 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15101 14590 603 41 0 15060 0
vsize: 60404
[startup+1050.02 s]
Raw data (loadavg): 1.07 1.00 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 14620 0 0 0 104970 46 0 0 25 0 1 0 542441316 61853696 14590 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15101 14590 603 41 0 15060 0
vsize: 60404
[startup+1060.02 s]
Raw data (loadavg): 1.06 1.00 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 14620 0 0 0 105970 46 0 0 25 0 1 0 542441316 61853696 14590 4294967295 134512640 134672761 3221224544 3221223680 134560661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15101 14590 603 41 0 15060 0
vsize: 60404
[startup+1070.02 s]
Raw data (loadavg): 1.05 1.00 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 14620 0 0 0 106970 46 0 0 25 0 1 0 542441316 61853696 14590 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15101 14590 603 41 0 15060 0
vsize: 60404
[startup+1080.02 s]
Raw data (loadavg): 1.04 1.00 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 14741 0 0 0 107970 47 0 0 25 0 1 0 542441316 62390272 14711 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15232 14711 603 41 0 15191 0
vsize: 60928
[startup+1090.02 s]
Raw data (loadavg): 1.04 1.00 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 15089 0 0 0 108969 48 0 0 25 0 1 0 542441316 63733760 15059 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15560 15059 603 41 0 15519 0
vsize: 62240
[startup+1100.02 s]
Raw data (loadavg): 1.03 1.00 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 15378 0 0 0 109968 48 0 0 25 0 1 0 542441316 64942080 15348 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15855 15348 603 41 0 15814 0
vsize: 63420
[startup+1110.03 s]
Raw data (loadavg): 1.03 1.00 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 15635 0 0 0 110968 49 0 0 25 0 1 0 542441316 66015232 15605 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16117 15605 603 41 0 16076 0
vsize: 64468
[startup+1120.03 s]
Raw data (loadavg): 1.02 1.00 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 15908 0 0 0 111967 50 0 0 25 0 1 0 542441316 67088384 15878 4294967295 134512640 134672761 3221224544 3221223728 134559019 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16379 15878 603 41 0 16338 0
vsize: 65516
[startup+1130.03 s]
Raw data (loadavg): 1.02 1.00 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 16167 0 0 0 112967 51 0 0 25 0 1 0 542441316 68689920 16137 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16770 16137 603 41 0 16729 0
vsize: 67080
[startup+1140.03 s]
Raw data (loadavg): 1.01 1.00 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 16428 0 0 0 113966 51 0 0 25 0 1 0 542441316 69767168 16398 4294967295 134512640 134672761 3221224544 3221223648 134554662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17033 16398 603 41 0 16992 0
vsize: 68132
[startup+1150.03 s]
Raw data (loadavg): 1.01 1.00 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 16428 0 0 0 114966 52 0 0 25 0 1 0 542441316 69767168 16398 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17033 16398 603 41 0 16992 0
vsize: 68132
[startup+1160.03 s]
Raw data (loadavg): 1.01 1.00 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 16428 0 0 0 115966 52 0 0 25 0 1 0 542441316 69767168 16398 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17033 16398 603 41 0 16992 0
vsize: 68132
[startup+1170.03 s]
Raw data (loadavg): 1.01 1.00 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 16428 0 0 0 116966 52 0 0 25 0 1 0 542441316 69767168 16398 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17033 16398 603 41 0 16992 0
vsize: 68132
[startup+1180.03 s]
Raw data (loadavg): 1.01 1.00 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 16428 0 0 0 117966 52 0 0 25 0 1 0 542441316 69767168 16398 4294967295 134512640 134672761 3221224544 3221223680 134560706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17033 16398 603 41 0 16992 0
vsize: 68132
[startup+1190.03 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 16428 0 0 0 118966 52 0 0 25 0 1 0 542441316 69767168 16398 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17033 16398 603 41 0 16992 0
vsize: 68132
[startup+1200.03 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 27269
Raw data (stat): 27269 (minisat+) R 27268 26298 26297 0 -1 0 16428 0 0 0 119966 52 0 0 25 0 1 0 542441316 69767168 16398 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17033 16398 603 41 0 16992 0
vsize: 68132
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 1.00 1.00 0.96 1/54 27269
Raw data (stat): 27269 (minisat+) Z 27268 26298 26297 0 -1 12 16431 0 0 0 119966 55 0 0 25 0 1 0 542441316 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.06
CPU time (s): 1200.22
CPU user time (s): 1199.66
CPU system time (s): 0.557915
CPU usage (%): 100.013
Max. virtual memory (Kb): 68132
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####