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/miplib2003/normalized-mps-v2-13-7-markshare2.opb
MD5SUM	3b5121187baf09367bd50bdc4d869d21
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	8448
Optimality of the best value was proved	NO
Number of terms in the objective function	140
Biggest coefficient in the objective function	524288
Number of bits for the biggest coefficient in the objective function	20
Sum of the numbers in the objective function	7340025
Number of bits of the sum of numbers in the objective function	23
Biggest number in a constraint	524288
Number of bits of the biggest number in a constraint	20
Biggest sum of numbers in a constraint	7340025
Number of bits of the biggest sum of numbers	23
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.43
Number of variables	200
Total number of constraints	67
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	60
Number of constraints which are nor clauses,nor cardinality constraints	7
Minimum length of a constraint	1
Maximum length of a constraint	80
Trace number 18695

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc24 THE 2005-04-21 16:01:52 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=17654 boxname=wulflinc24 idbench=1358 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  3b5121187baf09367bd50bdc4d869d21  /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-13-7-markshare2.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-13-7-markshare2.opb /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-13-7-markshare2.opb
IDLAUNCH: 17654
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.080
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.080
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:        789472 kB
Buffers:         27896 kB
Cached:         193192 kB
SwapCached:        524 kB
Active:          77724 kB
Inactive:       145340 kB
HighTotal:      131008 kB
HighFree:         1540 kB
LowTotal:       903652 kB
LowFree:        787932 kB
SwapTotal:     2097892 kB
SwapFree:      2096476 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5108 kB
Slab:            16532 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 16:21:55 (client local time) WITH STATUS 10 IN 1200.2 SECONDS
stats: 17654 7 1200.2 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 14 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #######
c   -- Clauses(.)/Splits(s): (none)
c ---[  12]---> Adder-cost: 354   maxlim: 431615   bits: 20/19
c ---[  10]---> Adder-cost: 380   maxlim: 461183   bits: 20/19
c ---[   8]---> Adder-cost: 350   maxlim: 445183   bits: 20/19
c ---[   6]---> Adder-cost: 340   maxlim: 477951   bits: 20/19
c ---[   4]---> Adder-cost: 390   maxlim: 451839   bits: 20/19
c ---[   2]---> Adder-cost: 358   maxlim: 468735   bits: 20/19
c ---[   0]---> Adder-cost: 374   maxlim: 444543   bits: 20/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   17222    61228 |    5740       0        0     nan |  0.000 % |
c |       100 |   17222    61228 |    6314     100      436     4.4 |  9.969 % |
c |       251 |   17222    61228 |    6945     251     1589     6.3 |  9.969 % |
c |       476 |   17222    61228 |    7639     476     4122     8.7 |  9.969 % |
c ==============================================================================
c [1mFound solution: 651648[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 1069     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       699 |   20136    68102 |    6712     699    10913    15.6 |  9.969 % |
c |       799 |   20128    68076 |    7383     798    21519    27.0 |  7.575 % |
c |       949 |   20128    68076 |    8121     948    30181    31.8 |  7.575 % |
c ==============================================================================
c [1mFound solution: 612096[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1058 |   20209    68289 |    6736    1057    40766    38.6 |  7.575 % |
c |      1158 |   20209    68289 |    7409    1157    46287    40.0 |  7.570 % |
c |      1309 |   20209    68289 |    8150    1308    52924    40.5 |  7.570 % |
c |      1534 |   20209    68289 |    8965    1533    81998    53.5 |  7.570 % |
c |      1871 |   20209    68289 |    9862    1870   121887    65.2 |  7.570 % |
c |      2378 |   20185    68211 |   10848    2374   162760    68.6 |  7.648 % |
c ==============================================================================
c [1mFound solution: 574080[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   11     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2793 |   20200    68242 |    6733    2788   210465    75.5 |  7.648 % |
c ==============================================================================
c [1mFound solution: 239872[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2845 |   20232    68318 |    6744    2840   211547    74.5 |  7.648 % |
c |      2946 |   20224    68292 |    7418    2940   214114    72.8 |  7.716 % |
c |      3097 |   20224    68292 |    8160    3091   215459    69.7 |  7.716 % |
c |      3322 |   20224    68292 |    8976    3316   226783    68.4 |  7.716 % |
c |      3659 |   20200    68214 |    9873    3650   253941    69.6 |  7.794 % |
c |      4166 |   20200    68214 |   10861    4157   276163    66.4 |  7.794 % |
c |      4925 |   20184    68162 |   11947    4914   293765    59.8 |  7.846 % |
c |      6066 |   20184    68162 |   13142    6055   389521    64.3 |  7.846 % |
c |      7774 |   20184    68162 |   14456    7763   530254    68.3 |  7.846 % |
c ==============================================================================
c [1mFound solution: 233472[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8457 |   20206    68216 |    6735    8446   554750    65.7 |  7.846 % |
c |      8557 |   20206    68216 |    7408    4323   242172    56.0 |  7.858 % |
c |      8707 |   20206    68216 |    8149    4473   243252    54.4 |  7.858 % |
c |      8932 |   20206    68216 |    8964    4698   245846    52.3 |  7.858 % |
c |      9270 |   20206    68216 |    9860    5036   254179    50.5 |  7.858 % |
c |      9779 |   20200    68198 |   10846    5544   268398    48.4 |  7.884 % |
c |     10539 |   20200    68198 |   11931    6304   294399    46.7 |  7.884 % |
c |     11680 |   20200    68198 |   13124    7445   351264    47.2 |  7.884 % |
c |     13388 |   20200    68198 |   14437    9153   446317    48.8 |  7.884 % |
c |     15950 |   20200    68198 |   15880   11715   577221    49.3 |  7.884 % |
c |     19794 |   20183    68145 |   17468   15557   857831    55.1 |  7.962 % |
c |     25561 |   20049    67812 |   19215   12157   724474    59.6 |  8.895 % |
c |     34210 |   20017    67733 |   21137   10751   499120    46.4 |  9.077 % |
c |     47184 |   20003    67697 |   23251   12920   530179    41.0 |  9.155 % |
c |     66646 |   20003    67697 |   25576   20218   949013    46.9 |  9.155 % |
c |     95838 |   19995    67671 |   28133   22421  1069802    47.7 |  9.181 % |
c |    139628 |   19995    67671 |   30947   21035  1279848    60.8 |  9.181 % |
c |    205312 |   19934    67518 |   34041   15912   771109    48.5 |  9.621 % |
c |    303841 |   19934    67518 |   37446   33182  1877834    56.6 |  9.621 % |
c |    451632 |   19924    67495 |   41190   22072  1191172    54.0 |  9.673 % |
c ==============================================================================
c [1mFound solution: 131456[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    500118 |   19908    67463 |    6636   15146   633146    41.8 |  9.673 % |
c |    500219 |   19908    67463 |    7299    3888   123690    31.8 |  9.876 % |
c |    500369 |   19908    67463 |    8029    4038   126129    31.2 |  9.876 % |
c |    500594 |   19908    67463 |    8832    4263   130256    30.6 |  9.876 % |
c |    500931 |   19908    67463 |    9715    4600   136695    29.7 |  9.876 % |
c |    501437 |   19908    67463 |   10687    5106   149285    29.2 |  9.876 % |
c |    502197 |   19908    67463 |   11756    5866   170398    29.0 |  9.876 % |
c |    503336 |   19908    67463 |   12931    7005   219323    31.3 |  9.876 % |
c |    505044 |   19908    67463 |   14224    8713   304374    34.9 |  9.876 % |
c |    507606 |   19908    67463 |   15647   11275   412063    36.5 |  9.876 % |
c |    511451 |   19908    67463 |   17212   15120   602595    39.9 |  9.876 % |
c |    517218 |   19908    67463 |   18933   11593   389204    33.6 |  9.876 % |
c |    525867 |   19908    67463 |   20826   10250   426781    41.6 |  9.876 % |
c |    538842 |   19895    67433 |   22909   12420   530893    42.7 |  9.979 % |
c |    558303 |   19895    67433 |   25200   19850   991637    50.0 |  9.979 % |
c |    587498 |   19895    67433 |   27720   22344   834383    37.3 |  9.979 % |
c ==============================================================================
c [1mFound solution: 119552[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    595514 |   19843    67252 |    6614   12662   510577    40.3 |  9.979 % |
c |    595614 |   19843    67252 |    7275    6431   251107    39.0 | 10.375 % |
c |    595765 |   19843    67252 |    8002    6582   254009    38.6 | 10.375 % |
c |    595990 |   19843    67252 |    8803    6807   259710    38.2 | 10.375 % |
c |    596328 |   19843    67252 |    9683    7145   268031    37.5 | 10.375 % |
c |    596835 |   19843    67252 |   10651    7652   288100    37.7 | 10.375 % |
c |    597594 |   19843    67252 |   11717    8411   306034    36.4 | 10.375 % |
c |    598736 |   19843    67252 |   12888    9553   344822    36.1 | 10.375 % |
c |    600446 |   19682    66882 |   14177   11248   423649    37.7 | 11.617 % |
c |    603008 |   19682    66882 |   15595   13810   528082    38.2 | 11.617 % |
c |    606852 |   19682    66882 |   17155    9379   323702    34.5 | 11.617 % |
c |    612618 |   19682    66882 |   18870   15145   566404    37.4 | 11.617 % |
c |    621269 |   19672    66859 |   20757   13664   620799    45.4 | 11.669 % |
c |    634243 |   19609    66707 |   22833   15806   725391    45.9 | 12.290 % |
c |    653705 |   19609    66707 |   25116   23281  1040677    44.7 | 12.290 % |
c |    682897 |   19609    66707 |   27628   26068  1393797    53.5 | 12.290 % |
c |    726686 |   19609    66707 |   30391   23711  1513201    63.8 | 12.290 % |
#### 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.54 0.85 0.89 2/54 12668
Raw data (stat): 12668 (runsolver) R 12667 28546 28545 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 546358490 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0006 s]
Raw data (loadavg): 0.61 0.85 0.89 2/54 12668
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 1324 0 0 0 996 3 0 0 25 0 1 0 546358490 7069696 1302 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1726 1302 603 41 0 1685 0
vsize: 6904
[startup+20.0017 s]
Raw data (loadavg): 0.67 0.86 0.90 2/54 12668
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 1592 0 0 0 1993 5 0 0 25 0 1 0 546358490 8056832 1570 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1967 1570 603 41 0 1926 0
vsize: 7868
[startup+30.0021 s]
Raw data (loadavg): 0.72 0.86 0.90 2/54 12668
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 1987 0 0 0 2991 6 0 0 25 0 1 0 546358490 9719808 1965 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2373 1965 603 41 0 2332 0
vsize: 9492
[startup+40.0031 s]
Raw data (loadavg): 0.76 0.87 0.90 2/54 12668
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 2012 0 0 0 3991 7 0 0 25 0 1 0 546358490 9854976 1990 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2406 1990 603 41 0 2365 0
vsize: 9624
[startup+50.0038 s]
Raw data (loadavg): 0.80 0.87 0.90 2/54 12668
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 2195 0 0 0 4990 7 0 0 25 0 1 0 546358490 10649600 2173 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2600 2173 603 41 0 2559 0
vsize: 10400
[startup+60.0032 s]
Raw data (loadavg): 0.83 0.87 0.90 2/54 12668
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 2196 0 0 0 5990 7 0 0 25 0 1 0 546358490 10649600 2174 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2600 2174 603 41 0 2559 0
vsize: 10400
[startup+70.0045 s]
Raw data (loadavg): 0.85 0.88 0.90 2/54 12668
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 2196 0 0 0 6990 8 0 0 25 0 1 0 546358490 10649600 2174 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2600 2174 603 41 0 2559 0
vsize: 10400
[startup+80.0049 s]
Raw data (loadavg): 0.88 0.88 0.90 2/54 12668
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 2337 0 0 0 7990 8 0 0 25 0 1 0 546358490 11190272 2315 4294967295 134512640 134672761 3221224544 3221223680 134560619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2732 2315 603 41 0 2691 0
vsize: 10928
[startup+90.0054 s]
Raw data (loadavg): 0.89 0.89 0.90 2/54 12668
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 2391 0 0 0 8990 8 0 0 25 0 1 0 546358490 11460608 2369 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2798 2369 603 41 0 2757 0
vsize: 11192
[startup+100.005 s]
Raw data (loadavg): 0.91 0.89 0.90 2/54 12668
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 2444 0 0 0 9990 8 0 0 25 0 1 0 546358490 11595776 2422 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2831 2422 603 41 0 2790 0
vsize: 11324
[startup+110.005 s]
Raw data (loadavg): 0.92 0.89 0.90 2/54 12668
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 2444 0 0 0 10990 8 0 0 25 0 1 0 546358490 11595776 2422 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2831 2422 603 41 0 2790 0
vsize: 11324
[startup+120.005 s]
Raw data (loadavg): 0.93 0.89 0.91 2/54 12668
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 2463 0 0 0 11990 8 0 0 25 0 1 0 546358490 11730944 2441 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2864 2441 603 41 0 2823 0
vsize: 11456
[startup+130.006 s]
Raw data (loadavg): 0.94 0.90 0.91 2/54 12668
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 2799 0 0 0 12990 9 0 0 25 0 1 0 546358490 13070336 2777 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3191 2777 603 41 0 3150 0
vsize: 12764
[startup+140.006 s]
Raw data (loadavg): 0.95 0.90 0.91 2/54 12668
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 2803 0 0 0 13989 9 0 0 25 0 1 0 546358490 13070336 2781 4294967295 134512640 134672761 3221224544 3221223712 134561025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3191 2781 603 41 0 3150 0
vsize: 12764
[startup+150.006 s]
Raw data (loadavg): 0.96 0.90 0.91 2/54 12668
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 2835 0 0 0 14989 9 0 0 25 0 1 0 546358490 13205504 2813 4294967295 134512640 134672761 3221224544 3221223696 134561244 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3224 2813 603 41 0 3183 0
vsize: 12896
[startup+160.006 s]
Raw data (loadavg): 0.97 0.91 0.91 2/54 12668
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 3091 0 0 0 15988 10 0 0 25 0 1 0 546358490 14266368 3069 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3483 3069 603 41 0 3442 0
vsize: 13932
[startup+170.007 s]
Raw data (loadavg): 0.97 0.91 0.91 2/54 12668
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 3100 0 0 0 16989 10 0 0 25 0 1 0 546358490 14266368 3078 4294967295 134512640 134672761 3221224544 3221223680 134560726 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3483 3078 603 41 0 3442 0
vsize: 13932
[startup+180.008 s]
Raw data (loadavg): 0.97 0.91 0.91 2/54 12668
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 3115 0 0 0 17989 10 0 0 25 0 1 0 546358490 14417920 3093 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3520 3093 603 41 0 3479 0
vsize: 14080
[startup+190.008 s]
Raw data (loadavg): 0.98 0.91 0.91 2/54 12668
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 3337 0 0 0 18988 11 0 0 25 0 1 0 546358490 15245312 3315 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3722 3315 603 41 0 3681 0
vsize: 14888
[startup+200.008 s]
Raw data (loadavg): 0.98 0.92 0.91 2/54 12668
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 3371 0 0 0 19988 11 0 0 25 0 1 0 546358490 15519744 3349 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3789 3349 603 41 0 3748 0
vsize: 15156
[startup+210.008 s]
Raw data (loadavg): 0.98 0.92 0.91 2/54 12668
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 3379 0 0 0 20989 11 0 0 25 0 1 0 546358490 15519744 3357 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3789 3357 603 41 0 3748 0
vsize: 15156
[startup+220.009 s]
Raw data (loadavg): 0.98 0.92 0.91 2/54 12668
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 3382 0 0 0 21989 11 0 0 25 0 1 0 546358490 15519744 3360 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3789 3360 603 41 0 3748 0
vsize: 15156
[startup+230.008 s]
Raw data (loadavg): 0.99 0.92 0.91 2/54 12668
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 3382 0 0 0 22989 11 0 0 25 0 1 0 546358490 15519744 3360 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3789 3360 603 41 0 3748 0
vsize: 15156
[startup+240.009 s]
Raw data (loadavg): 0.99 0.92 0.91 2/54 12668
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 3382 0 0 0 23989 11 0 0 25 0 1 0 546358490 15519744 3360 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3789 3360 603 41 0 3748 0
vsize: 15156
[startup+250.01 s]
Raw data (loadavg): 0.99 0.93 0.91 2/54 12668
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 3382 0 0 0 24989 11 0 0 25 0 1 0 546358490 15519744 3360 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3789 3360 603 41 0 3748 0
vsize: 15156
[startup+260.009 s]
Raw data (loadavg): 0.99 0.93 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 3387 0 0 0 25990 11 0 0 25 0 1 0 546358490 15519744 3365 4294967295 134512640 134672761 3221224544 3221223712 134561220 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3789 3365 603 41 0 3748 0
vsize: 15156
[startup+270.01 s]
Raw data (loadavg): 0.99 0.93 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 3396 0 0 0 26990 11 0 0 25 0 1 0 546358490 15519744 3374 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3789 3374 603 41 0 3748 0
vsize: 15156
[startup+280.01 s]
Raw data (loadavg): 0.99 0.93 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 3406 0 0 0 27990 11 0 0 25 0 1 0 546358490 15663104 3384 4294967295 134512640 134672761 3221224544 3221223704 134561238 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3824 3384 603 41 0 3783 0
vsize: 15296
[startup+290.01 s]
Raw data (loadavg): 0.99 0.93 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 3406 0 0 0 28990 11 0 0 25 0 1 0 546358490 15663104 3384 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3824 3384 603 41 0 3783 0
vsize: 15296
[startup+300.01 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 3413 0 0 0 29990 11 0 0 25 0 1 0 546358490 15663104 3391 4294967295 134512640 134672761 3221224544 3221223716 134565154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3824 3391 603 41 0 3783 0
vsize: 15296
[startup+310.01 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 3413 0 0 0 30990 11 0 0 25 0 1 0 546358490 15663104 3391 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3824 3391 603 41 0 3783 0
vsize: 15296
[startup+320.011 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 3413 0 0 0 31991 11 0 0 25 0 1 0 546358490 15663104 3391 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3824 3391 603 41 0 3783 0
vsize: 15296
[startup+330.01 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 3413 0 0 0 32991 11 0 0 25 0 1 0 546358490 15663104 3391 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3824 3391 603 41 0 3783 0
vsize: 15296
[startup+340.01 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 3558 0 0 0 33990 12 0 0 25 0 1 0 546358490 16334848 3536 4294967295 134512640 134672761 3221224544 3221223680 134560661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3988 3536 603 41 0 3947 0
vsize: 15952
[startup+350.011 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 3650 0 0 0 34990 12 0 0 25 0 1 0 546358490 16728064 3628 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4084 3628 603 41 0 4043 0
vsize: 16336
[startup+360.01 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 3665 0 0 0 35990 12 0 0 25 0 1 0 546358490 16875520 3643 4294967295 134512640 134672761 3221224544 3221223640 1075347141 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4120 3643 603 41 0 4079 0
vsize: 16480
[startup+370.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 3666 0 0 0 36991 12 0 0 25 0 1 0 546358490 16875520 3644 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4120 3644 603 41 0 4079 0
vsize: 16480
[startup+380.011 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 3690 0 0 0 37991 12 0 0 25 0 1 0 546358490 17010688 3668 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4153 3668 603 41 0 4112 0
vsize: 16612
[startup+390.011 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 3809 0 0 0 38991 13 0 0 25 0 1 0 546358490 17408000 3787 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4250 3787 603 41 0 4209 0
vsize: 17000
[startup+400.011 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 3809 0 0 0 39991 13 0 0 25 0 1 0 546358490 17408000 3787 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4250 3787 603 41 0 4209 0
vsize: 17000
[startup+410.011 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 3809 0 0 0 40991 13 0 0 25 0 1 0 546358490 17408000 3787 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4250 3787 603 41 0 4209 0
vsize: 17000
[startup+420.011 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 3809 0 0 0 41991 13 0 0 25 0 1 0 546358490 17408000 3787 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4250 3787 603 41 0 4209 0
vsize: 17000
[startup+430.012 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 3809 0 0 0 42991 13 0 0 25 0 1 0 546358490 17408000 3787 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4250 3787 603 41 0 4209 0
vsize: 17000
[startup+440.012 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 3809 0 0 0 43992 13 0 0 25 0 1 0 546358490 17408000 3787 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4250 3787 603 41 0 4209 0
vsize: 17000
[startup+450.011 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 3809 0 0 0 44992 13 0 0 25 0 1 0 546358490 17408000 3787 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4250 3787 603 41 0 4209 0
vsize: 17000
[startup+460.011 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 3824 0 0 0 45992 13 0 0 25 0 1 0 546358490 17547264 3802 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4284 3802 603 41 0 4243 0
vsize: 17136
[startup+470.012 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 3861 0 0 0 46992 13 0 0 25 0 1 0 546358490 17682432 3839 4294967295 134512640 134672761 3221224544 3221223680 134565080 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4317 3839 603 41 0 4276 0
vsize: 17268
[startup+480.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 3873 0 0 0 47992 13 0 0 25 0 1 0 546358490 17682432 3851 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4317 3851 603 41 0 4276 0
vsize: 17268
[startup+490.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 3892 0 0 0 48992 13 0 0 25 0 1 0 546358490 17817600 3870 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4350 3870 603 41 0 4309 0
vsize: 17400
[startup+500.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 3903 0 0 0 49992 13 0 0 25 0 1 0 546358490 17817600 3881 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4350 3881 603 41 0 4309 0
vsize: 17400
[startup+510.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 4086 0 0 0 50991 14 0 0 25 0 1 0 546358490 18632704 4064 4294967295 134512640 134672761 3221224544 3221223680 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4549 4064 603 41 0 4508 0
vsize: 18196
[startup+520.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 4086 0 0 0 51991 14 0 0 25 0 1 0 546358490 18632704 4064 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4549 4064 603 41 0 4508 0
vsize: 18196
[startup+530.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 4086 0 0 0 52991 14 0 0 25 0 1 0 546358490 18632704 4064 4294967295 134512640 134672761 3221224544 3221223680 134560569 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4549 4064 603 41 0 4508 0
vsize: 18196
[startup+540.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 4086 0 0 0 53992 14 0 0 25 0 1 0 546358490 18632704 4064 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4549 4064 603 41 0 4508 0
vsize: 18196
[startup+550.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 4086 0 0 0 54992 14 0 0 25 0 1 0 546358490 18632704 4064 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4549 4064 603 41 0 4508 0
vsize: 18196
[startup+560.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 4086 0 0 0 55992 14 0 0 25 0 1 0 546358490 18632704 4064 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4549 4064 603 41 0 4508 0
vsize: 18196
[startup+570.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 4086 0 0 0 56992 14 0 0 25 0 1 0 546358490 18632704 4064 4294967295 134512640 134672761 3221224544 3221223728 134559498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4549 4064 603 41 0 4508 0
vsize: 18196
[startup+580.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 4092 0 0 0 57992 14 0 0 25 0 1 0 546358490 18632704 4070 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4549 4070 603 41 0 4508 0
vsize: 18196
[startup+590.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 4092 0 0 0 58992 14 0 0 25 0 1 0 546358490 18632704 4070 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4549 4070 603 41 0 4508 0
vsize: 18196
[startup+600.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 4092 0 0 0 59992 14 0 0 25 0 1 0 546358490 18632704 4070 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4549 4070 603 41 0 4508 0
vsize: 18196
[startup+610.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 4092 0 0 0 60992 14 0 0 25 0 1 0 546358490 18632704 4070 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4549 4070 603 41 0 4508 0
vsize: 18196
[startup+620.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 4098 0 0 0 61993 14 0 0 25 0 1 0 546358490 18632704 4076 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4549 4076 603 41 0 4508 0
vsize: 18196
[startup+630.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 4098 0 0 0 62993 14 0 0 25 0 1 0 546358490 18632704 4076 4294967295 134512640 134672761 3221224544 3221223648 134560510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4549 4076 603 41 0 4508 0
vsize: 18196
[startup+640.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 4157 0 0 0 63993 14 0 0 25 0 1 0 546358490 18903040 4135 4294967295 134512640 134672761 3221224544 3221223744 134557822 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4615 4135 603 41 0 4574 0
vsize: 18460
[startup+650.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 4162 0 0 0 64993 15 0 0 25 0 1 0 546358490 18903040 4140 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4615 4140 603 41 0 4574 0
vsize: 18460
[startup+660.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 4178 0 0 0 65993 15 0 0 25 0 1 0 546358490 19054592 4156 4294967295 134512640 134672761 3221224544 3221223728 134559330 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4652 4156 603 41 0 4611 0
vsize: 18608
[startup+670.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 4179 0 0 0 66993 15 0 0 25 0 1 0 546358490 19054592 4157 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4652 4157 603 41 0 4611 0
vsize: 18608
[startup+680.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 4180 0 0 0 67994 15 0 0 25 0 1 0 546358490 19054592 4158 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4652 4158 603 41 0 4611 0
vsize: 18608
[startup+690.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 4327 0 0 0 68994 15 0 0 25 0 1 0 546358490 19587072 4305 4294967295 134512640 134672761 3221224544 3221223712 134561533 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4782 4305 603 41 0 4741 0
vsize: 19128
[startup+700.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 4327 0 0 0 69994 15 0 0 25 0 1 0 546358490 19587072 4305 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4782 4305 603 41 0 4741 0
vsize: 19128
[startup+710.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 4331 0 0 0 70994 15 0 0 25 0 1 0 546358490 19587072 4309 4294967295 134512640 134672761 3221224544 3221223696 134565086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4782 4309 603 41 0 4741 0
vsize: 19128
[startup+720.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 4335 0 0 0 71994 15 0 0 25 0 1 0 546358490 19722240 4313 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4815 4313 603 41 0 4774 0
vsize: 19260
[startup+730.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 4346 0 0 0 72994 15 0 0 25 0 1 0 546358490 19722240 4324 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4815 4324 603 41 0 4774 0
vsize: 19260
[startup+740.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 4352 0 0 0 73994 15 0 0 25 0 1 0 546358490 19722240 4330 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4815 4330 603 41 0 4774 0
vsize: 19260
[startup+750.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 4352 0 0 0 74994 15 0 0 25 0 1 0 546358490 19722240 4330 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4815 4330 603 41 0 4774 0
vsize: 19260
[startup+760.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 4352 0 0 0 75995 15 0 0 25 0 1 0 546358490 19722240 4330 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4815 4330 603 41 0 4774 0
vsize: 19260
[startup+770.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 4352 0 0 0 76995 15 0 0 25 0 1 0 546358490 19722240 4330 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4815 4330 603 41 0 4774 0
vsize: 19260
[startup+780.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 4352 0 0 0 77995 15 0 0 25 0 1 0 546358490 19722240 4330 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4815 4330 603 41 0 4774 0
vsize: 19260
[startup+790.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 4415 0 0 0 78995 16 0 0 25 0 1 0 546358490 19992576 4393 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4881 4393 603 41 0 4840 0
vsize: 19524
[startup+800.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 4415 0 0 0 79995 16 0 0 25 0 1 0 546358490 19992576 4393 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4881 4393 603 41 0 4840 0
vsize: 19524
[startup+810.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 4415 0 0 0 80995 16 0 0 25 0 1 0 546358490 19992576 4393 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4881 4393 603 41 0 4840 0
vsize: 19524
[startup+820.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 4415 0 0 0 81995 16 0 0 25 0 1 0 546358490 19992576 4393 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4881 4393 603 41 0 4840 0
vsize: 19524
[startup+830.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 4415 0 0 0 82995 16 0 0 25 0 1 0 546358490 19992576 4393 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4881 4393 603 41 0 4840 0
vsize: 19524
[startup+840.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 4541 0 0 0 83995 16 0 0 25 0 1 0 546358490 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5011 4519 603 41 0 4970 0
vsize: 20044
[startup+850.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 4541 0 0 0 84995 16 0 0 25 0 1 0 546358490 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5011 4519 603 41 0 4970 0
vsize: 20044
[startup+860.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 4541 0 0 0 85995 16 0 0 25 0 1 0 546358490 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5011 4519 603 41 0 4970 0
vsize: 20044
[startup+870.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 4541 0 0 0 86996 16 0 0 25 0 1 0 546358490 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5011 4519 603 41 0 4970 0
vsize: 20044
[startup+880.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 4541 0 0 0 87996 16 0 0 25 0 1 0 546358490 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5011 4519 603 41 0 4970 0
vsize: 20044
[startup+890.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 4541 0 0 0 88996 16 0 0 25 0 1 0 546358490 20525056 4519 4294967295 134512640 134672761 3221224544 3221223680 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5011 4519 603 41 0 4970 0
vsize: 20044
[startup+900.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 4541 0 0 0 89996 16 0 0 25 0 1 0 546358490 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5011 4519 603 41 0 4970 0
vsize: 20044
[startup+910.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 4541 0 0 0 90996 16 0 0 25 0 1 0 546358490 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5011 4519 603 41 0 4970 0
vsize: 20044
[startup+920.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 4541 0 0 0 91997 16 0 0 25 0 1 0 546358490 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5011 4519 603 41 0 4970 0
vsize: 20044
[startup+930.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 4541 0 0 0 92997 16 0 0 25 0 1 0 546358490 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5011 4519 603 41 0 4970 0
vsize: 20044
[startup+940.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 4541 0 0 0 93997 16 0 0 25 0 1 0 546358490 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134561156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5011 4519 603 41 0 4970 0
vsize: 20044
[startup+950.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 4541 0 0 0 94997 16 0 0 25 0 1 0 546358490 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5011 4519 603 41 0 4970 0
vsize: 20044
[startup+960.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 4541 0 0 0 95997 16 0 0 25 0 1 0 546358490 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5011 4519 603 41 0 4970 0
vsize: 20044
[startup+970.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 4541 0 0 0 96997 16 0 0 25 0 1 0 546358490 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5011 4519 603 41 0 4970 0
vsize: 20044
[startup+980.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 4541 0 0 0 97998 16 0 0 25 0 1 0 546358490 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5011 4519 603 41 0 4970 0
vsize: 20044
[startup+990.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 4541 0 0 0 98998 16 0 0 25 0 1 0 546358490 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5011 4519 603 41 0 4970 0
vsize: 20044
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 4541 0 0 0 99998 16 0 0 25 0 1 0 546358490 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134560885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5011 4519 603 41 0 4970 0
vsize: 20044
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 4541 0 0 0 100998 16 0 0 25 0 1 0 546358490 20525056 4519 4294967295 134512640 134672761 3221224544 3221223648 134560198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5011 4519 603 41 0 4970 0
vsize: 20044
[startup+1020.03 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 4541 0 0 0 101998 16 0 0 25 0 1 0 546358490 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134561133 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5011 4519 603 41 0 4970 0
vsize: 20044
[startup+1030.03 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 4541 0 0 0 102998 16 0 0 25 0 1 0 546358490 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5011 4519 603 41 0 4970 0
vsize: 20044
[startup+1040.03 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 4541 0 0 0 103998 16 0 0 25 0 1 0 546358490 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5011 4519 603 41 0 4970 0
vsize: 20044
[startup+1050.03 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 4541 0 0 0 104999 16 0 0 25 0 1 0 546358490 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5011 4519 603 41 0 4970 0
vsize: 20044
[startup+1060.03 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 4541 0 0 0 105999 16 0 0 25 0 1 0 546358490 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5011 4519 603 41 0 4970 0
vsize: 20044
[startup+1070.03 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 4541 0 0 0 106999 16 0 0 25 0 1 0 546358490 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5011 4519 603 41 0 4970 0
vsize: 20044
[startup+1080.03 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 4541 0 0 0 107999 16 0 0 25 0 1 0 546358490 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5011 4519 603 41 0 4970 0
vsize: 20044
[startup+1090.03 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 4541 0 0 0 109000 16 0 0 25 0 1 0 546358490 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5011 4519 603 41 0 4970 0
vsize: 20044
[startup+1100.03 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 4541 0 0 0 110000 16 0 0 25 0 1 0 546358490 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5011 4519 603 41 0 4970 0
vsize: 20044
[startup+1110.03 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 4541 0 0 0 111000 16 0 0 25 0 1 0 546358490 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5011 4519 603 41 0 4970 0
vsize: 20044
[startup+1120.03 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 4541 0 0 0 112000 16 0 0 25 0 1 0 546358490 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5011 4519 603 41 0 4970 0
vsize: 20044
[startup+1130.03 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 4541 0 0 0 113000 16 0 0 25 0 1 0 546358490 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5011 4519 603 41 0 4970 0
vsize: 20044
[startup+1140.03 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 4541 0 0 0 114000 16 0 0 25 0 1 0 546358490 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5011 4519 603 41 0 4970 0
vsize: 20044
[startup+1150.03 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 4541 0 0 0 115001 16 0 0 25 0 1 0 546358490 20525056 4519 4294967295 134512640 134672761 3221224544 3221223728 134559179 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5011 4519 603 41 0 4970 0
vsize: 20044
[startup+1160.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 4541 0 0 0 116001 16 0 0 25 0 1 0 546358490 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5011 4519 603 41 0 4970 0
vsize: 20044
[startup+1170.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 4541 0 0 0 117001 16 0 0 25 0 1 0 546358490 20525056 4519 4294967295 134512640 134672761 3221224544 3221223728 134559330 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5011 4519 603 41 0 4970 0
vsize: 20044
[startup+1180.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 4541 0 0 0 118001 17 0 0 25 0 1 0 546358490 20525056 4519 4294967295 134512640 134672761 3221224544 3221223744 134557822 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5011 4519 603 41 0 4970 0
vsize: 20044
[startup+1190.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 4541 0 0 0 119001 17 0 0 25 0 1 0 546358490 20525056 4519 4294967295 134512640 134672761 3221224544 3221223712 134560906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5011 4519 603 41 0 4970 0
vsize: 20044
[startup+1200.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12670
Raw data (stat): 12668 (minisat+) R 12667 28546 28545 0 -1 0 4541 0 0 0 120001 17 0 0 25 0 1 0 546358490 20525056 4519 4294967295 134512640 134672761 3221224544 3221223680 134565086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5011 4519 603 41 0 4970 0
vsize: 20044
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.04 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 12670
Raw data (stat): 12668 (minisat+) Z 12667 28546 28545 0 -1 12 4544 0 0 0 120002 18 0 0 25 0 1 0 546358490 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.04
CPU time (s): 1200.2
CPU user time (s): 1200.02
CPU system time (s): 0.180972
CPU usage (%): 100.013
Max. virtual memory (Kb): 20044
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####