PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

Name	normalized-opb/mps-v2-20-10/plato.asu.edu/pub/milp/normalized-mps-v2-20-10-markshare2_1.opb
MD5SUM	a84a96a9314212f3d8ecd5227c500cef
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	91392
Optimality of the best value was proved	NO
Number of terms in the objective function	210
Biggest coefficient in the objective function	536870912
Number of bits for the biggest coefficient in the objective function	30
Sum of the numbers in the objective function	7516192761
Number of bits of the sum of numbers in the objective function	33
Biggest number in a constraint	536870912
Number of bits of the biggest number in a constraint	30
Biggest sum of numbers in a constraint	7516192761
Number of bits of the biggest sum of numbers	33
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1202.31
Number of variables	330
Total number of constraints	67
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	54
Number of constraints which are nor clauses,nor cardinality constraints	13
Minimum length of a constraint	1
Maximum length of a constraint	150
Trace number 20774

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc19 THE 2005-04-21 21:47:48 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=14487 boxname=wulflinc19 idbench=1115 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  a84a96a9314212f3d8ecd5227c500cef  /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-20-10-markshare2_1.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-20-10-markshare2_1.opb
IDLAUNCH: 14487
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        631392 kB
Buffers:         27992 kB
Cached:         351568 kB
SwapCached:        560 kB
Active:         134040 kB
Inactive:       247516 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        631140 kB
SwapTotal:     2097892 kB
SwapFree:      2096388 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           5168 kB
Slab:            15948 kB
Committed_AS:    63820 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 22:07:51 (client local time) WITH STATUS 10 IN 1200.46 SECONDS
stats: 14487 7 1200.46 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 20 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #######
c   -- Clauses(.)/Splits(s): (none)
c ---[  19]---> BDD-cost:   10
c ---[  18]---> BDD-cost:   10
c ---[  17]---> BDD-cost:   10
c ---[  16]---> BDD-cost:   10
c ---[  15]---> BDD-cost:   10
c ---[  14]---> BDD-cost:   10
c ---[  12]---> Adder-cost: 708   maxlim: 3756758   bits: 23/22
c ---[  10]---> Adder-cost: 758   maxlim: 4064912   bits: 23/22
c ---[   8]---> Adder-cost: 714   maxlim: 3859164   bits: 23/22
c ---[   6]---> Adder-cost: 676   maxlim: 4153021   bits: 23/22
c ---[   4]---> Adder-cost: 812   maxlim: 3812158   bits: 23/22
c ---[   2]---> Adder-cost: 766   maxlim: 4131466   bits: 23/22
c ---[   0]---> Adder-cost: 692   maxlim: 3780388   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   34933   124179 |   11644       0        0     nan |  0.000 % |
c |       100 |   34933   124179 |   12808     100      416     4.2 |  6.830 % |
c |       250 |   34933   124179 |   14089     250     1526     6.1 |  6.830 % |
c |       475 |   34933   124179 |   15498     475     3526     7.4 |  6.830 % |
c ==============================================================================
c [1mFound solution: 8658716[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 2158     Base: 2 2 2 2 2 2 2 2 2 2 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 |       805 |   40455   137066 |   13485     804     7989     9.9 |  6.830 % |
c ==============================================================================
c [1mFound solution: 5260062[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   19     Base: 2 2 2 2 2 2 2 2 2 2 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 |       835 |   40500   137210 |   13500     834     8278     9.9 |  6.830 % |
c |       935 |   40492   137184 |   14850     933     9140     9.8 |  5.136 % |
c |      1085 |   40460   137080 |   16335    1079    10291     9.5 |  5.189 % |
c |      1310 |   40460   137080 |   17968    1304    11927     9.1 |  5.189 % |
c |      1647 |   40460   137080 |   19765    1641    13700     8.3 |  5.189 % |
c |      2154 |   40436   137002 |   21741    2145    20816     9.7 |  5.228 % |
c |      2914 |   40428   136976 |   23916    2904    37504    12.9 |  5.242 % |
c |      4054 |   40428   136976 |   26307    4044    60613    15.0 |  5.242 % |
c ==============================================================================
c [1mFound solution: 4950048[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   20     Base: 2 2 2 2 2 2 2 2 2 2 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 |      4373 |   40449   137020 |   13483    4356    90869    20.9 |  5.242 % |
c |      4473 |   40449   137020 |   14831    4456    93625    21.0 |  5.271 % |
c |      4623 |   40449   137020 |   16314    4606    94532    20.5 |  5.271 % |
c |      4848 |   40449   137020 |   17945    4831    97424    20.2 |  5.271 % |
c |      5186 |   40449   137020 |   19740    5169   101715    19.7 |  5.271 % |
c |      5693 |   40449   137020 |   21714    5676   114014    20.1 |  5.271 % |
c |      6452 |   40449   137020 |   23885    6435   142255    22.1 |  5.271 % |
c ==============================================================================
c [1mFound solution: 4620607[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   21     Base: 2 2 2 2 2 2 2 2 2 2 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 |      6683 |   40491   137120 |   13497    6666   159247    23.9 |  5.271 % |
c |      6783 |   40483   137094 |   14846    6765   160692    23.8 |  5.282 % |
c |      6933 |   40483   137094 |   16331    6915   164982    23.9 |  5.282 % |
c |      7158 |   40483   137094 |   17964    7140   169116    23.7 |  5.282 % |
c |      7495 |   40483   137094 |   19760    7477   174450    23.3 |  5.282 % |
c |      8004 |   40467   137042 |   21737    7984   180282    22.6 |  5.308 % |
c |      8763 |   40461   137024 |   23910    8742   191914    22.0 |  5.321 % |
c |      9902 |   40453   136998 |   26301    9880   257083    26.0 |  5.335 % |
c |     11611 |   40453   136998 |   28932   11589   499552    43.1 |  5.335 % |
c ==============================================================================
c [1mFound solution: 4249759[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   17     Base: 2 2 2 2 2 2 2 2 2 2 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 |     11737 |   40475   137049 |   13491   11715   502214    42.9 |  5.335 % |
c |     11837 |   40475   137049 |   14840   11815   507717    43.0 |  5.341 % |
c |     11987 |   40475   137049 |   16324   11965   515534    43.1 |  5.341 % |
c |     12212 |   40475   137049 |   17956   12190   524302    43.0 |  5.341 % |
c |     12550 |   40475   137049 |   19752   12528   540452    43.1 |  5.341 % |
c |     13056 |   40467   137023 |   21727   13033   550988    42.3 |  5.354 % |
c |     13815 |   40467   137023 |   23900   13792   578807    42.0 |  5.354 % |
c |     14955 |   40467   137023 |   26290   14932   644252    43.1 |  5.354 % |
c ==============================================================================
c [1mFound solution: 3339853[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   21     Base: 2 2 2 2 2 2 2 2 2 2 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 |     15826 |   40493   137087 |   13497   15803   672645    42.6 |  5.354 % |
c |     15926 |   40493   137087 |   14846    8002   416550    52.1 |  5.356 % |
c |     16076 |   40493   137087 |   16331    8152   422105    51.8 |  5.356 % |
c |     16301 |   40493   137087 |   17964    8377   437923    52.3 |  5.356 % |
c |     16638 |   40493   137087 |   19760    8714   445487    51.1 |  5.356 % |
c |     17144 |   40493   137087 |   21737    9220   455219    49.4 |  5.356 % |
c ==============================================================================
c [1mFound solution: 3334229[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   19     Base: 2 2 2 2 2 2 2 2 2 2 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 |     17762 |   40515   137139 |   13505    9838   522989    53.2 |  5.356 % |
c |     17863 |   40515   137139 |   14855    9939   525768    52.9 |  5.363 % |
c |     18013 |   40515   137139 |   16341   10089   527063    52.2 |  5.363 % |
c |     18241 |   40515   137139 |   17975   10317   529533    51.3 |  5.363 % |
c |     18578 |   40515   137139 |   19772   10654   536878    50.4 |  5.363 % |
c ==============================================================================
c [1mFound solution: 3287413[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   17     Base: 2 2 2 2 2 2 2 2 2 2 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 |     19079 |   40536   137188 |   13512   11155   547166    49.1 |  5.363 % |
c |     19180 |   40536   137188 |   14863   11256   550369    48.9 |  5.368 % |
c |     19330 |   40536   137188 |   16349   11406   553026    48.5 |  5.368 % |
c |     19555 |   40536   137188 |   17984   11631   558823    48.0 |  5.368 % |
c |     19893 |   40536   137188 |   19782   11969   572765    47.9 |  5.368 % |
c |     20399 |   40528   137162 |   21761   12474   580989    46.6 |  5.381 % |
c |     21158 |   40522   137149 |   23937   13228   596004    45.1 |  5.407 % |
c ==============================================================================
c [1mFound solution: 2290547[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   20     Base: 2 2 2 2 2 2 2 2 2 2 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 |     21322 |   40544   137206 |   13514   13392   600636    44.9 |  5.407 % |
c |     21422 |   40544   137206 |   14865   13492   604346    44.8 |  5.412 % |
c |     21573 |   40544   137206 |   16351   13643   607938    44.6 |  5.412 % |
c |     21798 |   40544   137206 |   17987   13868   614171    44.3 |  5.412 % |
c |     22135 |   40544   137206 |   19785   14205   624729    44.0 |  5.412 % |
c |     22644 |   40544   137206 |   21764   14714   638820    43.4 |  5.412 % |
c |     23404 |   40544   137206 |   23940   15474   661163    42.7 |  5.412 % |
c |     24543 |   40544   137206 |   26334   16613   721090    43.4 |  5.412 % |
c |     26252 |   40544   137206 |   28968   18322   789853    43.1 |  5.412 % |
c |     28815 |   40544   137206 |   31865   20885   905885    43.4 |  5.412 % |
c |     32661 |   40535   137179 |   35051   24730  1011947    40.9 |  5.438 % |
c |     38427 |   40535   137179 |   38557   30496  1345865    44.1 |  5.438 % |
c ==============================================================================
c [1mFound solution: 1436307[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   17     Base: 2 2 2 2 2 2 2 2 2 2 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 |     45811 |   40559   137239 |   13519   37880  1653565    43.7 |  5.438 % |
c |     45912 |   40559   137239 |   14870    7144   239022    33.5 |  5.440 % |
c |     46063 |   40559   137239 |   16357    7295   247734    34.0 |  5.440 % |
c |     46288 |   40559   137239 |   17993    7520   249720    33.2 |  5.440 % |
c |     46627 |   40559   137239 |   19793    7859   253146    32.2 |  5.440 % |
c |     47134 |   40559   137239 |   21772    8366   269347    32.2 |  5.440 % |
c |     47893 |   40559   137239 |   23949    9125   361442    39.6 |  5.440 % |
c |     49032 |   40559   137239 |   26344   10264   396132    38.6 |  5.440 % |
c |     50741 |   40559   137239 |   28979   11973   437100    36.5 |  5.440 % |
c |     53303 |   40559   137239 |   31877   14535   538464    37.0 |  5.440 % |
c ==============================================================================
c [1mFound solution: 1226125[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   16     Base: 2 2 2 2 2 2 2 2 2 2 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 |     53727 |   40579   137287 |   13526   14959   548574    36.7 |  5.440 % |
c |     53828 |   40579   137287 |   14878    7581   202510    26.7 |  5.445 % |
c |     53978 |   40579   137287 |   16366    7731   204888    26.5 |  5.445 % |
c |     54204 |   40579   137287 |   18003    7957   208315    26.2 |  5.445 % |
c |     54542 |   40579   137287 |   19803    8295   216444    26.1 |  5.445 % |
c |     55048 |   40579   137287 |   21783    8801   224770    25.5 |  5.445 % |
c |     55809 |   40579   137287 |   23962    9562   252224    26.4 |  5.445 % |
c |     56950 |   40579   137287 |   26358   10703   296178    27.7 |  5.445 % |
c |     58660 |   40573   137269 |   28994   12412   374420    30.2 |  5.458 % |
c |     61223 |   40573   137269 |   31893   14975   496937    33.2 |  5.458 % |
c |     65067 |   40573   137269 |   35082   18819   695359    36.9 |  5.458 % |
c |     70834 |   40573   137269 |   38591   24586   924178    37.6 |  5.458 % |
c |     79483 |   40547   137211 |   42450   33229  1386072    41.7 |  5.549 % |
c |     92457 |   40547   137211 |   46695   16206   718044    44.3 |  5.549 % |
c |    111919 |   40547   137211 |   51364   35668  1877866    52.6 |  5.549 % |
c |    141112 |   40547   137211 |   56501   26554  1476960    55.6 |  5.549 % |
c |    184902 |   40547   137211 |   62151   25536  2450937    96.0 |  5.549 % |
c |    250586 |   40535   137180 |   68366   43565  2228582    51.2 |  5.588 % |
c |    349114 |   40535   137180 |   75203   35537  2570698    72.3 |  5.588 % |
c |    496904 |   40535   137180 |   82723   63098  3631157    57.5 |  5.588 % |
c ==============================================================================
c [1mFound solution: 937675[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   18     Base: 2 2 2 2 2 2 2 2 2 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 |    611637 |   40477   136981 |   13492   41360  3147226    76.1 |  5.588 % |
c |    611737 |   40477   136981 |   14841    7432   636521    85.6 |  5.761 % |
c |    611887 |   40477   136981 |   16325    7582   639768    84.4 |  5.761 % |
c |    612112 |   40477   136981 |   17957    7807   641772    82.2 |  5.761 % |
c |    612449 |   40477   136981 |   19753    8144   651973    80.1 |  5.761 % |
c |    612956 |   40477   136981 |   21729    8651   667626    77.2 |  5.761 % |
c |    613717 |   40477   136981 |   23901    9412   691168    73.4 |  5.761 % |
c |    614857 |   40477   136981 |   26292   10552   723865    68.6 |  5.761 % |
c |    616566 |   40477   136981 |   28921   12261   788603    64.3 |  5.761 % |
c |    619128 |   40472   136970 |   31813   14822   938756    63.3 |  5.787 % |
c |    622973 |   40472   136970 |   34994   18667  1092890    58.5 |  5.787 % |
c |    628739 |   40472   136970 |   38494   24433  1322315    54.1 |  5.787 % |
c |    637388 |   40448   136917 |   42343   33079  1753094    53.0 |  5.892 % |
c |    650363 |   40404   136818 |   46578   17084   937926    54.9 |  6.061 % |
c |    669828 |   40396   136796 |   51235   36548  1867018    51.1 |  6.087 % |
c |    699020 |   40396   136796 |   56359   27623  1424195    51.6 |  6.087 % |
c |    742811 |   40396   136796 |   61995   27073  1822699    67.3 |  6.087 % |
c ==============================================================================
c [1mFound solution: 681120[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 2 2 2 2 2 2 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 |    749104 |   40314   136607 |   13438   33351  2060389    61.8 |  6.087 % |
c |    749204 |   40314   136607 |   14781    7777   221057    28.4 |  6.533 % |
c |    749355 |   40314   136607 |   16259    7928   223104    28.1 |  6.533 % |
c |    749580 |   40314   136607 |   17885    8153   227139    27.9 |  6.533 % |
c |    749918 |   40314   136607 |   19674    8491   236519    27.9 |  6.533 % |
c |    750424 |   40314   136607 |   21642    8997   248399    27.6 |  6.533 % |
c |    751183 |   40314   136607 |   23806    9756   265928    27.3 |  6.533 % |
c |    752322 |   40314   136607 |   26186   10895   306954    28.2 |  6.533 % |
c |    754030 |   40314   136607 |   28805   12603   375521    29.8 |  6.533 % |
c |    756592 |   40314   136607 |   31686   15165   477461    31.5 |  6.533 % |
c |    760437 |   40314   136607 |   34854   19010   626240    32.9 |  6.533 % |
c |    766203 |   40314   136607 |   38340   24776   878769    35.5 |  6.533 % |
c |    774852 |   40314   136607 |   42174   33425  1385351    41.4 |  6.533 % |
#### 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.84 0.94 0.91 2/55 9542
Raw data (stat): 9542 (runsolver) R 9541 22929 22928 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 548432572 1052672 99 4294967295 134512640 135381576 3221224512 3221219756 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0003 s]
Raw data (loadavg): 0.87 0.94 0.91 2/55 9542
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 1814 0 0 0 993 5 0 0 25 0 1 0 548432572 9093120 1788 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2220 1788 603 41 0 2179 0
vsize: 8880
[startup+20.0008 s]
Raw data (loadavg): 0.89 0.94 0.91 2/55 9542
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 2233 0 0 0 1991 7 0 0 25 0 1 0 548432572 10829824 2207 4294967295 134512640 134672761 3221224624 3221223808 134559590 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2644 2207 603 41 0 2603 0
vsize: 10576
[startup+30.0003 s]
Raw data (loadavg): 0.90 0.94 0.91 2/55 9542
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 3027 0 0 0 2988 10 0 0 25 0 1 0 548432572 14188544 3001 4294967295 134512640 134672761 3221224624 3221223760 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3464 3001 603 41 0 3423 0
vsize: 13856
[startup+40.0004 s]
Raw data (loadavg): 0.92 0.94 0.91 2/55 9542
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 3246 0 0 0 3988 11 0 0 25 0 1 0 548432572 14995456 3220 4294967295 134512640 134672761 3221224624 3221223792 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3661 3220 603 41 0 3620 0
vsize: 14644
[startup+50.0012 s]
Raw data (loadavg): 0.93 0.94 0.91 2/55 9542
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 3246 0 0 0 4988 11 0 0 25 0 1 0 548432572 14995456 3220 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3661 3220 603 41 0 3620 0
vsize: 14644
[startup+60.0009 s]
Raw data (loadavg): 0.94 0.95 0.91 2/55 9542
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 3246 0 0 0 5987 11 0 0 25 0 1 0 548432572 14995456 3220 4294967295 134512640 134672761 3221224624 3221223792 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3661 3220 603 41 0 3620 0
vsize: 14644
[startup+70.0019 s]
Raw data (loadavg): 0.95 0.95 0.91 2/55 9542
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 3716 0 0 0 6986 12 0 0 25 0 1 0 548432572 17002496 3690 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4151 3690 603 41 0 4110 0
vsize: 16604
[startup+80.0026 s]
Raw data (loadavg): 0.96 0.95 0.91 2/55 9542
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 3716 0 0 0 7986 12 0 0 25 0 1 0 548432572 17002496 3690 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4151 3690 603 41 0 4110 0
vsize: 16604
[startup+90.0032 s]
Raw data (loadavg): 0.96 0.95 0.91 2/55 9542
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 3719 0 0 0 8986 12 0 0 25 0 1 0 548432572 17002496 3693 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4151 3693 603 41 0 4110 0
vsize: 16604
[startup+100.003 s]
Raw data (loadavg): 0.97 0.95 0.91 2/55 9542
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 4077 0 0 0 9985 13 0 0 25 0 1 0 548432572 18489344 4051 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4514 4051 603 41 0 4473 0
vsize: 18056
[startup+110.003 s]
Raw data (loadavg): 0.97 0.95 0.91 2/55 9542
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 4441 0 0 0 10984 14 0 0 25 0 1 0 548432572 19959808 4415 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4873 4416 603 41 0 4832 0
vsize: 19492
[startup+120.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 9542
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 4812 0 0 0 11983 16 0 0 25 0 1 0 548432572 21438464 4786 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5234 4786 603 41 0 5193 0
vsize: 20936
[startup+130.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 9544
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 4812 0 0 0 12983 16 0 0 25 0 1 0 548432572 21438464 4786 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5234 4786 603 41 0 5193 0
vsize: 20936
[startup+140.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 9544
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 4817 0 0 0 13983 16 0 0 25 0 1 0 548432572 21438464 4791 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5234 4791 603 41 0 5193 0
vsize: 20936
[startup+150.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 9544
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 4817 0 0 0 14984 16 0 0 25 0 1 0 548432572 21438464 4791 4294967295 134512640 134672761 3221224624 3221223776 134565213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5234 4791 603 41 0 5193 0
vsize: 20936
[startup+160.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 9544
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 4821 0 0 0 15984 16 0 0 25 0 1 0 548432572 21438464 4795 4294967295 134512640 134672761 3221224624 3221223624 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5234 4795 603 41 0 5193 0
vsize: 20936
[startup+170.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 9544
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 5375 0 0 0 16983 17 0 0 25 0 1 0 548432572 23728128 5349 4294967295 134512640 134672761 3221224624 3221223792 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5793 5349 603 41 0 5752 0
vsize: 23172
[startup+180.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 9544
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 5821 0 0 0 17982 18 0 0 25 0 1 0 548432572 25595904 5795 4294967295 134512640 134672761 3221224624 3221223792 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6249 5795 603 41 0 6208 0
vsize: 24996
[startup+190.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 9544
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 5821 0 0 0 18982 18 0 0 25 0 1 0 548432572 25595904 5795 4294967295 134512640 134672761 3221224624 3221223728 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6249 5795 603 41 0 6208 0
vsize: 24996
[startup+200.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 9544
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 5821 0 0 0 19983 19 0 0 25 0 1 0 548432572 25595904 5795 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6249 5795 603 41 0 6208 0
vsize: 24996
[startup+210.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 9544
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 5821 0 0 0 20983 19 0 0 25 0 1 0 548432572 25595904 5795 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6249 5795 603 41 0 6208 0
vsize: 24996
[startup+220.027 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 9544
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 5874 0 0 0 21984 19 0 0 25 0 1 0 548432572 25731072 5848 4294967295 134512640 134672761 3221224624 3221223728 134560276 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6282 5848 603 41 0 6241 0
vsize: 25128
[startup+230.027 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 9544
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 6376 0 0 0 22983 20 0 0 25 0 1 0 548432572 27746304 6350 4294967295 134512640 134672761 3221224624 3221223792 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6774 6350 603 41 0 6733 0
vsize: 27096
[startup+240.029 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 9544
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 6962 0 0 0 23982 21 0 0 25 0 1 0 548432572 30167040 6936 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7365 6936 603 41 0 7324 0
vsize: 29460
[startup+250.029 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 9544
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 7212 0 0 0 24981 22 0 0 25 0 1 0 548432572 31236096 7186 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7626 7186 603 41 0 7585 0
vsize: 30504
[startup+260.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9544
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 7212 0 0 0 25982 22 0 0 25 0 1 0 548432572 31236096 7186 4294967295 134512640 134672761 3221224624 3221223792 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7626 7186 603 41 0 7585 0
vsize: 30504
[startup+270.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9544
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 7212 0 0 0 26982 22 0 0 25 0 1 0 548432572 31236096 7186 4294967295 134512640 134672761 3221224624 3221223792 134561133 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7626 7186 603 41 0 7585 0
vsize: 30504
[startup+280.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9544
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 7212 0 0 0 27982 22 0 0 25 0 1 0 548432572 31236096 7186 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7626 7186 603 41 0 7585 0
vsize: 30504
[startup+290.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9544
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 7212 0 0 0 28982 22 0 0 25 0 1 0 548432572 31236096 7186 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7626 7186 603 41 0 7585 0
vsize: 30504
[startup+300.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9544
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 7212 0 0 0 29982 22 0 0 25 0 1 0 548432572 31236096 7186 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7626 7186 603 41 0 7585 0
vsize: 30504
[startup+310.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9544
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 7219 0 0 0 30982 22 0 0 25 0 1 0 548432572 31498240 7193 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7690 7193 603 41 0 7649 0
vsize: 30760
[startup+320.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9544
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 7220 0 0 0 31984 22 0 0 25 0 1 0 548432572 31498240 7194 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7690 7194 603 41 0 7649 0
vsize: 30760
[startup+330.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9544
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 7220 0 0 0 32985 22 0 0 25 0 1 0 548432572 31498240 7194 4294967295 134512640 134672761 3221224624 3221223808 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7690 7194 603 41 0 7649 0
vsize: 30760
[startup+340.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9544
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 7220 0 0 0 33985 22 0 0 25 0 1 0 548432572 31498240 7194 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7690 7194 603 41 0 7649 0
vsize: 30760
[startup+350.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9544
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 7220 0 0 0 34985 22 0 0 25 0 1 0 548432572 31498240 7194 4294967295 134512640 134672761 3221224624 3221223728 134560059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7690 7194 603 41 0 7649 0
vsize: 30760
[startup+360.166 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9544
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 7220 0 0 0 35997 22 0 0 25 0 1 0 548432572 31498240 7194 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7690 7194 603 41 0 7649 0
vsize: 30760
[startup+370.167 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9544
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 7220 0 0 0 36997 22 0 0 25 0 1 0 548432572 31498240 7194 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7690 7194 603 41 0 7649 0
vsize: 30760
[startup+380.167 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9544
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 7220 0 0 0 37997 22 0 0 25 0 1 0 548432572 31498240 7194 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7690 7194 603 41 0 7649 0
vsize: 30760
[startup+390.167 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9544
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 7220 0 0 0 38997 22 0 0 25 0 1 0 548432572 31498240 7194 4294967295 134512640 134672761 3221224624 3221223792 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7690 7194 603 41 0 7649 0
vsize: 30760
[startup+400.177 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9544
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 7220 0 0 0 39999 22 0 0 25 0 1 0 548432572 31498240 7194 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7690 7194 603 41 0 7649 0
vsize: 30760
[startup+410.179 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9544
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 7220 0 0 0 40999 22 0 0 25 0 1 0 548432572 31498240 7194 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7690 7194 603 41 0 7649 0
vsize: 30760
[startup+420.179 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9544
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 7478 0 0 0 41998 23 0 0 25 0 1 0 548432572 32579584 7452 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7954 7452 603 41 0 7913 0
vsize: 31816
[startup+430.18 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9546
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 7761 0 0 0 42997 24 0 0 25 0 1 0 548432572 33787904 7735 4294967295 134512640 134672761 3221224624 3221223792 134561161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8249 7735 603 41 0 8208 0
vsize: 32996
[startup+440.181 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9546
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 7983 0 0 0 43998 24 0 0 25 0 1 0 548432572 34586624 7957 4294967295 134512640 134672761 3221224624 3221223792 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8444 7957 603 41 0 8403 0
vsize: 33776
[startup+450.18 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9546
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 8145 0 0 0 44997 25 0 0 25 0 1 0 548432572 35254272 8119 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8607 8119 603 41 0 8566 0
vsize: 34428
[startup+460.18 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9546
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 8145 0 0 0 45997 25 0 0 25 0 1 0 548432572 35254272 8119 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8607 8119 603 41 0 8566 0
vsize: 34428
[startup+470.185 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9546
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 8145 0 0 0 46998 25 0 0 25 0 1 0 548432572 35254272 8119 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8607 8119 603 41 0 8566 0
vsize: 34428
[startup+480.185 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9546
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 8150 0 0 0 47998 25 0 0 25 0 1 0 548432572 35414016 8124 4294967295 134512640 134672761 3221224624 3221223792 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8646 8124 603 41 0 8605 0
vsize: 34584
[startup+490.194 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9546
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 8150 0 0 0 48999 25 0 0 25 0 1 0 548432572 35414016 8124 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8646 8124 603 41 0 8605 0
vsize: 34584
[startup+500.203 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9546
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 8151 0 0 0 49999 25 0 0 25 0 1 0 548432572 35414016 8125 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8646 8125 603 41 0 8605 0
vsize: 34584
[startup+510.202 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9546
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 8151 0 0 0 50999 25 0 0 25 0 1 0 548432572 35414016 8125 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8646 8125 603 41 0 8605 0
vsize: 34584
[startup+520.203 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9546
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 8151 0 0 0 51999 25 0 0 25 0 1 0 548432572 35414016 8125 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8646 8125 603 41 0 8605 0
vsize: 34584
[startup+530.208 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9546
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 8154 0 0 0 53000 25 0 0 25 0 1 0 548432572 35414016 8128 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8646 8128 603 41 0 8605 0
vsize: 34584
[startup+540.213 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9546
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 8157 0 0 0 54001 25 0 0 25 0 1 0 548432572 35414016 8131 4294967295 134512640 134672761 3221224624 3221223728 134555116 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8646 8131 603 41 0 8605 0
vsize: 34584
[startup+550.221 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9546
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 8157 0 0 0 55002 25 0 0 25 0 1 0 548432572 35414016 8131 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8646 8131 603 41 0 8605 0
vsize: 34584
[startup+560.225 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9546
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 8172 0 0 0 56002 26 0 0 25 0 1 0 548432572 35414016 8146 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8646 8146 603 41 0 8605 0
vsize: 34584
[startup+570.225 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9546
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 8258 0 0 0 57002 26 0 0 25 0 1 0 548432572 35815424 8232 4294967295 134512640 134672761 3221224624 3221223792 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8744 8232 603 41 0 8703 0
vsize: 34976
[startup+580.225 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9546
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 8259 0 0 0 58002 26 0 0 25 0 1 0 548432572 35815424 8233 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8744 8233 603 41 0 8703 0
vsize: 34976
[startup+590.226 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9546
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 8259 0 0 0 59002 26 0 0 25 0 1 0 548432572 35815424 8233 4294967295 134512640 134672761 3221224624 3221223792 134560906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8744 8233 603 41 0 8703 0
vsize: 34976
[startup+600.226 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9546
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 8259 0 0 0 60003 26 0 0 25 0 1 0 548432572 35815424 8233 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8744 8233 603 41 0 8703 0
vsize: 34976
[startup+610.234 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9546
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 8259 0 0 0 61004 26 0 0 25 0 1 0 548432572 35815424 8233 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8744 8233 603 41 0 8703 0
vsize: 34976
[startup+620.239 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9546
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 8261 0 0 0 62004 26 0 0 25 0 1 0 548432572 35815424 8235 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8744 8235 603 41 0 8703 0
vsize: 34976
[startup+630.239 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9546
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 8271 0 0 0 63004 26 0 0 25 0 1 0 548432572 35815424 8245 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8744 8245 603 41 0 8703 0
vsize: 34976
[startup+640.252 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9546
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 8271 0 0 0 64006 26 0 0 25 0 1 0 548432572 35815424 8245 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8744 8245 603 41 0 8703 0
vsize: 34976
[startup+650.271 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9546
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 8271 0 0 0 65008 26 0 0 25 0 1 0 548432572 35815424 8245 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8744 8245 603 41 0 8703 0
vsize: 34976
[startup+660.271 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9546
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 8271 0 0 0 66008 26 0 0 25 0 1 0 548432572 35815424 8245 4294967295 134512640 134672761 3221224624 3221223792 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8744 8245 603 41 0 8703 0
vsize: 34976
[startup+670.271 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9546
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 8271 0 0 0 67008 26 0 0 25 0 1 0 548432572 35815424 8245 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8744 8245 603 41 0 8703 0
vsize: 34976
[startup+680.271 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9546
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 8271 0 0 0 68008 26 0 0 25 0 1 0 548432572 35815424 8245 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8744 8245 603 41 0 8703 0
vsize: 34976
[startup+690.272 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9546
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 8354 0 0 0 69008 26 0 0 25 0 1 0 548432572 36216832 8328 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8842 8328 603 41 0 8801 0
vsize: 35368
[startup+700.272 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9546
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 8507 0 0 0 70008 27 0 0 25 0 1 0 548432572 36880384 8481 4294967295 134512640 134672761 3221224624 3221223728 134559796 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9004 8481 603 41 0 8963 0
vsize: 36016
[startup+710.271 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9546
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 8507 0 0 0 71008 27 0 0 25 0 1 0 548432572 36880384 8481 4294967295 134512640 134672761 3221224624 3221223760 134560577 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9004 8481 603 41 0 8963 0
vsize: 36016
[startup+720.272 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9546
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 8507 0 0 0 72008 27 0 0 25 0 1 0 548432572 36880384 8481 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9004 8481 603 41 0 8963 0
vsize: 36016
[startup+730.272 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 9548
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 8507 0 0 0 73009 27 0 0 25 0 1 0 548432572 36880384 8481 4294967295 134512640 134672761 3221224624 3221223792 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9004 8481 603 41 0 8963 0
vsize: 36016
[startup+740.272 s]
Raw data (loadavg): 1.15 1.00 0.93 2/55 9601
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 8507 0 0 0 74008 27 0 0 25 0 1 0 548432572 36880384 8481 4294967295 134512640 134672761 3221224624 3221223792 134560797 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9004 8481 603 41 0 8963 0
vsize: 36016
[startup+750.273 s]
Raw data (loadavg): 1.13 1.00 0.93 2/55 9601
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 8519 0 0 0 75008 27 0 0 25 0 1 0 548432572 36880384 8493 4294967295 134512640 134672761 3221224624 3221223792 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9004 8493 603 41 0 8963 0
vsize: 36016
[startup+760.272 s]
Raw data (loadavg): 1.11 1.00 0.93 2/55 9601
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 8519 0 0 0 76008 27 0 0 25 0 1 0 548432572 36880384 8493 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9004 8493 603 41 0 8963 0
vsize: 36016
[startup+770.272 s]
Raw data (loadavg): 1.09 1.00 0.93 2/55 9601
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 8519 0 0 0 77008 27 0 0 25 0 1 0 548432572 36880384 8493 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9004 8493 603 41 0 8963 0
vsize: 36016
[startup+780.272 s]
Raw data (loadavg): 1.08 1.00 0.93 2/55 9601
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 8519 0 0 0 78008 27 0 0 25 0 1 0 548432572 36880384 8493 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9004 8493 603 41 0 8963 0
vsize: 36016
[startup+790.273 s]
Raw data (loadavg): 1.07 1.00 0.93 2/55 9601
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 8524 0 0 0 79008 27 0 0 25 0 1 0 548432572 36880384 8498 4294967295 134512640 134672761 3221224624 3221223792 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9004 8498 603 41 0 8963 0
vsize: 36016
[startup+800.273 s]
Raw data (loadavg): 1.06 1.00 0.93 2/55 9601
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 8530 0 0 0 80008 27 0 0 25 0 1 0 548432572 37027840 8504 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9040 8504 603 41 0 8999 0
vsize: 36160
[startup+810.272 s]
Raw data (loadavg): 1.05 1.00 0.93 2/55 9601
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 8535 0 0 0 81008 27 0 0 25 0 1 0 548432572 37027840 8509 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9040 8509 603 41 0 8999 0
vsize: 36160
[startup+820.273 s]
Raw data (loadavg): 1.04 1.00 0.93 2/55 9603
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 8656 0 0 0 82009 27 0 0 25 0 1 0 548432572 37433344 8630 4294967295 134512640 134672761 3221224624 3221223792 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9139 8630 603 41 0 9098 0
vsize: 36556
[startup+830.277 s]
Raw data (loadavg): 1.03 1.00 0.93 2/55 9603
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 8656 0 0 0 83009 27 0 0 25 0 1 0 548432572 37433344 8630 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9139 8630 603 41 0 9098 0
vsize: 36556
[startup+840.277 s]
Raw data (loadavg): 1.03 1.00 0.93 2/55 9603
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 8656 0 0 0 84009 27 0 0 25 0 1 0 548432572 37433344 8630 4294967295 134512640 134672761 3221224624 3221223728 134560174 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9139 8630 603 41 0 9098 0
vsize: 36556
[startup+850.277 s]
Raw data (loadavg): 1.02 1.00 0.93 2/55 9603
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 8656 0 0 0 85009 27 0 0 25 0 1 0 548432572 37433344 8630 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9139 8630 603 41 0 9098 0
vsize: 36556
[startup+860.277 s]
Raw data (loadavg): 1.02 1.00 0.93 2/55 9603
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 8656 0 0 0 86009 27 0 0 25 0 1 0 548432572 37433344 8630 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9139 8630 603 41 0 9098 0
vsize: 36556
[startup+870.277 s]
Raw data (loadavg): 1.02 1.00 0.93 2/55 9603
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 8656 0 0 0 87009 27 0 0 25 0 1 0 548432572 37433344 8630 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9139 8630 603 41 0 9098 0
vsize: 36556
[startup+880.277 s]
Raw data (loadavg): 1.01 1.00 0.93 2/55 9603
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 8656 0 0 0 88010 27 0 0 25 0 1 0 548432572 37433344 8630 4294967295 134512640 134672761 3221224624 3221223792 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9139 8630 603 41 0 9098 0
vsize: 36556
[startup+890.278 s]
Raw data (loadavg): 1.01 1.00 0.93 2/55 9603
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 8657 0 0 0 89010 28 0 0 25 0 1 0 548432572 37433344 8631 4294967295 134512640 134672761 3221224624 3221223792 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9139 8631 603 41 0 9098 0
vsize: 36556
[startup+900.278 s]
Raw data (loadavg): 1.01 1.00 0.93 2/55 9603
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 8657 0 0 0 90010 28 0 0 25 0 1 0 548432572 37433344 8631 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9139 8631 603 41 0 9098 0
vsize: 36556
[startup+910.278 s]
Raw data (loadavg): 1.01 1.00 0.93 2/55 9603
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 8657 0 0 0 91010 28 0 0 25 0 1 0 548432572 37433344 8631 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9139 8631 603 41 0 9098 0
vsize: 36556
[startup+920.279 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 9603
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 8995 0 0 0 92009 29 0 0 25 0 1 0 548432572 38789120 8969 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9470 8969 603 41 0 9429 0
vsize: 37880
[startup+930.279 s]
Raw data (loadavg): 1.14 1.03 0.94 2/55 9603
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 9303 0 0 0 93009 29 0 0 25 0 1 0 548432572 40148992 9277 4294967295 134512640 134672761 3221224624 3221223792 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9802 9277 603 41 0 9761 0
vsize: 39208
[startup+940.279 s]
Raw data (loadavg): 1.12 1.03 0.94 2/55 9603
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 9602 0 0 0 94008 31 0 0 25 0 1 0 548432572 41361408 9576 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10098 9576 603 41 0 10057 0
vsize: 40392
[startup+950.279 s]
Raw data (loadavg): 1.10 1.03 0.94 2/55 9603
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 9900 0 0 0 95007 32 0 0 25 0 1 0 548432572 42639360 9874 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10410 9874 603 41 0 10369 0
vsize: 41640
[startup+960.279 s]
Raw data (loadavg): 1.08 1.03 0.94 2/55 9603
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 9916 0 0 0 96007 32 0 0 25 0 1 0 548432572 42639360 9890 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10410 9890 603 41 0 10369 0
vsize: 41640
[startup+970.28 s]
Raw data (loadavg): 1.07 1.03 0.94 2/55 9603
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 9916 0 0 0 97007 32 0 0 25 0 1 0 548432572 42639360 9890 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10410 9890 603 41 0 10369 0
vsize: 41640
[startup+980.279 s]
Raw data (loadavg): 1.06 1.03 0.94 2/55 9603
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 9916 0 0 0 98007 32 0 0 25 0 1 0 548432572 42639360 9890 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10410 9890 603 41 0 10369 0
vsize: 41640
[startup+990.28 s]
Raw data (loadavg): 1.05 1.02 0.94 2/55 9603
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 9917 0 0 0 99007 32 0 0 25 0 1 0 548432572 42639360 9891 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10410 9891 603 41 0 10369 0
vsize: 41640
[startup+1000.28 s]
Raw data (loadavg): 1.04 1.02 0.94 2/55 9603
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 9917 0 0 0 100007 32 0 0 25 0 1 0 548432572 42639360 9891 4294967295 134512640 134672761 3221224624 3221223792 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10410 9891 603 41 0 10369 0
vsize: 41640
[startup+1010.28 s]
Raw data (loadavg): 1.03 1.02 0.94 2/55 9603
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 9917 0 0 0 101008 32 0 0 25 0 1 0 548432572 42639360 9891 4294967295 134512640 134672761 3221224624 3221223808 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10410 9891 603 41 0 10369 0
vsize: 41640
[startup+1020.28 s]
Raw data (loadavg): 1.03 1.02 0.94 2/55 9603
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 9919 0 0 0 102008 32 0 0 25 0 1 0 548432572 42639360 9893 4294967295 134512640 134672761 3221224624 3221223760 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10410 9893 603 41 0 10369 0
vsize: 41640
[startup+1030.29 s]
Raw data (loadavg): 1.02 1.02 0.94 2/55 9605
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 9919 0 0 0 103007 33 0 0 25 0 1 0 548432572 42639360 9893 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10410 9893 603 41 0 10369 0
vsize: 41640
[startup+1040.29 s]
Raw data (loadavg): 1.02 1.02 0.94 2/55 9605
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 9919 0 0 0 104007 33 0 0 25 0 1 0 548432572 42639360 9893 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10410 9893 603 41 0 10369 0
vsize: 41640
[startup+1050.29 s]
Raw data (loadavg): 1.02 1.02 0.94 2/55 9605
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 9919 0 0 0 105007 33 0 0 25 0 1 0 548432572 42639360 9893 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10410 9893 603 41 0 10369 0
vsize: 41640
[startup+1060.29 s]
Raw data (loadavg): 1.01 1.02 0.94 2/55 9605
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 9919 0 0 0 106007 33 0 0 25 0 1 0 548432572 42639360 9893 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10410 9893 603 41 0 10369 0
vsize: 41640
[startup+1070.29 s]
Raw data (loadavg): 1.01 1.02 0.94 2/55 9605
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 9919 0 0 0 107007 34 0 0 25 0 1 0 548432572 42639360 9893 4294967295 134512640 134672761 3221224624 3221223792 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10410 9893 603 41 0 10369 0
vsize: 41640
[startup+1080.29 s]
Raw data (loadavg): 1.01 1.02 0.94 2/55 9605
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 9919 0 0 0 108007 34 0 0 25 0 1 0 548432572 42639360 9893 4294967295 134512640 134672761 3221224624 3221223728 134559818 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10410 9893 603 41 0 10369 0
vsize: 41640
[startup+1090.29 s]
Raw data (loadavg): 1.01 1.01 0.94 2/55 9605
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 9919 0 0 0 109007 34 0 0 25 0 1 0 548432572 42639360 9893 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10410 9893 603 41 0 10369 0
vsize: 41640
[startup+1100.29 s]
Raw data (loadavg): 1.01 1.01 0.94 2/55 9605
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 9919 0 0 0 110007 34 0 0 25 0 1 0 548432572 42639360 9893 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10410 9893 603 41 0 10369 0
vsize: 41640
[startup+1110.29 s]
Raw data (loadavg): 1.00 1.01 0.94 2/55 9605
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 9919 0 0 0 111006 35 0 0 25 0 1 0 548432572 42639360 9893 4294967295 134512640 134672761 3221224624 3221223792 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10410 9893 603 41 0 10369 0
vsize: 41640
[startup+1120.29 s]
Raw data (loadavg): 1.00 1.01 0.94 2/55 9607
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 9919 0 0 0 112006 35 0 0 25 0 1 0 548432572 42639360 9893 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10410 9893 603 41 0 10369 0
vsize: 41640
[startup+1130.29 s]
Raw data (loadavg): 1.00 1.01 0.94 2/55 9607
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 9919 0 0 0 113006 35 0 0 25 0 1 0 548432572 42639360 9893 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10410 9893 603 41 0 10369 0
vsize: 41640
[startup+1140.29 s]
Raw data (loadavg): 1.00 1.01 0.94 2/55 9607
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 9919 0 0 0 114007 35 0 0 25 0 1 0 548432572 42639360 9893 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10410 9893 603 41 0 10369 0
vsize: 41640
[startup+1150.29 s]
Raw data (loadavg): 1.00 1.01 0.94 2/55 9607
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 9919 0 0 0 115007 35 0 0 25 0 1 0 548432572 42639360 9893 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10410 9893 603 41 0 10369 0
vsize: 41640
[startup+1160.29 s]
Raw data (loadavg): 1.00 1.01 0.94 2/55 9607
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 9919 0 0 0 116007 35 0 0 25 0 1 0 548432572 42639360 9893 4294967295 134512640 134672761 3221224624 3221223748 134566012 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10410 9893 603 41 0 10369 0
vsize: 41640
[startup+1170.29 s]
Raw data (loadavg): 1.00 1.01 0.94 2/55 9607
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 9919 0 0 0 117007 35 0 0 25 0 1 0 548432572 42639360 9893 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10410 9893 603 41 0 10369 0
vsize: 41640
[startup+1180.29 s]
Raw data (loadavg): 1.00 1.01 0.94 2/55 9607
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 9919 0 0 0 118007 35 0 0 25 0 1 0 548432572 42639360 9893 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10410 9893 603 41 0 10369 0
vsize: 41640
[startup+1190.3 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 9607
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 9919 0 0 0 119007 35 0 0 25 0 1 0 548432572 42639360 9893 4294967295 134512640 134672761 3221224624 3221223728 134560376 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10410 9893 603 41 0 10369 0
vsize: 41640
[startup+1200.3 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 9607
Raw data (stat): 9542 (minisat+) R 9541 22929 22928 0 -1 0 9919 0 0 0 120007 35 0 0 25 0 1 0 548432572 42639360 9893 4294967295 134512640 134672761 3221224624 3221223760 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10410 9893 603 41 0 10369 0
vsize: 41640
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.32 s]
Raw data (loadavg): 1.00 1.00 0.94 1/55 9607
Raw data (stat): 9542 (minisat+) Z 9541 22929 22928 0 -1 12 9922 0 0 0 120007 37 0 0 25 0 1 0 548432572 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.32
CPU time (s): 1200.46
CPU user time (s): 1200.08
CPU system time (s): 0.378942
CPU usage (%): 100.012
Max. virtual memory (Kb): 41640
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####