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/miplib2003/normalized-mps-v2-20-10-markshare1.opb
MD5SUM	10386fd19d9976c249ce2be861b38a70
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.12
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 16749

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc5 THE 2005-04-21 08:23:29 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=12649 boxname=wulflinc5 idbench=973 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  10386fd19d9976c249ce2be861b38a70  /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-20-10-markshare1.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-20-10-markshare1.opb /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-20-10-markshare1.opb
IDLAUNCH: 12649
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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:        547380 kB
Buffers:         23124 kB
Cached:         441452 kB
SwapCached:          0 kB
Active:          32780 kB
Inactive:       434496 kB
HighTotal:      131008 kB
HighFree:        15148 kB
LowTotal:       903652 kB
LowFree:        532232 kB
SwapTotal:     2097136 kB
SwapFree:      2097044 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           6816 kB
Slab:            14180 kB
Committed_AS:    63592 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 08:43:32 (client local time) WITH STATUS 10 IN 1200.32 SECONDS
stats: 12649 7 1200.32 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 |       103 |   12820    45524 |    4700     103      864     8.4 | 14.261 % |
c ==============================================================================
c [1mFound solution: 4091904[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:  855     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 |       127 |   15144    51006 |    5048     127     1062     8.4 | 14.261 % |
c ==============================================================================
c [1mFound solution: 1132544[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 |       178 |   15207    51167 |    5069     178     1647     9.3 | 14.261 % |
c |       278 |   15199    51141 |    5575     277     7046    25.4 | 10.781 % |
c |       429 |   15199    51141 |    6133     428    17519    40.9 | 10.781 % |
c |       655 |   15199    51141 |    6746     654    21728    33.2 | 10.781 % |
c |       992 |   15191    51115 |    7421     990    32805    33.1 | 10.814 % |
c |      1500 |   15183    51089 |    8163    1497    47566    31.8 | 10.847 % |
c |      2261 |   15164    51047 |    8980    2257    81335    36.0 | 11.045 % |
c |      3400 |   15156    51021 |    9878    3395   124783    36.8 | 11.078 % |
c |      5108 |   15148    50995 |   10865    5102   203811    39.9 | 11.111 % |
c |      7670 |   15148    50995 |   11952    7664   324220    42.3 | 11.111 % |
c |     11515 |   15109    50891 |   13147   11505   498082    43.3 | 11.408 % |
c |     17281 |   15097    50857 |   14462   10333   385152    37.3 | 11.474 % |
c |     25930 |   15069    50787 |   15908   11504   439860    38.2 | 11.672 % |
c |     38906 |   15063    50769 |   17499   16288   587149    36.0 | 11.705 % |
c ==============================================================================
c [1mFound solution: 1104896[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 |     39074 |   15076    50804 |    5025   16456   599459    36.4 | 11.705 % |
c |     39174 |   15076    50804 |    5527    4214   133920    31.8 | 11.726 % |
c |     39324 |   15076    50804 |    6080    4364   134839    30.9 | 11.726 % |
c |     39549 |   15076    50804 |    6688    4589   140160    30.5 | 11.726 % |
c |     39888 |   15076    50804 |    7357    4928   154134    31.3 | 11.726 % |
c |     40395 |   15076    50804 |    8092    5435   175488    32.3 | 11.726 % |
c |     41154 |   15076    50804 |    8902    6194   195786    31.6 | 11.726 % |
c |     42295 |   15076    50804 |    9792    7335   230777    31.5 | 11.726 % |
c |     44003 |   15076    50804 |   10771    9043   290016    32.1 | 11.726 % |
c |     46565 |   15076    50804 |   11848   11605   428378    36.9 | 11.726 % |
c |     50409 |   15076    50804 |   13033    9145   372889    40.8 | 11.726 % |
c ==============================================================================
c [1mFound solution: 973824[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     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 |     50921 |   14962    50491 |    4987    9635   402903    41.8 | 11.726 % |
c |     51022 |   14962    50491 |    5485    4919   184394    37.5 | 12.829 % |
c |     51173 |   14962    50491 |    6034    5070   187138    36.9 | 12.829 % |
c |     51399 |   14962    50491 |    6637    5296   195271    36.9 | 12.829 % |
c |     51739 |   14962    50491 |    7301    5636   205021    36.4 | 12.829 % |
c |     52246 |   14962    50491 |    8031    6143   222749    36.3 | 12.829 % |
c |     53005 |   14962    50491 |    8834    6902   241930    35.1 | 12.829 % |
c |     54149 |   14962    50491 |    9718    8046   281408    35.0 | 12.829 % |
c |     55858 |   14946    50455 |   10690    9754   355536    36.5 | 12.961 % |
c |     58423 |   14922    50401 |   11759    6477   212986    32.9 | 13.158 % |
c |     62267 |   14922    50401 |   12934   10321   387813    37.6 | 13.158 % |
c |     68033 |   14922    50401 |   14228    9173   345876    37.7 | 13.158 % |
c |     76686 |   14922    50401 |   15651   10223   403020    39.4 | 13.158 % |
c ==============================================================================
c [1mFound solution: 954368[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     82538 |   14933    50429 |    4977   16074   710585    44.2 | 13.158 % |
c |     82638 |   14933    50429 |    5474    4119   170107    41.3 | 13.287 % |
c |     82788 |   14933    50429 |    6022    4269   172662    40.4 | 13.287 % |
c |     83013 |   14933    50429 |    6624    4494   177203    39.4 | 13.287 % |
c |     83350 |   14933    50429 |    7286    4831   193705    40.1 | 13.287 % |
c |     83856 |   14933    50429 |    8015    5337   205373    38.5 | 13.287 % |
c |     84615 |   14933    50429 |    8817    6096   221893    36.4 | 13.287 % |
c |     85755 |   14933    50429 |    9698    7236   266721    36.9 | 13.287 % |
c |     87463 |   14892    50336 |   10668    8943   341067    38.1 | 13.714 % |
c |     90026 |   14863    50264 |   11735   11505   445843    38.8 | 14.009 % |
c |     93871 |   14863    50264 |   12909    8943   341353    38.2 | 14.009 % |
c |     99637 |   14863    50264 |   14199    7847   337461    43.0 | 14.009 % |
c |    108286 |   14863    50264 |   15619    8911   329916    37.0 | 14.009 % |
c |    121260 |   14829    50187 |   17181   13687   550551    40.2 | 14.337 % |
c ==============================================================================
c [1mFound solution: 903168[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 |    122771 |   14843    50221 |    4947   15198   607158    39.9 | 14.337 % |
c |    122871 |   14843    50221 |    5441    3900   116941    30.0 | 14.347 % |
c |    123021 |   14843    50221 |    5985    4050   120495    29.8 | 14.347 % |
c |    123246 |   14843    50221 |    6584    4275   126430    29.6 | 14.347 % |
c |    123583 |   14843    50221 |    7242    4612   142454    30.9 | 14.347 % |
c |    124089 |   14843    50221 |    7967    5118   159747    31.2 | 14.347 % |
c ==============================================================================
c [1mFound solution: 795648[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 |    124651 |   14860    50264 |    4953    5680   180124    31.7 | 14.347 % |
c |    124751 |   14860    50264 |    5448    2940    73395    25.0 | 14.356 % |
c |    124903 |   14860    50264 |    5993    3092    76751    24.8 | 14.356 % |
c |    125128 |   14860    50264 |    6592    3317    81843    24.7 | 14.356 % |
c |    125467 |   14860    50264 |    7251    3656    90156    24.7 | 14.356 % |
c |    125973 |   14860    50264 |    7976    4162   104801    25.2 | 14.356 % |
c |    126735 |   14860    50264 |    8774    4924   132843    27.0 | 14.356 % |
c |    127875 |   14860    50264 |    9651    6064   174308    28.7 | 14.356 % |
c |    129583 |   14860    50264 |   10617    7772   228080    29.3 | 14.356 % |
c |    132148 |   14860    50264 |   11678   10337   326118    31.5 | 14.356 % |
c |    135997 |   14860    50264 |   12846    7871   287876    36.6 | 14.356 % |
c |    141764 |   14860    50264 |   14131   13638   568773    41.7 | 14.356 % |
c |    150413 |   14788    50093 |   15544   14763   585604    39.7 | 15.043 % |
c |    163387 |   14750    50004 |   17099   11452   478771    41.8 | 15.533 % |
c |    182851 |   14750    50004 |   18809   12997   585632    45.1 | 15.533 % |
c |    212043 |   14750    50004 |   20689   12784   486280    38.0 | 15.533 % |
c |    255832 |   14742    49978 |   22758   13739   656269    47.8 | 15.566 % |
c |    321518 |   14718    49915 |   25034   20568   903592    43.9 | 15.729 % |
c ==============================================================================
c [1mFound solution: 729088[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 |    397065 |   14724    49924 |    4908   18668   743468    39.8 | 15.729 % |
c |    397165 |   14724    49924 |    5398    4766   141852    29.8 | 15.862 % |
c |    397315 |   14718    49906 |    5938    4916   142722    29.0 | 15.862 % |
c |    397540 |   14718    49906 |    6532    5141   148255    28.8 | 15.862 % |
c |    397877 |   14718    49906 |    7185    5478   157103    28.7 | 15.862 % |
c |    398384 |   14718    49906 |    7904    5985   173340    29.0 | 15.862 % |
c |    399144 |   14710    49880 |    8694    6744   207977    30.8 | 15.894 % |
c |    400284 |   14710    49880 |    9564    7884   247975    31.5 | 15.894 % |
c |    401994 |   14710    49880 |   10520    9594   293718    30.6 | 15.894 % |
c |    404556 |   14710    49880 |   11572    6408   190994    29.8 | 15.894 % |
c |    408400 |   14710    49880 |   12730   10252   335931    32.8 | 15.894 % |
c |    414166 |   14702    49858 |   14003    9168   326616    35.6 | 15.960 % |
c |    422816 |   14702    49858 |   15403   10455   447505    42.8 | 15.960 % |
c |    435790 |   14702    49858 |   16943   15281   640290    41.9 | 15.960 % |
c ==============================================================================
c [1mFound solution: 675840[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    453583 |   14716    49892 |    4905   15139   896006    59.2 | 15.960 % |
c |    453684 |   14716    49892 |    5395    3886   157152    40.4 | 15.966 % |
c |    453836 |   14716    49892 |    5935    4038   159531    39.5 | 15.966 % |
c |    454063 |   14716    49892 |    6528    4265   164520    38.6 | 15.966 % |
c |    454400 |   14716    49892 |    7181    4602   172401    37.5 | 15.966 % |
c |    454906 |   14716    49892 |    7899    5108   183491    35.9 | 15.966 % |
c |    455665 |   14716    49892 |    8689    5867   211155    36.0 | 15.966 % |
c |    456808 |   14716    49892 |    9558    7010   253036    36.1 | 15.966 % |
c |    458517 |   14716    49892 |   10514    8719   340787    39.1 | 15.966 % |
c |    461079 |   14716    49892 |   11565   11281   440475    39.0 | 15.966 % |
c |    464923 |   14716    49892 |   12722    8951   327865    36.6 | 15.966 % |
c |    470692 |   14716    49892 |   13994    7875   311819    39.6 | 15.966 % |
c |    479342 |   14716    49892 |   15393    9135   378808    41.5 | 15.966 % |
c |    492319 |   14716    49892 |   16933   14076   597895    42.5 | 15.966 % |
c |    511780 |   14716    49892 |   18626   15892   676084    42.5 | 15.966 % |
c |    540973 |   14716    49892 |   20489   15935   734016    46.1 | 15.966 % |
c |    584763 |   14716    49892 |   22538   16904   730313    43.2 | 15.966 % |
c |    650447 |   14692    49838 |   24792   12329   431846    35.0 | 16.162 % |
c ==============================================================================
c [1mFound solution: 481280[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    711494 |   14611    49600 |    4870   22020   991521    45.0 | 16.162 % |
c |    711594 |   14611    49600 |    5357    2853    84659    29.7 | 16.970 % |
c |    711744 |   14414    49120 |    5892    2975    87821    29.5 | 18.953 % |
c |    711970 |   14414    49120 |    6481    3201    94708    29.6 | 18.953 % |
c |    712308 |   14414    49120 |    7130    3539   101066    28.6 | 18.953 % |
c |    712814 |   14414    49120 |    7843    4045   115274    28.5 | 18.953 % |
c ==============================================================================
c [1mFound solution: 475136[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 |    713352 |   14433    49165 |    4811    4583   128721    28.1 | 18.953 % |
c |    713453 |   14433    49165 |    5292    4684   131299    28.0 | 18.943 % |
c |    713603 |   14433    49165 |    5821    4834   134437    27.8 | 18.943 % |
c |    713828 |   14433    49165 |    6403    5059   142634    28.2 | 18.943 % |
c |    714166 |   14433    49165 |    7043    5397   149662    27.7 | 18.943 % |
c |    714672 |   14433    49165 |    7748    5903   168962    28.6 | 18.943 % |
c |    715433 |   14433    49165 |    8522    6664   196629    29.5 | 18.943 % |
c |    716572 |   14433    49165 |    9375    7803   235000    30.1 | 18.943 % |
c |    718280 |   14433    49165 |   10312    9511   309479    32.5 | 18.943 % |
c |    720843 |   14433    49165 |   11344    6341   197795    31.2 | 18.943 % |
c |    724687 |   14433    49165 |   12478   10185   370323    36.4 | 18.943 % |
c |    730458 |   14433    49165 |   13726    9313   347945    37.4 | 18.943 % |
c |    739107 |   14433    49165 |   15098   10660   339720    31.9 | 18.943 % |
c |    752081 |   14433    49165 |   16608   15621   630791    40.4 | 18.943 % |
c ==============================================================================
c [1mFound solution: 456704[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 |    757122 |   14445    49195 |    4815   11976   446697    37.3 | 18.943 % |
c |    757224 |   14445    49195 |    5296    3096    85589    27.6 | 18.950 % |
c |    757374 |   14445    49195 |    5826    3246    89292    27.5 | 18.950 % |
c |    757599 |   14445    49195 |    6408    3471    94156    27.1 | 18.950 % |
c |    757936 |   14445    49195 |    7049    3808   104375    27.4 | 18.950 % |
c |    758443 |   14445    49195 |    7754    4315   123461    28.6 | 18.950 % |
c |    759203 |   14445    49195 |    8530    5075   154197    30.4 | 18.950 % |
c |    760342 |   14445    49195 |    9383    6214   191455    30.8 | 18.950 % |
c |    762050 |   14445    49195 |   10321    7922   251318    31.7 | 18.950 % |
c |    764615 |   14445    49195 |   11353   10487   338625    32.3 | 18.950 % |
c ==============================================================================
c [1mFound solution: 453632[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    764802 |   14451    49209 |    4817   10674   346422    32.5 | 18.950 % |
c |    764902 |   14451    49209 |    5298    5437   149799    27.6 | 18.964 % |
c |    765052 |   14451    49209 |    5828    5587   153476    27.5 | 18.964 % |
c |    765278 |   14451    49209 |    6411    5813   158350    27.2 | 18.964 % |
c |    765615 |   14451    49209 |    7052    6150   165807    27.0 | 18.964 % |
c |    766121 |   14451    49209 |    7757    6656   182693    27.4 | 18.964 % |
c |    766881 |   14451    49209 |    8533    7416   205071    27.7 | 18.964 % |
c |    768021 |   14451    49209 |    9386    8556   243975    28.5 | 18.964 % |
c |    769731 |   14451    49209 |   10325    5153   137206    26.6 | 18.964 % |
c |    772293 |   14451    49209 |   11358    7715   246078    31.9 | 18.964 % |
c |    776137 |   14451    49209 |   12494   11559   414875    35.9 | 18.964 % |
c |    781903 |   14436    49174 |   13743   10642   392600    36.9 | 19.094 % |
c |    790552 |   14436    49174 |   15117   11988   432160    36.0 | 19.094 % |
c |    803527 |   14436    49174 |   16629    8981   311696    34.7 | 19.094 % |
c |    822988 |   14431    49162 |   18292   10946   403382    36.9 | 19.159 % |
c ==============================================================================
c [1mFound solution: 451584[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 |    832643 |   14444    49193 |    4814   10982   402906    36.7 | 19.159 % |
c |    832743 |   14444    49193 |    5295    2846    78918    27.7 | 19.160 % |
c |    832894 |   14444    49193 |    5824    2997    84027    28.0 | 19.160 % |
c |    833119 |   14444    49193 |    6407    3222    93216    28.9 | 19.160 % |
c |    833459 |   14444    49193 |    7048    3562   102262    28.7 | 19.160 % |
c |    833965 |   14444    49193 |    7752    4068   116666    28.7 | 19.160 % |
c |    834724 |   14444    49193 |    8528    4827   140631    29.1 | 19.160 % |
c |    835865 |   14444    49193 |    9381    5968   185649    31.1 | 19.160 % |
c |    837573 |   14444    49193 |   10319    7676   252054    32.8 | 19.160 % |
c |    840135 |   14444    49193 |   11351   10238   361989    35.4 | 19.160 % |
c |    843982 |   14444    49193 |   12486    7814   291623    37.3 | 19.160 % |
c |    849749 |   14444    49193 |   13734    6865   242736    35.4 | 19.160 % |
c |    858398 |   14444    49193 |   15108    8108   298205    36.8 | 19.160 % |
c |    871372 |   14444    49193 |   16619   13082   568606    43.5 | 19.160 % |
c ==============================================================================
c [1mFound solution: 322560[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
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    875958 |   14448    49203 |    4816    8935   343478    38.4 | 19.160 % |
c |    876059 |   14448    49203 |    5297    4569   161756    35.4 | 19.180 % |
c |    876209 |   14448    49203 |    5827    4719   162721    34.5 | 19.180 % |
c |    876434 |   14448    49203 |    6410    4944   164906    33.4 | 19.180 % |
c |    876771 |   14448    49203 |    7051    5281   172776    32.7 | 19.180 % |
c |    877278 |   14448    49203 |    7756    5788   189592    32.8 | 19.180 % |
c |    878038 |   14448    49203 |    8531    6548   209870    32.1 | 19.180 % |
c |    879180 |   14448    49203 |    9385    7690   251121    32.7 | 19.180 % |
c |    880889 |   14448    49203 |   10323    9399   312321    33.2 | 19.180 % |
c |    883451 |   14448    49203 |   11355    6196   191807    31.0 | 19.180 % |
c ==============================================================================
c [1mFound solution: 316416[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    884601 |   14461    49236 |    4820    7346   231741    31.5 | 19.180 % |
c |    884701 |   14461    49236 |    5302    3773   106426    28.2 | 19.187 % |
c |    884851 |   14461    49236 |    5832    3923   108396    27.6 | 19.187 % |
c |    885077 |   14461    49236 |    6415    4149   112424    27.1 | 19.187 % |
c |    885417 |   14461    49236 |    7056    4489   119946    26.7 | 19.187 % |
c |    885923 |   14461    49236 |    7762    4995   140492    28.1 | 19.187 % |
c |    886682 |   14461    49236 |    8538    5754   160406    27.9 | 19.187 % |
c |    887821 |   14461    49236 |    9392    6893   224238    32.5 | 19.187 % |
c |    889531 |   14461    49236 |   10332    8603   335726    39.0 | 19.187 % |
c |    892093 |   14461    49236 |   11365   11165   416598    37.3 | 19.187 % |
c |    895938 |   14457    49227 |   12501    8894   307574    34.6 | 19.252 % |
c |    901705 |   14457    49227 |   13752    7996   271379    33.9 | 19.252 % |
c |    910356 |   14457    49227 |   15127    9399   347794    37.0 | 19.252 % |
c |    923330 |   14452    49216 |   16639   14357   596442    41.5 | 19.316 % |
c |    942791 |   14447    49205 |   18303   16340   676023    41.4 | 19.381 % |
c |    971983 |   14447    49205 |   20134   16562   658864    39.8 | 19.381 % |
c |   1015772 |   14447    49205 |   22147   18097   676749    37.4 | 19.381 % |
#### 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.77 0.94 0.93 2/54 20150
Raw data (stat): 20150 (runsolver) R 20149 24215 24214 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 485390105 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 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+9.99977 s]
Raw data (loadavg): 0.80 0.95 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 1293 0 0 0 994 4 0 0 25 0 1 0 485390105 6770688 1271 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1653 1271 603 41 0 1612 0
vsize: 6612
[startup+19.9994 s]
Raw data (loadavg): 0.83 0.95 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 1439 0 0 0 1994 5 0 0 25 0 1 0 485390105 7442432 1417 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1817 1417 603 41 0 1776 0
vsize: 7268
[startup+30.0002 s]
Raw data (loadavg): 0.86 0.95 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 1552 0 0 0 2993 6 0 0 25 0 1 0 485390105 7987200 1530 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1950 1530 603 41 0 1909 0
vsize: 7800
[startup+39.9999 s]
Raw data (loadavg): 0.88 0.95 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 1552 0 0 0 3993 6 0 0 25 0 1 0 485390105 7987200 1530 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1950 1530 603 41 0 1909 0
vsize: 7800
[startup+50.0007 s]
Raw data (loadavg): 0.90 0.95 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 1552 0 0 0 4993 6 0 0 25 0 1 0 485390105 7987200 1530 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1950 1530 603 41 0 1909 0
vsize: 7800
[startup+60.0004 s]
Raw data (loadavg): 0.91 0.95 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 1552 0 0 0 5993 6 0 0 25 0 1 0 485390105 7987200 1530 4294967295 134512640 134672761 3221224544 3221223712 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1950 1530 603 41 0 1909 0
vsize: 7800
[startup+70.0002 s]
Raw data (loadavg): 0.93 0.95 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 1714 0 0 0 6992 7 0 0 25 0 1 0 485390105 8519680 1692 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2080 1692 603 41 0 2039 0
vsize: 8320
[startup+80.0009 s]
Raw data (loadavg): 0.94 0.95 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 1715 0 0 0 7992 7 0 0 25 0 1 0 485390105 8650752 1693 4294967295 134512640 134672761 3221224544 3221223648 134560477 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2112 1693 603 41 0 2071 0
vsize: 8448
[startup+90.0009 s]
Raw data (loadavg): 0.95 0.95 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 1715 0 0 0 8992 8 0 0 25 0 1 0 485390105 8650752 1693 4294967295 134512640 134672761 3221224544 3221223648 134555116 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2112 1693 603 41 0 2071 0
vsize: 8448
[startup+100.002 s]
Raw data (loadavg): 0.95 0.95 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 1715 0 0 0 9992 8 0 0 25 0 1 0 485390105 8650752 1693 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2112 1693 603 41 0 2071 0
vsize: 8448
[startup+110.002 s]
Raw data (loadavg): 0.96 0.95 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 1721 0 0 0 10992 8 0 0 25 0 1 0 485390105 8650752 1699 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2112 1699 603 41 0 2071 0
vsize: 8448
[startup+120.002 s]
Raw data (loadavg): 0.97 0.96 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 1721 0 0 0 11992 8 0 0 25 0 1 0 485390105 8650752 1699 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2112 1699 603 41 0 2071 0
vsize: 8448
[startup+130.002 s]
Raw data (loadavg): 0.97 0.96 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 1761 0 0 0 12992 8 0 0 25 0 1 0 485390105 8781824 1739 4294967295 134512640 134672761 3221224544 3221223712 134561161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2144 1739 603 41 0 2103 0
vsize: 8576
[startup+140.001 s]
Raw data (loadavg): 0.97 0.96 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 1850 0 0 0 13992 8 0 0 25 0 1 0 485390105 9183232 1828 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2242 1828 603 41 0 2201 0
vsize: 8968
[startup+150.002 s]
Raw data (loadavg): 0.98 0.96 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 1940 0 0 0 14992 8 0 0 25 0 1 0 485390105 9449472 1918 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2307 1918 603 41 0 2266 0
vsize: 9228
[startup+160.002 s]
Raw data (loadavg): 0.98 0.96 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 1943 0 0 0 15992 8 0 0 25 0 1 0 485390105 9588736 1921 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2341 1921 603 41 0 2300 0
vsize: 9364
[startup+170.002 s]
Raw data (loadavg): 0.98 0.96 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 2018 0 0 0 16992 9 0 0 25 0 1 0 485390105 9863168 1996 4294967295 134512640 134672761 3221224544 3221223648 134560287 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2408 1996 603 41 0 2367 0
vsize: 9632
[startup+180.001 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 2170 0 0 0 17992 9 0 0 25 0 1 0 485390105 10399744 2148 4294967295 134512640 134672761 3221224544 3221223712 134560874 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2539 2148 603 41 0 2498 0
vsize: 10156
[startup+190.001 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 2250 0 0 0 18992 10 0 0 25 0 1 0 485390105 10797056 2228 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2636 2228 603 41 0 2595 0
vsize: 10544
[startup+200.001 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 2258 0 0 0 19992 10 0 0 25 0 1 0 485390105 10797056 2236 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2636 2236 603 41 0 2595 0
vsize: 10544
[startup+210.001 s]
Raw data (loadavg): 0.99 0.96 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 2259 0 0 0 20992 10 0 0 25 0 1 0 485390105 10797056 2237 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2636 2237 603 41 0 2595 0
vsize: 10544
[startup+220.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 2267 0 0 0 21992 10 0 0 25 0 1 0 485390105 10797056 2245 4294967295 134512640 134672761 3221224544 3221223728 134559575 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2636 2245 603 41 0 2595 0
vsize: 10544
[startup+230.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 2267 0 0 0 22992 10 0 0 25 0 1 0 485390105 10797056 2245 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2636 2245 603 41 0 2595 0
vsize: 10544
[startup+240.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 2267 0 0 0 23992 10 0 0 25 0 1 0 485390105 10797056 2245 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2636 2245 603 41 0 2595 0
vsize: 10544
[startup+250.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 2389 0 0 0 24992 10 0 0 25 0 1 0 485390105 11329536 2367 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2766 2367 603 41 0 2725 0
vsize: 11064
[startup+260.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 2523 0 0 0 25992 11 0 0 25 0 1 0 485390105 11866112 2501 4294967295 134512640 134672761 3221224544 3221223712 134560806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2897 2501 603 41 0 2856 0
vsize: 11588
[startup+270.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 2526 0 0 0 26992 11 0 0 25 0 1 0 485390105 11866112 2504 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2897 2504 603 41 0 2856 0
vsize: 11588
[startup+280.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 2526 0 0 0 27992 11 0 0 25 0 1 0 485390105 11866112 2504 4294967295 134512640 134672761 3221224544 3221223728 134559161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2897 2504 603 41 0 2856 0
vsize: 11588
[startup+290.003 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 2526 0 0 0 28992 11 0 0 25 0 1 0 485390105 11866112 2504 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2897 2504 603 41 0 2856 0
vsize: 11588
[startup+300.003 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 2533 0 0 0 29993 11 0 0 25 0 1 0 485390105 11866112 2511 4294967295 134512640 134672761 3221224544 3221223712 134560954 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2897 2511 603 41 0 2856 0
vsize: 11588
[startup+310.003 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 2537 0 0 0 30993 11 0 0 25 0 1 0 485390105 12001280 2515 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2930 2515 603 41 0 2889 0
vsize: 11720
[startup+320.003 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 2549 0 0 0 31993 11 0 0 25 0 1 0 485390105 12001280 2527 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2930 2527 603 41 0 2889 0
vsize: 11720
[startup+330.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 2561 0 0 0 32993 11 0 0 25 0 1 0 485390105 12001280 2539 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2930 2539 603 41 0 2889 0
vsize: 11720
[startup+340.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 2582 0 0 0 33993 11 0 0 25 0 1 0 485390105 12165120 2560 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2970 2560 603 41 0 2929 0
vsize: 11880
[startup+350.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 2646 0 0 0 34993 11 0 0 25 0 1 0 485390105 12435456 2624 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3036 2624 603 41 0 2995 0
vsize: 12144
[startup+360.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 2658 0 0 0 35993 11 0 0 25 0 1 0 485390105 12435456 2636 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3036 2636 603 41 0 2995 0
vsize: 12144
[startup+370.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 2711 0 0 0 36993 12 0 0 25 0 1 0 485390105 12709888 2689 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3103 2689 603 41 0 3062 0
vsize: 12412
[startup+380.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 2758 0 0 0 37993 12 0 0 25 0 1 0 485390105 12845056 2736 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3136 2736 603 41 0 3095 0
vsize: 12544
[startup+390.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 2839 0 0 0 38993 12 0 0 25 0 1 0 485390105 13250560 2817 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3235 2817 603 41 0 3194 0
vsize: 12940
[startup+400.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 2858 0 0 0 39993 12 0 0 25 0 1 0 485390105 13393920 2836 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3270 2836 603 41 0 3229 0
vsize: 13080
[startup+410.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 2858 0 0 0 40993 12 0 0 25 0 1 0 485390105 13393920 2836 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3270 2836 603 41 0 3229 0
vsize: 13080
[startup+420.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 2858 0 0 0 41993 13 0 0 25 0 1 0 485390105 13393920 2836 4294967295 134512640 134672761 3221224544 3221223680 134560697 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3270 2836 603 41 0 3229 0
vsize: 13080
[startup+430.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 2861 0 0 0 42993 13 0 0 25 0 1 0 485390105 13393920 2839 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3270 2839 603 41 0 3229 0
vsize: 13080
[startup+440.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 2867 0 0 0 43993 13 0 0 25 0 1 0 485390105 13393920 2845 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3270 2845 603 41 0 3229 0
vsize: 13080
[startup+450.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 2867 0 0 0 44993 13 0 0 25 0 1 0 485390105 13393920 2845 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3270 2845 603 41 0 3229 0
vsize: 13080
[startup+460.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 2867 0 0 0 45993 13 0 0 25 0 1 0 485390105 13393920 2845 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3270 2845 603 41 0 3229 0
vsize: 13080
[startup+470.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 2867 0 0 0 46993 13 0 0 25 0 1 0 485390105 13393920 2845 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3270 2845 603 41 0 3229 0
vsize: 13080
[startup+480.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 2867 0 0 0 47992 13 0 0 25 0 1 0 485390105 13393920 2845 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3270 2845 603 41 0 3229 0
vsize: 13080
[startup+490.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 2867 0 0 0 48992 13 0 0 25 0 1 0 485390105 13393920 2845 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3270 2845 603 41 0 3229 0
vsize: 13080
[startup+500.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 2867 0 0 0 49993 13 0 0 25 0 1 0 485390105 13393920 2845 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3270 2845 603 41 0 3229 0
vsize: 13080
[startup+510.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 2867 0 0 0 50993 13 0 0 25 0 1 0 485390105 13393920 2845 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3270 2845 603 41 0 3229 0
vsize: 13080
[startup+520.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 2867 0 0 0 51993 13 0 0 25 0 1 0 485390105 13393920 2845 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3270 2845 603 41 0 3229 0
vsize: 13080
[startup+530.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 2867 0 0 0 52993 13 0 0 25 0 1 0 485390105 13393920 2845 4294967295 134512640 134672761 3221224544 3221223680 134560697 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3270 2845 603 41 0 3229 0
vsize: 13080
[startup+540.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 2867 0 0 0 53993 13 0 0 25 0 1 0 485390105 13393920 2845 4294967295 134512640 134672761 3221224544 3221223712 134561016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3270 2845 603 41 0 3229 0
vsize: 13080
[startup+550.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 2867 0 0 0 54994 13 0 0 25 0 1 0 485390105 13393920 2845 4294967295 134512640 134672761 3221224544 3221223648 134559869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3270 2845 603 41 0 3229 0
vsize: 13080
[startup+560.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 2867 0 0 0 55994 13 0 0 25 0 1 0 485390105 13393920 2845 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3270 2845 603 41 0 3229 0
vsize: 13080
[startup+570.025 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 2867 0 0 0 56995 13 0 0 25 0 1 0 485390105 13393920 2845 4294967295 134512640 134672761 3221224544 3221223712 134561156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3270 2845 603 41 0 3229 0
vsize: 13080
[startup+580.025 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 2867 0 0 0 57995 13 0 0 25 0 1 0 485390105 13393920 2845 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3270 2845 603 41 0 3229 0
vsize: 13080
[startup+590.024 s]
Raw data (loadavg): 1.07 0.99 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 2867 0 0 0 58996 13 0 0 25 0 1 0 485390105 13393920 2845 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3270 2845 603 41 0 3229 0
vsize: 13080
[startup+600.025 s]
Raw data (loadavg): 1.06 0.99 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 2867 0 0 0 59996 13 0 0 25 0 1 0 485390105 13393920 2845 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3270 2845 603 41 0 3229 0
vsize: 13080
[startup+610.026 s]
Raw data (loadavg): 1.05 0.99 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 2886 0 0 0 60996 13 0 0 25 0 1 0 485390105 13529088 2864 4294967295 134512640 134672761 3221224544 3221223680 134560642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3303 2864 603 41 0 3262 0
vsize: 13212
[startup+620.025 s]
Raw data (loadavg): 1.04 0.99 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 2995 0 0 0 61994 14 0 0 25 0 1 0 485390105 13922304 2973 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3399 2973 603 41 0 3358 0
vsize: 13596
[startup+630.025 s]
Raw data (loadavg): 1.04 0.99 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 2995 0 0 0 62995 14 0 0 25 0 1 0 485390105 13922304 2973 4294967295 134512640 134672761 3221224544 3221223680 134565116 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3399 2973 603 41 0 3358 0
vsize: 13596
[startup+640.133 s]
Raw data (loadavg): 1.03 0.99 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 2998 0 0 0 64006 14 0 0 25 0 1 0 485390105 13922304 2976 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3399 2976 603 41 0 3358 0
vsize: 13596
[startup+650.135 s]
Raw data (loadavg): 1.03 0.99 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 3020 0 0 0 65006 15 0 0 25 0 1 0 485390105 14057472 2998 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3432 2998 603 41 0 3391 0
vsize: 13728
[startup+660.134 s]
Raw data (loadavg): 1.02 0.99 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 3028 0 0 0 66006 15 0 0 25 0 1 0 485390105 14057472 3006 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3432 3006 603 41 0 3391 0
vsize: 13728
[startup+670.134 s]
Raw data (loadavg): 1.02 0.99 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 3080 0 0 0 67006 15 0 0 25 0 1 0 485390105 14323712 3058 4294967295 134512640 134672761 3221224544 3221223712 134560888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3497 3058 603 41 0 3456 0
vsize: 13988
[startup+680.135 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 3087 0 0 0 68006 15 0 0 25 0 1 0 485390105 14323712 3065 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3497 3065 603 41 0 3456 0
vsize: 13988
[startup+690.135 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 3090 0 0 0 69006 15 0 0 25 0 1 0 485390105 14323712 3068 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3497 3068 603 41 0 3456 0
vsize: 13988
[startup+700.136 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 3090 0 0 0 70006 15 0 0 25 0 1 0 485390105 14323712 3068 4294967295 134512640 134672761 3221224544 3221223728 134559367 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3497 3068 603 41 0 3456 0
vsize: 13988
[startup+710.136 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 3096 0 0 0 71007 15 0 0 25 0 1 0 485390105 14323712 3074 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3497 3074 603 41 0 3456 0
vsize: 13988
[startup+720.136 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 3110 0 0 0 72006 15 0 0 25 0 1 0 485390105 14454784 3088 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3529 3088 603 41 0 3488 0
vsize: 14116
[startup+730.136 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 3114 0 0 0 73007 15 0 0 25 0 1 0 485390105 14454784 3092 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3529 3092 603 41 0 3488 0
vsize: 14116
[startup+740.135 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 3138 0 0 0 74007 15 0 0 25 0 1 0 485390105 14594048 3116 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3563 3116 603 41 0 3522 0
vsize: 14252
[startup+750.136 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 3148 0 0 0 75007 15 0 0 25 0 1 0 485390105 14594048 3126 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3563 3126 603 41 0 3522 0
vsize: 14252
[startup+760.136 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 3149 0 0 0 76007 15 0 0 25 0 1 0 485390105 14594048 3127 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3563 3127 603 41 0 3522 0
vsize: 14252
[startup+770.136 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 3156 0 0 0 77007 15 0 0 25 0 1 0 485390105 14594048 3134 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3563 3134 603 41 0 3522 0
vsize: 14252
[startup+780.136 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 3270 0 0 0 78007 16 0 0 25 0 1 0 485390105 15126528 3248 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3693 3248 603 41 0 3652 0
vsize: 14772
[startup+790.136 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 3275 0 0 0 79007 16 0 0 25 0 1 0 485390105 15126528 3253 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3693 3253 603 41 0 3652 0
vsize: 14772
[startup+800.137 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 3393 0 0 0 80007 17 0 0 25 0 1 0 485390105 15654912 3371 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3822 3371 603 41 0 3781 0
vsize: 15288
[startup+810.137 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 3396 0 0 0 81007 17 0 0 25 0 1 0 485390105 15654912 3374 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3822 3374 603 41 0 3781 0
vsize: 15288
[startup+820.137 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 3399 0 0 0 82007 17 0 0 25 0 1 0 485390105 15654912 3377 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3822 3377 603 41 0 3781 0
vsize: 15288
[startup+830.137 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 3408 0 0 0 83007 17 0 0 25 0 1 0 485390105 15654912 3386 4294967295 134512640 134672761 3221224544 3221223680 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3822 3386 603 41 0 3781 0
vsize: 15288
[startup+840.137 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 3408 0 0 0 84007 17 0 0 25 0 1 0 485390105 15654912 3386 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3822 3386 603 41 0 3781 0
vsize: 15288
[startup+850.138 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 3410 0 0 0 85007 17 0 0 25 0 1 0 485390105 15654912 3388 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3822 3388 603 41 0 3781 0
vsize: 15288
[startup+860.137 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 3410 0 0 0 86008 17 0 0 25 0 1 0 485390105 15654912 3388 4294967295 134512640 134672761 3221224544 3221223728 134559376 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3822 3388 603 41 0 3781 0
vsize: 15288
[startup+870.137 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 3410 0 0 0 87008 17 0 0 25 0 1 0 485390105 15654912 3388 4294967295 134512640 134672761 3221224544 3221223648 134560303 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3822 3388 603 41 0 3781 0
vsize: 15288
[startup+880.137 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 3410 0 0 0 88008 17 0 0 25 0 1 0 485390105 15654912 3388 4294967295 134512640 134672761 3221224544 3221223712 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3822 3388 603 41 0 3781 0
vsize: 15288
[startup+890.138 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 3410 0 0 0 89008 17 0 0 25 0 1 0 485390105 15654912 3388 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3822 3388 603 41 0 3781 0
vsize: 15288
[startup+900.139 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 3410 0 0 0 90008 17 0 0 25 0 1 0 485390105 15654912 3388 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3822 3388 603 41 0 3781 0
vsize: 15288
[startup+910.138 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 3410 0 0 0 91008 17 0 0 25 0 1 0 485390105 15654912 3388 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3822 3388 603 41 0 3781 0
vsize: 15288
[startup+920.138 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 3410 0 0 0 92008 17 0 0 25 0 1 0 485390105 15654912 3388 4294967295 134512640 134672761 3221224544 3221223648 134560408 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3822 3388 603 41 0 3781 0
vsize: 15288
[startup+930.138 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 3410 0 0 0 93008 17 0 0 25 0 1 0 485390105 15654912 3388 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3822 3388 603 41 0 3781 0
vsize: 15288
[startup+940.138 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 3410 0 0 0 94009 17 0 0 25 0 1 0 485390105 15654912 3388 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3822 3388 603 41 0 3781 0
vsize: 15288
[startup+950.138 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 3410 0 0 0 95009 17 0 0 25 0 1 0 485390105 15654912 3388 4294967295 134512640 134672761 3221224544 3221223712 134560867 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3822 3388 603 41 0 3781 0
vsize: 15288
[startup+960.139 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 3410 0 0 0 96009 17 0 0 25 0 1 0 485390105 15654912 3388 4294967295 134512640 134672761 3221224544 3221222480 134565859 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3822 3388 603 41 0 3781 0
vsize: 15288
[startup+970.139 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 3410 0 0 0 97009 17 0 0 25 0 1 0 485390105 15654912 3388 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3822 3388 603 41 0 3781 0
vsize: 15288
[startup+980.139 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 3410 0 0 0 98009 17 0 0 25 0 1 0 485390105 15654912 3388 4294967295 134512640 134672761 3221224544 3221223744 134557913 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3822 3388 603 41 0 3781 0
vsize: 15288
[startup+990.138 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 3410 0 0 0 99009 17 0 0 25 0 1 0 485390105 15654912 3388 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3822 3388 603 41 0 3781 0
vsize: 15288
[startup+1000.14 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 3410 0 0 0 100010 17 0 0 25 0 1 0 485390105 15654912 3388 4294967295 134512640 134672761 3221224544 3221223668 134566100 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3822 3388 603 41 0 3781 0
vsize: 15288
[startup+1010.14 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 3410 0 0 0 101010 17 0 0 25 0 1 0 485390105 15654912 3388 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3822 3388 603 41 0 3781 0
vsize: 15288
[startup+1020.14 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 3410 0 0 0 102010 17 0 0 25 0 1 0 485390105 15654912 3388 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3822 3388 603 41 0 3781 0
vsize: 15288
[startup+1030.14 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 3410 0 0 0 103010 17 0 0 25 0 1 0 485390105 15654912 3388 4294967295 134512640 134672761 3221224544 3221223636 1075346988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3822 3388 603 41 0 3781 0
vsize: 15288
[startup+1040.14 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 3410 0 0 0 104010 17 0 0 25 0 1 0 485390105 15654912 3388 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3822 3388 603 41 0 3781 0
vsize: 15288
[startup+1050.14 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 3410 0 0 0 105010 17 0 0 25 0 1 0 485390105 15654912 3388 4294967295 134512640 134672761 3221224544 3221223728 134558914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3822 3388 603 41 0 3781 0
vsize: 15288
[startup+1060.14 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 3410 0 0 0 106011 17 0 0 25 0 1 0 485390105 15654912 3388 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3822 3388 603 41 0 3781 0
vsize: 15288
[startup+1070.14 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 3410 0 0 0 107011 17 0 0 25 0 1 0 485390105 15654912 3388 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3822 3388 603 41 0 3781 0
vsize: 15288
[startup+1080.14 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 3410 0 0 0 108011 17 0 0 25 0 1 0 485390105 15654912 3388 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3822 3388 603 41 0 3781 0
vsize: 15288
[startup+1090.14 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 3410 0 0 0 109011 17 0 0 25 0 1 0 485390105 15654912 3388 4294967295 134512640 134672761 3221224544 3221223712 134561148 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3822 3388 603 41 0 3781 0
vsize: 15288
[startup+1100.14 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 3410 0 0 0 110011 17 0 0 25 0 1 0 485390105 15654912 3388 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3822 3388 603 41 0 3781 0
vsize: 15288
[startup+1110.14 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 3410 0 0 0 111012 17 0 0 25 0 1 0 485390105 15654912 3388 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3822 3388 603 41 0 3781 0
vsize: 15288
[startup+1120.14 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 3410 0 0 0 112012 17 0 0 25 0 1 0 485390105 15654912 3388 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3822 3388 603 41 0 3781 0
vsize: 15288
[startup+1130.14 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 3410 0 0 0 113012 17 0 0 25 0 1 0 485390105 15654912 3388 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3822 3388 603 41 0 3781 0
vsize: 15288
[startup+1140.14 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 3410 0 0 0 114012 17 0 0 25 0 1 0 485390105 15654912 3388 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3822 3388 603 41 0 3781 0
vsize: 15288
[startup+1150.14 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 3410 0 0 0 115012 17 0 0 25 0 1 0 485390105 15654912 3388 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3822 3388 603 41 0 3781 0
vsize: 15288
[startup+1160.14 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 3410 0 0 0 116012 17 0 0 25 0 1 0 485390105 15654912 3388 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3822 3388 603 41 0 3781 0
vsize: 15288
[startup+1170.14 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 3411 0 0 0 117013 17 0 0 25 0 1 0 485390105 15654912 3389 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3822 3389 603 41 0 3781 0
vsize: 15288
[startup+1180.14 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 3434 0 0 0 118012 18 0 0 25 0 1 0 485390105 15790080 3412 4294967295 134512640 134672761 3221224544 3221223500 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3855 3412 603 41 0 3814 0
vsize: 15420
[startup+1190.14 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 3592 0 0 0 119012 18 0 0 25 0 1 0 485390105 16453632 3570 4294967295 134512640 134672761 3221224544 3221223728 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4017 3570 603 41 0 3976 0
vsize: 16068
[startup+1200.14 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 20150
Raw data (stat): 20150 (minisat+) R 20149 24215 24214 0 -1 0 3592 0 0 0 120013 18 0 0 25 0 1 0 485390105 16453632 3570 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4017 3570 603 41 0 3976 0
vsize: 16068
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.15 s]
Raw data (loadavg): 1.00 0.99 0.93 1/54 20150
Raw data (stat): 20150 (minisat+) Z 20149 24215 24214 0 -1 12 3595 0 0 0 120013 18 0 0 25 0 1 0 485390105 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.15
CPU time (s): 1200.32
CPU user time (s): 1200.13
CPU system time (s): 0.189971
CPU usage (%): 100.014
Max. virtual memory (Kb): 16068
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####