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-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-lp4l.opb
MD5SUM	3c39e3c2b993ee2185e2a1a3e73b9723
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	3744
Optimality of the best value was proved	NO
Number of terms in the objective function	1086
Biggest coefficient in the objective function	283
Number of bits for the biggest coefficient in the objective function	9
Sum of the numbers in the objective function	197191
Number of bits of the sum of numbers in the objective function	18
Biggest number in a constraint	283
Number of bits of the biggest number in a constraint	9
Biggest sum of numbers in a constraint	197191
Number of bits of the biggest sum of numbers	18
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.09
Number of variables	1086
Total number of constraints	1171
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	1170
Number of constraints which are nor clauses,nor cardinality constraints	1
Minimum length of a constraint	1
Maximum length of a constraint	1086
Trace number 22231

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc2 THE 2005-04-22 02:27:42 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=11918 boxname=wulflinc2 idbench=917 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  3c39e3c2b993ee2185e2a1a3e73b9723  /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-20-10-lp4l.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-20-10-lp4l.opb /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-20-10-lp4l.opb
IDLAUNCH: 11918
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.191
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.191
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:        309944 kB
Buffers:         33776 kB
Cached:         667380 kB
SwapCached:       3324 kB
Active:         356088 kB
Inactive:       349876 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        309692 kB
SwapTotal:     2097136 kB
SwapFree:      2092928 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5108 kB
Slab:            12984 kB
Committed_AS:    71784 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-22 02:47:45 (client local time) WITH STATUS 10 IN 1200.25 SECONDS
stats: 11918 7 1200.25 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 169 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ####################################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 168]---> Adder-cost: 592   maxlim: 2471   bits: 12/12
c ---[ 166]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[ 164]---> Adder-cost: 64   maxlim: 34   bits: 6/6
c ---[ 162]---> Adder-cost: 94   maxlim: 50   bits: 6/6
c ---[ 160]---> Adder-cost: 76   maxlim: 40   bits: 6/6
c ---[ 158]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[ 156]---> Adder-cost: 66   maxlim: 35   bits: 6/6
c ---[ 154]---> Adder-cost: 50   maxlim: 28   bits: 5/5
c ---[ 152]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[ 150]---> Adder-cost: 22   maxlim: 14   bits: 4/4
c ---[ 148]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 146]---> Adder-cost: 76   maxlim: 40   bits: 6/6
c ---[ 144]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[ 142]---> Adder-cost: 70   maxlim: 38   bits: 6/6
c ---[ 140]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[ 138]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[ 136]---> Adder-cost: 68   maxlim: 38   bits: 6/6
c ---[ 134]---> Adder-cost: 100   maxlim: 54   bits: 6/6
c ---[ 132]---> Adder-cost: 92   maxlim: 47   bits: 6/6
c ---[ 130]---> Adder-cost: 126   maxlim: 64   bits: 7/7
c ---[ 128]---> Adder-cost: 114   maxlim: 62   bits: 6/6
c ---[ 126]---> Adder-cost: 84   maxlim: 45   bits: 6/6
c ---[ 124]---> Adder-cost: 50   maxlim: 29   bits: 5/5
c ---[ 122]---> Adder-cost: 82   maxlim: 45   bits: 6/6
c ---[ 120]---> Adder-cost: 70   maxlim: 37   bits: 6/6
c ---[ 118]---> Adder-cost: 98   maxlim: 52   bits: 6/6
c ---[ 116]---> Adder-cost: 112   maxlim: 59   bits: 6/6
c ---[ 114]---> Adder-cost: 126   maxlim: 63   bits: 7/6
c ---[ 112]---> Adder-cost: 74   maxlim: 46   bits: 6/6
c ---[ 110]---> Adder-cost: 52   maxlim: 30   bits: 5/5
c ---[ 108]---> Adder-cost: 84   maxlim: 45   bits: 6/6
c ---[ 106]---> Adder-cost: 68   maxlim: 36   bits: 6/6
c ---[ 104]---> Adder-cost: 128   maxlim: 65   bits: 7/7
c ---[ 102]---> Adder-cost: 108   maxlim: 57   bits: 6/6
c ---[ 100]---> Adder-cost: 100   maxlim: 62   bits: 6/6
c ---[  98]---> Adder-cost: 72   maxlim: 45   bits: 6/6
c ---[  96]---> Adder-cost: 62   maxlim: 31   bits: 6/5
c ---[  94]---> Adder-cost: 52   maxlim: 30   bits: 5/5
c ---[  92]---> Adder-cost: 32   maxlim: 17   bits: 5/5
c ---[  90]---> Adder-cost: 114   maxlim: 62   bits: 6/6
c ---[  88]---> Adder-cost: 114   maxlim: 61   bits: 6/6
c ---[  86]---> Adder-cost: 72   maxlim: 50   bits: 6/6
c ---[  84]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[  82]---> Adder-cost: 68   maxlim: 35   bits: 6/6
c ---[  80]---> Adder-cost: 52   maxlim: 30   bits: 5/5
c ---[  78]---> Adder-cost: 32   maxlim: 17   bits: 5/5
c ---[  76]---> Adder-cost: 70   maxlim: 37   bits: 6/6
c ---[  74]---> Adder-cost: 56   maxlim: 35   bits: 6/6
c ---[  72]---> Adder-cost: 44   maxlim: 24   bits: 5/5
c ---[  70]---> Adder-cost: 64   maxlim: 34   bits: 6/6
c ---[  68]---> Adder-cost: 92   maxlim: 48   bits: 6/6
c ---[  66]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  64]---> Adder-cost: 100   maxlim: 54   bits: 6/6
c ---[  62]---> Adder-cost: 94   maxlim: 49   bits: 6/6
c ---[  60]---> Adder-cost: 32   maxlim: 17   bits: 5/5
c ---[  58]---> Adder-cost: 76   maxlim: 40   bits: 6/6
c ---[  56]---> Adder-cost: 82   maxlim: 44   bits: 6/6
c ---[  54]---> Adder-cost: 70   maxlim: 38   bits: 6/6
c ---[  52]---> Adder-cost: 64   maxlim: 34   bits: 6/6
c ---[  50]---> Adder-cost: 38   maxlim: 22   bits: 5/5
c ---[  48]---> Adder-cost: 70   maxlim: 38   bits: 6/6
c ---[  46]---> Adder-cost: 100   maxlim: 53   bits: 6/6
c ---[  44]---> Adder-cost: 82   maxlim: 44   bits: 6/6
c ---[  42]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[  40]---> Adder-cost: 62   maxlim: 32   bits: 6/6
c ---[  38]---> Adder-cost: 36   maxlim: 20   bits: 5/5
c ---[  36]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[  34]---> Adder-cost: 62   maxlim: 32   bits: 6/6
c ---[  32]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[  30]---> Adder-cost: 164   maxlim: 85   bits: 7/7
c ---[  28]---> Adder-cost: 148   maxlim: 78   bits: 7/7
c ---[  26]---> Adder-cost: 108   maxlim: 58   bits: 6/6
c ---[  24]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[  22]---> Adder-cost: 78   maxlim: 42   bits: 6/6
c ---[  20]---> Adder-cost: 106   maxlim: 56   bits: 6/6
c ---[  18]---> Adder-cost: 106   maxlim: 55   bits: 6/6
c ---[  16]---> Adder-cost: 158   maxlim: 81   bits: 7/7
c ---[  14]---> Adder-cost: 146   maxlim: 76   bits: 7/7
c ---[  12]---> Adder-cost: 112   maxlim: 59   bits: 6/6
c ---[  10]---> Adder-cost: 46   maxlim: 29   bits: 5/5
c ---[   8]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[   6]---> Adder-cost: 68   maxlim: 36   bits: 6/6
c ---[   4]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[   2]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[   0]---> Adder-cost: 1682   maxlim: 1059   bits: 11/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   56219   199971 |   18739       0        0     nan |  0.000 % |
c |       100 |   55916   198922 |   20612      66      209     3.2 | 11.162 % |
c |       250 |   55374   197058 |   22674     167      689     4.1 | 12.117 % |
c |       476 |   54717   194755 |   24941     314     1515     4.8 | 13.231 % |
c |       814 |   54036   192388 |   27435     562     2673     4.8 | 14.345 % |
c |      1321 |   53744   191403 |   30179    1027     4806     4.7 | 14.883 % |
c |      2081 |   53587   190848 |   33197    1769    25501    14.4 | 15.092 % |
c |      3225 |   53216   189573 |   36517    2872    50338    17.5 | 15.758 % |
c |      4933 |   51448   183429 |   40168    4377    81463    18.6 | 18.782 % |
c |      7495 |   47696   170393 |   44185    6450   110065    17.1 | 25.090 % |
c |     11342 |   45398   162421 |   48604    9979   173069    17.3 | 28.959 % |
c |     17108 |   43349   155408 |   53464   15457   283024    18.3 | 32.352 % |
c |     25758 |   41044   147461 |   58811   23764   551073    23.2 | 36.232 % |
c |     38733 |   38255   137924 |   64692   36302  1246741    34.3 | 40.738 % |
c |     58194 |   35722   129267 |   71161   55293  2930051    53.0 | 45.066 % |
c ==============================================================================
c [1mFound solution: 4482[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 8018   maxlim: 192709   bits: 18/18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     67765 |   90246   323689 |   30082   64689  4009282    62.0 | 45.066 % |
c |     67865 |   90239   323666 |   33090   24754  1406991    56.8 | 26.133 % |
c |     68015 |   90239   323666 |   36399   24904  1420240    57.0 | 26.133 % |
c |     68241 |   90224   323617 |   40039   25127  1432790    57.0 | 26.144 % |
c |     68579 |   90192   323513 |   44043   25458  1461168    57.4 | 26.177 % |
c |     69085 |   90153   323386 |   48447   25957  1509939    58.2 | 26.216 % |
c |     69846 |   90123   323278 |   53292   26714  1606100    60.1 | 26.249 % |
c |     70986 |   89965   322726 |   58621   27832  1699521    61.1 | 26.387 % |
c ==============================================================================
c [1mFound solution: 4459[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 192732   bits: 18/18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     71169 |   89977   322817 |   29992   28015  1717556    61.3 | 26.387 % |
c |     71270 |   89977   322817 |   32991   28116  1722259    61.3 | 26.402 % |
c |     71423 |   89927   322639 |   36290   28260  1728167    61.2 | 26.446 % |
c ==============================================================================
c [1mFound solution: 4313[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 192878   bits: 18/18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     71508 |   89942   322768 |   29980   28345  1733985    61.2 | 26.446 % |
c |     71608 |   89926   322716 |   32978   28442  1740853    61.2 | 26.491 % |
c |     71758 |   89926   322716 |   36275   28592  1754922    61.4 | 26.491 % |
c |     71983 |   89850   322460 |   39903   28784  1768832    61.5 | 26.558 % |
c |     72320 |   89745   322104 |   43893   29089  1771081    60.9 | 26.657 % |
c |     72826 |   89745   322104 |   48283   29595  1862220    62.9 | 26.657 % |
c |     73585 |   89745   322104 |   53111   30354  2113694    69.6 | 26.657 % |
c |     74725 |   89714   322001 |   58422   31491  2308008    73.3 | 26.685 % |
c |     76433 |   89678   321877 |   64264   33193  2704148    81.5 | 26.723 % |
c |     78996 |   89175   320143 |   70691   35673  3039687    85.2 | 27.193 % |
c |     82842 |   88888   319178 |   77760   39461  3689801    93.5 | 27.475 % |
c |     88611 |   88668   318436 |   85536   45203  4948529   109.5 | 27.641 % |
c ==============================================================================
c [1mFound solution: 4279[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 192912   bits: 18/18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     88851 |   88671   318479 |   29557   45443  4995605   109.9 | 27.641 % |
c |     88951 |   88671   318479 |   32512   22822  2149329    94.2 | 27.653 % |
c |     89104 |   88662   318450 |   35763   22974  2150755    93.6 | 27.664 % |
c |     89329 |   88519   317929 |   39340   23170  2195160    94.7 | 27.797 % |
c |     89668 |   88519   317929 |   43274   23509  2243925    95.4 | 27.797 % |
c |     90174 |   88519   317929 |   47601   24015  2321859    96.7 | 27.797 % |
c |     90933 |   88519   317929 |   52362   24774  2431674    98.2 | 27.797 % |
c |     92072 |   88485   317817 |   57598   25906  2658310   102.6 | 27.830 % |
c |     93780 |   88429   317625 |   63358   27607  3073113   111.3 | 27.874 % |
c |     96342 |   88379   317461 |   69693   30162  3755633   124.5 | 27.924 % |
c |    100186 |   88286   317150 |   76663   33983  4672756   137.5 | 28.012 % |
c ==============================================================================
c [1mFound solution: 4061[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 193130   bits: 18/18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    103843 |   88221   316987 |   29407   37630  5494132   146.0 | 28.012 % |
c |    103945 |   88221   316987 |   32347   18917  2126820   112.4 | 28.088 % |
c |    104096 |   88221   316987 |   35582   19068  2142560   112.4 | 28.088 % |
c |    104321 |   88221   316987 |   39140   19293  2176276   112.8 | 28.088 % |
c |    104661 |   88138   316700 |   43054   19619  2216894   113.0 | 28.166 % |
c |    105167 |   88129   316671 |   47360   20124  2255003   112.1 | 28.177 % |
c |    105926 |   88102   316576 |   52096   20878  2395605   114.7 | 28.204 % |
c |    107065 |   88030   316330 |   57305   22013  2660459   120.9 | 28.238 % |
c |    108774 |   88021   316299 |   63036   23719  3124005   131.7 | 28.243 % |
c |    111341 |   87995   316211 |   69340   26284  3930175   149.5 | 28.271 % |
c |    115186 |   87920   315960 |   76274   30116  4775396   158.6 | 28.348 % |
c |    120959 |   87841   315673 |   83901   35876  6469912   180.3 | 28.420 % |
c |    129609 |   87824   315614 |   92291   44523  9084210   204.0 | 28.436 % |
c |    142584 |   87565   314735 |  101520   57456 12539787   218.3 | 28.641 % |
c |    162048 |   87253   313685 |  111673   76869 18170700   236.4 | 28.934 % |
c |    191241 |   86919   312557 |  122840  106009 27183831   256.4 | 29.227 % |
c |    235031 |   86508   311180 |  135124   49409 10620039   214.9 | 29.564 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -CO100001_bit0 -CO100002_bit0 -CO100003_bit0 -CO100004_bit0 -CO100005_bit0 -CO100006_bit0 -CO100007_bit0 -CO100008_bit0 -CO100009_bit0 -CO100010_bit0 -CO100011_bit0 -CO100012_bit0 -CO100013_bit0 -CO100014_bit0 -CO100015_bit0 -CO100016_bit0 -CO100017_bit0 -CO100018_bit0 -CO100019_bit0 -CO100020_bit0 -CO100021_bit0 -CO100022_bit0 -CO100023_bit0 -CO100024_bit0 -CO100025_bit0 -CO100026_bit0 CO100027_bit0 -CO100028_bit0 -CO100029_bit0 -CO100030_bit0 -CO100031_bit0 -CO100032_bit0 -CO100033_bit0 -CO100034_bit0 -CO100035_bit0 -CO100036_bit0 -CO100037_bit0 -CO100038_bit0 -CO100039_bit0 -CO100040_bit0 -CO100041_bit0 -CO100042_bit0 -CO100043_bit0 -CO100044_bit0 -CO100045_bit0 -CO100046_bit0 -CO100047_bit0 -CO100048_bit0 -CO100049_bit0 -CO100050_bit0 -CO100051_bit0 -CO100052_bit0 -CO100053_bit0 CO100054_bit0 -CO100055_bit0 -CO100056_bit0 -CO100057_bit0 -CO100058_bit0 -CO100059_bit0 -CO100060_bit0 CO100061_bit0 -CO100062_bit0 -CO100063_bit0 -CO100064_bit0 -CO100065_bit0 -CO100066_bit0 -CO100067_bit0 -CO100068_bit0 -CO100069_bit0 -CO100070_bit0 -CO100071_bit0 -CO100072_bit0 -CO100073_bit0 -CO100074_bit0 -CO100075_bit0 -CO100076_bit0 -CO100077_bit0 -CO100078_bit0 -CO100079_bit0 -CO100080_bit0 -CO100081_bit0 -CO100082_bit0 -CO100083_bit0 CO100084_bit0 -CO100085_bit0 -CO100086_bit0 -CO100087_bit0 -CO100088_bit0 -CO100089_bit0 -CO100090_bit0 -CO100091_bit0 -CO100092_bit0 -CO100093_bit0 -CO100094_bit0 -CO100095_bit0 -CO100096_bit0 -CO100097_bit0 -CO100098_bit0 -CO100099_bit0 CO100100_bit0 -CO100101_bit0 -CO100102_bit0 -CO100103_bit0 -CO100104_bit0 -CO100105_bit0 -CO100106_bit0 -CO100107_bit0 -CO100108_bit0 -CO100109_bit0 CO100110_bit0 -CO100111_bit0 -CO100112_bit0 -CO100113_bit0 -CO100114_bit0 -CO100115_bit0 -CO100116_bit0 -CO100117_bit0 -CO100118_bit0 -CO100119_bit0 -CO100120_bit0 -CO100121_bit0 -CO100122_bit0 -CO100123_bit0 -CO100124_bit0 -CO100125_bit0 -CO100126_bit0 -CO100127_bit0 -CO100128_bit0 -CO100129_bit0 -CO100130_bit0 -CO100131_bit0 -CO100132_bit0 -CO100133_bit0 -CO100134_bit0 -CO100135_bit0 -CO100136_bit0 -CO100137_bit0 -CO100138_bit0 -CO100139_bit0 -CO100140_bit0 -CO100141_bit0 -CO100142_bit0 -CO100143_bit0 -CO100144_bit0 -CO100145_bit0 -CO100146_bit0 -CO100147_bit0 -CO100148_bit0 -CO100149_bit0 -CO100150_bit0 CO100151_bit0 -CO100152_bit0 -CO100153_bit0 -CO100154_bit0 -CO100155_bit0 -CO100156_bit0 -CO100157_bit0 -CO100158_bit0 -CO100159_bit0 CO100160_bit0 -CO100161_bit0 -CO100162_bit0 -CO100163_bit0 -CO100164_bit0 -CO100165_bit0 CO100166_bit0 -CO100167_bit0 -CO100168_bit0 CO100169_bit0 -CO100170_bit0 -CO100171_bit0 -CO100172_bit0 -CO100173_bit0 -CO100174_bit0 -CO100175_bit0 -CO100176_bit0 -CO100177_bit0 CO100178_bit0 -CO100179_bit0 -CO100180_bit0 -CO100181_bit0 -CO100182_bit0 -CO100183_bit0 -CO100184_bit0 -CO100185_bit0 -CO100186_bit0 -CO100187_bit0 -CO100188_bit0 -CO100189_bit0 -CO100190_bit0 -CO100191_bit0 -CO100192_bit0 -CO100193_bit0 -CO100194_bit0 -CO100195_bit0 -CO100196_bit0 -CO100197_bit0 -CO100198_bit0 -CO100199_bit0 -CO100200_bit0 -CO100201_bit0 -CO100202_bit0 -CO100203_bit0 -CO100204_bit0 -CO100205_bit0 -CO100206_bit0 -CO100207_bit0 -CO100208_bit0 -CO100209_bit0 -CO100210_bit0 -CO100211_bit0 -CO100212_bit0 -CO100213_bit0 -CO100214_bit0 -CO100215_bit0 -CO100216_bit0 -CO100217_bit0 -CO100218_bit0 -CO100219_bit0 -CO100220_bit0 -CO100221_bit0 -CO100222_bit0 -CO100223_bit0 -CO100224_bit0 -CO100225_bit0 -CO100226_bit0 -CO100227_bit0 -CO100228_bit0 -CO100229_bit0 -CO100230_bit0 CO100231_bit0 -CO100232_bit0 -CO100233_bit0 -CO100234_bit0 -CO100235_bit0 -CO100236_bit0 -CO100237_bit0 -CO100238_bit0 -CO100239_bit0 -CO100240_bit0 -CO100241_bit0 -CO100242_bit0 -CO100243_bit0 -CO100244_bit0 -CO100245_bit0 -CO100246_bit0 -CO100247_bit0 -CO100248_bit0 -CO100249_bit0 -CO100250_bit0 -CO100251_bit0 -CO100252_bit0 -CO100253_bit0 -CO100254_bit0 -CO100255_bit0 -CO100256_bit0 -CO100257_bit0 -CO100258_bit0 -CO100259_bit0 -CO100260_bit0 -CO100261_bit0 -CO100262_bit0 -CO100263_bit0 -CO100264_bit0 -CO100265_bit0 -CO100266_bit0 -CO100267_bit0 -CO100268_bit0 -CO100269_bit0 -CO100270_bit0 -CO100271_bit0 -CO100272_bit0 -CO100273_bit0 -CO100274_bit0 -CO100275_bit0 -CO100276_bit0 -CO100277_bit0 -CO100278_bit0 -CO100279_bit0 -CO100280_bit0 -CO100281_bit0 -CO100282_bit0 -CO100283_bit0 -CO100284_bit0 -CO100285_bit0 -CO100286_bit0 -CO100287_bit0 -CO100288_bit0 -CO100289_bit0 -CO100290_bit0 -CO100291_bit0 -CO100292_bit0 -CO100293_bit0 -CO100294_bit0 -CO100295_bit0 -CO100296_bit0 -CO100297_bit0 -CO100298_bit0 -CO100299_bit0 -CO100300_bit0 -CO100301_bit0 -CO100302_bit0 -CO100303_bit0 -CO100304_bit0 -CO100305_bit0 -CO100306_bit0 -CO100307_bit0 -CO100308_bit0 -CO100309_bit0 -CO100310_bit0 -CO100311_bit0 CO100312_bit0 -CO100313_bit0 -CO100314_bit0 -CO100315_bit0 -CO100316_bit0 -CO100317_bit0 -CO100318_bit0 -CO100319_bit0 -CO100320_bit0 -CO100321_bit0 -CO100322_bit0 -CO100323_bit0 -CO100324_bit0 -CO100325_bit0 -CO100326_bit0 -CO100327_bit0 -CO100328_bit0 -CO100329_bit0 -CO100330_bit0 -CO100331_bit0 -CO100332_bit0 -CO100333_bit0 -CO100334_bit0 -CO100335_bit0 -CO100336_bit0 -CO100337_bit0 -CO100338_bit0 -CO100339_bit0 -CO100340_bit0 -CO100341_bit0 -CO100342_bit0 -CO100343_bit0 -CO100344_bit0 -CO100345_bit0 -CO100346_bit0 -CO100347_bit0 -CO100348_bit0 -CO100349_bit0 -CO100350_bit0 -CO100351_bit0 -CO100352_bit0 -CO100353_bit0 -CO100354_bit0 -CO100355_bit0 -CO100356_bit0 -CO100357_bit0 -CO100358_bit0 -CO100359_bit0 -CO100360_bit0 -CO100361_bit0 -CO100362_bit0 -CO100363_bit0 -CO100364_bit0 -CO100365_bit0 -CO100366_bit0 -CO100367_bit0 -CO100368_bit0 -CO100369_bit0 -CO100370_bit0 -CO100371_bit0 -CO100372_bit0 -CO100373_bit0 -CO100374_bit0 -CO100375_bit0 -CO100376_bit0 -CO100377_bit0 CO100378_bit0 -CO100379_bit0 -CO100380_bit0 -CO100381_bit0 -CO100382_bit0 -CO100383_bit0 -CO100384_bit0 -CO100385_bit0 -CO100386_bit0 -CO100387_bit0 -CO100388_bit0 -CO100389_bit0 -CO100390_bit0 -CO100391_bit0 -CO100392_bit0 -CO100393_bit0 -CO100394_bit0 -CO100395_bit0 -CO100396_bit0 -CO100397_bit0 -CO100398_bit0 -CO100399_bit0 -CO100400_bit0 -CO100401_bit0 -CO100402_bit0 -CO100403_bit0 -CO100404_bit0 -CO100405_bit0 -CO100406_bit0 -CO100407_bit0 -CO100408_bit0 -CO100409_bit0 -CO100410_bit0 -CO100411_bit0 -CO100412_bit0 -CO100413_bit0 -CO100414_bit0 -CO100415_bit0 -CO100416_bit0 -CO100417_bit0 -CO100418_bit0 -CO100419_bit0 -CO100420_bit0 -CO100421_bit0 -CO100422_bit0 -CO100423_bit0 -CO100424_bit0 -CO100425_bit0 -CO100426_bit0 -CO100427_bit0 CO100428_bit0 -CO100429_bit0 -CO100430_bit0 -CO100431_bit0 -CO100432_bit0 -CO100433_bit0 -CO100434_bit0 -CO100435_bit0 -CO100436_bit0 -CO100437_bit0 -CO100438_bit0 -CO100439_bit0 -CO100440_bit0 -CO100441_bit0 -CO100442_bit0 -CO100443_bit0 -CO100444_bit0 -CO100445_bit0 -CO100446_bit0 -CO100447_bit0 -CO100448_bit0 -CO100449_bit0 -CO100450_bit0 -CO100451_bit0 -CO100452_bit0 -CO100453_bit0 -CO100454_bit0 CO100455_bit0 -CO100456_bit0 -CO100457_bit0 -CO100458_bit0 -CO100459_bit0 -CO100460_bit0 -CO100461_bit0 -CO100462_bit0 -CO100463_bit0 -CO100464_bit0 -CO100465_bit0 -CO100466_bit0 -CO100467_bit0 -CO100468_bit0 -CO100469_bit0 -CO100470_bit0 -CO100471_bit0 -CO100472_bit0 -CO100473_bit0 -CO100474_bit0 -CO100475_bit0 -CO100476_bit0 -CO100477_bit0 -CO100478_bit0 -CO100479_bit0 -CO100480_bit0 -CO100481_bit0 -CO100482_bit0 -CO100483_bit0 -CO100484_bit0 -CO100485_bit0 -CO100486_bit0 -CO100487_bit0 -CO100488_bit0 -CO100489_bit0 -CO100490_bit0 -CO100491_bit0 -CO100492_bit0 -CO100493_bit0 -CO100494_bit0 -CO100495_bit0 CO100496_bit0 -CO100497_bit0 -CO100498_bit0 -CO100499_bit0 -CO100500_bit0 -CO100501_bit0 -CO100502_bit0 -CO100503_bit0 -CO100504_bit0 -CO100505_bit0 -CO100506_bit0 -CO100507_bit0 -CO100508_bit0 -CO100509_bit0 -CO100510_bit0 -CO100511_bit0 -CO100512_bit0 -CO100513_bit0 -CO100514_bit0 -CO100515_bit0 -CO100516_bit0 -CO100517_bit0 -CO100518_bit0 -CO100519_bit0 -CO100520_bit0 -CO100521_bit0 -CO100522_bit0 -CO100523_bit0 -CO100524_bit0 -CO100525_bit0 -CO100526_bit0 -CO100527_bit0 -CO100528_bit0 -CO100529_bit0 -CO100530_bit0 CO100531_bit0 -CO100532_bit0 -CO100533_bit0 -CO100534_bit0 -CO100535_bit0 -CO100536_bit0 -CO100537_bit0 -CO100538_bit0 -CO100539_bit0 -CO100540_bit0 -CO100541_bit0 -CO100542_bit0 -CO100543_bit0 -CO100544_bit0 -CO100545_bit0 -CO100546_bit0 -CO100547_bit0 -CO100548_bit0 -CO100549_bit0 -CO100550_bit0 -CO100551_bit0 -CO100552_bit0 -CO100553_bit0 -CO100554_bit0 -CO100555_bit0 -CO100556_bit0 -CO100557_bit0 -CO100558_bit0 -CO100559_bit0 -CO100560_bit0 -CO100561_bit0 -CO100562_bit0 -CO100563_bit0 -CO100564_bit0 -CO100565_bit0 -CO100566_bit0 -CO100567_bit0 -CO100568_bit0 -CO100569_bit0 -CO100570_bit0 -CO100571_bit0 -CO100572_bit0 -CO100573_bit0 -CO100574_bit0 -CO100575_bit0 -CO100576_bit0 -CO100577_bit0 -CO100578_bit0 -CO100579_bit0 -CO100580_bit0 -CO100581_bit0 -CO100582_bit0 -CO100583_bit0 -CO100584_bit0 -CO100585_bit0 -CO100586_bit0 -CO100587_bit0 -CO100588_bit0 -CO100589_bit0 -CO100590_bit0 -CO100591_bit0 -CO100592_bit0 -CO100593_bit0 -CO100594_bit0 -CO100595_bit0 -CO100596_bit0 -CO100597_bit0 -CO100598_bit0 -CO100599_bit0 -CO100600_bit0 -CO100601_bit0 -CO100602_bit0 -CO100603_bit0 -CO100604_bit0 -CO100605_bit0 -CO100606_bit0 -CO100607_bit0 -CO100608_bit0 -CO100609_bit0 -CO100610_bit0 -CO100611_bit0 -CO100612_bit0 -CO100613_bit0 -CO100614_bit0 -CO100615_bit0 -CO100616_bit0 -CO100617_bit0 -CO100618_bit0 -CO100619_bit0 -CO100620_bit0 -CO100621_bit0 -CO100622_bit0 -CO100623_bit0 -CO100624_bit0 CO100625_bit0 -CO100626_bit0 -CO100627_bit0 -CO100628_bit0 -CO100629_bit0 -CO100630_bit0 -CO100631_bit0 -CO100632_bit0 -CO100633_bit0 -CO100634_bit0 -CO100635_bit0 -CO100636_bit0 -CO100637_bit0 -CO100638_bit0 -CO100639_bit0 -CO100640_bit0 -CO100641_bit0 -CO100642_bit0 -CO100643_bit0 -CO100644_bit0 -CO100645_bit0 -CO100646_bit0 -CO100647_bit0 -CO100648_bit0 -CO100649_bit0 -CO100650_bit0 -CO100651_bit0 -CO100652_bit0 -CO100653_bit0 -CO100654_bit0 -CO100655_bit0 -CO100656_bit0 -CO100657_bit0 -CO100658_bit0 -CO100659_bit0 -CO100660_bit0 -CO100661_bit0 -CO100662_bit0 -CO100663_bit0 -CO100664_bit0 -CO100665_bit0 -CO100666_bit0 -CO100667_bit0 -CO100668_bit0 -CO100669_bit0 -CO100670_bit0 -CO100671_bit0 -CO100672_bit0 -CO100673_bit0 -CO100674_bit0 -CO100675_bit0 -CO100676_bit0 -CO100677_bit0 -CO100678_bit0 -CO100679_bit0 -CO100680_bit0 -CO100681_bit0 -CO100682_bit0 -CO100683_bit0 -CO100684_bit0 -CO100685_bit0 -CO100686_bit0 -CO100687_bit0 -CO100688_bit0 -CO100689_bit0 -CO100690_bit0 -CO100691_bit0 -CO100692_bit0 -CO100693_bit0 -CO100694_bit0 -CO100695_bit0 -CO100696_bit0 -CO100697_bit0 -CO100698_bit0 -CO100699_bit0 -CO100700_bit0 -CO100701_bit0 -CO100702_bit0 -CO100703_bit0 -CO100704_bit0 -CO100705_bit0 -CO100706_bit0 -CO100707_bit0 -CO100708_bit0 -CO100709_bit0 -CO100710_bit0 -CO100711_bit0 -CO100712_bit0 -CO100713_bit0 -CO100714_bit0 -CO100715_bit0 -CO100716_bit0 -CO100717_bit0 -CO100718_bit0 -CO100719_bit0 -CO100720_bit0 -CO100721_bit0 -CO100722_bit0 -CO100723_bit0 -CO100724_bit0 -CO100725_bit0 -CO100726_bit0 -CO100727_bit0 -CO100728_bit0 -CO100729_bit0 -CO100730_bit0 -CO100731_bit0 -CO100732_bit0 -CO100733_bit0 -CO100734_bit0 -CO100735_bit0 -CO100736_bit0 -CO100737_bit0 -CO100738_bit0 -CO100739_bit0 -CO100740_bit0 -CO100741_bit0 -CO100742_bit0 -CO100743_bit0 -CO100744_bit0 -CO100745_bit0 -CO100746_bit0 -CO100747_bit0 -CO100748_bit0 -CO100749_bit0 -CO100750_bit0 -CO100751_bit0 -CO100752_bit0 -CO100753_bit0 -CO100754_bit0 -CO100755_bit0 -CO100756_bit0 -CO100757_bit0 -CO100758_bit0 -CO100759_bit0 -CO100760_bit0 -CO100761_bit0 -CO100762_bit0 -CO100763_bit0 -CO100764_bit0 -CO100765_bit0 -CO100766_bit0 -CO100767_bit0 -CO100768_bit0 -CO100769_bit0 -CO100770_bit0 -CO100771_bit0 -CO100772_bit0 -CO100773_bit0 -CO100774_bit0 -CO100775_bit0 -CO100776_bit0 CO100777_bit0 -CO100778_bit0 -CO100779_bit0 -CO100780_bit0 -CO100781_bit0 -CO100782_bit0 -CO100783_bit0 -CO100784_bit0 -CO100785_bit0 -CO100786_bit0 -CO100787_bit0 -CO100788_bit0 -CO100789_bit0 -CO100790_bit0 -CO100791_bit0 -CO100792_bit0 -CO100793_bit0 -CO100794_bit0 -CO100795_bit0 -CO100796_bit0 -CO100797_bit0 -CO100798_bit0 -CO100799_bit0 CO100800_bit0 -CO100801_bit0 -CO100802_bit0 -CO100803_bit0 -CO100804_bit0 -CO100805_bit0 -CO100806_bit0 -CO100807_bit0 -CO100808_bit0 -CO100809_bit0 -CO100810_bit0 CO100811_bit0 -CO100812_bit0 -CO100813_bit0 -CO100814_bit0 -CO100815_bit0 -CO100816_bit0 -CO100817_bit0 -CO100818_bit0 #### 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.92 2/54 18369
Raw data (stat): 18369 (runsolver) R 18368 20937 20936 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 491898011 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.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 1497 0 0 0 994 3 0 0 25 0 1 0 491898011 7938048 1471 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1938 1471 603 41 0 1897 0
vsize: 7752
[startup+20.0014 s]
Raw data (loadavg): 0.94 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 1580 0 0 0 1994 3 0 0 25 0 1 0 491898011 8335360 1554 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2035 1554 603 41 0 1994 0
vsize: 8140
[startup+30.0024 s]
Raw data (loadavg): 0.95 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 1742 0 0 0 2993 3 0 0 25 0 1 0 491898011 9011200 1716 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2200 1717 603 41 0 2159 0
vsize: 8800
[startup+40.0024 s]
Raw data (loadavg): 0.96 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 1917 0 0 0 3992 4 0 0 25 0 1 0 491898011 9826304 1891 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2399 1891 603 41 0 2358 0
vsize: 9596
[startup+50.0025 s]
Raw data (loadavg): 0.96 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 2206 0 0 0 4991 5 0 0 25 0 1 0 491898011 10903552 2180 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2662 2180 603 41 0 2621 0
vsize: 10648
[startup+60.0026 s]
Raw data (loadavg): 0.97 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 2519 0 0 0 5989 7 0 0 25 0 1 0 491898011 12242944 2493 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2989 2493 603 41 0 2948 0
vsize: 11956
[startup+70.0032 s]
Raw data (loadavg): 0.97 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 2837 0 0 0 6988 8 0 0 25 0 1 0 491898011 13586432 2811 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3317 2811 603 41 0 3276 0
vsize: 13268
[startup+80.0036 s]
Raw data (loadavg): 0.98 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 3153 0 0 0 7988 8 0 0 25 0 1 0 491898011 14811136 3127 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3616 3127 603 41 0 3575 0
vsize: 14464
[startup+90.0037 s]
Raw data (loadavg): 0.98 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 3582 0 0 0 8987 9 0 0 25 0 1 0 491898011 16551936 3556 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4041 3556 603 41 0 4000 0
vsize: 16164
[startup+100.004 s]
Raw data (loadavg): 0.98 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 3935 0 0 0 9987 10 0 0 25 0 1 0 491898011 18026496 3909 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4401 3909 603 41 0 4360 0
vsize: 17604
[startup+110.005 s]
Raw data (loadavg): 0.98 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 4242 0 0 0 10986 11 0 0 25 0 1 0 491898011 19243008 4216 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4698 4216 603 41 0 4657 0
vsize: 18792
[startup+120.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 4631 0 0 0 11985 12 0 0 25 0 1 0 491898011 20865024 4605 4294967295 134512640 134672761 3221224544 3221223712 134560970 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5094 4605 603 41 0 5053 0
vsize: 20376
[startup+130.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 4894 0 0 0 12985 13 0 0 25 0 1 0 491898011 21934080 4868 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5355 4868 603 41 0 5314 0
vsize: 21420
[startup+140.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 5099 0 0 0 13984 14 0 0 25 0 1 0 491898011 22740992 5073 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5552 5073 603 41 0 5511 0
vsize: 22208
[startup+150.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 5529 0 0 0 14983 15 0 0 25 0 1 0 491898011 24477696 5503 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5976 5503 603 41 0 5935 0
vsize: 23904
[startup+160.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 5957 0 0 0 15982 16 0 0 25 0 1 0 491898011 26222592 5931 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6402 5931 603 41 0 6361 0
vsize: 25608
[startup+170.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 6813 0 0 0 16981 18 0 0 25 0 1 0 491898011 30453760 6782 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7435 6782 603 41 0 7394 0
vsize: 29740
[startup+180.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 6832 0 0 0 17981 18 0 0 25 0 1 0 491898011 30613504 6801 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7474 6801 603 41 0 7433 0
vsize: 29896
[startup+190.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 6832 0 0 0 18981 18 0 0 25 0 1 0 491898011 30613504 6801 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7474 6801 603 41 0 7433 0
vsize: 29896
[startup+200.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 6842 0 0 0 19981 18 0 0 25 0 1 0 491898011 30613504 6811 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7474 6811 603 41 0 7433 0
vsize: 29896
[startup+210.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 6842 0 0 0 20981 18 0 0 25 0 1 0 491898011 30613504 6811 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7474 6811 603 41 0 7433 0
vsize: 29896
[startup+220.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 6842 0 0 0 21981 18 0 0 25 0 1 0 491898011 30613504 6811 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7474 6811 603 41 0 7433 0
vsize: 29896
[startup+230.008 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 6842 0 0 0 22981 18 0 0 25 0 1 0 491898011 30613504 6811 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7474 6811 603 41 0 7433 0
vsize: 29896
[startup+240.008 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 7387 0 0 0 23980 19 0 0 25 0 1 0 491898011 32894976 7356 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8031 7356 603 41 0 7990 0
vsize: 32124
[startup+250.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 7917 0 0 0 24978 21 0 0 25 0 1 0 491898011 34983936 7886 4294967295 134512640 134672761 3221224544 3221223844 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8541 7886 603 41 0 8500 0
vsize: 34164
[startup+260.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 7917 0 0 0 25978 21 0 0 25 0 1 0 491898011 34983936 7886 4294967295 134512640 134672761 3221224544 3221223648 134560390 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8541 7886 603 41 0 8500 0
vsize: 34164
[startup+270.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 7917 0 0 0 26979 21 0 0 25 0 1 0 491898011 34983936 7886 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8541 7886 603 41 0 8500 0
vsize: 34164
[startup+280.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 7917 0 0 0 27979 21 0 0 25 0 1 0 491898011 34983936 7886 4294967295 134512640 134672761 3221224544 3221223500 1075349639 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8541 7886 603 41 0 8500 0
vsize: 34164
[startup+290.008 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 7917 0 0 0 28979 21 0 0 25 0 1 0 491898011 34983936 7886 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8541 7886 603 41 0 8500 0
vsize: 34164
[startup+300.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 7917 0 0 0 29979 21 0 0 25 0 1 0 491898011 34983936 7886 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8541 7886 603 41 0 8500 0
vsize: 34164
[startup+310.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 8365 0 0 0 30978 23 0 0 25 0 1 0 491898011 36868096 8334 4294967295 134512640 134672761 3221224544 3221223712 134561133 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9001 8334 603 41 0 8960 0
vsize: 36004
[startup+320.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 8456 0 0 0 31978 23 0 0 25 0 1 0 491898011 37171200 8425 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9075 8425 603 41 0 9034 0
vsize: 36300
[startup+330.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 8456 0 0 0 32978 23 0 0 25 0 1 0 491898011 37171200 8425 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9075 8425 603 41 0 9034 0
vsize: 36300
[startup+340.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 8456 0 0 0 33978 23 0 0 25 0 1 0 491898011 37171200 8425 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9075 8425 603 41 0 9034 0
vsize: 36300
[startup+350.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 8456 0 0 0 34978 23 0 0 25 0 1 0 491898011 37171200 8425 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9075 8425 603 41 0 9034 0
vsize: 36300
[startup+360.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 8456 0 0 0 35978 23 0 0 25 0 1 0 491898011 37171200 8425 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9075 8425 603 41 0 9034 0
vsize: 36300
[startup+370.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 8651 0 0 0 36978 23 0 0 25 0 1 0 491898011 37969920 8620 4294967295 134512640 134672761 3221224544 3221223776 134541850 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9270 8620 603 41 0 9229 0
vsize: 37080
[startup+380.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 9397 0 0 0 37975 26 0 0 25 0 1 0 491898011 41017344 9366 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10014 9366 603 41 0 9973 0
vsize: 40056
[startup+390.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 9962 0 0 0 38974 28 0 0 25 0 1 0 491898011 43421696 9931 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10601 9931 603 41 0 10560 0
vsize: 42404
[startup+400.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 10542 0 0 0 39973 29 0 0 25 0 1 0 491898011 45699072 10511 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11157 10511 603 41 0 11116 0
vsize: 44628
[startup+410.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 11147 0 0 0 40972 31 0 0 25 0 1 0 491898011 48222208 11116 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11773 11116 603 41 0 11732 0
vsize: 47092
[startup+420.011 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 11840 0 0 0 41970 32 0 0 25 0 1 0 491898011 51052544 11809 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12464 11809 603 41 0 12423 0
vsize: 49856
[startup+430.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 12467 0 0 0 42969 34 0 0 25 0 1 0 491898011 53612544 12436 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13089 12436 603 41 0 13048 0
vsize: 52356
[startup+440.013 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 12901 0 0 0 43967 36 0 0 25 0 1 0 491898011 55484416 12870 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13546 12870 603 41 0 13505 0
vsize: 54184
[startup+450.014 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 13513 0 0 0 44966 37 0 0 25 0 1 0 491898011 57884672 13482 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14132 13482 603 41 0 14091 0
vsize: 56528
[startup+460.013 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 14056 0 0 0 45965 38 0 0 25 0 1 0 491898011 60153856 14025 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14686 14025 603 41 0 14645 0
vsize: 58744
[startup+470.014 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 14528 0 0 0 46965 39 0 0 25 0 1 0 491898011 62038016 14497 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15146 14497 603 41 0 15105 0
vsize: 60584
[startup+480.014 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 15044 0 0 0 47963 41 0 0 25 0 1 0 491898011 64200704 15013 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15674 15013 603 41 0 15633 0
vsize: 62696
[startup+490.013 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 15599 0 0 0 48962 42 0 0 25 0 1 0 491898011 66478080 15568 4294967295 134512640 134672761 3221224544 3221223712 134560806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16230 15568 603 41 0 16189 0
vsize: 64920
[startup+500.013 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 15822 0 0 0 49961 43 0 0 25 0 1 0 491898011 67420160 15791 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16460 15791 603 41 0 16419 0
vsize: 65840
[startup+510.014 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 16351 0 0 0 50960 44 0 0 25 0 1 0 491898011 69570560 16320 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16985 16320 603 41 0 16944 0
vsize: 67940
[startup+520.014 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 16762 0 0 0 51960 45 0 0 25 0 1 0 491898011 71176192 16731 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17377 16731 603 41 0 17336 0
vsize: 69508
[startup+530.014 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 17363 0 0 0 52958 47 0 0 25 0 1 0 491898011 73719808 17332 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17998 17332 603 41 0 17957 0
vsize: 71992
[startup+540.014 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 17756 0 0 0 53957 48 0 0 25 0 1 0 491898011 75599872 17725 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18457 17725 603 41 0 18416 0
vsize: 73828
[startup+550.015 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 18101 0 0 0 54957 48 0 0 25 0 1 0 491898011 76939264 18070 4294967295 134512640 134672761 3221224544 3221223680 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18784 18070 603 41 0 18743 0
vsize: 75136
[startup+560.015 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 18651 0 0 0 55955 50 0 0 25 0 1 0 491898011 79204352 18620 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19337 18620 603 41 0 19296 0
vsize: 77348
[startup+570.015 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 19224 0 0 0 56954 52 0 0 25 0 1 0 491898011 81616896 19193 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19926 19193 603 41 0 19885 0
vsize: 79704
[startup+580.016 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 19759 0 0 0 57952 53 0 0 25 0 1 0 491898011 83755008 19728 4294967295 134512640 134672761 3221224544 3221223500 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20448 19728 603 41 0 20407 0
vsize: 81792
[startup+590.015 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 20225 0 0 0 58952 54 0 0 25 0 1 0 491898011 85622784 20194 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20904 20194 603 41 0 20863 0
vsize: 83616
[startup+600.015 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 20720 0 0 0 59951 55 0 0 25 0 1 0 491898011 87740416 20689 4294967295 134512640 134672761 3221224544 3221223648 134560370 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21421 20689 603 41 0 21380 0
vsize: 85684
[startup+610.016 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 21205 0 0 0 60950 56 0 0 25 0 1 0 491898011 89612288 21174 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21878 21174 603 41 0 21837 0
vsize: 87512
[startup+620.017 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 21653 0 0 0 61948 58 0 0 25 0 1 0 491898011 91496448 21622 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22338 21622 603 41 0 22297 0
vsize: 89352
[startup+630.018 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 22108 0 0 0 62945 61 0 0 25 0 1 0 491898011 93372416 22077 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22796 22077 603 41 0 22755 0
vsize: 91184
[startup+640.017 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 22583 0 0 0 63944 62 0 0 25 0 1 0 491898011 95244288 22552 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23253 22552 603 41 0 23212 0
vsize: 93012
[startup+650.018 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 23085 0 0 0 64943 64 0 0 25 0 1 0 491898011 97382400 23054 4294967295 134512640 134672761 3221224544 3221223700 134561032 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23775 23054 603 41 0 23734 0
vsize: 95100
[startup+660.018 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 23577 0 0 0 65941 65 0 0 25 0 1 0 491898011 99397632 23546 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24267 23546 603 41 0 24226 0
vsize: 97068
[startup+670.018 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 24057 0 0 0 66940 67 0 0 25 0 1 0 491898011 101261312 24026 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24722 24026 603 41 0 24681 0
vsize: 98888
[startup+680.019 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 24470 0 0 0 67939 68 0 0 25 0 1 0 491898011 102998016 24439 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25146 24439 603 41 0 25105 0
vsize: 100584
[startup+690.019 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 24830 0 0 0 68939 68 0 0 25 0 1 0 491898011 104472576 24799 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25506 24799 603 41 0 25465 0
vsize: 102024
[startup+700.019 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 25256 0 0 0 69938 69 0 0 25 0 1 0 491898011 106221568 25225 4294967295 134512640 134672761 3221224544 3221223680 134560661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25933 25225 603 41 0 25892 0
vsize: 103732
[startup+710.019 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 25702 0 0 0 70937 70 0 0 25 0 1 0 491898011 108089344 25671 4294967295 134512640 134672761 3221224544 3221223728 134558899 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26389 25671 603 41 0 26348 0
vsize: 105556
[startup+720.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 26065 0 0 0 71936 71 0 0 25 0 1 0 491898011 109563904 26034 4294967295 134512640 134672761 3221224544 3221223500 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26749 26034 603 41 0 26708 0
vsize: 106996
[startup+730.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 26404 0 0 0 72936 72 0 0 25 0 1 0 491898011 110907392 26373 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27077 26373 603 41 0 27036 0
vsize: 108308
[startup+740.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 26750 0 0 0 73935 73 0 0 25 0 1 0 491898011 112373760 26719 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27435 26719 603 41 0 27394 0
vsize: 109740
[startup+750.021 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 27176 0 0 0 74935 74 0 0 25 0 1 0 491898011 114106368 27145 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27858 27145 603 41 0 27817 0
vsize: 111432
[startup+760.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 27664 0 0 0 75933 75 0 0 25 0 1 0 491898011 116109312 27633 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28347 27633 603 41 0 28306 0
vsize: 113388
[startup+770.021 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 28026 0 0 0 76933 76 0 0 25 0 1 0 491898011 117583872 27995 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28707 27995 603 41 0 28666 0
vsize: 114828
[startup+780.021 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 28378 0 0 0 77932 77 0 0 25 0 1 0 491898011 118931456 28347 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29036 28347 603 41 0 28995 0
vsize: 116144
[startup+790.021 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 28704 0 0 0 78932 77 0 0 25 0 1 0 491898011 120266752 28673 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29362 28673 603 41 0 29321 0
vsize: 117448
[startup+800.021 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 29153 0 0 0 79931 78 0 0 25 0 1 0 491898011 122142720 29122 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29820 29122 603 41 0 29779 0
vsize: 119280
[startup+810.021 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 29575 0 0 0 80930 79 0 0 25 0 1 0 491898011 123879424 29544 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30244 29544 603 41 0 30203 0
vsize: 120976
[startup+820.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 30026 0 0 0 81930 80 0 0 25 0 1 0 491898011 125657088 29995 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30678 29995 603 41 0 30637 0
vsize: 122712
[startup+830.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 30277 0 0 0 82929 81 0 0 25 0 1 0 491898011 126730240 30246 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30940 30246 603 41 0 30899 0
vsize: 123760
[startup+840.026 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 30712 0 0 0 83928 83 0 0 25 0 1 0 491898011 128450560 30681 4294967295 134512640 134672761 3221224544 3221223648 134560424 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31360 30681 603 41 0 31319 0
vsize: 125440
[startup+850.027 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 30969 0 0 0 84928 83 0 0 25 0 1 0 491898011 129511424 30938 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31619 30938 603 41 0 31578 0
vsize: 126476
[startup+860.028 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 31382 0 0 0 85927 85 0 0 25 0 1 0 491898011 131239936 31351 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32041 31351 603 41 0 32000 0
vsize: 128164
[startup+870.028 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 31684 0 0 0 86926 85 0 0 25 0 1 0 491898011 132435968 31653 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32333 31653 603 41 0 32292 0
vsize: 129332
[startup+880.029 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 32034 0 0 0 87925 86 0 0 25 0 1 0 491898011 133922816 32003 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32696 32003 603 41 0 32655 0
vsize: 130784
[startup+890.028 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 32452 0 0 0 88925 87 0 0 25 0 1 0 491898011 135655424 32421 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33119 32421 603 41 0 33078 0
vsize: 132476
[startup+900.028 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 32745 0 0 0 89924 88 0 0 25 0 1 0 491898011 136863744 32714 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33414 32714 603 41 0 33373 0
vsize: 133656
[startup+910.028 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 33180 0 0 0 90923 89 0 0 25 0 1 0 491898011 138616832 33149 4294967295 134512640 134672761 3221224544 3221223728 134559498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33842 33149 603 41 0 33801 0
vsize: 135368
[startup+920.028 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 33648 0 0 0 91922 90 0 0 25 0 1 0 491898011 140488704 33617 4294967295 134512640 134672761 3221224544 3221223728 134559161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34299 33617 603 41 0 34258 0
vsize: 137196
[startup+930.029 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 34079 0 0 0 92921 91 0 0 25 0 1 0 491898011 142237696 34048 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34726 34048 603 41 0 34685 0
vsize: 138904
[startup+940.028 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 34376 0 0 0 93921 92 0 0 25 0 1 0 491898011 143446016 34345 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35021 34345 603 41 0 34980 0
vsize: 140084
[startup+950.028 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 34700 0 0 0 94920 92 0 0 25 0 1 0 491898011 144781312 34669 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35347 34669 603 41 0 35306 0
vsize: 141388
[startup+960.027 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 35105 0 0 0 95919 93 0 0 25 0 1 0 491898011 146497536 35074 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35766 35074 603 41 0 35725 0
vsize: 143064
[startup+970.027 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 35491 0 0 0 96919 94 0 0 25 0 1 0 491898011 147976192 35460 4294967295 134512640 134672761 3221224544 3221223648 134560229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36127 35460 603 41 0 36086 0
vsize: 144508
[startup+980.028 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 35876 0 0 0 97918 95 0 0 25 0 1 0 491898011 149565440 35845 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36515 35845 603 41 0 36474 0
vsize: 146060
[startup+990.027 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 36219 0 0 0 98917 96 0 0 25 0 1 0 491898011 151035904 36188 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36874 36188 603 41 0 36833 0
vsize: 147496
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 36593 0 0 0 99916 97 0 0 25 0 1 0 491898011 152518656 36562 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37236 36562 603 41 0 37195 0
vsize: 148944
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 36900 0 0 0 100916 98 0 0 25 0 1 0 491898011 153726976 36869 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37531 36869 603 41 0 37490 0
vsize: 150124
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 37172 0 0 0 101915 99 0 0 25 0 1 0 491898011 154939392 37141 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37827 37141 603 41 0 37786 0
vsize: 151308
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 37535 0 0 0 102915 99 0 0 25 0 1 0 491898011 156405760 37504 4294967295 134512640 134672761 3221224544 3221223696 134561035 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38185 37504 603 41 0 38144 0
vsize: 152740
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 37868 0 0 0 103914 100 0 0 25 0 1 0 491898011 157736960 37837 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38510 37837 603 41 0 38469 0
vsize: 154040
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 37958 0 0 0 104914 100 0 0 25 0 1 0 491898011 158142464 37927 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38609 37927 603 41 0 38568 0
vsize: 154436
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 37958 0 0 0 105915 100 0 0 25 0 1 0 491898011 158142464 37927 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38609 37927 603 41 0 38568 0
vsize: 154436
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 37958 0 0 0 106915 100 0 0 25 0 1 0 491898011 158142464 37927 4294967295 134512640 134672761 3221224544 3221223680 134560654 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38609 37927 603 41 0 38568 0
vsize: 154436
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 37958 0 0 0 107915 100 0 0 25 0 1 0 491898011 158142464 37927 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38609 37927 603 41 0 38568 0
vsize: 154436
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 37958 0 0 0 108916 100 0 0 25 0 1 0 491898011 158142464 37927 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38609 37927 603 41 0 38568 0
vsize: 154436
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 37958 0 0 0 109916 100 0 0 25 0 1 0 491898011 158142464 37927 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38609 37927 603 41 0 38568 0
vsize: 154436
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 37958 0 0 0 110916 100 0 0 25 0 1 0 491898011 158142464 37927 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38609 37927 603 41 0 38568 0
vsize: 154436
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 37958 0 0 0 111916 100 0 0 25 0 1 0 491898011 158142464 37927 4294967295 134512640 134672761 3221224544 3221223668 134566100 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38609 37927 603 41 0 38568 0
vsize: 154436
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 37958 0 0 0 112916 100 0 0 25 0 1 0 491898011 158142464 37927 4294967295 134512640 134672761 3221224544 3221223648 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38609 37927 603 41 0 38568 0
vsize: 154436
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 37958 0 0 0 113916 100 0 0 25 0 1 0 491898011 158142464 37927 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38609 37927 603 41 0 38568 0
vsize: 154436
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 37958 0 0 0 114917 100 0 0 25 0 1 0 491898011 158142464 37927 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38609 37927 603 41 0 38568 0
vsize: 154436
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 37958 0 0 0 115916 100 0 0 25 0 1 0 491898011 158142464 37927 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38609 37927 603 41 0 38568 0
vsize: 154436
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 37958 0 0 0 116916 100 0 0 25 0 1 0 491898011 158142464 37927 4294967295 134512640 134672761 3221224544 3221223712 134560882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38609 37927 603 41 0 38568 0
vsize: 154436
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 37958 0 0 0 117917 100 0 0 25 0 1 0 491898011 158142464 37927 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38609 37927 603 41 0 38568 0
vsize: 154436
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 37958 0 0 0 118917 100 0 0 25 0 1 0 491898011 158142464 37927 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38609 37927 603 41 0 38568 0
vsize: 154436
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 18369
Raw data (stat): 18369 (minisat+) R 18368 20937 20936 0 -1 0 37958 0 0 0 119917 100 0 0 25 0 1 0 491898011 158142464 37927 4294967295 134512640 134672761 3221224544 3221223648 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38609 37927 603 41 0 38568 0
vsize: 154436
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.11 s]
Raw data (loadavg): 0.99 0.98 0.92 1/54 18369
Raw data (stat): 18369 (minisat+) Z 18368 20937 20936 0 -1 12 37961 0 0 0 119917 107 0 0 25 0 1 0 491898011 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.11
CPU time (s): 1200.25
CPU user time (s): 1199.18
CPU system time (s): 1.07784
CPU usage (%): 100.012
Max. virtual memory (Kb): 154436
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####