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/submitted/manquinho/primes-dimacs-cnf/normalized-ii32b1.opb
MD5SUM	c4653389ddee2820797c664a0856c651
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	191
Optimality of the best value was proved	NO
Number of terms in the objective function	456
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	456
Number of bits of the sum of numbers in the objective function	9
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	456
Number of bits of the biggest sum of numbers	9
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.02784
Number of variables	456
Total number of constraints	1602
Number of constraints which are clauses	1602
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	2
Maximum length of a constraint	32
Trace number 4691

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.077
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:        913044 kB
Buffers:         33844 kB
Cached:          52036 kB
SwapCached:          4 kB
Active:          46904 kB
Inactive:        41848 kB
HighTotal:      131008 kB
HighFree:        75348 kB
LowTotal:       903652 kB
LowFree:        837696 kB
SwapTotal:     2097640 kB
SwapFree:      2097636 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            27300 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 20:12:37 (client local time) WITH STATUS 10 IN 1200.18 SECONDS
stats: 3531 7 1200.18 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1602 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ..................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    1602     6636 |     534       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 216[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 904   maxlim: 240   bits: 9/8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        34 |    7887    29066 |    2629      34     1715    50.4 |  0.000 % |
c ==============================================================================
c [1mFound solution: 211[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 245   bits: 9/8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        57 |    7891    29089 |    2630      57     2218    38.9 |  0.000 % |
c |       157 |    7891    29089 |    2893     157     4908    31.3 |  0.512 % |
c |       308 |    7891    29089 |    3182     308    10485    34.0 |  0.512 % |
c |       534 |    7891    29089 |    3500     534    16813    31.5 |  0.512 % |
c ==============================================================================
c [1mFound solution: 210[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 246   bits: 9/8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       838 |    7894    29105 |    2631     838    27549    32.9 |  0.512 % |
c |       938 |    7894    29105 |    2894     938    30191    32.2 |  0.585 % |
c |      1088 |    7894    29105 |    3183    1088    37031    34.0 |  0.585 % |
c |      1314 |    7894    29105 |    3501    1314    44937    34.2 |  0.585 % |
c |      1651 |    7894    29105 |    3852    1651    52953    32.1 |  0.585 % |
c |      2158 |    7894    29105 |    4237    2158    80653    37.4 |  0.585 % |
c |      2917 |    7894    29105 |    4660    2917   115607    39.6 |  0.586 % |
c |      4059 |    7894    29105 |    5127    4059   155689    38.4 |  0.585 % |
c |      5768 |    7894    29105 |    5639    5768   284732    49.4 |  0.585 % |
c ==============================================================================
c [1mFound solution: 209[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 247   bits: 9/8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7301 |    7895    29112 |    2631    4417   241876    54.8 |  0.585 % |
c |      7401 |    7895    29112 |    2894    2309   104788    45.4 |  0.658 % |
c |      7552 |    7895    29112 |    3183    2460   111183    45.2 |  0.657 % |
c |      7778 |    7895    29112 |    3501    2686   119080    44.3 |  0.657 % |
c |      8115 |    7895    29112 |    3852    3023   150369    49.7 |  0.658 % |
c |      8622 |    7895    29112 |    4237    3530   164061    46.5 |  0.657 % |
c |      9382 |    7895    29112 |    4660    4290   205319    47.9 |  0.657 % |
c |     10521 |    7895    29112 |    5127    5429   283149    52.2 |  0.657 % |
c |     12229 |    7895    29112 |    5639    4423   203916    46.1 |  0.657 % |
c ==============================================================================
c [1mFound solution: 206[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 250   bits: 9/8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12521 |    7901    29147 |    2633    4715   212239    45.0 |  0.657 % |
c |     12624 |    7901    29147 |    2896    2461    73336    29.8 |  0.802 % |
c |     12774 |    7901    29147 |    3185    2611    76660    29.4 |  0.802 % |
c |     13001 |    7901    29147 |    3504    2838    81260    28.6 |  0.802 % |
c |     13339 |    7901    29147 |    3854    3176   106953    33.7 |  0.802 % |
c |     13847 |    7901    29147 |    4240    3684   123249    33.5 |  0.802 % |
c ==============================================================================
c [1mFound solution: 203[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 253   bits: 9/8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14445 |    7903    29164 |    2634    4282   142292    33.2 |  0.802 % |
c |     14545 |    7903    29164 |    2897    2241    53123    23.7 |  0.947 % |
c |     14695 |    7903    29164 |    3187    2391    55530    23.2 |  0.947 % |
c |     14920 |    7903    29164 |    3505    2616    71186    27.2 |  0.947 % |
c |     15257 |    7903    29164 |    3856    2953    84761    28.7 |  0.947 % |
c |     15765 |    7903    29164 |    4242    3461   100972    29.2 |  0.947 % |
c |     16525 |    7903    29164 |    4666    4221   123162    29.2 |  0.947 % |
c |     17665 |    7903    29164 |    5132    5361   224957    42.0 |  0.947 % |
c |     19375 |    7903    29164 |    5646    4391   220292    50.2 |  0.947 % |
c |     21938 |    7903    29164 |    6210    3642   159283    43.7 |  0.947 % |
c |     25783 |    7903    29164 |    6831    3950   255873    64.8 |  0.947 % |
c |     31549 |    7903    29164 |    7515    6171   397018    64.3 |  0.947 % |
c ==============================================================================
c [1mFound solution: 202[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 254   bits: 9/8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     36449 |    7905    29176 |    2635    6973   545034    78.2 |  0.947 % |
c |     36551 |    7905    29176 |    2898    1846    47944    26.0 |  1.018 % |
c |     36702 |    7905    29176 |    3188    1997    60587    30.3 |  1.018 % |
c |     36928 |    7905    29176 |    3507    2223    70629    31.8 |  1.018 % |
c |     37266 |    7905    29176 |    3857    2561    80347    31.4 |  1.018 % |
c |     37773 |    7905    29176 |    4243    3068    92850    30.3 |  1.018 % |
c |     38532 |    7905    29176 |    4668    3827   120956    31.6 |  1.018 % |
c |     39672 |    7905    29176 |    5134    4967   175493    35.3 |  1.018 % |
c |     41380 |    7905    29176 |    5648    3996   102254    25.6 |  1.018 % |
c ==============================================================================
c [1mFound solution: 201[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 255   bits: 9/8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     42382 |    7891    29069 |    2630    4998   147323    29.5 |  1.018 % |
c |     42482 |    7891    29069 |    2893    2599    65595    25.2 |  1.092 % |
c |     42632 |    7891    29069 |    3182    2749    69683    25.3 |  1.091 % |
c |     42857 |    7891    29069 |    3500    2974    81019    27.2 |  1.091 % |
c ==============================================================================
c [1mFound solution: 200[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 256   bits: 9/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     43085 |    7893    29080 |    2631    3202    84530    26.4 |  1.091 % |
c |     43185 |    7893    29080 |    2894    1701    33108    19.5 |  1.162 % |
c |     43336 |    7893    29080 |    3183    1852    37826    20.4 |  1.162 % |
c |     43563 |    7893    29080 |    3501    2079    43376    20.9 |  1.162 % |
c |     43900 |    7893    29080 |    3852    2416    51530    21.3 |  1.162 % |
c |     44406 |    7893    29080 |    4237    2922    81572    27.9 |  1.162 % |
c |     45165 |    7893    29080 |    4660    3681   129536    35.2 |  1.162 % |
c |     46306 |    7893    29080 |    5127    4822   181396    37.6 |  1.162 % |
c |     48014 |    7893    29080 |    5639    3907   136119    34.8 |  1.162 % |
c |     50576 |    7893    29080 |    6203    6469   286654    44.3 |  1.162 % |
c |     54421 |    7893    29080 |    6824    3871   111029    28.7 |  1.162 % |
c |     60188 |    7893    29080 |    7506    5702   337976    59.3 |  1.162 % |
c ==============================================================================
c [1mFound solution: 199[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 257   bits: 9/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     62136 |    7894    29088 |    2631    7650   399361    52.2 |  1.162 % |
c |     62236 |    7894    29088 |    2894    2013    43617    21.7 |  1.234 % |
c |     62386 |    7894    29088 |    3183    2163    50459    23.3 |  1.234 % |
c |     62611 |    7894    29088 |    3501    2388    58208    24.4 |  1.234 % |
c |     62948 |    7894    29088 |    3852    2725    68563    25.2 |  1.234 % |
c |     63455 |    7894    29088 |    4237    3232    83895    26.0 |  1.234 % |
c |     64214 |    7894    29088 |    4660    3991   116676    29.2 |  1.234 % |
c |     65354 |    7894    29088 |    5127    2764    63537    23.0 |  1.234 % |
c |     67063 |    7894    29088 |    5639    4473   148280    33.2 |  1.234 % |
c |     69625 |    7894    29088 |    6203    3792   176284    46.5 |  1.234 % |
c |     73469 |    7894    29088 |    6824    4061   271265    66.8 |  1.235 % |
c |     79235 |    7894    29088 |    7506    6284   333219    53.0 |  1.234 % |
c |     87884 |    7894    29088 |    8257    6428   603190    93.8 |  1.234 % |
c |    100858 |    7894    29088 |    9082    5501   329468    59.9 |  1.234 % |
c |    120320 |    7894    29088 |    9991    5231   446832    85.4 |  1.238 % |
c ==============================================================================
c [1mFound solution: 198[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 258   bits: 9/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    123419 |    7896    29099 |    2632    8330   632463    75.9 |  1.238 % |
c |    123523 |    7896    29099 |    2895    2187    82114    37.5 |  1.306 % |
c |    123673 |    7896    29099 |    3184    2337    91404    39.1 |  1.304 % |
c |    123900 |    7896    29099 |    3503    2564    94729    36.9 |  1.304 % |
c |    124239 |    7896    29099 |    3853    2903   104361    35.9 |  1.304 % |
c |    124746 |    7896    29099 |    4238    3410   128302    37.6 |  1.304 % |
c |    125506 |    7896    29099 |    4662    4170   153212    36.7 |  1.304 % |
c |    126645 |    7896    29099 |    5129    2658    74948    28.2 |  1.304 % |
c |    128354 |    7896    29099 |    5641    4367   157846    36.1 |  1.304 % |
c |    130916 |    7896    29099 |    6206    3615   174544    48.3 |  1.304 % |
c |    134760 |    7896    29099 |    6826    3894   158216    40.6 |  1.304 % |
c |    140526 |    7896    29099 |    7509    5747   340107    59.2 |  1.305 % |
c |    149176 |    7896    29099 |    8260    6799   334271    49.2 |  1.304 % |
c |    162150 |    7896    29099 |    9086    6901   345195    50.0 |  1.304 % |
c |    181611 |    7896    29099 |    9995    6669   491937    73.8 |  1.304 % |
c |    210803 |    7896    29099 |   10994    9277  1011754   109.1 |  1.304 % |
c ==============================================================================
c [1mFound solution: 197[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 259   bits: 9/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    230871 |    7897    29106 |    2632   11899   784127    65.9 |  1.304 % |
c |    230971 |    7897    29106 |    2895    1588    41091    25.9 |  1.376 % |
c |    231122 |    7897    29106 |    3184    1739    49379    28.4 |  1.376 % |
c |    231347 |    7897    29106 |    3503    1964    53794    27.4 |  1.377 % |
c |    231684 |    7897    29106 |    3853    2301    69601    30.2 |  1.376 % |
c |    232192 |    7897    29106 |    4238    2809    82326    29.3 |  1.376 % |
c |    232951 |    7897    29106 |    4662    3568   130214    36.5 |  1.376 % |
c |    234092 |    7897    29106 |    5129    4709   217857    46.3 |  1.376 % |
c |    235801 |    7897    29106 |    5641    3672   162981    44.4 |  1.376 % |
c |    238364 |    7897    29106 |    6206    6235   292464    46.9 |  1.376 % |
c |    242208 |    7897    29106 |    6826    3664   161245    44.0 |  1.376 % |
c ==============================================================================
c [1mFound solution: 196[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 260   bits: 9/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    247721 |    7898    29115 |    2632    5662   221196    39.1 |  1.376 % |
c |    247824 |    7898    29115 |    2895    1519    26983    17.8 |  1.447 % |
c |    247974 |    7898    29115 |    3184    1669    36816    22.1 |  1.447 % |
c |    248200 |    7898    29115 |    3503    1895    43698    23.1 |  1.447 % |
c |    248539 |    7898    29115 |    3853    2234    58589    26.2 |  1.447 % |
c |    249045 |    7898    29115 |    4238    2740    74917    27.3 |  1.447 % |
c |    249804 |    7898    29115 |    4662    3499   113552    32.5 |  1.447 % |
c |    250946 |    7898    29115 |    5129    4641   172429    37.2 |  1.447 % |
c |    252654 |    7898    29115 |    5641    3691   144227    39.1 |  1.447 % |
c |    255216 |    7898    29115 |    6206    6253   283942    45.4 |  1.447 % |
c |    259062 |    7898    29115 |    6826    6973   389090    55.8 |  1.447 % |
c |    264828 |    7898    29115 |    7509    5351   408611    76.4 |  1.447 % |
c |    273478 |    7898    29115 |    8260    5547   299334    54.0 |  1.447 % |
c |    286452 |    7898    29115 |    9086    5683   321289    56.5 |  1.447 % |
c |    305914 |    7898    29115 |    9995    5244   311857    59.5 |  1.447 % |
c |    335106 |    7898    29115 |   10994    7345   484438    66.0 |  1.447 % |
c |    378895 |    7898    29115 |   12093    5999   252168    42.0 |  1.447 % |
c |    444581 |    7898    29115 |   13303    7575   494777    65.3 |  1.447 % |
c |    543107 |    7898    29115 |   14633    7813   437799    56.0 |  1.447 % |
c ==============================================================================
c [1mFound solution: 195[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 261   bits: 9/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    679214 |    7900    29125 |    2633   14226  1259329    88.5 |  1.447 % |
c |    679314 |    7900    29125 |    2896    1879    43408    23.1 |  1.517 % |
c |    679465 |    7900    29125 |    3185    2030    54355    26.8 |  1.517 % |
c |    679692 |    7900    29125 |    3504    2257    60222    26.7 |  1.517 % |
c |    680029 |    7900    29125 |    3854    2594    84387    32.5 |  1.517 % |
c |    680536 |    7900    29125 |    4240    3101   100524    32.4 |  1.517 % |
c |    681296 |    7900    29125 |    4664    3861   143396    37.1 |  1.517 % |
c |    682435 |    7900    29125 |    5130    2550    75835    29.7 |  1.517 % |
c |    684143 |    7900    29125 |    5644    4258   157397    37.0 |  1.517 % |
c |    686708 |    7900    29125 |    6208    3656   128209    35.1 |  1.517 % |
c |    690552 |    7900    29125 |    6829    4058   232649    57.3 |  1.517 % |
c |    696319 |    7900    29125 |    7512    5998   306001    51.0 |  1.517 % |
c |    704968 |    7900    29125 |    8263    6601   500832    75.9 |  1.517 % |
c |    717943 |    7900    29125 |    9089    5892   477865    81.1 |  1.517 % |
c |    737404 |    7900    29125 |    9998    5352   428924    80.1 |  1.517 % |
c |    766596 |    7900    29125 |   10998    8045   575790    71.6 |  1.517 % |
c |    810385 |    7900    29125 |   12098   10474  1212819   115.8 |  1.517 % |
c |    876069 |    7900    29125 |   13308   12158  1197201    98.5 |  1.517 % |
c |    974596 |    7900    29125 |   14639    7175   343590    47.9 |  1.517 % |
c ==============================================================================
c [1mFound solution: 194[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 262   bits: 9/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |   1102559 |    7902    29135 |    2634   12983   792532    61.0 |  1.517 % |
c |   1102659 |    7902    29135 |    2897    1723    15247     8.8 |  1.587 % |
c |   1102810 |    7902    29135 |    3187    1874    20443    10.9 |  1.587 % |
c |   1103035 |    7902    29135 |    3505    2099    25048    11.9 |  1.587 % |
c |   1103372 |    7902    29135 |    3856    2436    36989    15.2 |  1.587 % |
c |   1103878 |    7902    29135 |    4242    2942    60599    20.6 |  1.587 % |
c |   1104637 |    7902    29135 |    4666    3701    92309    24.9 |  1.587 % |
c |   1105777 |    7902    29135 |    5132    4841   165925    34.3 |  1.587 % |
c |   1107485 |    7902    29135 |    5646    3857   167199    43.3 |  1.587 % |
c |   1110048 |    7902    29135 |    6210    6420   284670    44.3 |  1.587 % |
c |   1113896 |    7902    29135 |    6831    3841    91959    23.9 |  1.587 % |
c |   1119666 |    7902    29135 |    7515    5740   289140    50.4 |  1.587 % |
c |   1128317 |    7902    29135 |    8266    6369   443739    69.7 |  1.587 % |
c |   1141291 |    7902    29135 |    9093    6014   378583    63.0 |  1.587 % |
c |   1160752 |    7902    29135 |   10002    5585   283110    50.7 |  1.587 % |
c |   1189945 |    7902    29135 |   11002    8979   365521    40.7 |  1.587 % |
c ==============================================================================
c [1mFound solution: 193[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 263   bits: 9/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |   1230545 |    7903    29141 |    2634    8081   572421    70.8 |  1.587 % |
c |   1230645 |    7903    29141 |    2897    2121    61597    29.0 |  1.658 % |
c |   1230795 |    7903    29141 |    3187    2271    66626    29.3 |  1.658 % |
c |   1231020 |    7903    29141 |    3505    2496    76486    30.6 |  1.658 % |
c |   1231359 |    7903    29141 |    3856    2835    93463    33.0 |  1.658 % |
c |   1231866 |    7903    29141 |    4242    3342   110100    32.9 |  1.658 % |
c |   1232625 |    7903    29141 |    4666    4101   160328    39.1 |  1.658 % |
c |   1233764 |    7903    29141 |    5132    5240   244557    46.7 |  1.658 % |
c |   1235472 |    7903    29141 |    5646    4328   198039    45.8 |  1.658 % |
c |   1238034 |    7903    29141 |    6210    3915   148196    37.9 |  1.658 % |
c |   1241878 |    7903    29141 |    6831    4249   260359    61.3 |  1.659 % |
c |   1247645 |    7903    29141 |    7515    6072   535109    88.1 |  1.658 % |
c |   1256294 |    7903    29141 |    8266    6884   371821    54.0 |  1.658 % |
c |   1269268 |    7903    29141 |    9093    6081   342079    56.3 |  1.658 % |
c |   1288729 |    7903    29141 |   10002    5853   397468    67.9 |  1.658 % |
c |   1317924 |    7903    29141 |   11002    8339   631802    75.8 |  1.658 % |
c |   1361713 |    7903    29141 |   12103   11452   805962    70.4 |  1.658 % |
c |   1427397 |    7903    29141 |   13313    7431   486621    65.5 |  1.658 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.92 0.95 0.82 2/54 12083
Raw data (stat): 12083 (runsolver) R 12082 10614 10613 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 478621313 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 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.0007 s]
Raw data (loadavg): 0.93 0.96 0.82 2/54 12083
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 897 0 0 0 996 2 0 0 25 0 1 0 478621313 5136384 875 4294967295 134512640 134672761 3221224576 3221223704 1075347105 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1254 875 603 41 0 1213 0
vsize: 5016
[startup+20.001 s]
Raw data (loadavg): 0.94 0.96 0.82 2/54 12083
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 1187 0 0 0 1995 2 0 0 25 0 1 0 478621313 6348800 1165 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1550 1165 603 41 0 1509 0
vsize: 6200
[startup+30.0014 s]
Raw data (loadavg): 0.95 0.96 0.83 2/54 12083
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 1187 0 0 0 2995 2 0 0 25 0 1 0 478621313 6348800 1165 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1550 1165 603 41 0 1509 0
vsize: 6200
[startup+40.0024 s]
Raw data (loadavg): 0.96 0.96 0.83 2/54 12083
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 1187 0 0 0 3995 2 0 0 25 0 1 0 478621313 6348800 1165 4294967295 134512640 134672761 3221224576 3221223668 1075351210 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1550 1165 603 41 0 1509 0
vsize: 6200
[startup+50.0031 s]
Raw data (loadavg): 0.96 0.96 0.83 2/54 12083
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 1494 0 0 0 4995 3 0 0 25 0 1 0 478621313 7680000 1472 4294967295 134512640 134672761 3221224576 3221223744 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1875 1472 603 41 0 1834 0
vsize: 7500
[startup+60.0025 s]
Raw data (loadavg): 0.97 0.96 0.83 2/54 12083
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 1495 0 0 0 5995 3 0 0 25 0 1 0 478621313 7680000 1473 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1875 1473 603 41 0 1834 0
vsize: 7500
[startup+70.0034 s]
Raw data (loadavg): 0.97 0.96 0.83 2/54 12083
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 1604 0 0 0 6995 3 0 0 25 0 1 0 478621313 8085504 1582 4294967295 134512640 134672761 3221224576 3221223728 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1974 1582 603 41 0 1933 0
vsize: 7896
[startup+80.0041 s]
Raw data (loadavg): 0.98 0.96 0.83 2/54 12083
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 1658 0 0 0 7995 3 0 0 25 0 1 0 478621313 8351744 1636 4294967295 134512640 134672761 3221224576 3221223680 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2039 1636 603 41 0 1998 0
vsize: 8156
[startup+90.0045 s]
Raw data (loadavg): 0.98 0.96 0.83 2/54 12083
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 1658 0 0 0 8995 3 0 0 25 0 1 0 478621313 8351744 1636 4294967295 134512640 134672761 3221224576 3221223532 1075350060 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2039 1636 603 41 0 1998 0
vsize: 8156
[startup+100.004 s]
Raw data (loadavg): 0.98 0.96 0.83 2/54 12083
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 1658 0 0 0 9995 3 0 0 25 0 1 0 478621313 8351744 1636 4294967295 134512640 134672761 3221224576 3221223680 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2039 1636 603 41 0 1998 0
vsize: 8156
[startup+110.004 s]
Raw data (loadavg): 0.98 0.97 0.83 2/54 12083
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 1715 0 0 0 10995 4 0 0 25 0 1 0 478621313 8622080 1693 4294967295 134512640 134672761 3221224576 3221223680 134560335 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2105 1693 603 41 0 2064 0
vsize: 8420
[startup+120.005 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 12083
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 1904 0 0 0 11995 4 0 0 25 0 1 0 478621313 9285632 1882 4294967295 134512640 134672761 3221224576 3221223760 134559417 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2267 1882 603 41 0 2226 0
vsize: 9068
[startup+130.004 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 12083
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2081 0 0 0 12994 5 0 0 25 0 1 0 478621313 10084352 2059 4294967295 134512640 134672761 3221224576 3221223680 134555116 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2462 2059 603 41 0 2421 0
vsize: 9848
[startup+140.005 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 12083
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2111 0 0 0 13994 5 0 0 25 0 1 0 478621313 10215424 2089 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2494 2089 603 41 0 2453 0
vsize: 9976
[startup+150.006 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 12083
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2111 0 0 0 14994 5 0 0 25 0 1 0 478621313 10215424 2089 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2494 2089 603 41 0 2453 0
vsize: 9976
[startup+160.006 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 12083
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2111 0 0 0 15994 5 0 0 25 0 1 0 478621313 10190848 2089 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2488 2089 603 41 0 2447 0
vsize: 9952
[startup+170.006 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 12083
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2111 0 0 0 16994 5 0 0 25 0 1 0 478621313 10190848 2089 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2488 2089 603 41 0 2447 0
vsize: 9952
[startup+180.006 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 12083
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2111 0 0 0 17994 5 0 0 25 0 1 0 478621313 10190848 2089 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2488 2089 603 41 0 2447 0
vsize: 9952
[startup+190.007 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 12083
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2111 0 0 0 18995 5 0 0 25 0 1 0 478621313 10190848 2089 4294967295 134512640 134672761 3221224576 3221223680 134559929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2488 2089 603 41 0 2447 0
vsize: 9952
[startup+200.007 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 12083
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2111 0 0 0 19995 5 0 0 25 0 1 0 478621313 10190848 2089 4294967295 134512640 134672761 3221224576 3221223680 134560174 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2488 2089 603 41 0 2447 0
vsize: 9952
[startup+210.007 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 12083
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2111 0 0 0 20995 5 0 0 25 0 1 0 478621313 10190848 2089 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2488 2089 603 41 0 2447 0
vsize: 9952
[startup+220.008 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 12083
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2111 0 0 0 21995 5 0 0 25 0 1 0 478621313 10190848 2089 4294967295 134512640 134672761 3221224576 3221223744 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2488 2089 603 41 0 2447 0
vsize: 9952
[startup+230.007 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 12083
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2111 0 0 0 22995 5 0 0 25 0 1 0 478621313 10190848 2089 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2488 2089 603 41 0 2447 0
vsize: 9952
[startup+240.008 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 12083
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2111 0 0 0 23995 5 0 0 25 0 1 0 478621313 10190848 2089 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2488 2089 603 41 0 2447 0
vsize: 9952
[startup+250.008 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 12083
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2129 0 0 0 24995 6 0 0 25 0 1 0 478621313 10190848 2107 4294967295 134512640 134672761 3221224576 3221223760 134559622 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2488 2107 603 41 0 2447 0
vsize: 9952
[startup+260.007 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 12083
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2129 0 0 0 25996 6 0 0 25 0 1 0 478621313 10190848 2107 4294967295 134512640 134672761 3221224576 3221223680 134560243 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2488 2107 603 41 0 2447 0
vsize: 9952
[startup+270.008 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 12083
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2153 0 0 0 26996 6 0 0 25 0 1 0 478621313 10321920 2131 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2520 2131 603 41 0 2479 0
vsize: 10080
[startup+280.008 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 12083
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2153 0 0 0 27996 6 0 0 25 0 1 0 478621313 10321920 2131 4294967295 134512640 134672761 3221224576 3221223744 134560900 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2520 2131 603 41 0 2479 0
vsize: 10080
[startup+290.008 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 12083
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2160 0 0 0 28996 6 0 0 25 0 1 0 478621313 10321920 2138 4294967295 134512640 134672761 3221224576 3221223680 134560212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2520 2138 603 41 0 2479 0
vsize: 10080
[startup+300.008 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 12083
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2165 0 0 0 29996 6 0 0 25 0 1 0 478621313 10452992 2143 4294967295 134512640 134672761 3221224576 3221223744 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2552 2143 603 41 0 2511 0
vsize: 10208
[startup+310.008 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 12083
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2166 0 0 0 30996 6 0 0 25 0 1 0 478621313 10452992 2144 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2552 2144 603 41 0 2511 0
vsize: 10208
[startup+320.008 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 12083
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2166 0 0 0 31997 6 0 0 25 0 1 0 478621313 10452992 2144 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2552 2144 603 41 0 2511 0
vsize: 10208
[startup+330.009 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 12083
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2166 0 0 0 32997 6 0 0 25 0 1 0 478621313 10452992 2144 4294967295 134512640 134672761 3221224576 3221223680 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2552 2144 603 41 0 2511 0
vsize: 10208
[startup+340.01 s]
Raw data (loadavg): 0.99 0.97 0.86 2/54 12083
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2175 0 0 0 33997 6 0 0 25 0 1 0 478621313 10452992 2153 4294967295 134512640 134672761 3221224576 3221223776 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2552 2153 603 41 0 2511 0
vsize: 10208
[startup+350.009 s]
Raw data (loadavg): 0.99 0.97 0.86 2/54 12083
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2268 0 0 0 34997 6 0 0 25 0 1 0 478621313 10858496 2246 4294967295 134512640 134672761 3221224576 3221223744 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2651 2246 603 41 0 2610 0
vsize: 10604
[startup+360.009 s]
Raw data (loadavg): 0.99 0.97 0.86 2/54 12083
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2268 0 0 0 35997 6 0 0 25 0 1 0 478621313 10858496 2246 4294967295 134512640 134672761 3221224576 3221223680 134559979 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2651 2246 603 41 0 2610 0
vsize: 10604
[startup+370.01 s]
Raw data (loadavg): 0.99 0.97 0.86 2/54 12083
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2268 0 0 0 36997 6 0 0 25 0 1 0 478621313 10858496 2246 4294967295 134512640 134672761 3221224576 3221223744 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2651 2246 603 41 0 2610 0
vsize: 10604
[startup+380.009 s]
Raw data (loadavg): 0.99 0.97 0.86 2/54 12083
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2336 0 0 0 37997 7 0 0 25 0 1 0 478621313 11124736 2314 4294967295 134512640 134672761 3221224576 3221223680 134560510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2716 2314 603 41 0 2675 0
vsize: 10864
[startup+390.009 s]
Raw data (loadavg): 0.99 0.97 0.86 2/54 12083
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2336 0 0 0 38997 7 0 0 25 0 1 0 478621313 11124736 2314 4294967295 134512640 134672761 3221224576 3221223680 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2716 2314 603 41 0 2675 0
vsize: 10864
[startup+400.009 s]
Raw data (loadavg): 0.99 0.97 0.86 2/54 12083
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2337 0 0 0 39997 7 0 0 25 0 1 0 478621313 11124736 2315 4294967295 134512640 134672761 3221224576 3221223740 134560077 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2716 2315 603 41 0 2675 0
vsize: 10864
[startup+410.008 s]
Raw data (loadavg): 0.99 0.97 0.86 2/54 12083
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2461 0 0 0 40997 7 0 0 25 0 1 0 478621313 11644928 2439 4294967295 134512640 134672761 3221224576 3221223744 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2843 2439 603 41 0 2802 0
vsize: 11372
[startup+420.009 s]
Raw data (loadavg): 0.99 0.97 0.86 2/54 12083
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2553 0 0 0 41997 7 0 0 25 0 1 0 478621313 11907072 2531 4294967295 134512640 134672761 3221224576 3221223744 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2907 2531 603 41 0 2866 0
vsize: 11628
[startup+430.01 s]
Raw data (loadavg): 0.99 0.97 0.86 2/54 12083
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2553 0 0 0 42997 7 0 0 25 0 1 0 478621313 11907072 2531 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2907 2531 603 41 0 2866 0
vsize: 11628
[startup+440.01 s]
Raw data (loadavg): 0.99 0.97 0.87 2/54 12083
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2553 0 0 0 43997 7 0 0 25 0 1 0 478621313 11907072 2531 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2907 2531 603 41 0 2866 0
vsize: 11628
[startup+450.01 s]
Raw data (loadavg): 0.99 0.97 0.87 4/57 12104
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2553 0 0 0 44997 7 0 0 25 0 1 0 478621313 11907072 2531 4294967295 134512640 134672761 3221224576 3221223744 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2907 2531 603 41 0 2866 0
vsize: 11628
[startup+460.01 s]
Raw data (loadavg): 1.07 0.99 0.87 2/54 12136
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2741 0 0 0 45997 8 0 0 25 0 1 0 478621313 12705792 2719 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3102 2719 603 41 0 3061 0
vsize: 12408
[startup+470.011 s]
Raw data (loadavg): 1.06 0.99 0.87 2/54 12136
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2785 0 0 0 46997 8 0 0 25 0 1 0 478621313 12976128 2763 4294967295 134512640 134672761 3221224576 3221223680 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3168 2763 603 41 0 3127 0
vsize: 12672
[startup+480.011 s]
Raw data (loadavg): 1.05 0.99 0.87 2/54 12136
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2791 0 0 0 47997 8 0 0 25 0 1 0 478621313 12976128 2769 4294967295 134512640 134672761 3221224576 3221223744 134560994 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3168 2769 603 41 0 3127 0
vsize: 12672
[startup+490.01 s]
Raw data (loadavg): 1.04 0.99 0.88 2/54 12136
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2791 0 0 0 48997 8 0 0 25 0 1 0 478621313 12976128 2769 4294967295 134512640 134672761 3221224576 3221223680 134560344 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3168 2769 603 41 0 3127 0
vsize: 12672
[startup+500.011 s]
Raw data (loadavg): 1.03 0.99 0.88 2/54 12136
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2791 0 0 0 49997 8 0 0 25 0 1 0 478621313 12976128 2769 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3168 2769 603 41 0 3127 0
vsize: 12672
[startup+510.01 s]
Raw data (loadavg): 1.03 0.99 0.88 2/54 12136
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2854 0 0 0 50997 9 0 0 25 0 1 0 478621313 13254656 2832 4294967295 134512640 134672761 3221224576 3221223680 134560355 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3236 2832 603 41 0 3195 0
vsize: 12944
[startup+520.011 s]
Raw data (loadavg): 1.02 0.99 0.88 2/54 12138
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2854 0 0 0 51997 9 0 0 25 0 1 0 478621313 13254656 2832 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3236 2832 603 41 0 3195 0
vsize: 12944
[startup+530.011 s]
Raw data (loadavg): 1.02 0.99 0.88 2/54 12138
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2854 0 0 0 52997 9 0 0 25 0 1 0 478621313 13254656 2832 4294967295 134512640 134672761 3221224576 3221223680 134560248 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3236 2832 603 41 0 3195 0
vsize: 12944
[startup+540.011 s]
Raw data (loadavg): 1.02 0.99 0.88 2/54 12138
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2875 0 0 0 53997 9 0 0 25 0 1 0 478621313 13254656 2853 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3236 2853 603 41 0 3195 0
vsize: 12944
[startup+550.011 s]
Raw data (loadavg): 1.01 0.99 0.88 2/54 12138
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2875 0 0 0 54997 9 0 0 25 0 1 0 478621313 13254656 2853 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3236 2853 603 41 0 3195 0
vsize: 12944
[startup+560.011 s]
Raw data (loadavg): 1.01 0.99 0.88 2/54 12138
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2875 0 0 0 55997 9 0 0 25 0 1 0 478621313 13254656 2853 4294967295 134512640 134672761 3221224576 3221223744 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3236 2853 603 41 0 3195 0
vsize: 12944
[startup+570.011 s]
Raw data (loadavg): 1.01 0.99 0.88 2/54 12138
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2875 0 0 0 56998 9 0 0 25 0 1 0 478621313 13254656 2853 4294967295 134512640 134672761 3221224576 3221223760 134559388 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3236 2853 603 41 0 3195 0
vsize: 12944
[startup+580.011 s]
Raw data (loadavg): 1.01 0.99 0.88 2/54 12138
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2875 0 0 0 57998 9 0 0 25 0 1 0 478621313 13254656 2853 4294967295 134512640 134672761 3221224576 3221223744 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3236 2853 603 41 0 3195 0
vsize: 12944
[startup+590.011 s]
Raw data (loadavg): 1.00 0.99 0.89 2/54 12138
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2875 0 0 0 58998 9 0 0 25 0 1 0 478621313 13254656 2853 4294967295 134512640 134672761 3221224576 3221223712 134560697 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3236 2853 603 41 0 3195 0
vsize: 12944
[startup+600.012 s]
Raw data (loadavg): 1.00 0.99 0.89 2/54 12138
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2875 0 0 0 59998 9 0 0 25 0 1 0 478621313 13254656 2853 4294967295 134512640 134672761 3221224576 3221223712 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3236 2853 603 41 0 3195 0
vsize: 12944
[startup+610.011 s]
Raw data (loadavg): 1.00 0.99 0.89 2/54 12138
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2875 0 0 0 60998 9 0 0 25 0 1 0 478621313 13254656 2853 4294967295 134512640 134672761 3221224576 3221223760 134558831 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3236 2853 603 41 0 3195 0
vsize: 12944
[startup+620.011 s]
Raw data (loadavg): 1.00 0.99 0.89 2/54 12138
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2875 0 0 0 61998 9 0 0 25 0 1 0 478621313 13254656 2853 4294967295 134512640 134672761 3221224576 3221223680 134559877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3236 2853 603 41 0 3195 0
vsize: 12944
[startup+630.011 s]
Raw data (loadavg): 1.00 0.99 0.89 2/54 12138
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2875 0 0 0 62999 9 0 0 25 0 1 0 478621313 13254656 2853 4294967295 134512640 134672761 3221224576 3221223680 134560212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3236 2853 603 41 0 3195 0
vsize: 12944
[startup+640.011 s]
Raw data (loadavg): 1.00 0.99 0.89 2/54 12138
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2875 0 0 0 63999 9 0 0 25 0 1 0 478621313 13254656 2853 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3236 2853 603 41 0 3195 0
vsize: 12944
[startup+650.011 s]
Raw data (loadavg): 1.00 0.99 0.89 2/54 12138
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2875 0 0 0 64999 9 0 0 25 0 1 0 478621313 13254656 2853 4294967295 134512640 134672761 3221224576 3221223744 134561121 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3236 2853 603 41 0 3195 0
vsize: 12944
[startup+660.011 s]
Raw data (loadavg): 1.00 0.99 0.89 2/54 12138
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2875 0 0 0 65999 9 0 0 25 0 1 0 478621313 13254656 2853 4294967295 134512640 134672761 3221224576 3221223744 134560900 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3236 2853 603 41 0 3195 0
vsize: 12944
[startup+670.011 s]
Raw data (loadavg): 1.00 0.99 0.89 2/54 12138
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2875 0 0 0 66999 9 0 0 25 0 1 0 478621313 13254656 2853 4294967295 134512640 134672761 3221224576 3221223764 1075346941 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3236 2853 603 41 0 3195 0
vsize: 12944
[startup+680.011 s]
Raw data (loadavg): 1.00 0.99 0.89 2/54 12138
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2875 0 0 0 67999 9 0 0 25 0 1 0 478621313 13254656 2853 4294967295 134512640 134672761 3221224576 3221223680 134554636 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3236 2853 603 41 0 3195 0
vsize: 12944
[startup+690.01 s]
Raw data (loadavg): 1.00 0.99 0.90 2/54 12138
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2875 0 0 0 68999 9 0 0 25 0 1 0 478621313 13254656 2853 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3236 2853 603 41 0 3195 0
vsize: 12944
[startup+700.011 s]
Raw data (loadavg): 1.00 0.99 0.90 2/54 12138
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2875 0 0 0 70000 9 0 0 25 0 1 0 478621313 13254656 2853 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3236 2853 603 41 0 3195 0
vsize: 12944
[startup+710.011 s]
Raw data (loadavg): 1.00 0.99 0.90 2/54 12138
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2875 0 0 0 71000 9 0 0 25 0 1 0 478621313 13254656 2853 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3236 2853 603 41 0 3195 0
vsize: 12944
[startup+720.012 s]
Raw data (loadavg): 1.00 0.99 0.90 2/54 12138
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2875 0 0 0 72000 9 0 0 25 0 1 0 478621313 13254656 2853 4294967295 134512640 134672761 3221224576 3221223744 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3236 2853 603 41 0 3195 0
vsize: 12944
[startup+730.012 s]
Raw data (loadavg): 1.00 0.99 0.90 2/54 12138
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2875 0 0 0 73000 9 0 0 25 0 1 0 478621313 13254656 2853 4294967295 134512640 134672761 3221224576 3221223744 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3236 2853 603 41 0 3195 0
vsize: 12944
[startup+740.012 s]
Raw data (loadavg): 1.00 0.99 0.90 2/54 12138
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2875 0 0 0 74000 9 0 0 25 0 1 0 478621313 13254656 2853 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3236 2853 603 41 0 3195 0
vsize: 12944
[startup+750.012 s]
Raw data (loadavg): 1.00 0.99 0.90 2/54 12138
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2875 0 0 0 75001 9 0 0 25 0 1 0 478621313 13254656 2853 4294967295 134512640 134672761 3221224576 3221223680 134560410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3236 2853 603 41 0 3195 0
vsize: 12944
[startup+760.011 s]
Raw data (loadavg): 1.00 0.99 0.90 2/54 12138
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2875 0 0 0 76001 9 0 0 25 0 1 0 478621313 13254656 2853 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3236 2853 603 41 0 3195 0
vsize: 12944
[startup+770.012 s]
Raw data (loadavg): 1.00 0.99 0.90 2/54 12140
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2875 0 0 0 77001 9 0 0 25 0 1 0 478621313 13254656 2853 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3236 2853 603 41 0 3195 0
vsize: 12944
[startup+780.012 s]
Raw data (loadavg): 1.00 0.99 0.90 2/54 12140
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2875 0 0 0 78001 9 0 0 25 0 1 0 478621313 13254656 2853 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3236 2853 603 41 0 3195 0
vsize: 12944
[startup+790.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12140
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2875 0 0 0 79001 9 0 0 25 0 1 0 478621313 13254656 2853 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3236 2853 603 41 0 3195 0
vsize: 12944
[startup+800.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12140
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2875 0 0 0 80001 10 0 0 25 0 1 0 478621313 13254656 2853 4294967295 134512640 134672761 3221224576 3221223760 134559038 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3236 2853 603 41 0 3195 0
vsize: 12944
[startup+810.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12140
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2875 0 0 0 81001 10 0 0 25 0 1 0 478621313 13254656 2853 4294967295 134512640 134672761 3221224576 3221223636 1075346603 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3236 2853 603 41 0 3195 0
vsize: 12944
[startup+820.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12140
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2875 0 0 0 82002 10 0 0 25 0 1 0 478621313 13254656 2853 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3236 2853 603 41 0 3195 0
vsize: 12944
[startup+830.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12140
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2875 0 0 0 83002 10 0 0 25 0 1 0 478621313 13254656 2853 4294967295 134512640 134672761 3221224576 3221223680 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3236 2853 603 41 0 3195 0
vsize: 12944
[startup+840.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12140
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2875 0 0 0 84002 10 0 0 25 0 1 0 478621313 13254656 2853 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3236 2853 603 41 0 3195 0
vsize: 12944
[startup+850.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12140
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2875 0 0 0 85002 10 0 0 25 0 1 0 478621313 13254656 2853 4294967295 134512640 134672761 3221224576 3221223752 134559668 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3236 2853 603 41 0 3195 0
vsize: 12944
[startup+860.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12140
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2875 0 0 0 86002 10 0 0 25 0 1 0 478621313 13254656 2853 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3236 2853 603 41 0 3195 0
vsize: 12944
[startup+870.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12140
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2875 0 0 0 87003 10 0 0 25 0 1 0 478621313 13254656 2853 4294967295 134512640 134672761 3221224576 3221223760 134559045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3236 2853 603 41 0 3195 0
vsize: 12944
[startup+880.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12140
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2875 0 0 0 88003 10 0 0 25 0 1 0 478621313 13254656 2853 4294967295 134512640 134672761 3221224576 3221223744 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3236 2853 603 41 0 3195 0
vsize: 12944
[startup+890.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12140
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2875 0 0 0 89003 10 0 0 25 0 1 0 478621313 13254656 2853 4294967295 134512640 134672761 3221224576 3221223744 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3236 2853 603 41 0 3195 0
vsize: 12944
[startup+900.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12140
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2875 0 0 0 90003 10 0 0 25 0 1 0 478621313 13254656 2853 4294967295 134512640 134672761 3221224576 3221223744 134561021 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3236 2853 603 41 0 3195 0
vsize: 12944
[startup+910.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12140
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2889 0 0 0 91003 10 0 0 25 0 1 0 478621313 13389824 2867 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3269 2867 603 41 0 3228 0
vsize: 13076
[startup+920.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12140
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2892 0 0 0 92003 10 0 0 25 0 1 0 478621313 13389824 2870 4294967295 134512640 134672761 3221224576 3221223760 134559376 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3269 2870 603 41 0 3228 0
vsize: 13076
[startup+930.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12140
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2892 0 0 0 93003 10 0 0 25 0 1 0 478621313 13389824 2870 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3269 2870 603 41 0 3228 0
vsize: 13076
[startup+940.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12140
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2892 0 0 0 94002 10 0 0 25 0 1 0 478621313 13389824 2870 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3269 2870 603 41 0 3228 0
vsize: 13076
[startup+950.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12140
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2892 0 0 0 95002 11 0 0 25 0 1 0 478621313 13389824 2870 4294967295 134512640 134672761 3221224576 3221223760 134558632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3269 2870 603 41 0 3228 0
vsize: 13076
[startup+960.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12140
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2892 0 0 0 96001 11 0 0 25 0 1 0 478621313 13389824 2870 4294967295 134512640 134672761 3221224576 3221223712 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3269 2870 603 41 0 3228 0
vsize: 13076
[startup+970.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12140
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2892 0 0 0 97001 11 0 0 25 0 1 0 478621313 13389824 2870 4294967295 134512640 134672761 3221224576 3221223728 134561244 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3269 2870 603 41 0 3228 0
vsize: 13076
[startup+980.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12140
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2892 0 0 0 98002 11 0 0 25 0 1 0 478621313 13389824 2870 4294967295 134512640 134672761 3221224576 3221223532 1075350544 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3269 2870 603 41 0 3228 0
vsize: 13076
[startup+990.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12140
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2892 0 0 0 99002 11 0 0 25 0 1 0 478621313 13389824 2870 4294967295 134512640 134672761 3221224576 3221223680 134560477 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3269 2870 603 41 0 3228 0
vsize: 13076
[startup+1000.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12140
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2892 0 0 0 100002 11 0 0 25 0 1 0 478621313 13389824 2870 4294967295 134512640 134672761 3221224576 3221223680 134560510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3269 2870 603 41 0 3228 0
vsize: 13076
[startup+1010.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12140
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2892 0 0 0 101002 11 0 0 25 0 1 0 478621313 13389824 2870 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3269 2870 603 41 0 3228 0
vsize: 13076
[startup+1020.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12140
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2892 0 0 0 102002 11 0 0 25 0 1 0 478621313 13389824 2870 4294967295 134512640 134672761 3221224576 3221223744 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3269 2870 603 41 0 3228 0
vsize: 13076
[startup+1030.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12140
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2892 0 0 0 103002 11 0 0 25 0 1 0 478621313 13389824 2870 4294967295 134512640 134672761 3221224576 3221223760 134559342 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3269 2870 603 41 0 3228 0
vsize: 13076
[startup+1040.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12140
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2892 0 0 0 104003 11 0 0 25 0 1 0 478621313 13389824 2870 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3269 2870 603 41 0 3228 0
vsize: 13076
[startup+1050.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12140
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2892 0 0 0 105003 11 0 0 25 0 1 0 478621313 13389824 2870 4294967295 134512640 134672761 3221224576 3221223760 134558648 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3269 2870 603 41 0 3228 0
vsize: 13076
[startup+1060.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12140
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2892 0 0 0 106003 11 0 0 25 0 1 0 478621313 13389824 2870 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3269 2870 603 41 0 3228 0
vsize: 13076
[startup+1070.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12140
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2892 0 0 0 107003 11 0 0 25 0 1 0 478621313 13389824 2870 4294967295 134512640 134672761 3221224576 3221223776 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3269 2870 603 41 0 3228 0
vsize: 13076
[startup+1080.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12140
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2892 0 0 0 108003 11 0 0 25 0 1 0 478621313 13389824 2870 4294967295 134512640 134672761 3221224576 3221223744 134561406 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3269 2870 603 41 0 3228 0
vsize: 13076
[startup+1090.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12140
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2892 0 0 0 109003 11 0 0 25 0 1 0 478621313 13389824 2870 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3269 2870 603 41 0 3228 0
vsize: 13076
[startup+1100.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12140
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2892 0 0 0 110003 11 0 0 25 0 1 0 478621313 13389824 2870 4294967295 134512640 134672761 3221224576 3221223776 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3269 2870 603 41 0 3228 0
vsize: 13076
[startup+1110.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12140
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2892 0 0 0 111004 11 0 0 25 0 1 0 478621313 13389824 2870 4294967295 134512640 134672761 3221224576 3221223680 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3269 2870 603 41 0 3228 0
vsize: 13076
[startup+1120.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12140
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2892 0 0 0 112004 11 0 0 25 0 1 0 478621313 13389824 2870 4294967295 134512640 134672761 3221224576 3221223744 134564451 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3269 2870 603 41 0 3228 0
vsize: 13076
[startup+1130.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12140
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2892 0 0 0 113004 11 0 0 25 0 1 0 478621313 13389824 2870 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3269 2870 603 41 0 3228 0
vsize: 13076
[startup+1140.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12140
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2892 0 0 0 114004 11 0 0 25 0 1 0 478621313 13389824 2870 4294967295 134512640 134672761 3221224576 3221223744 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3269 2870 603 41 0 3228 0
vsize: 13076
[startup+1150.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12140
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2892 0 0 0 115004 11 0 0 25 0 1 0 478621313 13389824 2870 4294967295 134512640 134672761 3221224576 3221223744 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3269 2870 603 41 0 3228 0
vsize: 13076
[startup+1160.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12140
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2892 0 0 0 116005 11 0 0 25 0 1 0 478621313 13389824 2870 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3269 2870 603 41 0 3228 0
vsize: 13076
[startup+1170.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12140
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2892 0 0 0 117005 11 0 0 25 0 1 0 478621313 13389824 2870 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3269 2870 603 41 0 3228 0
vsize: 13076
[startup+1180.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12140
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2892 0 0 0 118005 11 0 0 25 0 1 0 478621313 13389824 2870 4294967295 134512640 134672761 3221224576 3221223760 134559538 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3269 2870 603 41 0 3228 0
vsize: 13076
[startup+1190.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12140
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2892 0 0 0 119005 11 0 0 25 0 1 0 478621313 13389824 2870 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3269 2870 603 41 0 3228 0
vsize: 13076
[startup+1200.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 12140
Raw data (stat): 12083 (minisat+) R 12082 10614 10613 0 -1 0 2892 0 0 0 120005 11 0 0 25 0 1 0 478621313 13389824 2870 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3269 2870 603 41 0 3228 0
vsize: 13076
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.02 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 12140
Raw data (stat): 12083 (minisat+) Z 12082 10614 10613 0 -1 12 2895 0 0 0 120006 12 0 0 25 0 1 0 478621313 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.02
CPU time (s): 1200.18
CPU user time (s): 1200.06
CPU system time (s): 0.121981
CPU usage (%): 100.013
Max. virtual memory (Kb): 13076
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####