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/web/www.nlsde.buaa.edu.cn/~kexu/benchmarks/frb35-17-opb/normalized-frb35-17-5.opb
MD5SUM	70070c820bc7d178cc8f33b42e0deead
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-28
Optimality of the best value was proved	NO
Number of terms in the objective function	595
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	595
Number of bits of the sum of numbers in the objective function	10
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	595
Number of bits of the biggest sum of numbers	10
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.05
Number of variables	595
Total number of constraints	28143
Number of constraints which are clauses	28143
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	2
Maximum length of a constraint	2
Trace number 5239

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc12 THE 2005-04-13 22:50:40 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3707 boxname=wulflinc12 idbench=323 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  70070c820bc7d178cc8f33b42e0deead  /oldhome/oroussel/tmp/wulflinc12/normalized-frb35-17-5.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc12/normalized-frb35-17-5.opb /oldhome/oroussel/tmp/wulflinc12/normalized-frb35-17-5.opb
IDLAUNCH: 3707
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.091
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.091
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:        918032 kB
Buffers:         34796 kB
Cached:          62632 kB
SwapCached:         16 kB
Active:          60384 kB
Inactive:        39860 kB
HighTotal:      131008 kB
HighFree:        64512 kB
LowTotal:       903652 kB
LowFree:        853520 kB
SwapTotal:     2097136 kB
SwapFree:      2097120 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            10948 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 23:10:42 (client local time) WITH STATUS 10 IN 1200.17 SECONDS
stats: 3707 7 1200.17 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 28143 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ...............................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   28143    56286 |    9381       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: -21[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 1165   maxlim: 21   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   36101    84741 |   12033       0        0     nan |  0.000 % |
c |       100 |   36101    84741 |   13236     100     1163    11.6 |  0.177 % |
c |       250 |   36101    84741 |   14559     250     2484     9.9 |  0.172 % |
c ==============================================================================
c [1mFound solution: -22[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 22   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       365 |   36110    84780 |   12036     365     3527     9.7 |  0.172 % |
c |       465 |   36110    84780 |   13239     465     5075    10.9 |  0.232 % |
c |       617 |   36101    84749 |   14563     610     6239    10.2 |  0.286 % |
c ==============================================================================
c [1mFound solution: -23[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 23   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       741 |   36102    84753 |   12034     734     7681    10.5 |  0.286 % |
c |       844 |   36093    84722 |   13237     834     9135    11.0 |  0.400 % |
c ==============================================================================
c [1mFound solution: -24[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 24   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       930 |   36096    84735 |   12032     920    10039    10.9 |  0.400 % |
c |      1030 |   36087    84704 |   13235    1017    11684    11.5 |  0.519 % |
c |      1181 |   36063    84622 |   14558    1163    14118    12.1 |  0.691 % |
c |      1406 |   36054    84591 |   16014    1386    17386    12.5 |  0.743 % |
c |      1744 |   36027    84498 |   17616    1716    22319    13.0 |  0.919 % |
c ==============================================================================
c [1mFound solution: -25[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 25   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1883 |   36028    84504 |   12009    1855    25294    13.6 |  0.919 % |
c |      1983 |   36028    84504 |   13209    1955    26238    13.4 |  0.971 % |
c |      2133 |   36019    84473 |   14530    2102    28249    13.4 |  1.033 % |
c |      2361 |   36010    84442 |   15983    2326    33754    14.5 |  1.085 % |
c |      2698 |   35956    84256 |   17582    2646    39058    14.8 |  1.432 % |
c |      3205 |   35899    84061 |   19340    3137    49155    15.7 |  1.832 % |
c |      3964 |   35480    82628 |   21274    3764    63671    16.9 |  4.969 % |
c ==============================================================================
c [1mFound solution: -26[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 26   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4515 |   35341    82153 |   11780    4272    74597    17.5 |  4.969 % |
c |      4615 |   35341    82153 |   12958    4372    77222    17.7 |  6.221 % |
c |      4765 |   35332    82122 |   14253    4519    80061    17.7 |  6.279 % |
c |      4990 |   35237    81795 |   15679    4720    83804    17.8 |  7.078 % |
c |      5327 |   35177    81587 |   17247    5043    96133    19.1 |  7.648 % |
c |      5833 |   35069    81219 |   18971    5521   113249    20.5 |  8.448 % |
c ==============================================================================
c [1mFound solution: -27[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 27   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6483 |   34835    80411 |   11611    6092   133615    21.9 |  8.448 % |
c |      6583 |   34744    80098 |   12772    6166   136198    22.1 | 11.585 % |
c |      6733 |   34744    80098 |   14049    6316   140060    22.2 | 11.580 % |
c |      6959 |   34726    80036 |   15454    6536   147481    22.6 | 11.694 % |
c |      7297 |   34708    79974 |   16999    6867   157111    22.9 | 11.814 % |
c |      7805 |   34616    79654 |   18699    7341   174815    23.8 | 12.611 % |
c |      8564 |   34581    79533 |   20569    8061   207977    25.8 | 12.892 % |
c |      9705 |   34519    79319 |   22626    9184   311530    33.9 | 13.463 % |
c ==============================================================================
c [1mFound solution: -28[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 28   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     10256 |   34446    79070 |   11482    9682   335078    34.6 | 13.463 % |
c |     10356 |   34429    79011 |   12630    9773   336266    34.4 | 14.310 % |
c |     10506 |   34429    79011 |   13893    9923   348268    35.1 | 14.310 % |
c |     10733 |   34401    78917 |   15282   10142   360700    35.6 | 14.652 % |
c |     11071 |   34375    78827 |   16810   10437   379825    36.4 | 14.880 % |
c |     11577 |   34317    78625 |   18491   10931   415056    38.0 | 15.450 % |
c |     12336 |   34292    78538 |   20341   11686   465604    39.8 | 15.741 % |
c |     13475 |   34239    78355 |   22375   12808   565144    44.1 | 16.253 % |
c |     15183 |   34177    78143 |   24612   14428   659625    45.7 | 16.762 % |
c |     17745 |   34115    77931 |   27073   16966   963360    56.8 | 17.446 % |
c |     21589 |   33845    76997 |   29781   20555  1183069    57.6 | 20.074 % |
c |     27356 |   33834    76958 |   32759   26318  1847608    70.2 | 20.187 % |
c |     36006 |   33834    76958 |   36035   15707  1114508    71.0 | 20.182 % |
c ==============================================================================
c [1mFound solution: -29[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 29   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     37004 |   33835    76964 |   11278   16705  1174855    70.3 | 20.182 % |
c |     37104 |   33835    76964 |   12405    8453   514747    60.9 | 20.234 % |
c |     37255 |   33835    76964 |   13646    8604   517801    60.2 | 20.228 % |
c |     37480 |   33756    76691 |   15011    8819   525936    59.6 | 21.083 % |
c |     37818 |   33756    76691 |   16512    9157   536437    58.6 | 21.083 % |
c |     38324 |   33756    76691 |   18163    9663   567451    58.7 | 21.087 % |
c |     39083 |   33734    76613 |   19979   10418   610457    58.6 | 21.311 % |
c |     40222 |   33734    76613 |   21977   11557   718310    62.2 | 21.315 % |
c |     41930 |   33725    76582 |   24175   13260   840942    63.4 | 21.368 % |
c |     44492 |   33680    76429 |   26592   15796  1036951    65.6 | 21.716 % |
c ==============================================================================
c [1mFound solution: -30[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 30   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     44944 |   33682    76438 |   11227   16248  1069251    65.8 | 21.716 % |
c |     45045 |   33682    76438 |   12349    8225   494828    60.2 | 21.745 % |
c |     45195 |   33682    76438 |   13584    8375   499675    59.7 | 21.742 % |
c |     45420 |   33682    76438 |   14943    8600   507467    59.0 | 21.746 % |
c |     45757 |   33682    76438 |   16437    8937   527977    59.1 | 21.748 % |
c |     46264 |   33664    76376 |   18081    9416   553647    58.8 | 21.855 % |
c |     47023 |   33636    76282 |   19889   10171   584191    57.4 | 22.197 % |
c |     48162 |   33606    76176 |   21878   11297   663440    58.7 | 22.538 % |
c |     49872 |   33606    76176 |   24066   13007   808827    62.2 | 22.544 % |
c |     52434 |   33536    75932 |   26472   15556   998471    64.2 | 23.278 % |
c |     56279 |   33536    75932 |   29119   19401  1384240    71.3 | 23.278 % |
c |     62046 |   33536    75932 |   32031   25168  1934417    76.9 | 23.284 % |
c |     70696 |   33463    75677 |   35235   15338  1064191    69.4 | 24.137 % |
c |     83670 |   33454    75646 |   38758   28307  2294448    81.1 | 24.194 % |
c |    103132 |   33404    75476 |   42634   22620  1640426    72.5 | 24.701 % |
c |    132324 |   33404    75476 |   46897   22042  1951618    88.5 | 24.701 % |
c |    176115 |   33239    74903 |   51587   31538  2912876    92.4 | 26.466 % |
c ==============================================================================
c [1mFound solution: -31[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 31   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    186700 |   33218    74803 |   11072   40948  3543868    86.5 | 26.466 % |
c |    186801 |   33218    74803 |   12179    7164   364940    50.9 | 26.584 % |
c |    186951 |   33218    74803 |   13397    7314   369609    50.5 | 26.579 % |
c |    187177 |   33218    74803 |   14736    7540   381681    50.6 | 26.584 % |
c |    187514 |   33210    74775 |   16210    7873   397823    50.5 | 26.698 % |
c |    188020 |   33202    74747 |   17831    8375   427968    51.1 | 26.807 % |
c |    188781 |   33202    74747 |   19614    9136   473935    51.9 | 26.807 % |
c |    189921 |   33181    74672 |   21576   10267   526660    51.3 | 27.092 % |
c |    191629 |   33181    74672 |   23733   11975   628906    52.5 | 27.096 % |
c |    194192 |   33181    74672 |   26107   14538   791381    54.4 | 27.092 % |
c |    198038 |   33181    74672 |   28717   18384  1043836    56.8 | 27.092 % |
c |    203804 |   33181    74672 |   31589   24150  1601403    66.3 | 27.092 % |
c |    212454 |   33181    74672 |   34748   32800  2608188    79.5 | 27.097 % |
c |    225429 |   33181    74672 |   38223   23671  2229221    94.2 | 27.096 % |
c |    244890 |   33175    74652 |   42045   17966  1498822    83.4 | 27.152 % |
c |    274083 |   33175    74652 |   46250   17738  1472813    83.0 | 27.153 % |
c |    317872 |   33110    74429 |   50875   27986  3537495   126.4 | 27.775 % |
c |    383556 |   33081    74332 |   55963   19681   931131    47.3 | 28.059 % |
c ==============================================================================
c [1mFound solution: -32[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 26   maxlim: 32   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    388658 |   33160    74591 |   11053   24783  1188869    48.0 | 28.059 % |
c |    388758 |   33160    74591 |   12158    6297   212150    33.7 | 28.054 % |
c |    388908 |   33160    74591 |   13374    6447   216384    33.6 | 28.049 % |
c |    389133 |   33160    74591 |   14711    6672   221396    33.2 | 28.050 % |
c |    389470 |   33160    74591 |   16182    7009   238156    34.0 | 28.049 % |
c |    389976 |   33160    74591 |   17800    7515   264868    35.2 | 28.049 % |
c |    390735 |   33160    74591 |   19581    8274   303119    36.6 | 28.055 % |
c |    391876 |   33160    74591 |   21539    9415   364934    38.8 | 28.055 % |
c |    393584 |   33160    74591 |   23693   11123   492392    44.3 | 28.050 % |
c |    396147 |   33160    74591 |   26062   13686   722846    52.8 | 28.049 % |
c |    399991 |   33160    74591 |   28668   17530  1008079    57.5 | 28.049 % |
c |    405757 |   33160    74591 |   31535   23296  1541127    66.2 | 28.049 % |
c |    414406 |   33124    74467 |   34689   31929  2189444    68.6 | 28.387 % |
c |    427380 |   33124    74467 |   38157   23346  1470958    63.0 | 28.391 % |
c |    446842 |   33124    74467 |   41973   17779  1338626    75.3 | 28.391 % |
c |    476034 |   33124    74467 |   46171   18854  1485856    78.8 | 28.390 % |
c |    519825 |   33118    74447 |   50788   30102  2592981    86.1 | 28.447 % |
c |    585509 |   33104    74399 |   55867   22844  2072675    90.7 | 28.612 % |
c |    684035 |   33066    74267 |   61453   42318  2856598    67.5 | 28.893 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.85 0.95 0.90 2/54 29036
Raw data (stat): 29036 (runsolver) R 29035 25285 25284 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 421461184 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0015 s]
Raw data (loadavg): 0.87 0.95 0.90 2/54 29036
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 1599 0 0 0 994 4 0 0 25 0 1 0 421461184 7999488 1577 4294967295 134512640 134672761 3221224560 3221223684 134566077 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1953 1577 603 41 0 1912 0
vsize: 7812
[startup+20.0023 s]
Raw data (loadavg): 0.89 0.96 0.91 2/54 29036
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 2630 0 0 0 1990 8 0 0 25 0 1 0 421461184 12333056 2608 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3011 2608 603 41 0 2970 0
vsize: 12044
[startup+30.0027 s]
Raw data (loadavg): 0.91 0.96 0.91 2/54 29036
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 3417 0 0 0 2988 10 0 0 25 0 1 0 421461184 15544320 3395 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3795 3395 603 41 0 3754 0
vsize: 15180
[startup+40.003 s]
Raw data (loadavg): 0.92 0.96 0.91 2/54 29036
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 3660 0 0 0 3987 11 0 0 25 0 1 0 421461184 16613376 3638 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4056 3638 603 41 0 4015 0
vsize: 16224
[startup+50.0039 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 29036
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 3660 0 0 0 4986 12 0 0 25 0 1 0 421461184 16613376 3638 4294967295 134512640 134672761 3221224560 3221223696 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4056 3638 603 41 0 4015 0
vsize: 16224
[startup+60.0043 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 29036
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 3660 0 0 0 5986 12 0 0 25 0 1 0 421461184 16613376 3638 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4056 3638 603 41 0 4015 0
vsize: 16224
[startup+70.0058 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 29036
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 3832 0 0 0 6985 13 0 0 25 0 1 0 421461184 17285120 3810 4294967295 134512640 134672761 3221224560 3221223744 134559161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4220 3810 603 41 0 4179 0
vsize: 16880
[startup+80.0064 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 29036
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 3832 0 0 0 7985 13 0 0 25 0 1 0 421461184 17285120 3810 4294967295 134512640 134672761 3221224560 3221223728 134561145 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4220 3810 603 41 0 4179 0
vsize: 16880
[startup+90.0068 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 29036
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 4045 0 0 0 8983 14 0 0 25 0 1 0 421461184 18223104 4023 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4449 4023 603 41 0 4408 0
vsize: 17796
[startup+100.007 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 29036
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 4508 0 0 0 9981 17 0 0 25 0 1 0 421461184 20099072 4486 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4907 4486 603 41 0 4866 0
vsize: 19628
[startup+110.008 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 29036
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 4550 0 0 0 10981 17 0 0 25 0 1 0 421461184 20230144 4528 4294967295 134512640 134672761 3221224560 3221223728 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4939 4528 603 41 0 4898 0
vsize: 19756
[startup+120.008 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 29036
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 4550 0 0 0 11980 18 0 0 25 0 1 0 421461184 20230144 4528 4294967295 134512640 134672761 3221224560 3221223744 134559572 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4939 4528 603 41 0 4898 0
vsize: 19756
[startup+130.009 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 29036
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 4550 0 0 0 12980 18 0 0 25 0 1 0 421461184 20230144 4528 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4939 4528 603 41 0 4898 0
vsize: 19756
[startup+140.009 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 29036
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 4810 0 0 0 13980 18 0 0 25 0 1 0 421461184 21282816 4788 4294967295 134512640 134672761 3221224560 3221223560 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5196 4788 603 41 0 5155 0
vsize: 20784
[startup+150.01 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 29036
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 5238 0 0 0 14979 19 0 0 25 0 1 0 421461184 23015424 5216 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5619 5216 603 41 0 5578 0
vsize: 22476
[startup+160.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29036
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 5268 0 0 0 15979 19 0 0 25 0 1 0 421461184 23146496 5246 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5651 5246 603 41 0 5610 0
vsize: 22604
[startup+170.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29036
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 5268 0 0 0 16979 19 0 0 25 0 1 0 421461184 23146496 5246 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5651 5246 603 41 0 5610 0
vsize: 22604
[startup+180.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29036
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 5268 0 0 0 17979 19 0 0 25 0 1 0 421461184 23146496 5246 4294967295 134512640 134672761 3221224560 3221223744 134558629 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5651 5246 603 41 0 5610 0
vsize: 22604
[startup+190.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29036
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 5268 0 0 0 18979 19 0 0 25 0 1 0 421461184 23146496 5246 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5651 5246 603 41 0 5610 0
vsize: 22604
[startup+200.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29036
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 5268 0 0 0 19980 19 0 0 25 0 1 0 421461184 23146496 5246 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5651 5246 603 41 0 5610 0
vsize: 22604
[startup+210.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29036
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 5667 0 0 0 20979 20 0 0 25 0 1 0 421461184 24870912 5645 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6072 5645 603 41 0 6031 0
vsize: 24288
[startup+220.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29036
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 5737 0 0 0 21979 20 0 0 25 0 1 0 421461184 25137152 5715 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6137 5715 603 41 0 6096 0
vsize: 24548
[startup+230.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29036
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 5737 0 0 0 22979 20 0 0 25 0 1 0 421461184 25137152 5715 4294967295 134512640 134672761 3221224560 3221223664 134560376 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6137 5715 603 41 0 6096 0
vsize: 24548
[startup+240.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29036
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 5738 0 0 0 23979 20 0 0 25 0 1 0 421461184 25137152 5716 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6137 5716 603 41 0 6096 0
vsize: 24548
[startup+250.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29036
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 5738 0 0 0 24979 20 0 0 25 0 1 0 421461184 25137152 5716 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6137 5716 603 41 0 6096 0
vsize: 24548
[startup+260.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29036
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 5738 0 0 0 25979 20 0 0 25 0 1 0 421461184 25137152 5716 4294967295 134512640 134672761 3221224560 3221223696 134560642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6137 5716 603 41 0 6096 0
vsize: 24548
[startup+270.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29036
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 5738 0 0 0 26978 21 0 0 25 0 1 0 421461184 25137152 5716 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6137 5716 603 41 0 6096 0
vsize: 24548
[startup+280.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29036
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 5738 0 0 0 27978 21 0 0 25 0 1 0 421461184 25137152 5716 4294967295 134512640 134672761 3221224560 3221223728 134560906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6137 5716 603 41 0 6096 0
vsize: 24548
[startup+290.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29036
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 5738 0 0 0 28978 21 0 0 25 0 1 0 421461184 25137152 5716 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6137 5716 603 41 0 6096 0
vsize: 24548
[startup+300.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29036
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 5738 0 0 0 29978 21 0 0 25 0 1 0 421461184 25112576 5716 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6131 5716 603 41 0 6090 0
vsize: 24524
[startup+310.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29036
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 5738 0 0 0 30978 21 0 0 25 0 1 0 421461184 25112576 5716 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6131 5716 603 41 0 6090 0
vsize: 24524
[startup+320.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29036
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 5738 0 0 0 31979 21 0 0 25 0 1 0 421461184 25112576 5716 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6131 5716 603 41 0 6090 0
vsize: 24524
[startup+330.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29036
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 5738 0 0 0 32979 21 0 0 25 0 1 0 421461184 25112576 5716 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6131 5716 603 41 0 6090 0
vsize: 24524
[startup+340.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29036
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 5738 0 0 0 33979 21 0 0 25 0 1 0 421461184 25088000 5716 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6125 5716 603 41 0 6084 0
vsize: 24500
[startup+350.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29036
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 5738 0 0 0 34979 21 0 0 25 0 1 0 421461184 25088000 5716 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6125 5716 603 41 0 6084 0
vsize: 24500
[startup+360.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29036
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 5738 0 0 0 35979 21 0 0 25 0 1 0 421461184 25088000 5716 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6125 5716 603 41 0 6084 0
vsize: 24500
[startup+370.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29036
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 5738 0 0 0 36979 21 0 0 25 0 1 0 421461184 25088000 5716 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6125 5716 603 41 0 6084 0
vsize: 24500
[startup+380.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29036
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 5738 0 0 0 37980 21 0 0 25 0 1 0 421461184 25088000 5716 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6125 5716 603 41 0 6084 0
vsize: 24500
[startup+390.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29036
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 5865 0 0 0 38979 21 0 0 25 0 1 0 421461184 25616384 5843 4294967295 134512640 134672761 3221224560 3221223728 134561264 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6254 5843 603 41 0 6213 0
vsize: 25016
[startup+400.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29036
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 5865 0 0 0 39979 22 0 0 25 0 1 0 421461184 25616384 5843 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6254 5843 603 41 0 6213 0
vsize: 25016
[startup+410.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29036
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 5865 0 0 0 40980 22 0 0 25 0 1 0 421461184 25616384 5843 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6254 5843 603 41 0 6213 0
vsize: 25016
[startup+420.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29036
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 5865 0 0 0 41980 22 0 0 25 0 1 0 421461184 25616384 5843 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6254 5843 603 41 0 6213 0
vsize: 25016
[startup+430.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29036
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 5872 0 0 0 42980 22 0 0 25 0 1 0 421461184 25616384 5850 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6254 5850 603 41 0 6213 0
vsize: 25016
[startup+440.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29036
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 6363 0 0 0 43978 23 0 0 25 0 1 0 421461184 27607040 6341 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6740 6341 603 41 0 6699 0
vsize: 26960
[startup+450.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29036
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 6364 0 0 0 44978 23 0 0 25 0 1 0 421461184 27607040 6342 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6740 6342 603 41 0 6699 0
vsize: 26960
[startup+460.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29036
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 6364 0 0 0 45979 23 0 0 25 0 1 0 421461184 27607040 6342 4294967295 134512640 134672761 3221224560 3221223744 134559385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6740 6342 603 41 0 6699 0
vsize: 26960
[startup+470.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29036
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 6364 0 0 0 46979 23 0 0 25 0 1 0 421461184 27607040 6342 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6740 6342 603 41 0 6699 0
vsize: 26960
[startup+480.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29036
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 6364 0 0 0 47979 23 0 0 25 0 1 0 421461184 27607040 6342 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6740 6342 603 41 0 6699 0
vsize: 26960
[startup+490.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29036
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 6731 0 0 0 48977 25 0 0 25 0 1 0 421461184 29208576 6709 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7131 6709 603 41 0 7090 0
vsize: 28524
[startup+500.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29036
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 7144 0 0 0 49976 26 0 0 25 0 1 0 421461184 30830592 7122 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7527 7122 603 41 0 7486 0
vsize: 30108
[startup+510.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29036
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 7531 0 0 0 50976 27 0 0 25 0 1 0 421461184 32452608 7509 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7923 7509 603 41 0 7882 0
vsize: 31692
[startup+520.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29036
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 7873 0 0 0 51974 29 0 0 25 0 1 0 421461184 33910784 7851 4294967295 134512640 134672761 3221224560 3221223728 134560968 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8279 7851 603 41 0 8238 0
vsize: 33116
[startup+530.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29036
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8322 0 0 0 52973 30 0 0 25 0 1 0 421461184 35651584 8300 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8704 8300 603 41 0 8663 0
vsize: 34816
[startup+540.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29036
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 53973 30 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8769 8358 603 41 0 8728 0
vsize: 35076
[startup+550.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29036
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 54974 30 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8769 8358 603 41 0 8728 0
vsize: 35076
[startup+560.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29036
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 55974 30 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8769 8358 603 41 0 8728 0
vsize: 35076
[startup+570.023 s]
Raw data (loadavg): 1.07 0.99 0.91 4/59 29088
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 56974 30 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8769 8358 603 41 0 8728 0
vsize: 35076
[startup+580.022 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 29089
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 57974 30 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223728 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8769 8358 603 41 0 8728 0
vsize: 35076
[startup+590.022 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 29089
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 58974 30 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8769 8358 603 41 0 8728 0
vsize: 35076
[startup+600.021 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 29089
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 59974 30 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8769 8358 603 41 0 8728 0
vsize: 35076
[startup+610.022 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 29089
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 60975 30 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223744 134558899 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8769 8358 603 41 0 8728 0
vsize: 35076
[startup+620.021 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 29089
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 61974 30 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223664 134560224 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8769 8358 603 41 0 8728 0
vsize: 35076
[startup+630.021 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 29089
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 62974 30 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223744 134559572 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8769 8358 603 41 0 8728 0
vsize: 35076
[startup+640.022 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 29089
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 63975 30 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8769 8358 603 41 0 8728 0
vsize: 35076
[startup+650.022 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 29091
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 64975 30 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223744 134559031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8769 8358 603 41 0 8728 0
vsize: 35076
[startup+660.022 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 29091
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 65975 31 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223696 134560625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8769 8358 603 41 0 8728 0
vsize: 35076
[startup+670.023 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 29091
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 66975 31 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8769 8358 603 41 0 8728 0
vsize: 35076
[startup+680.022 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 29091
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 67975 31 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8769 8358 603 41 0 8728 0
vsize: 35076
[startup+690.022 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 29091
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 68975 31 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223664 134554662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8769 8358 603 41 0 8728 0
vsize: 35076
[startup+700.022 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 29091
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 69975 31 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8769 8358 603 41 0 8728 0
vsize: 35076
[startup+710.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29091
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 70976 31 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8769 8358 603 41 0 8728 0
vsize: 35076
[startup+720.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29091
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 71976 31 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8769 8358 603 41 0 8728 0
vsize: 35076
[startup+730.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29091
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 72976 31 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223728 134561003 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8769 8358 603 41 0 8728 0
vsize: 35076
[startup+740.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29091
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 73976 31 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223696 134560673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8769 8358 603 41 0 8728 0
vsize: 35076
[startup+750.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29091
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 74976 31 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8769 8358 603 41 0 8728 0
vsize: 35076
[startup+760.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29091
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 75976 31 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223728 134561156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8769 8358 603 41 0 8728 0
vsize: 35076
[startup+770.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29091
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 76976 31 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8769 8358 603 41 0 8728 0
vsize: 35076
[startup+780.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29091
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 77977 31 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223664 134560191 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8769 8358 603 41 0 8728 0
vsize: 35076
[startup+790.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29091
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 78977 31 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8769 8358 603 41 0 8728 0
vsize: 35076
[startup+800.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29091
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 79977 31 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8769 8358 603 41 0 8728 0
vsize: 35076
[startup+810.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29091
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 80977 31 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223744 134559601 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8769 8358 603 41 0 8728 0
vsize: 35076
[startup+820.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29091
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 81977 31 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8769 8358 603 41 0 8728 0
vsize: 35076
[startup+830.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29091
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 82977 31 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8769 8358 603 41 0 8728 0
vsize: 35076
[startup+840.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29091
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 83978 31 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223728 134561025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8769 8358 603 41 0 8728 0
vsize: 35076
[startup+850.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29091
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 84978 31 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223664 134560285 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8769 8358 603 41 0 8728 0
vsize: 35076
[startup+860.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29091
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 85978 31 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8769 8358 603 41 0 8728 0
vsize: 35076
[startup+870.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29091
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 86978 31 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8769 8358 603 41 0 8728 0
vsize: 35076
[startup+880.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29091
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 87978 31 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8769 8358 603 41 0 8728 0
vsize: 35076
[startup+890.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29091
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 88978 31 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223728 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8769 8358 603 41 0 8728 0
vsize: 35076
[startup+900.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29091
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 89979 31 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8769 8358 603 41 0 8728 0
vsize: 35076
[startup+910.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29093
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 90979 31 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223744 134558851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8769 8358 603 41 0 8728 0
vsize: 35076
[startup+920.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29093
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 91979 31 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223728 134561021 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8769 8358 603 41 0 8728 0
vsize: 35076
[startup+930.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29093
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 92979 31 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8769 8358 603 41 0 8728 0
vsize: 35076
[startup+940.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29093
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 93979 31 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223728 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8769 8358 603 41 0 8728 0
vsize: 35076
[startup+950.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29093
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 94980 31 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8769 8358 603 41 0 8728 0
vsize: 35076
[startup+960.025 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29093
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 95979 31 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8769 8358 603 41 0 8728 0
vsize: 35076
[startup+970.025 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29093
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 96979 31 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8769 8358 603 41 0 8728 0
vsize: 35076
[startup+980.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29093
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 97979 31 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8769 8358 603 41 0 8728 0
vsize: 35076
[startup+990.025 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29093
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 98979 31 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8769 8358 603 41 0 8728 0
vsize: 35076
[startup+1000.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29093
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8380 0 0 0 99980 31 0 0 25 0 1 0 421461184 35917824 8358 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8769 8358 603 41 0 8728 0
vsize: 35076
[startup+1010.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29093
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8384 0 0 0 100980 31 0 0 25 0 1 0 421461184 35917824 8362 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8769 8362 603 41 0 8728 0
vsize: 35076
[startup+1020.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29093
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8385 0 0 0 101980 31 0 0 25 0 1 0 421461184 35917824 8363 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8769 8363 603 41 0 8728 0
vsize: 35076
[startup+1030.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29093
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8385 0 0 0 102980 31 0 0 25 0 1 0 421461184 35917824 8363 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8769 8363 603 41 0 8728 0
vsize: 35076
[startup+1040.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29093
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8385 0 0 0 103980 31 0 0 25 0 1 0 421461184 35917824 8363 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8769 8363 603 41 0 8728 0
vsize: 35076
[startup+1050.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29093
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8385 0 0 0 104981 31 0 0 25 0 1 0 421461184 35917824 8363 4294967295 134512640 134672761 3221224560 3221223728 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8769 8363 603 41 0 8728 0
vsize: 35076
[startup+1060.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29093
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8385 0 0 0 105981 31 0 0 25 0 1 0 421461184 35917824 8363 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8769 8363 603 41 0 8728 0
vsize: 35076
[startup+1070.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29093
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8385 0 0 0 106981 31 0 0 25 0 1 0 421461184 35917824 8363 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8769 8363 603 41 0 8728 0
vsize: 35076
[startup+1080.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29093
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8385 0 0 0 107981 31 0 0 25 0 1 0 421461184 35917824 8363 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8769 8363 603 41 0 8728 0
vsize: 35076
[startup+1090.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29093
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8385 0 0 0 108981 31 0 0 25 0 1 0 421461184 35917824 8363 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8769 8363 603 41 0 8728 0
vsize: 35076
[startup+1100.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29093
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8385 0 0 0 109982 31 0 0 25 0 1 0 421461184 35917824 8363 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8769 8363 603 41 0 8728 0
vsize: 35076
[startup+1110.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29093
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8385 0 0 0 110982 31 0 0 25 0 1 0 421461184 35917824 8363 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8769 8363 603 41 0 8728 0
vsize: 35076
[startup+1120.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29093
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8385 0 0 0 111982 31 0 0 25 0 1 0 421461184 35917824 8363 4294967295 134512640 134672761 3221224560 3221223728 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8769 8363 603 41 0 8728 0
vsize: 35076
[startup+1130.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29093
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8385 0 0 0 112982 31 0 0 25 0 1 0 421461184 35917824 8363 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8769 8363 603 41 0 8728 0
vsize: 35076
[startup+1140.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29093
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8385 0 0 0 113982 31 0 0 25 0 1 0 421461184 35917824 8363 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8769 8363 603 41 0 8728 0
vsize: 35076
[startup+1150.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29093
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8385 0 0 0 114982 31 0 0 25 0 1 0 421461184 35917824 8363 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8769 8363 603 41 0 8728 0
vsize: 35076
[startup+1160.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29093
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8386 0 0 0 115982 31 0 0 25 0 1 0 421461184 35917824 8364 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8769 8364 603 41 0 8728 0
vsize: 35076
[startup+1170.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29093
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8390 0 0 0 116983 31 0 0 25 0 1 0 421461184 35917824 8368 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8769 8368 603 41 0 8728 0
vsize: 35076
[startup+1180.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29093
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8391 0 0 0 117983 31 0 0 25 0 1 0 421461184 35917824 8369 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8769 8369 603 41 0 8728 0
vsize: 35076
[startup+1190.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29093
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8391 0 0 0 118983 31 0 0 25 0 1 0 421461184 35917824 8369 4294967295 134512640 134672761 3221224560 3221223664 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8769 8369 603 41 0 8728 0
vsize: 35076
[startup+1200.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29093
Raw data (stat): 29036 (minisat+) R 29035 25285 25284 0 -1 0 8391 0 0 0 119983 31 0 0 25 0 1 0 421461184 35917824 8369 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8769 8369 603 41 0 8728 0
vsize: 35076
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 29093
Raw data (stat): 29036 (minisat+) Z 29035 25285 25284 0 -1 12 8394 0 0 0 119983 33 0 0 25 0 1 0 421461184 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.05
CPU time (s): 1200.17
CPU user time (s): 1199.84
CPU system time (s): 0.332949
CPU usage (%): 100.01
Max. virtual memory (Kb): 35076
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####