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/MIPLIB/miplib3/normalized-mps-v2-20-10-markshare1.opb
MD5SUM	c8b965306fec2c21edee64824d12f378
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	63488
Optimality of the best value was proved	NO
Number of terms in the objective function	180
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	6442450938
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	6442450938
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	1175.08
Number of variables	230
Total number of constraints	56
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	50
Number of constraints which are nor clauses,nor cardinality constraints	6
Minimum length of a constraint	1
Maximum length of a constraint	80
Trace number 16398

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc21 THE 2005-04-21 07:07:38 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=13512 boxname=wulflinc21 idbench=1040 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  c8b965306fec2c21edee64824d12f378  /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-20-10-markshare1.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-20-10-markshare1.opb
IDLAUNCH: 13512
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.161
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.161
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:        560624 kB
Buffers:          9800 kB
Cached:         441108 kB
SwapCached:          0 kB
Active:          94380 kB
Inactive:       359416 kB
HighTotal:      131008 kB
HighFree:          308 kB
LowTotal:       903652 kB
LowFree:        560316 kB
SwapTotal:     2097892 kB
SwapFree:      2097804 kB
Dirty:              36 kB
Writeback:           0 kB
Mapped:           6948 kB
Slab:            14452 kB
Committed_AS:    63796 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 07:27:40 (client local time) WITH STATUS 10 IN 1200.17 SECONDS
stats: 13512 7 1200.17 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 12 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ######
c   -- Clauses(.)/Splits(s): (none)
c ---[  10]---> Adder-cost: 304   maxlim: 3240959   bits: 23/22
c ---[   8]---> Adder-cost: 314   maxlim: 3453951   bits: 23/22
c ---[   6]---> Adder-cost: 348   maxlim: 3482623   bits: 23/22
c ---[   4]---> Adder-cost: 318   maxlim: 3294207   bits: 23/22
c ---[   2]---> Adder-cost: 312   maxlim: 3286015   bits: 23/22
c ---[   0]---> Adder-cost: 314   maxlim: 3289087   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   12820    45524 |    4273       0        0     nan |  0.000 % |
c |       100 |   12820    45524 |    4700     100      594     5.9 | 14.261 % |
c ==============================================================================
c [1mFound solution: 4615168[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:  850     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       141 |   14814    50194 |    4938     141     1027     7.3 | 14.261 % |
c |       241 |   14814    50194 |    5431     241    12192    50.6 | 10.969 % |
c |       393 |   14814    50194 |    5974     393    26032    66.2 | 10.969 % |
c |       618 |   14814    50194 |    6572     618    37060    60.0 | 10.969 % |
c |       955 |   14814    50194 |    7229     955    69049    72.3 | 10.969 % |
c ==============================================================================
c [1mFound solution: 4444160[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   11     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1006 |   14929    50490 |    4976    1006    70987    70.6 | 10.969 % |
c |      1107 |   14929    50490 |    5473    1107    85930    77.6 | 10.770 % |
c ==============================================================================
c [1mFound solution: 4152320[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1139 |   14941    50532 |    4980    1139    86375    75.8 | 10.770 % |
c |      1240 |   14941    50532 |    5478    1240    94355    76.1 | 10.771 % |
c |      1390 |   14941    50532 |    6025    1390   106104    76.3 | 10.771 % |
c ==============================================================================
c [1mFound solution: 3231744[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1590 |   14951    50556 |    4983    1590   117597    74.0 | 10.771 % |
c |      1691 |   14951    50556 |    5481    1691   130635    77.3 | 10.786 % |
c |      1841 |   14951    50556 |    6029    1841   142489    77.4 | 10.786 % |
c |      2067 |   14943    50530 |    6632    2066   165570    80.1 | 10.819 % |
c |      2404 |   14943    50530 |    7295    2403   186034    77.4 | 10.819 % |
c |      2910 |   14943    50530 |    8025    2909   234223    80.5 | 10.819 % |
c |      3669 |   14935    50504 |    8827    3667   297711    81.2 | 10.852 % |
c |      4810 |   14919    50452 |    9710    4806   397534    82.7 | 10.917 % |
c |      6518 |   14919    50452 |   10681    6514   543132    83.4 | 10.917 % |
c |      9081 |   14919    50452 |   11749    9077   695094    76.6 | 10.917 % |
c ==============================================================================
c [1mFound solution: 3212288[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11955 |   14931    50479 |    4977   11951   922500    77.2 | 10.917 % |
c |     12056 |   14931    50479 |    5474    3089   184035    59.6 | 10.932 % |
c |     12207 |   14931    50479 |    6022    3240   193746    59.8 | 10.932 % |
c |     12433 |   14931    50479 |    6624    3466   204232    58.9 | 10.932 % |
c |     12770 |   14931    50479 |    7286    3803   246752    64.9 | 10.932 % |
c |     13278 |   14923    50453 |    8015    4310   287955    66.8 | 10.965 % |
c |     14042 |   14923    50453 |    8817    5074   357875    70.5 | 10.965 % |
c |     15182 |   14923    50453 |    9698    6214   454785    73.2 | 10.965 % |
c |     16891 |   14923    50453 |   10668    7923   596983    75.3 | 10.965 % |
c |     19453 |   14915    50427 |   11735   10484   806542    76.9 | 10.998 % |
c |     23299 |   14907    50401 |   12909    7910   531028    67.1 | 11.031 % |
c |     29065 |   14891    50349 |   14199   13674  1005814    73.6 | 11.097 % |
c |     37715 |   14884    50334 |   15619   14705  1118217    76.0 | 11.162 % |
c ==============================================================================
c [1mFound solution: 3169280[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     45485 |   14886    50339 |    4962   14152  1130949    79.9 | 11.162 % |
c |     45586 |   14886    50339 |    5458    3639   207343    57.0 | 11.253 % |
c |     45736 |   14886    50339 |    6004    3789   218603    57.7 | 11.253 % |
c |     45961 |   14886    50339 |    6604    4014   238535    59.4 | 11.253 % |
c |     46300 |   14886    50339 |    7264    4353   272968    62.7 | 11.253 % |
c |     46807 |   14878    50313 |    7991    4859   321893    66.2 | 11.286 % |
c |     47567 |   14878    50313 |    8790    5619   395734    70.4 | 11.286 % |
c |     48706 |   14878    50313 |    9669    6758   514295    76.1 | 11.286 % |
c |     50414 |   14878    50313 |   10636    8466   674245    79.6 | 11.286 % |
c |     52979 |   14878    50313 |   11700   11031   894758    81.1 | 11.286 % |
c |     56823 |   14878    50313 |   12870    8476   585487    69.1 | 11.286 % |
c |     62589 |   14878    50313 |   14157    7246   470267    64.9 | 11.286 % |
c |     71238 |   14878    50313 |   15572    8340   484689    58.1 | 11.286 % |
c ==============================================================================
c [1mFound solution: 3042304[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     81326 |   14886    50332 |    4962   10127   656025    64.8 | 11.286 % |
c |     81428 |   14886    50332 |    5458    5166   279097    54.0 | 11.300 % |
c |     81579 |   14886    50332 |    6004    5317   292474    55.0 | 11.300 % |
c |     81804 |   14886    50332 |    6604    5542   307973    55.6 | 11.300 % |
c |     82141 |   14886    50332 |    7264    5879   344300    58.6 | 11.300 % |
c |     82647 |   14886    50332 |    7991    6385   389480    61.0 | 11.300 % |
c |     83406 |   14886    50332 |    8790    7144   439505    61.5 | 11.300 % |
c |     84547 |   14886    50332 |    9669    8285   529161    63.9 | 11.300 % |
c |     86259 |   14886    50332 |   10636    9997   662102    66.2 | 11.300 % |
c |     88822 |   14886    50332 |   11700    6767   420905    62.2 | 11.300 % |
c |     92668 |   14886    50332 |   12870   10613   744951    70.2 | 11.300 % |
c |     98434 |   14886    50332 |   14157    9409   652200    69.3 | 11.300 % |
c |    107085 |   14886    50332 |   15572   10478   637247    60.8 | 11.300 % |
c ==============================================================================
c [1mFound solution: 3005440[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    111385 |   14888    50336 |    4962   14777   921886    62.4 | 11.300 % |
c |    111486 |   14888    50336 |    5458    3796   173019    45.6 | 11.344 % |
c |    111636 |   14888    50336 |    6004    3946   179318    45.4 | 11.344 % |
c |    111861 |   14888    50336 |    6604    4171   192217    46.1 | 11.344 % |
c |    112199 |   14880    50310 |    7264    4508   220479    48.9 | 11.376 % |
c |    112705 |   14880    50310 |    7991    5014   263662    52.6 | 11.376 % |
c |    113465 |   14880    50310 |    8790    5774   310667    53.8 | 11.376 % |
c |    114604 |   14880    50310 |    9669    6913   409090    59.2 | 11.376 % |
c |    116313 |   14872    50284 |   10636    8621   542723    63.0 | 11.409 % |
c |    118875 |   14864    50258 |   11700   11182   716184    64.0 | 11.442 % |
c |    122719 |   14864    50258 |   12870    8765   560433    63.9 | 11.442 % |
c ==============================================================================
c [1mFound solution: 2816000[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   11     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    124383 |   14877    50289 |    4959   10429   657968    63.1 | 11.442 % |
c |    124484 |   14877    50289 |    5454    5316   265689    50.0 | 11.448 % |
c |    124635 |   14877    50289 |    6000    5467   270323    49.4 | 11.448 % |
c |    124860 |   14877    50289 |    6600    5692   292327    51.4 | 11.448 % |
c |    125197 |   14877    50289 |    7260    6029   329895    54.7 | 11.448 % |
c |    125703 |   14877    50289 |    7986    6535   361239    55.3 | 11.448 % |
c |    126462 |   14877    50289 |    8785    7294   391859    53.7 | 11.448 % |
c |    127603 |   14877    50289 |    9663    8435   478713    56.8 | 11.448 % |
c |    129311 |   14877    50289 |   10630   10143   570334    56.2 | 11.448 % |
c |    131874 |   14877    50289 |   11693    7035   309663    44.0 | 11.448 % |
c ==============================================================================
c [1mFound solution: 1213440[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    132830 |   14885    50302 |    4961    7990   344228    43.1 | 11.448 % |
c |    132930 |   14885    50302 |    5457    4095   130652    31.9 | 11.487 % |
c |    133082 |   14885    50302 |    6002    4247   140906    33.2 | 11.487 % |
c |    133308 |   14885    50302 |    6603    4473   145839    32.6 | 11.487 % |
c |    133645 |   14885    50302 |    7263    4810   163247    33.9 | 11.487 % |
c |    134152 |   14885    50302 |    7989    5317   180646    34.0 | 11.487 % |
c |    134911 |   14867    50262 |    8788    6074   210613    34.7 | 11.650 % |
c |    136050 |   14867    50262 |    9667    7213   249425    34.6 | 11.650 % |
c |    137760 |   14839    50199 |   10634    8921   304715    34.2 | 11.910 % |
c |    140322 |   14839    50199 |   11697   11483   433802    37.8 | 11.910 % |
c |    144166 |   14839    50199 |   12867    9063   353815    39.0 | 11.910 % |
c |    149933 |   14839    50199 |   14154    7885   325078    41.2 | 11.910 % |
c |    158582 |   14839    50199 |   15569    9129   370373    40.6 | 11.910 % |
c |    171556 |   14839    50199 |   17126   13879   596591    43.0 | 11.910 % |
c ==============================================================================
c [1mFound solution: 1145856[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    183021 |   14849    50222 |    4949   16407   675729    41.2 | 11.910 % |
c |    183123 |   14849    50222 |    5443    4204   124504    29.6 | 11.927 % |
c |    183273 |   14849    50222 |    5988    4354   127342    29.2 | 11.927 % |
c |    183498 |   14849    50222 |    6587    4579   133579    29.2 | 11.927 % |
c |    183836 |   14849    50222 |    7245    4917   140722    28.6 | 11.927 % |
c |    184343 |   14849    50222 |    7970    5424   153528    28.3 | 11.927 % |
c |    185102 |   14849    50222 |    8767    6183   178163    28.8 | 11.927 % |
c |    186244 |   14849    50222 |    9644    7325   224903    30.7 | 11.927 % |
c |    187953 |   14849    50222 |   10608    9034   306970    34.0 | 11.927 % |
c |    190516 |   14849    50222 |   11669    5935   207351    34.9 | 11.927 % |
c |    194361 |   14849    50222 |   12836    9780   381421    39.0 | 11.927 % |
c |    200127 |   14849    50222 |   14120    8789   336369    38.3 | 11.927 % |
c |    208776 |   14849    50222 |   15532   10045   375187    37.4 | 11.927 % |
c |    221750 |   14849    50222 |   17085   14863   663052    44.6 | 11.927 % |
c ==============================================================================
c [1mFound solution: 882688[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    226679 |   14815    50095 |    4938   10932   449646    41.1 | 11.927 % |
c |    226780 |   14815    50095 |    5431    2834    95029    33.5 | 12.131 % |
c |    226930 |   14815    50095 |    5974    2984   100132    33.6 | 12.131 % |
c |    227155 |   14815    50095 |    6572    3209   103870    32.4 | 12.131 % |
c |    227493 |   14815    50095 |    7229    3547   112944    31.8 | 12.131 % |
c |    228002 |   14815    50095 |    7952    4056   131115    32.3 | 12.131 % |
c |    228763 |   14815    50095 |    8747    4817   152790    31.7 | 12.131 % |
c |    229903 |   14815    50095 |    9622    5957   192874    32.4 | 12.131 % |
c |    231611 |   14815    50095 |   10585    7665   256994    33.5 | 12.131 % |
c |    234173 |   14815    50095 |   11643   10227   369004    36.1 | 12.131 % |
c |    238017 |   14815    50095 |   12807    7881   286356    36.3 | 12.131 % |
c |    243784 |   14815    50095 |   14088    6898   265127    38.4 | 12.131 % |
c |    252433 |   14725    49888 |   15497    8166   240170    29.4 | 13.104 % |
c |    265408 |   14698    49827 |   17047   12985   490542    37.8 | 13.428 % |
c ==============================================================================
c [1mFound solution: 804864[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    267580 |   14710    49855 |    4903   15157   570717    37.7 | 13.428 % |
c |    267682 |   14710    49855 |    5393    3892   103008    26.5 | 13.430 % |
c |    267833 |   14710    49855 |    5932    4043   104747    25.9 | 13.430 % |
c |    268058 |   14710    49855 |    6525    4268   108961    25.5 | 13.430 % |
c |    268395 |   14710    49855 |    7178    4605   114605    24.9 | 13.430 % |
c |    268901 |   14710    49855 |    7896    5111   127137    24.9 | 13.430 % |
c |    269662 |   14710    49855 |    8685    5872   146984    25.0 | 13.430 % |
c |    270803 |   14710    49855 |    9554    7013   203504    29.0 | 13.430 % |
c |    272514 |   14710    49855 |   10510    8724   270568    31.0 | 13.430 % |
c |    275076 |   14710    49855 |   11561    5653   166684    29.5 | 13.430 % |
c |    278920 |   14710    49855 |   12717    9497   351916    37.1 | 13.430 % |
c |    284686 |   14697    49825 |   13988    8584   333786    38.9 | 13.592 % |
c |    293335 |   14697    49825 |   15387    9940   408374    41.1 | 13.592 % |
c |    306309 |   14697    49825 |   16926   14883   678759    45.6 | 13.592 % |
c |    325770 |   14697    49825 |   18619   16738   728728    43.5 | 13.592 % |
c |    354962 |   14697    49825 |   20481   16697   780600    46.8 | 13.592 % |
c |    398751 |   14673    49772 |   22529   18038   685094    38.0 | 13.819 % |
c |    464435 |   14665    49750 |   24782   13779   573078    41.6 | 13.884 % |
c |    562961 |   14665    49750 |   27260   22883  1101452    48.1 | 13.884 % |
c |    710752 |   14658    49735 |   29986   15376   652286    42.4 | 13.948 % |
c ==============================================================================
c [1mFound solution: 623616[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    746664 |   14638    49690 |    4879   17992   706327    39.3 | 13.948 % |
c |    746764 |   14638    49690 |    5366    4598   126096    27.4 | 14.193 % |
c |    746914 |   14638    49690 |    5903    4748   127793    26.9 | 14.193 % |
c |    747139 |   14638    49690 |    6493    4973   134208    27.0 | 14.193 % |
c |    747476 |   14638    49690 |    7143    5310   144194    27.2 | 14.193 % |
c |    747983 |   14638    49690 |    7857    5817   154204    26.5 | 14.193 % |
c |    748742 |   14638    49690 |    8643    6576   178501    27.1 | 14.193 % |
c |    749883 |   14638    49690 |    9507    7717   235750    30.5 | 14.193 % |
c |    751592 |   14638    49690 |   10458    9426   293678    31.2 | 14.193 % |
c |    754155 |   14638    49690 |   11504    6266   192414    30.7 | 14.193 % |
c |    758000 |   14613    49633 |   12654   10109   337355    33.4 | 14.452 % |
c |    763767 |   14613    49633 |   13920    9088   320912    35.3 | 14.452 % |
c |    772417 |   14613    49633 |   15312   10244   395768    38.6 | 14.452 % |
c |    785392 |   14613    49633 |   16843   15023   729672    48.6 | 14.452 % |
c ==============================================================================
c [1mFound solution: 500736[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    800439 |   14548    49432 |    4849   12558   596683    47.5 | 14.452 % |
c |    800539 |   14548    49432 |    5333    3240   104489    32.2 | 15.010 % |
c |    800690 |   14548    49432 |    5867    3391   107542    31.7 | 15.010 % |
c |    800917 |   14548    49432 |    6454    3618   115679    32.0 | 15.010 % |
c |    801254 |   14548    49432 |    7099    3955   123167    31.1 | 15.010 % |
c |    801762 |   14548    49432 |    7809    4463   134634    30.2 | 15.010 % |
c |    802521 |   14548    49432 |    8590    5222   157497    30.2 | 15.010 % |
c |    803660 |   14548    49432 |    9449    6361   201480    31.7 | 15.010 % |
c ==============================================================================
c [1mFound solution: 478208[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    805121 |   14555    49450 |    4851    7822   238002    30.4 | 15.010 % |
c |    805221 |   14555    49450 |    5336    4011    93709    23.4 | 15.018 % |
c |    805371 |   14555    49450 |    5869    4161    95436    22.9 | 15.018 % |
c |    805596 |   14555    49450 |    6456    4386    98503    22.5 | 15.018 % |
c |    805933 |   14555    49450 |    7102    4723   109884    23.3 | 15.018 % |
c |    806441 |   14555    49450 |    7812    5231   133539    25.5 | 15.018 % |
c |    807201 |   14515    49360 |    8593    5987   160022    26.7 | 15.404 % |
c |    808340 |   14515    49360 |    9453    7126   199759    28.0 | 15.404 % |
c |    810048 |   14515    49360 |   10398    8834   256370    29.0 | 15.404 % |
c |    812610 |   14515    49360 |   11438    5831   160906    27.6 | 15.404 % |
c |    816457 |   14515    49360 |   12582    9678   325951    33.7 | 15.404 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.91 0.95 0.90 2/55 4780
Raw data (stat): 4780 (runsolver) R 4779 30927 30926 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 420419567 1052672 99 4294967295 134512640 135381576 3221224512 3221219756 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0005 s]
Raw data (loadavg): 0.93 0.95 0.90 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 1221 0 0 0 996 3 0 0 25 0 1 0 420419567 6565888 1199 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1603 1199 603 41 0 1562 0
vsize: 6412
[startup+20.0011 s]
Raw data (loadavg): 0.94 0.96 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 1586 0 0 0 1995 3 0 0 25 0 1 0 420419567 8060928 1564 4294967295 134512640 134672761 3221224624 3221223808 134559542 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1968 1564 603 41 0 1927 0
vsize: 7872
[startup+30.0018 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 1732 0 0 0 2994 4 0 0 25 0 1 0 420419567 8597504 1710 4294967295 134512640 134672761 3221224624 3221223728 134560194 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2099 1710 603 41 0 2058 0
vsize: 8396
[startup+40.0019 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 1732 0 0 0 3994 5 0 0 25 0 1 0 420419567 8597504 1710 4294967295 134512640 134672761 3221224624 3221223808 134559038 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2099 1710 603 41 0 2058 0
vsize: 8396
[startup+50.0022 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 1868 0 0 0 4994 5 0 0 25 0 1 0 420419567 9125888 1846 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2228 1846 603 41 0 2187 0
vsize: 8912
[startup+60.0019 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 1868 0 0 0 5994 5 0 0 25 0 1 0 420419567 9125888 1846 4294967295 134512640 134672761 3221224624 3221223808 134559365 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2228 1846 603 41 0 2187 0
vsize: 8912
[startup+70.0015 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 2073 0 0 0 6994 6 0 0 25 0 1 0 420419567 10063872 2051 4294967295 134512640 134672761 3221224624 3221223760 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2457 2051 603 41 0 2416 0
vsize: 9828
[startup+80.0022 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 2073 0 0 0 7994 6 0 0 25 0 1 0 420419567 10063872 2051 4294967295 134512640 134672761 3221224624 3221223808 134558667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2457 2051 603 41 0 2416 0
vsize: 9828
[startup+90.0019 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 2090 0 0 0 8994 6 0 0 25 0 1 0 420419567 10063872 2068 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2457 2068 603 41 0 2416 0
vsize: 9828
[startup+100.002 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 2273 0 0 0 9994 6 0 0 25 0 1 0 420419567 10944512 2251 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2672 2251 603 41 0 2631 0
vsize: 10688
[startup+110.002 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 2280 0 0 0 10994 6 0 0 25 0 1 0 420419567 10944512 2258 4294967295 134512640 134672761 3221224624 3221223792 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2672 2258 603 41 0 2631 0
vsize: 10688
[startup+120.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 2280 0 0 0 11994 6 0 0 25 0 1 0 420419567 10944512 2258 4294967295 134512640 134672761 3221224624 3221223760 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2672 2258 603 41 0 2631 0
vsize: 10688
[startup+130.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 2280 0 0 0 12994 7 0 0 25 0 1 0 420419567 10944512 2258 4294967295 134512640 134672761 3221224624 3221223760 134560604 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2672 2258 603 41 0 2631 0
vsize: 10688
[startup+140.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 2280 0 0 0 13993 7 0 0 25 0 1 0 420419567 10944512 2258 4294967295 134512640 134672761 3221224624 3221223780 134560075 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2672 2258 603 41 0 2631 0
vsize: 10688
[startup+150.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 2280 0 0 0 14993 7 0 0 25 0 1 0 420419567 10944512 2258 4294967295 134512640 134672761 3221224624 3221223728 134560326 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2672 2258 603 41 0 2631 0
vsize: 10688
[startup+160.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 2280 0 0 0 15993 7 0 0 25 0 1 0 420419567 10944512 2258 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2672 2258 603 41 0 2631 0
vsize: 10688
[startup+170.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 2280 0 0 0 16993 7 0 0 25 0 1 0 420419567 10944512 2258 4294967295 134512640 134672761 3221224624 3221223792 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2672 2258 603 41 0 2631 0
vsize: 10688
[startup+180.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 2280 0 0 0 17993 7 0 0 25 0 1 0 420419567 10944512 2258 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2672 2258 603 41 0 2631 0
vsize: 10688
[startup+190.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 2280 0 0 0 18994 8 0 0 25 0 1 0 420419567 10944512 2258 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2672 2258 603 41 0 2631 0
vsize: 10688
[startup+200.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 2280 0 0 0 19994 8 0 0 25 0 1 0 420419567 10944512 2258 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2672 2258 603 41 0 2631 0
vsize: 10688
[startup+210.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 2280 0 0 0 20993 8 0 0 25 0 1 0 420419567 10944512 2258 4294967295 134512640 134672761 3221224624 3221223792 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2672 2258 603 41 0 2631 0
vsize: 10688
[startup+220.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 2280 0 0 0 21993 8 0 0 25 0 1 0 420419567 10944512 2258 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2672 2258 603 41 0 2631 0
vsize: 10688
[startup+230.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 2280 0 0 0 22993 8 0 0 25 0 1 0 420419567 10944512 2258 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2672 2258 603 41 0 2631 0
vsize: 10688
[startup+240.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 2280 0 0 0 23993 9 0 0 25 0 1 0 420419567 10944512 2258 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2672 2258 603 41 0 2631 0
vsize: 10688
[startup+250.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 2280 0 0 0 24993 9 0 0 25 0 1 0 420419567 10944512 2258 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2672 2258 603 41 0 2631 0
vsize: 10688
[startup+260.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 2280 0 0 0 25993 9 0 0 25 0 1 0 420419567 10944512 2258 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2672 2258 603 41 0 2631 0
vsize: 10688
[startup+270.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 2280 0 0 0 26993 9 0 0 25 0 1 0 420419567 10944512 2258 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2672 2258 603 41 0 2631 0
vsize: 10688
[startup+280.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 2280 0 0 0 27993 9 0 0 25 0 1 0 420419567 10944512 2258 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2672 2258 603 41 0 2631 0
vsize: 10688
[startup+290.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 2280 0 0 0 28993 10 0 0 25 0 1 0 420419567 10944512 2258 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2672 2258 603 41 0 2631 0
vsize: 10688
[startup+300.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 2280 0 0 0 29993 10 0 0 25 0 1 0 420419567 10944512 2258 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2672 2258 603 41 0 2631 0
vsize: 10688
[startup+310.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 2280 0 0 0 30993 10 0 0 25 0 1 0 420419567 10944512 2258 4294967295 134512640 134672761 3221224624 3221223792 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2672 2258 603 41 0 2631 0
vsize: 10688
[startup+320.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 2280 0 0 0 31993 10 0 0 25 0 1 0 420419567 10944512 2258 4294967295 134512640 134672761 3221224624 3221223728 134560250 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2672 2258 603 41 0 2631 0
vsize: 10688
[startup+330.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 2280 0 0 0 32993 10 0 0 25 0 1 0 420419567 10944512 2258 4294967295 134512640 134672761 3221224624 3221223808 134558687 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2672 2258 603 41 0 2631 0
vsize: 10688
[startup+340.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 2280 0 0 0 33993 10 0 0 25 0 1 0 420419567 10944512 2258 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2672 2258 603 41 0 2631 0
vsize: 10688
[startup+350.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 2280 0 0 0 34992 11 0 0 25 0 1 0 420419567 10944512 2258 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2672 2258 603 41 0 2631 0
vsize: 10688
[startup+360.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 2282 0 0 0 35993 11 0 0 25 0 1 0 420419567 10944512 2260 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2672 2260 603 41 0 2631 0
vsize: 10688
[startup+370.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 2282 0 0 0 36993 11 0 0 25 0 1 0 420419567 10944512 2260 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2672 2260 603 41 0 2631 0
vsize: 10688
[startup+380.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 2282 0 0 0 37993 11 0 0 25 0 1 0 420419567 10944512 2260 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2672 2260 603 41 0 2631 0
vsize: 10688
[startup+390.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 2282 0 0 0 38993 11 0 0 25 0 1 0 420419567 10944512 2260 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2672 2260 603 41 0 2631 0
vsize: 10688
[startup+400.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 2282 0 0 0 39993 11 0 0 25 0 1 0 420419567 10944512 2260 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2672 2260 603 41 0 2631 0
vsize: 10688
[startup+410.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 2282 0 0 0 40993 11 0 0 25 0 1 0 420419567 10944512 2260 4294967295 134512640 134672761 3221224624 3221223792 134560964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2672 2260 603 41 0 2631 0
vsize: 10688
[startup+420.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 2282 0 0 0 41993 11 0 0 25 0 1 0 420419567 10944512 2260 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2672 2260 603 41 0 2631 0
vsize: 10688
[startup+430.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 2282 0 0 0 42993 11 0 0 25 0 1 0 420419567 10944512 2260 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2672 2260 603 41 0 2631 0
vsize: 10688
[startup+440.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 2282 0 0 0 43994 11 0 0 25 0 1 0 420419567 10944512 2260 4294967295 134512640 134672761 3221224624 3221223792 134560845 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2672 2260 603 41 0 2631 0
vsize: 10688
[startup+450.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 2282 0 0 0 44994 11 0 0 25 0 1 0 420419567 10944512 2260 4294967295 134512640 134672761 3221224624 3221223760 134560675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2672 2260 603 41 0 2631 0
vsize: 10688
[startup+460.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 2282 0 0 0 45994 11 0 0 25 0 1 0 420419567 10944512 2260 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2672 2260 603 41 0 2631 0
vsize: 10688
[startup+470.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 2282 0 0 0 46994 11 0 0 25 0 1 0 420419567 10944512 2260 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2672 2260 603 41 0 2631 0
vsize: 10688
[startup+480.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 2282 0 0 0 47994 11 0 0 25 0 1 0 420419567 10944512 2260 4294967295 134512640 134672761 3221224624 3221223792 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2672 2260 603 41 0 2631 0
vsize: 10688
[startup+490.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 2318 0 0 0 48994 11 0 0 25 0 1 0 420419567 11075584 2296 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2704 2296 603 41 0 2663 0
vsize: 10816
[startup+500.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 2324 0 0 0 49994 11 0 0 25 0 1 0 420419567 11075584 2302 4294967295 134512640 134672761 3221224624 3221223792 134561161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2704 2302 603 41 0 2663 0
vsize: 10816
[startup+510.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 2382 0 0 0 50994 11 0 0 25 0 1 0 420419567 11345920 2360 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2770 2360 603 41 0 2729 0
vsize: 11080
[startup+520.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 2467 0 0 0 51994 11 0 0 25 0 1 0 420419567 11755520 2445 4294967295 134512640 134672761 3221224624 3221223768 134560553 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2870 2445 603 41 0 2829 0
vsize: 11480
[startup+530.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 2599 0 0 0 52994 12 0 0 25 0 1 0 420419567 12288000 2577 4294967295 134512640 134672761 3221224624 3221223792 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3000 2577 603 41 0 2959 0
vsize: 12000
[startup+540.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 2608 0 0 0 53994 12 0 0 25 0 1 0 420419567 12288000 2586 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3000 2586 603 41 0 2959 0
vsize: 12000
[startup+550.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 2620 0 0 0 54995 12 0 0 25 0 1 0 420419567 12288000 2598 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3000 2598 603 41 0 2959 0
vsize: 12000
[startup+560.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 2620 0 0 0 55995 12 0 0 25 0 1 0 420419567 12288000 2598 4294967295 134512640 134672761 3221224624 3221223808 134559031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3000 2598 603 41 0 2959 0
vsize: 12000
[startup+570.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 2628 0 0 0 56995 12 0 0 25 0 1 0 420419567 12423168 2606 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3033 2606 603 41 0 2992 0
vsize: 12132
[startup+580.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 2635 0 0 0 57995 12 0 0 25 0 1 0 420419567 12423168 2613 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3033 2613 603 41 0 2992 0
vsize: 12132
[startup+590.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 2648 0 0 0 58995 12 0 0 25 0 1 0 420419567 12423168 2626 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3033 2626 603 41 0 2992 0
vsize: 12132
[startup+600.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 2696 0 0 0 59995 12 0 0 25 0 1 0 420419567 12701696 2674 4294967295 134512640 134672761 3221224624 3221223792 134560906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3101 2674 603 41 0 3060 0
vsize: 12404
[startup+610.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 2732 0 0 0 60995 12 0 0 25 0 1 0 420419567 12836864 2710 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3134 2710 603 41 0 3093 0
vsize: 12536
[startup+620.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 2755 0 0 0 61995 12 0 0 25 0 1 0 420419567 12836864 2733 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3134 2733 603 41 0 3093 0
vsize: 12536
[startup+630.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 2763 0 0 0 62996 12 0 0 25 0 1 0 420419567 12976128 2741 4294967295 134512640 134672761 3221224624 3221223792 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3168 2741 603 41 0 3127 0
vsize: 12672
[startup+640.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 2763 0 0 0 63996 12 0 0 25 0 1 0 420419567 12976128 2741 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3168 2741 603 41 0 3127 0
vsize: 12672
[startup+650.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 2779 0 0 0 64996 12 0 0 25 0 1 0 420419567 12976128 2757 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3168 2757 603 41 0 3127 0
vsize: 12672
[startup+660.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 2797 0 0 0 65996 12 0 0 25 0 1 0 420419567 13111296 2775 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3201 2775 603 41 0 3160 0
vsize: 12804
[startup+670.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 2812 0 0 0 66996 12 0 0 25 0 1 0 420419567 13111296 2790 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3201 2790 603 41 0 3160 0
vsize: 12804
[startup+680.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 2822 0 0 0 67996 12 0 0 25 0 1 0 420419567 13250560 2800 4294967295 134512640 134672761 3221224624 3221223728 134560254 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3235 2800 603 41 0 3194 0
vsize: 12940
[startup+690.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 2835 0 0 0 68997 12 0 0 25 0 1 0 420419567 13250560 2813 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3235 2813 603 41 0 3194 0
vsize: 12940
[startup+700.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 2945 0 0 0 69996 13 0 0 25 0 1 0 420419567 13651968 2923 4294967295 134512640 134672761 3221224624 3221223792 134560954 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3333 2923 603 41 0 3292 0
vsize: 13332
[startup+710.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 2954 0 0 0 70996 13 0 0 25 0 1 0 420419567 13791232 2932 4294967295 134512640 134672761 3221224624 3221223792 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3367 2932 603 41 0 3326 0
vsize: 13468
[startup+720.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 3003 0 0 0 71996 13 0 0 25 0 1 0 420419567 13926400 2981 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3400 2981 603 41 0 3359 0
vsize: 13600
[startup+730.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 3003 0 0 0 72997 13 0 0 25 0 1 0 420419567 13926400 2981 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3400 2981 603 41 0 3359 0
vsize: 13600
[startup+740.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 3011 0 0 0 73997 13 0 0 25 0 1 0 420419567 14061568 2989 4294967295 134512640 134672761 3221224624 3221223792 134560917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3433 2989 603 41 0 3392 0
vsize: 13732
[startup+750.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 3015 0 0 0 74997 13 0 0 25 0 1 0 420419567 14061568 2993 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3433 2994 603 41 0 3392 0
vsize: 13732
[startup+760.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 3059 0 0 0 75997 13 0 0 25 0 1 0 420419567 14192640 3037 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3465 3037 603 41 0 3424 0
vsize: 13860
[startup+770.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 3077 0 0 0 76997 14 0 0 25 0 1 0 420419567 14323712 3055 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3497 3055 603 41 0 3456 0
vsize: 13988
[startup+780.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 3132 0 0 0 77997 14 0 0 25 0 1 0 420419567 14454784 3110 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3529 3110 603 41 0 3488 0
vsize: 14116
[startup+790.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 3146 0 0 0 78997 14 0 0 25 0 1 0 420419567 14589952 3124 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3562 3124 603 41 0 3521 0
vsize: 14248
[startup+800.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 3163 0 0 0 79997 14 0 0 25 0 1 0 420419567 14589952 3141 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3562 3141 603 41 0 3521 0
vsize: 14248
[startup+810.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 3167 0 0 0 80997 14 0 0 25 0 1 0 420419567 14725120 3145 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3595 3145 603 41 0 3554 0
vsize: 14380
[startup+820.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 3180 0 0 0 81997 14 0 0 25 0 1 0 420419567 14725120 3158 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3595 3158 603 41 0 3554 0
vsize: 14380
[startup+830.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 3188 0 0 0 82996 14 0 0 25 0 1 0 420419567 14725120 3166 4294967295 134512640 134672761 3221224624 3221223792 134561400 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3595 3166 603 41 0 3554 0
vsize: 14380
[startup+840.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 3286 0 0 0 83996 15 0 0 25 0 1 0 420419567 15122432 3264 4294967295 134512640 134672761 3221224624 3221223792 134564748 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3692 3264 603 41 0 3651 0
vsize: 14768
[startup+850.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 3295 0 0 0 84996 15 0 0 25 0 1 0 420419567 15122432 3273 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3692 3273 603 41 0 3651 0
vsize: 14768
[startup+860.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 3301 0 0 0 85996 15 0 0 25 0 1 0 420419567 15265792 3279 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3727 3279 603 41 0 3686 0
vsize: 14908
[startup+870.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 3301 0 0 0 86996 16 0 0 25 0 1 0 420419567 15265792 3279 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3727 3279 603 41 0 3686 0
vsize: 14908
[startup+880.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 3303 0 0 0 87996 16 0 0 25 0 1 0 420419567 15265792 3281 4294967295 134512640 134672761 3221224624 3221223808 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3727 3281 603 41 0 3686 0
vsize: 14908
[startup+890.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 3306 0 0 0 88996 16 0 0 25 0 1 0 420419567 15265792 3284 4294967295 134512640 134672761 3221224624 3221223792 134561016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3727 3284 603 41 0 3686 0
vsize: 14908
[startup+900.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 3306 0 0 0 89996 16 0 0 25 0 1 0 420419567 15265792 3284 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3727 3284 603 41 0 3686 0
vsize: 14908
[startup+910.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 3306 0 0 0 90996 16 0 0 25 0 1 0 420419567 15265792 3284 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3727 3284 603 41 0 3686 0
vsize: 14908
[startup+920.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 3306 0 0 0 91996 16 0 0 25 0 1 0 420419567 15265792 3284 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3727 3284 603 41 0 3686 0
vsize: 14908
[startup+930.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 3373 0 0 0 92996 17 0 0 25 0 1 0 420419567 15532032 3351 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3792 3351 603 41 0 3751 0
vsize: 15168
[startup+940.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 3379 0 0 0 93996 17 0 0 25 0 1 0 420419567 15532032 3357 4294967295 134512640 134672761 3221224624 3221223760 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3792 3357 603 41 0 3751 0
vsize: 15168
[startup+950.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 3383 0 0 0 94996 17 0 0 25 0 1 0 420419567 15532032 3361 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3792 3361 603 41 0 3751 0
vsize: 15168
[startup+960.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 3469 0 0 0 95996 17 0 0 25 0 1 0 420419567 15945728 3447 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3893 3447 603 41 0 3852 0
vsize: 15572
[startup+970.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 3470 0 0 0 96995 18 0 0 25 0 1 0 420419567 15945728 3448 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3893 3448 603 41 0 3852 0
vsize: 15572
[startup+980.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 3485 0 0 0 97996 18 0 0 25 0 1 0 420419567 15945728 3463 4294967295 134512640 134672761 3221224624 3221223760 134560657 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3893 3463 603 41 0 3852 0
vsize: 15572
[startup+990.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 3507 0 0 0 98995 18 0 0 25 0 1 0 420419567 16076800 3485 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3925 3485 603 41 0 3884 0
vsize: 15700
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 3521 0 0 0 99995 18 0 0 25 0 1 0 420419567 16228352 3499 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3962 3499 603 41 0 3921 0
vsize: 15848
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 3536 0 0 0 100995 18 0 0 25 0 1 0 420419567 16228352 3514 4294967295 134512640 134672761 3221224624 3221223808 134558925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3962 3514 603 41 0 3921 0
vsize: 15848
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 3537 0 0 0 101995 18 0 0 25 0 1 0 420419567 16228352 3515 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3962 3515 603 41 0 3921 0
vsize: 15848
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 3537 0 0 0 102995 18 0 0 25 0 1 0 420419567 16228352 3515 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3962 3515 603 41 0 3921 0
vsize: 15848
[startup+1040.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 3537 0 0 0 103995 18 0 0 25 0 1 0 420419567 16228352 3515 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3962 3515 603 41 0 3921 0
vsize: 15848
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 3542 0 0 0 104995 18 0 0 25 0 1 0 420419567 16228352 3520 4294967295 134512640 134672761 3221224624 3221223792 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3962 3520 603 41 0 3921 0
vsize: 15848
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 3554 0 0 0 105995 19 0 0 25 0 1 0 420419567 16379904 3532 4294967295 134512640 134672761 3221224624 3221223716 1075351142 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3999 3532 603 41 0 3958 0
vsize: 15996
[startup+1070.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 3554 0 0 0 106995 19 0 0 25 0 1 0 420419567 16379904 3532 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3999 3532 603 41 0 3958 0
vsize: 15996
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 3560 0 0 0 107995 19 0 0 25 0 1 0 420419567 16379904 3538 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3999 3538 603 41 0 3958 0
vsize: 15996
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 3560 0 0 0 108995 19 0 0 25 0 1 0 420419567 16379904 3538 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3999 3538 603 41 0 3958 0
vsize: 15996
[startup+1100.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 3560 0 0 0 109995 19 0 0 25 0 1 0 420419567 16379904 3538 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3999 3538 603 41 0 3958 0
vsize: 15996
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 3562 0 0 0 110995 19 0 0 25 0 1 0 420419567 16379904 3540 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3999 3540 603 41 0 3958 0
vsize: 15996
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 3562 0 0 0 111995 20 0 0 25 0 1 0 420419567 16379904 3540 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3999 3540 603 41 0 3958 0
vsize: 15996
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 3562 0 0 0 112995 20 0 0 25 0 1 0 420419567 16379904 3540 4294967295 134512640 134672761 3221224624 3221223792 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3999 3540 603 41 0 3958 0
vsize: 15996
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 3562 0 0 0 113995 20 0 0 25 0 1 0 420419567 16379904 3540 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3999 3540 603 41 0 3958 0
vsize: 15996
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 3562 0 0 0 114995 20 0 0 25 0 1 0 420419567 16379904 3540 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3999 3540 603 41 0 3958 0
vsize: 15996
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 3562 0 0 0 115995 20 0 0 25 0 1 0 420419567 16379904 3540 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3999 3540 603 41 0 3958 0
vsize: 15996
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 3562 0 0 0 116995 20 0 0 25 0 1 0 420419567 16379904 3540 4294967295 134512640 134672761 3221224624 3221223824 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3999 3540 603 41 0 3958 0
vsize: 15996
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 3562 0 0 0 117995 20 0 0 25 0 1 0 420419567 16379904 3540 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3999 3540 603 41 0 3958 0
vsize: 15996
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 3562 0 0 0 118995 21 0 0 25 0 1 0 420419567 16379904 3540 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3999 3540 603 41 0 3958 0
vsize: 15996
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 4780
Raw data (stat): 4780 (minisat+) R 4779 30927 30926 0 -1 0 3562 0 0 0 119995 21 0 0 25 0 1 0 420419567 16379904 3540 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3999 3540 603 41 0 3958 0
vsize: 15996
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 1/55 4780
Raw data (stat): 4780 (minisat+) Z 4779 30927 30926 0 -1 12 3565 0 0 0 119995 22 0 0 25 0 1 0 420419567 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.03
CPU time (s): 1200.17
CPU user time (s): 1199.95
CPU system time (s): 0.220966
CPU usage (%): 100.012
Max. virtual memory (Kb): 15996
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####