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-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	3684
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.3
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 15674

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc23 THE 2005-04-21 05:27:02 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=16910 boxname=wulflinc23 idbench=1301 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  3c39e3c2b993ee2185e2a1a3e73b9723  /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-13-7-lp4l.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-13-7-lp4l.opb /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-13-7-lp4l.opb
IDLAUNCH: 16910
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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.037
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:        626568 kB
Buffers:         24116 kB
Cached:         354872 kB
SwapCached:        520 kB
Active:          60140 kB
Inactive:       320932 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        626316 kB
SwapTotal:     2097136 kB
SwapFree:      2095824 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5220 kB
Slab:            21408 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 05:47:04 (client local time) WITH STATUS 10 IN 1200.22 SECONDS
stats: 16910 7 1200.22 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.91 0.97 0.92 1/54 29567
Raw data (stat): 29567 (runsolver) R 29566 3260 3259 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 542551796 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 0 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0013 s]
Raw data (loadavg): 0.93 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 1497 0 0 0 995 3 0 0 25 0 1 0 542551796 7938048 1471 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1938 1471 603 41 0 1897 0
vsize: 7752
[startup+20.0015 s]
Raw data (loadavg): 0.94 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 1568 0 0 0 1993 4 0 0 25 0 1 0 542551796 8335360 1542 4294967295 134512640 134672761 3221224544 3221223744 134557849 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2035 1542 603 41 0 1994 0
vsize: 8140
[startup+30.0012 s]
Raw data (loadavg): 0.95 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 1726 0 0 0 2992 4 0 0 25 0 1 0 542551796 8876032 1700 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2167 1700 603 41 0 2126 0
vsize: 8668
[startup+40.0007 s]
Raw data (loadavg): 0.95 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 1902 0 0 0 3990 6 0 0 25 0 1 0 542551796 9687040 1876 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2365 1876 603 41 0 2324 0
vsize: 9460
[startup+50.0003 s]
Raw data (loadavg): 0.96 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 2171 0 0 0 4990 6 0 0 25 0 1 0 542551796 10768384 2145 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2629 2145 603 41 0 2588 0
vsize: 10516
[startup+60 s]
Raw data (loadavg): 0.97 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 2488 0 0 0 5989 7 0 0 25 0 1 0 542551796 12107776 2462 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2956 2462 603 41 0 2915 0
vsize: 11824
[startup+69.9999 s]
Raw data (loadavg): 0.97 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 2768 0 0 0 6988 8 0 0 25 0 1 0 542551796 13316096 2742 4294967295 134512640 134672761 3221224544 3221223648 134560184 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3251 2742 603 41 0 3210 0
vsize: 13004
[startup+79.9993 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 3100 0 0 0 7987 10 0 0 25 0 1 0 542551796 14675968 3074 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3583 3074 603 41 0 3542 0
vsize: 14332
[startup+89.9989 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 3491 0 0 0 8986 11 0 0 25 0 1 0 542551796 16285696 3465 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3976 3465 603 41 0 3935 0
vsize: 15904
[startup+99.9988 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 3844 0 0 0 9985 12 0 0 25 0 1 0 542551796 17625088 3818 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4303 3818 603 41 0 4262 0
vsize: 17212
[startup+109.999 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 4137 0 0 0 10984 13 0 0 25 0 1 0 542551796 18837504 4111 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4599 4111 603 41 0 4558 0
vsize: 18396
[startup+119.999 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 4508 0 0 0 11983 14 0 0 25 0 1 0 542551796 20324352 4482 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4962 4482 603 41 0 4921 0
vsize: 19848
[startup+129.999 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 4815 0 0 0 12983 14 0 0 25 0 1 0 542551796 21667840 4789 4294967295 134512640 134672761 3221224544 3221223680 134565098 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5290 4790 603 41 0 5249 0
vsize: 21160
[startup+139.998 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 5040 0 0 0 13982 16 0 0 25 0 1 0 542551796 22474752 5014 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5487 5014 603 41 0 5446 0
vsize: 21948
[startup+149.998 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 5273 0 0 0 14981 16 0 0 25 0 1 0 542551796 23543808 5247 4294967295 134512640 134672761 3221224544 3221223728 134558771 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5748 5247 603 41 0 5707 0
vsize: 22992
[startup+159.998 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 5745 0 0 0 15980 17 0 0 25 0 1 0 542551796 25423872 5719 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6207 5719 603 41 0 6166 0
vsize: 24828
[startup+169.997 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 6812 0 0 0 16978 19 0 0 25 0 1 0 542551796 30453760 6781 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7435 6781 603 41 0 7394 0
vsize: 29740
[startup+179.997 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 6832 0 0 0 17978 19 0 0 25 0 1 0 542551796 30613504 6801 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7474 6801 603 41 0 7433 0
vsize: 29896
[startup+189.998 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 6832 0 0 0 18979 19 0 0 25 0 1 0 542551796 30613504 6801 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7474 6801 603 41 0 7433 0
vsize: 29896
[startup+199.997 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 6832 0 0 0 19979 19 0 0 25 0 1 0 542551796 30613504 6801 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7474 6801 603 41 0 7433 0
vsize: 29896
[startup+209.997 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 6842 0 0 0 20979 19 0 0 25 0 1 0 542551796 30613504 6811 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7474 6811 603 41 0 7433 0
vsize: 29896
[startup+219.997 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 6842 0 0 0 21979 19 0 0 25 0 1 0 542551796 30613504 6811 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7474 6811 603 41 0 7433 0
vsize: 29896
[startup+229.996 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 6842 0 0 0 22979 19 0 0 25 0 1 0 542551796 30613504 6811 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7474 6811 603 41 0 7433 0
vsize: 29896
[startup+239.996 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 6951 0 0 0 23979 20 0 0 25 0 1 0 542551796 31019008 6920 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7573 6920 603 41 0 7532 0
vsize: 30292
[startup+249.996 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 7495 0 0 0 24978 21 0 0 25 0 1 0 542551796 33300480 7464 4294967295 134512640 134672761 3221224544 3221223728 134558890 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8130 7464 603 41 0 8089 0
vsize: 32520
[startup+259.996 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 7917 0 0 0 25977 22 0 0 25 0 1 0 542551796 34983936 7886 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8541 7886 603 41 0 8500 0
vsize: 34164
[startup+269.995 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 7917 0 0 0 26977 22 0 0 25 0 1 0 542551796 34983936 7886 4294967295 134512640 134672761 3221224544 3221223696 134541817 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8541 7886 603 41 0 8500 0
vsize: 34164
[startup+279.995 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 7917 0 0 0 27977 22 0 0 25 0 1 0 542551796 34983936 7886 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8541 7886 603 41 0 8500 0
vsize: 34164
[startup+289.996 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 7917 0 0 0 28978 22 0 0 25 0 1 0 542551796 34983936 7886 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8541 7886 603 41 0 8500 0
vsize: 34164
[startup+299.995 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 7917 0 0 0 29978 22 0 0 25 0 1 0 542551796 34983936 7886 4294967295 134512640 134672761 3221224544 3221223648 134560344 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8541 7886 603 41 0 8500 0
vsize: 34164
[startup+309.996 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 7917 0 0 0 30978 22 0 0 25 0 1 0 542551796 34983936 7886 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8541 7886 603 41 0 8500 0
vsize: 34164
[startup+319.996 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 8357 0 0 0 31977 23 0 0 25 0 1 0 542551796 36868096 8326 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9001 8326 603 41 0 8960 0
vsize: 36004
[startup+329.995 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 8456 0 0 0 32977 24 0 0 25 0 1 0 542551796 37171200 8425 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9075 8425 603 41 0 9034 0
vsize: 36300
[startup+339.995 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 8456 0 0 0 33977 24 0 0 25 0 1 0 542551796 37171200 8425 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9075 8425 603 41 0 9034 0
vsize: 36300
[startup+349.995 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 8456 0 0 0 34977 24 0 0 25 0 1 0 542551796 37171200 8425 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9075 8425 603 41 0 9034 0
vsize: 36300
[startup+359.995 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 8456 0 0 0 35977 24 0 0 25 0 1 0 542551796 37171200 8425 4294967295 134512640 134672761 3221224544 3221223648 134560492 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9075 8425 603 41 0 9034 0
vsize: 36300
[startup+369.995 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 8456 0 0 0 36977 24 0 0 25 0 1 0 542551796 37171200 8425 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9075 8425 603 41 0 9034 0
vsize: 36300
[startup+379.994 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 8456 0 0 0 37977 24 0 0 25 0 1 0 542551796 37171200 8425 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9075 8425 603 41 0 9034 0
vsize: 36300
[startup+389.995 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 9118 0 0 0 38976 25 0 0 25 0 1 0 542551796 39952384 9087 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9754 9087 603 41 0 9713 0
vsize: 39016
[startup+399.995 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 9697 0 0 0 39974 27 0 0 25 0 1 0 542551796 42352640 9666 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10340 9666 603 41 0 10299 0
vsize: 41360
[startup+409.995 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 10301 0 0 0 40973 29 0 0 25 0 1 0 542551796 44756992 10270 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10927 10270 603 41 0 10886 0
vsize: 43708
[startup+419.995 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 10788 0 0 0 41972 30 0 0 25 0 1 0 542551796 46772224 10757 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11419 10757 603 41 0 11378 0
vsize: 45676
[startup+429.995 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 11389 0 0 0 42970 32 0 0 25 0 1 0 542551796 49160192 11358 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12002 11358 603 41 0 11961 0
vsize: 48008
[startup+439.995 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 12109 0 0 0 43969 33 0 0 25 0 1 0 542551796 52125696 12078 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12726 12078 603 41 0 12685 0
vsize: 50904
[startup+449.995 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 12604 0 0 0 44967 36 0 0 25 0 1 0 542551796 54136832 12573 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13217 12573 603 41 0 13176 0
vsize: 52868
[startup+459.996 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 13119 0 0 0 45966 37 0 0 25 0 1 0 542551796 56291328 13088 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13743 13088 603 41 0 13702 0
vsize: 54972
[startup+469.995 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 13625 0 0 0 46964 38 0 0 25 0 1 0 542551796 58408960 13594 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14260 13594 603 41 0 14219 0
vsize: 57040
[startup+479.995 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 14213 0 0 0 47963 40 0 0 25 0 1 0 542551796 60825600 14182 4294967295 134512640 134672761 3221224544 3221223712 134560948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14850 14182 603 41 0 14809 0
vsize: 59400
[startup+489.995 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 14621 0 0 0 48962 41 0 0 25 0 1 0 542551796 62443520 14590 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15245 14590 603 41 0 15204 0
vsize: 60980
[startup+499.995 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 15141 0 0 0 49960 43 0 0 25 0 1 0 542551796 64606208 15110 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15773 15110 603 41 0 15732 0
vsize: 63092
[startup+509.995 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 15613 0 0 0 50959 44 0 0 25 0 1 0 542551796 66478080 15582 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16230 15582 603 41 0 16189 0
vsize: 64920
[startup+519.995 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 15876 0 0 0 51959 45 0 0 25 0 1 0 542551796 67555328 15845 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16493 15845 603 41 0 16452 0
vsize: 65972
[startup+529.994 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 16366 0 0 0 52959 45 0 0 25 0 1 0 542551796 69570560 16335 4294967295 134512640 134672761 3221224544 3221223712 134560920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16985 16335 603 41 0 16944 0
vsize: 67940
[startup+539.994 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 16759 0 0 0 53957 47 0 0 25 0 1 0 542551796 71176192 16728 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17377 16728 603 41 0 17336 0
vsize: 69508
[startup+549.994 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 17327 0 0 0 54956 49 0 0 25 0 1 0 542551796 73584640 17296 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17965 17296 603 41 0 17924 0
vsize: 71860
[startup+559.994 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 17712 0 0 0 55955 49 0 0 25 0 1 0 542551796 75067392 17681 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18327 17681 603 41 0 18286 0
vsize: 73308
[startup+569.994 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 18005 0 0 0 56955 50 0 0 25 0 1 0 542551796 76541952 17974 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18687 17974 603 41 0 18646 0
vsize: 74748
[startup+579.994 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 18513 0 0 0 57952 53 0 0 25 0 1 0 542551796 78671872 18482 4294967295 134512640 134672761 3221224544 3221223708 134565024 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19207 18482 603 41 0 19166 0
vsize: 76828
[startup+589.994 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 19090 0 0 0 58951 54 0 0 25 0 1 0 542551796 80949248 19059 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19763 19059 603 41 0 19722 0
vsize: 79052
[startup+599.994 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 19592 0 0 0 59950 55 0 0 25 0 1 0 542551796 83091456 19561 4294967295 134512640 134672761 3221224544 3221223616 134553557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20286 19561 603 41 0 20245 0
vsize: 81144
[startup+609.994 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 20049 0 0 0 60948 57 0 0 25 0 1 0 542551796 84955136 20018 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20741 20018 603 41 0 20700 0
vsize: 82964
[startup+619.994 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 20517 0 0 0 61947 58 0 0 25 0 1 0 542551796 86814720 20486 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21195 20486 603 41 0 21154 0
vsize: 84780
[startup+629.994 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 20991 0 0 0 62946 60 0 0 25 0 1 0 542551796 88801280 20960 4294967295 134512640 134672761 3221224544 3221223728 134559028 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21680 20960 603 41 0 21639 0
vsize: 86720
[startup+639.995 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 21416 0 0 0 63945 61 0 0 25 0 1 0 542551796 90554368 21385 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22108 21385 603 41 0 22067 0
vsize: 88432
[startup+649.994 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 21871 0 0 0 64943 62 0 0 25 0 1 0 542551796 92430336 21840 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22566 21840 603 41 0 22525 0
vsize: 90264
[startup+659.994 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 22298 0 0 0 65943 63 0 0 25 0 1 0 542551796 94175232 22267 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22992 22267 603 41 0 22951 0
vsize: 91968
[startup+669.995 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 22769 0 0 0 66941 64 0 0 25 0 1 0 542551796 96047104 22738 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23449 22738 603 41 0 23408 0
vsize: 93796
[startup+679.994 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 23264 0 0 0 67940 66 0 0 25 0 1 0 542551796 98045952 23233 4294967295 134512640 134672761 3221224544 3221223560 1075352732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23937 23233 603 41 0 23896 0
vsize: 95748
[startup+689.993 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 23724 0 0 0 68938 67 0 0 25 0 1 0 542551796 99938304 23693 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24399 23693 603 41 0 24358 0
vsize: 97596
[startup+699.993 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 24203 0 0 0 69937 69 0 0 25 0 1 0 542551796 101937152 24172 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24887 24172 603 41 0 24846 0
vsize: 99548
[startup+709.994 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 24528 0 0 0 70936 70 0 0 25 0 1 0 542551796 103264256 24497 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25211 24497 603 41 0 25170 0
vsize: 100844
[startup+719.993 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 24889 0 0 0 71935 71 0 0 25 0 1 0 542551796 104751104 24858 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25574 24858 603 41 0 25533 0
vsize: 102296
[startup+729.993 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 25282 0 0 0 72934 72 0 0 25 0 1 0 542551796 106356736 25251 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25966 25251 603 41 0 25925 0
vsize: 103864
[startup+739.994 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 25732 0 0 0 73934 73 0 0 25 0 1 0 542551796 108089344 25701 4294967295 134512640 134672761 3221224544 3221223648 134560350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26389 25701 603 41 0 26348 0
vsize: 105556
[startup+749.993 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 26069 0 0 0 74933 74 0 0 25 0 1 0 542551796 109563904 26038 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26749 26038 603 41 0 26708 0
vsize: 106996
[startup+759.993 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 26388 0 0 0 75932 75 0 0 25 0 1 0 542551796 110776320 26357 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27045 26357 603 41 0 27004 0
vsize: 108180
[startup+769.992 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 26723 0 0 0 76931 76 0 0 25 0 1 0 542551796 112242688 26692 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27403 26692 603 41 0 27362 0
vsize: 109612
[startup+779.992 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 27106 0 0 0 77930 77 0 0 25 0 1 0 542551796 113704960 27075 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27760 27075 603 41 0 27719 0
vsize: 111040
[startup+789.992 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 27597 0 0 0 78929 79 0 0 25 0 1 0 542551796 115838976 27566 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28281 27566 603 41 0 28240 0
vsize: 113124
[startup+799.991 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 27935 0 0 0 79929 79 0 0 25 0 1 0 542551796 117178368 27904 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28608 27904 603 41 0 28567 0
vsize: 114432
[startup+809.992 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 28276 0 0 0 80928 80 0 0 25 0 1 0 542551796 118530048 28245 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28938 28245 603 41 0 28897 0
vsize: 115752
[startup+819.992 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 28564 0 0 0 81927 81 0 0 25 0 1 0 542551796 119726080 28533 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29230 28533 603 41 0 29189 0
vsize: 116920
[startup+829.991 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 29011 0 0 0 82925 83 0 0 25 0 1 0 542551796 121610240 28980 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29690 28980 603 41 0 29649 0
vsize: 118760
[startup+839.991 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 29328 0 0 0 83925 83 0 0 25 0 1 0 542551796 122814464 29297 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29984 29297 603 41 0 29943 0
vsize: 119936
[startup+849.991 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 29866 0 0 0 84924 84 0 0 25 0 1 0 542551796 125112320 29835 4294967295 134512640 134672761 3221224544 3221223648 134560224 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30545 29835 603 41 0 30504 0
vsize: 122180
[startup+859.991 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 30112 0 0 0 85923 85 0 0 25 0 1 0 542551796 126054400 30081 4294967295 134512640 134672761 3221224544 3221223728 134558332 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30775 30081 603 41 0 30734 0
vsize: 123100
[startup+869.991 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 30438 0 0 0 86923 86 0 0 25 0 1 0 542551796 127377408 30407 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31098 30407 603 41 0 31057 0
vsize: 124392
[startup+879.991 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 30817 0 0 0 87922 87 0 0 25 0 1 0 542551796 128974848 30786 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31488 30786 603 41 0 31447 0
vsize: 125952
[startup+889.991 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 31112 0 0 0 88921 87 0 0 25 0 1 0 542551796 130187264 31081 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31784 31081 603 41 0 31743 0
vsize: 127136
[startup+899.991 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 31510 0 0 0 89921 88 0 0 25 0 1 0 542551796 131768320 31479 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32170 31479 603 41 0 32129 0
vsize: 128680
[startup+909.991 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 31758 0 0 0 90920 89 0 0 25 0 1 0 542551796 132841472 31727 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32432 31727 603 41 0 32391 0
vsize: 129728
[startup+919.991 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 32166 0 0 0 91920 89 0 0 25 0 1 0 542551796 134455296 32135 4294967295 134512640 134672761 3221224544 3221223728 134558899 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32826 32135 603 41 0 32785 0
vsize: 131304
[startup+929.991 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 32538 0 0 0 92919 90 0 0 25 0 1 0 542551796 135925760 32507 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33185 32507 603 41 0 33144 0
vsize: 132740
[startup+939.99 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 32820 0 0 0 93918 91 0 0 25 0 1 0 542551796 137134080 32789 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33480 32789 603 41 0 33439 0
vsize: 133920
[startup+949.99 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 33235 0 0 0 94918 92 0 0 25 0 1 0 542551796 138878976 33204 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33906 33204 603 41 0 33865 0
vsize: 135624
[startup+959.99 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 33681 0 0 0 95916 94 0 0 25 0 1 0 542551796 140623872 33650 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34332 33650 603 41 0 34291 0
vsize: 137328
[startup+969.99 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 34091 0 0 0 96915 95 0 0 25 0 1 0 542551796 142372864 34060 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34759 34060 603 41 0 34718 0
vsize: 139036
[startup+979.99 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 34376 0 0 0 97914 96 0 0 25 0 1 0 542551796 143446016 34345 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35021 34345 603 41 0 34980 0
vsize: 140084
[startup+989.99 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 34685 0 0 0 98913 97 0 0 25 0 1 0 542551796 144781312 34654 4294967295 134512640 134672761 3221224544 3221223712 134560979 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35347 34654 603 41 0 35306 0
vsize: 141388
[startup+999.99 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 35071 0 0 0 99913 98 0 0 25 0 1 0 542551796 146362368 35040 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35733 35040 603 41 0 35692 0
vsize: 142932
[startup+1009.99 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 35411 0 0 0 100912 99 0 0 25 0 1 0 542551796 147705856 35380 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36061 35380 603 41 0 36020 0
vsize: 144244
[startup+1019.99 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 35792 0 0 0 101911 99 0 0 25 0 1 0 542551796 149299200 35761 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36450 35761 603 41 0 36409 0
vsize: 145800
[startup+1029.99 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 36159 0 0 0 102910 100 0 0 25 0 1 0 542551796 150765568 36128 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36808 36128 603 41 0 36767 0
vsize: 147232
[startup+1039.99 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 36475 0 0 0 103910 101 0 0 25 0 1 0 542551796 152113152 36444 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37137 36445 603 41 0 37096 0
vsize: 148548
[startup+1049.99 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 36826 0 0 0 104909 102 0 0 25 0 1 0 542551796 153456640 36795 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37465 36795 603 41 0 37424 0
vsize: 149860
[startup+1059.99 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 37025 0 0 0 105909 102 0 0 25 0 1 0 542551796 154267648 36994 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37663 36994 603 41 0 37622 0
vsize: 150652
[startup+1069.99 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 37379 0 0 0 106908 103 0 0 25 0 1 0 542551796 155738112 37348 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38022 37348 603 41 0 37981 0
vsize: 152088
[startup+1079.99 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 37702 0 0 0 107908 104 0 0 25 0 1 0 542551796 157065216 37671 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38346 37671 603 41 0 38305 0
vsize: 153384
[startup+1089.99 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 37958 0 0 0 108907 104 0 0 25 0 1 0 542551796 158142464 37927 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38609 37927 603 41 0 38568 0
vsize: 154436
[startup+1099.99 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 37958 0 0 0 109907 104 0 0 25 0 1 0 542551796 158142464 37927 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38609 37927 603 41 0 38568 0
vsize: 154436
[startup+1109.99 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 37958 0 0 0 110907 104 0 0 25 0 1 0 542551796 158142464 37927 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38609 37927 603 41 0 38568 0
vsize: 154436
[startup+1119.99 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 37958 0 0 0 111908 104 0 0 25 0 1 0 542551796 158142464 37927 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38609 37927 603 41 0 38568 0
vsize: 154436
[startup+1129.99 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 37958 0 0 0 112908 104 0 0 25 0 1 0 542551796 158142464 37927 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38609 37927 603 41 0 38568 0
vsize: 154436
[startup+1139.99 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 37958 0 0 0 113908 104 0 0 25 0 1 0 542551796 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+1149.99 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 37958 0 0 0 114908 104 0 0 25 0 1 0 542551796 158142464 37927 4294967295 134512640 134672761 3221224544 3221223648 134559887 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38609 37927 603 41 0 38568 0
vsize: 154436
[startup+1159.99 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 37958 0 0 0 115908 104 0 0 25 0 1 0 542551796 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+1169.99 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 37958 0 0 0 116908 104 0 0 25 0 1 0 542551796 158142464 37927 4294967295 134512640 134672761 3221224544 3221223648 134555116 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38609 37927 603 41 0 38568 0
vsize: 154436
[startup+1179.99 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 37958 0 0 0 117908 104 0 0 25 0 1 0 542551796 158142464 37927 4294967295 134512640 134672761 3221224544 3221223600 134565058 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38609 37927 603 41 0 38568 0
vsize: 154436
[startup+1189.99 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 37958 0 0 0 118909 105 0 0 25 0 1 0 542551796 158142464 37927 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38609 37927 603 41 0 38568 0
vsize: 154436
[startup+1199.99 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 29567
Raw data (stat): 29567 (minisat+) R 29566 3260 3259 0 -1 0 37958 0 0 0 119909 105 0 0 25 0 1 0 542551796 158142464 37927 4294967295 134512640 134672761 3221224544 3221223712 134561164 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.07 s]
Raw data (loadavg): 0.99 0.97 0.92 1/54 29567
Raw data (stat): 29567 (minisat+) Z 29566 3260 3259 0 -1 12 37961 0 0 0 119909 112 0 0 25 0 1 0 542551796 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

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