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 21390

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc5 THE 2005-04-21 23:38:37 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=13520 boxname=wulflinc5 idbench=1040 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  c8b965306fec2c21edee64824d12f378  /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: 13520
/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:        564864 kB
Buffers:         30100 kB
Cached:         418256 kB
SwapCached:        444 kB
Active:          90972 kB
Inactive:       359500 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        564612 kB
SwapTotal:     2097136 kB
SwapFree:      2095948 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5200 kB
Slab:            13708 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 23:58:39 (client local time) WITH STATUS 10 IN 1200.22 SECONDS
stats: 13520 7 1200.22 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.56 0.84 0.88 2/54 5315
Raw data (stat): 5315 (runsolver) R 5314 24215 24214 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 490881606 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99995 s]
Raw data (loadavg): 0.63 0.85 0.88 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 1302 0 0 0 995 3 0 0 25 0 1 0 490881606 6905856 1280 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1686 1280 603 41 0 1645 0
vsize: 6744
[startup+20.0011 s]
Raw data (loadavg): 0.69 0.85 0.88 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 1439 0 0 0 1995 3 0 0 25 0 1 0 490881606 7442432 1417 4294967295 134512640 134672761 3221224544 3221223712 134560983 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.0014 s]
Raw data (loadavg): 0.73 0.85 0.88 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 1552 0 0 0 2995 4 0 0 25 0 1 0 490881606 7987200 1530 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1950 1530 603 41 0 1909 0
vsize: 7800
[startup+40.0022 s]
Raw data (loadavg): 0.77 0.86 0.88 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 1552 0 0 0 3994 4 0 0 25 0 1 0 490881606 7987200 1530 4294967295 134512640 134672761 3221224544 3221223712 134561167 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.0034 s]
Raw data (loadavg): 0.81 0.86 0.88 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 1552 0 0 0 4994 4 0 0 25 0 1 0 490881606 7987200 1530 4294967295 134512640 134672761 3221224544 3221223680 134565080 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.0027 s]
Raw data (loadavg): 0.84 0.87 0.88 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 1552 0 0 0 5994 5 0 0 25 0 1 0 490881606 7987200 1530 4294967295 134512640 134672761 3221224544 3221223712 134561011 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.0039 s]
Raw data (loadavg): 0.86 0.87 0.88 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 1715 0 0 0 6993 6 0 0 25 0 1 0 490881606 8650752 1693 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2112 1693 603 41 0 2071 0
vsize: 8448
[startup+80.0046 s]
Raw data (loadavg): 0.88 0.87 0.88 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 1715 0 0 0 7993 6 0 0 25 0 1 0 490881606 8650752 1693 4294967295 134512640 134672761 3221224544 3221223712 134560912 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.0049 s]
Raw data (loadavg): 0.90 0.88 0.88 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 1715 0 0 0 8993 7 0 0 25 0 1 0 490881606 8650752 1693 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2112 1693 603 41 0 2071 0
vsize: 8448
[startup+100.005 s]
Raw data (loadavg): 0.91 0.88 0.89 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 1715 0 0 0 9992 7 0 0 25 0 1 0 490881606 8650752 1693 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2112 1693 603 41 0 2071 0
vsize: 8448
[startup+110.005 s]
Raw data (loadavg): 0.93 0.89 0.89 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 1721 0 0 0 10992 7 0 0 25 0 1 0 490881606 8650752 1699 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2112 1699 603 41 0 2071 0
vsize: 8448
[startup+120.005 s]
Raw data (loadavg): 0.94 0.89 0.89 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 1721 0 0 0 11992 7 0 0 25 0 1 0 490881606 8650752 1699 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2112 1699 603 41 0 2071 0
vsize: 8448
[startup+130.005 s]
Raw data (loadavg): 0.95 0.89 0.89 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 1801 0 0 0 12992 8 0 0 25 0 1 0 490881606 8912896 1779 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2176 1779 603 41 0 2135 0
vsize: 8704
[startup+140.007 s]
Raw data (loadavg): 0.95 0.89 0.89 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 1850 0 0 0 13992 8 0 0 25 0 1 0 490881606 9183232 1828 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2242 1828 603 41 0 2201 0
vsize: 8968
[startup+150.007 s]
Raw data (loadavg): 0.96 0.90 0.89 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 1940 0 0 0 14991 9 0 0 25 0 1 0 490881606 9449472 1918 4294967295 134512640 134672761 3221224544 3221223648 134560344 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2307 1918 603 41 0 2266 0
vsize: 9228
[startup+160.007 s]
Raw data (loadavg): 0.97 0.90 0.89 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 2000 0 0 0 15990 9 0 0 25 0 1 0 490881606 9719808 1978 4294967295 134512640 134672761 3221224544 3221223680 134560714 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2373 1978 603 41 0 2332 0
vsize: 9492
[startup+170.008 s]
Raw data (loadavg): 0.97 0.90 0.89 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 2049 0 0 0 16990 9 0 0 25 0 1 0 490881606 9998336 2027 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2441 2027 603 41 0 2400 0
vsize: 9764
[startup+180.007 s]
Raw data (loadavg): 0.98 0.91 0.89 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 2170 0 0 0 17990 10 0 0 25 0 1 0 490881606 10399744 2148 4294967295 134512640 134672761 3221224544 3221223648 134560184 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.008 s]
Raw data (loadavg): 0.98 0.91 0.89 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 2253 0 0 0 18990 10 0 0 25 0 1 0 490881606 10797056 2231 4294967295 134512640 134672761 3221224544 3221223500 1075350790 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2636 2231 603 41 0 2595 0
vsize: 10544
[startup+200.008 s]
Raw data (loadavg): 0.98 0.91 0.90 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 2258 0 0 0 19990 10 0 0 25 0 1 0 490881606 10797056 2236 4294967295 134512640 134672761 3221224544 3221223712 134560830 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.008 s]
Raw data (loadavg): 0.98 0.91 0.90 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 2266 0 0 0 20990 10 0 0 25 0 1 0 490881606 10797056 2244 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2636 2244 603 41 0 2595 0
vsize: 10544
[startup+220.008 s]
Raw data (loadavg): 0.99 0.92 0.90 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 2267 0 0 0 21990 10 0 0 25 0 1 0 490881606 10797056 2245 4294967295 134512640 134672761 3221224544 3221223744 134557852 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.008 s]
Raw data (loadavg): 0.99 0.92 0.90 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 2267 0 0 0 22990 10 0 0 25 0 1 0 490881606 10797056 2245 4294967295 134512640 134672761 3221224544 3221223648 134554744 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.009 s]
Raw data (loadavg): 0.99 0.92 0.90 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 2314 0 0 0 23990 11 0 0 25 0 1 0 490881606 11063296 2292 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2701 2292 603 41 0 2660 0
vsize: 10804
[startup+250.009 s]
Raw data (loadavg): 0.99 0.92 0.90 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 2392 0 0 0 24990 11 0 0 25 0 1 0 490881606 11329536 2370 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2766 2370 603 41 0 2725 0
vsize: 11064
[startup+260.009 s]
Raw data (loadavg): 0.99 0.92 0.90 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 2523 0 0 0 25990 11 0 0 25 0 1 0 490881606 11866112 2501 4294967295 134512640 134672761 3221224544 3221223712 134561229 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.009 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 2526 0 0 0 26990 11 0 0 25 0 1 0 490881606 11866112 2504 4294967295 134512640 134672761 3221224544 3221223712 134561229 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.009 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 2526 0 0 0 27990 11 0 0 25 0 1 0 490881606 11866112 2504 4294967295 134512640 134672761 3221224544 3221223712 134560892 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.01 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 2526 0 0 0 28991 11 0 0 25 0 1 0 490881606 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.01 s]
Raw data (loadavg): 0.99 0.93 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 2533 0 0 0 29991 11 0 0 25 0 1 0 490881606 11866112 2511 4294967295 134512640 134672761 3221224544 3221223696 134561035 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.031 s]
Raw data (loadavg): 1.07 0.95 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 2544 0 0 0 30993 11 0 0 25 0 1 0 490881606 12001280 2522 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2930 2522 603 41 0 2889 0
vsize: 11720
[startup+320.031 s]
Raw data (loadavg): 1.06 0.95 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 2554 0 0 0 31993 11 0 0 25 0 1 0 490881606 12001280 2532 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2930 2532 603 41 0 2889 0
vsize: 11720
[startup+330.031 s]
Raw data (loadavg): 1.05 0.95 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 2561 0 0 0 32993 11 0 0 25 0 1 0 490881606 12001280 2539 4294967295 134512640 134672761 3221224544 3221223712 134561229 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.031 s]
Raw data (loadavg): 1.04 0.95 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 2638 0 0 0 33993 12 0 0 25 0 1 0 490881606 12435456 2616 4294967295 134512640 134672761 3221224544 3221223712 134561025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3036 2616 603 41 0 2995 0
vsize: 12144
[startup+350.031 s]
Raw data (loadavg): 1.03 0.95 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 2653 0 0 0 34994 12 0 0 25 0 1 0 490881606 12435456 2631 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3036 2631 603 41 0 2995 0
vsize: 12144
[startup+360.031 s]
Raw data (loadavg): 1.03 0.95 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 2700 0 0 0 35994 12 0 0 25 0 1 0 490881606 12570624 2678 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3069 2678 603 41 0 3028 0
vsize: 12276
[startup+370.032 s]
Raw data (loadavg): 1.02 0.96 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 2718 0 0 0 36994 12 0 0 25 0 1 0 490881606 12709888 2696 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3103 2696 603 41 0 3062 0
vsize: 12412
[startup+380.032 s]
Raw data (loadavg): 1.02 0.96 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 2839 0 0 0 37994 12 0 0 25 0 1 0 490881606 13250560 2817 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3235 2817 603 41 0 3194 0
vsize: 12940
[startup+390.032 s]
Raw data (loadavg): 1.02 0.96 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 2840 0 0 0 38994 12 0 0 25 0 1 0 490881606 13250560 2818 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3235 2818 603 41 0 3194 0
vsize: 12940
[startup+400.033 s]
Raw data (loadavg): 1.01 0.96 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 2858 0 0 0 39994 12 0 0 25 0 1 0 490881606 13393920 2836 4294967295 134512640 134672761 3221224544 3221223712 134560898 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.033 s]
Raw data (loadavg): 1.01 0.96 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 2858 0 0 0 40994 12 0 0 25 0 1 0 490881606 13393920 2836 4294967295 134512640 134672761 3221224544 3221223712 134561190 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.033 s]
Raw data (loadavg): 1.01 0.96 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 2858 0 0 0 41994 12 0 0 25 0 1 0 490881606 13393920 2836 4294967295 134512640 134672761 3221224544 3221223668 134566037 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.034 s]
Raw data (loadavg): 1.01 0.96 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 2867 0 0 0 42994 12 0 0 25 0 1 0 490881606 13393920 2845 4294967295 134512640 134672761 3221224544 3221223712 134560906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3270 2845 603 41 0 3229 0
vsize: 13080
[startup+440.034 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 2867 0 0 0 43995 12 0 0 25 0 1 0 490881606 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+450.034 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 2867 0 0 0 44995 12 0 0 25 0 1 0 490881606 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.033 s]
Raw data (loadavg): 1.00 0.96 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 2867 0 0 0 45994 12 0 0 25 0 1 0 490881606 13393920 2845 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3270 2845 603 41 0 3229 0
vsize: 13080
[startup+470.034 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 2867 0 0 0 46995 12 0 0 25 0 1 0 490881606 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+480.034 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 2867 0 0 0 47995 13 0 0 25 0 1 0 490881606 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+490.035 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 2867 0 0 0 48995 13 0 0 25 0 1 0 490881606 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+500.035 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 2867 0 0 0 49995 13 0 0 25 0 1 0 490881606 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+510.034 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 2867 0 0 0 50995 13 0 0 25 0 1 0 490881606 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+520.035 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 2867 0 0 0 51995 13 0 0 25 0 1 0 490881606 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+530.035 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 2867 0 0 0 52995 13 0 0 25 0 1 0 490881606 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+540.035 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 2867 0 0 0 53995 13 0 0 25 0 1 0 490881606 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+550.035 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 2867 0 0 0 54995 13 0 0 25 0 1 0 490881606 13393920 2845 4294967295 134512640 134672761 3221224544 3221223696 134561249 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.035 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 2867 0 0 0 55995 13 0 0 25 0 1 0 490881606 13393920 2845 4294967295 134512640 134672761 3221224544 3221223712 134560858 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.036 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 2867 0 0 0 56996 13 0 0 25 0 1 0 490881606 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+580.035 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 2867 0 0 0 57996 13 0 0 25 0 1 0 490881606 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+590.036 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 2867 0 0 0 58996 13 0 0 25 0 1 0 490881606 13393920 2845 4294967295 134512640 134672761 3221224544 3221223712 134561375 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.036 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 2883 0 0 0 59996 13 0 0 25 0 1 0 490881606 13393920 2861 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3270 2861 603 41 0 3229 0
vsize: 13080
[startup+610.036 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 2940 0 0 0 60996 13 0 0 25 0 1 0 490881606 13660160 2918 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3335 2918 603 41 0 3294 0
vsize: 13340
[startup+620.037 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 2995 0 0 0 61996 13 0 0 25 0 1 0 490881606 13922304 2973 4294967295 134512640 134672761 3221224544 3221223728 134558899 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.036 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 2998 0 0 0 62996 13 0 0 25 0 1 0 490881606 13922304 2976 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3399 2976 603 41 0 3358 0
vsize: 13596
[startup+640.037 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 2998 0 0 0 63996 14 0 0 25 0 1 0 490881606 13922304 2976 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3399 2976 603 41 0 3358 0
vsize: 13596
[startup+650.038 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 3028 0 0 0 64996 14 0 0 25 0 1 0 490881606 14057472 3006 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3432 3006 603 41 0 3391 0
vsize: 13728
[startup+660.037 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 3080 0 0 0 65996 14 0 0 25 0 1 0 490881606 14323712 3058 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3497 3058 603 41 0 3456 0
vsize: 13988
[startup+670.037 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 3083 0 0 0 66996 14 0 0 25 0 1 0 490881606 14323712 3061 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3497 3061 603 41 0 3456 0
vsize: 13988
[startup+680.038 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 3090 0 0 0 67996 14 0 0 25 0 1 0 490881606 14323712 3068 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3497 3068 603 41 0 3456 0
vsize: 13988
[startup+690.039 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 3090 0 0 0 68996 14 0 0 25 0 1 0 490881606 14323712 3068 4294967295 134512640 134672761 3221224544 3221223712 134560898 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.038 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 3094 0 0 0 69996 14 0 0 25 0 1 0 490881606 14323712 3072 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3497 3072 603 41 0 3456 0
vsize: 13988
[startup+710.038 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 3110 0 0 0 70996 14 0 0 25 0 1 0 490881606 14454784 3088 4294967295 134512640 134672761 3221224544 3221223680 134560675 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3529 3088 603 41 0 3488 0
vsize: 14116
[startup+720.039 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 3113 0 0 0 71996 14 0 0 25 0 1 0 490881606 14454784 3091 4294967295 134512640 134672761 3221224544 3221223728 134558875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3529 3091 603 41 0 3488 0
vsize: 14116
[startup+730.039 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 3125 0 0 0 72997 14 0 0 25 0 1 0 490881606 14454784 3103 4294967295 134512640 134672761 3221224544 3221223712 134560882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3529 3103 603 41 0 3488 0
vsize: 14116
[startup+740.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 3138 0 0 0 73997 14 0 0 25 0 1 0 490881606 14594048 3116 4294967295 134512640 134672761 3221224544 3221223712 134560898 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.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 3149 0 0 0 74997 14 0 0 25 0 1 0 490881606 14594048 3127 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3563 3127 603 41 0 3522 0
vsize: 14252
[startup+760.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 3156 0 0 0 75997 14 0 0 25 0 1 0 490881606 14594048 3134 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3563 3134 603 41 0 3522 0
vsize: 14252
[startup+770.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 3263 0 0 0 76997 15 0 0 25 0 1 0 490881606 15126528 3241 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3693 3241 603 41 0 3652 0
vsize: 14772
[startup+780.039 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 3275 0 0 0 77997 15 0 0 25 0 1 0 490881606 15126528 3253 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3693 3253 603 41 0 3652 0
vsize: 14772
[startup+790.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 3393 0 0 0 78997 15 0 0 25 0 1 0 490881606 15654912 3371 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3822 3371 603 41 0 3781 0
vsize: 15288
[startup+800.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 3396 0 0 0 79997 15 0 0 25 0 1 0 490881606 15654912 3374 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3822 3374 603 41 0 3781 0
vsize: 15288
[startup+810.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 3399 0 0 0 80997 15 0 0 25 0 1 0 490881606 15654912 3377 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3822 3377 603 41 0 3781 0
vsize: 15288
[startup+820.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 3408 0 0 0 81997 15 0 0 25 0 1 0 490881606 15654912 3386 4294967295 134512640 134672761 3221224544 3221223712 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3822 3386 603 41 0 3781 0
vsize: 15288
[startup+830.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 3408 0 0 0 82997 15 0 0 25 0 1 0 490881606 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+840.041 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 3410 0 0 0 83997 16 0 0 25 0 1 0 490881606 15654912 3388 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3822 3388 603 41 0 3781 0
vsize: 15288
[startup+850.041 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 3410 0 0 0 84998 16 0 0 25 0 1 0 490881606 15654912 3388 4294967295 134512640 134672761 3221224544 3221223712 134561205 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.041 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 3410 0 0 0 85998 16 0 0 25 0 1 0 490881606 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+870.041 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 3410 0 0 0 86998 16 0 0 25 0 1 0 490881606 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+880.041 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 3410 0 0 0 87998 16 0 0 25 0 1 0 490881606 15654912 3388 4294967295 134512640 134672761 3221224544 3221223680 134565110 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.042 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 3410 0 0 0 88998 16 0 0 25 0 1 0 490881606 15654912 3388 4294967295 134512640 134672761 3221224544 3221223712 134561205 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.041 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 3410 0 0 0 89999 16 0 0 25 0 1 0 490881606 15654912 3388 4294967295 134512640 134672761 3221224544 3221223712 134560869 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.041 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 3410 0 0 0 90999 16 0 0 25 0 1 0 490881606 15654912 3388 4294967295 134512640 134672761 3221224544 3221223712 134561229 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.042 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 3410 0 0 0 91999 16 0 0 25 0 1 0 490881606 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+930.043 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 3410 0 0 0 92999 16 0 0 25 0 1 0 490881606 15654912 3388 4294967295 134512640 134672761 3221224544 3221223712 134560929 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.043 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 3410 0 0 0 93999 16 0 0 25 0 1 0 490881606 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+950.043 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 3410 0 0 0 95000 16 0 0 25 0 1 0 490881606 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+960.043 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 3410 0 0 0 96000 16 0 0 25 0 1 0 490881606 15654912 3388 4294967295 134512640 134672761 3221224544 3221223712 134560839 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.043 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 3410 0 0 0 97000 16 0 0 25 0 1 0 490881606 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+980.043 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 3410 0 0 0 98000 16 0 0 25 0 1 0 490881606 15654912 3388 4294967295 134512640 134672761 3221224544 3221223712 134560869 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.043 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 3410 0 0 0 99000 16 0 0 25 0 1 0 490881606 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+1000.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 3410 0 0 0 100000 16 0 0 25 0 1 0 490881606 15654912 3388 4294967295 134512640 134672761 3221224544 3221223728 134559161 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.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 3410 0 0 0 101000 16 0 0 25 0 1 0 490881606 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+1020.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 3410 0 0 0 102001 16 0 0 25 0 1 0 490881606 15654912 3388 4294967295 134512640 134672761 3221224544 3221223648 134560196 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.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 3410 0 0 0 103001 16 0 0 25 0 1 0 490881606 15654912 3388 4294967295 134512640 134672761 3221224544 3221223712 134560999 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.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 3410 0 0 0 104001 16 0 0 25 0 1 0 490881606 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+1050.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 3410 0 0 0 105001 16 0 0 25 0 1 0 490881606 15654912 3388 4294967295 134512640 134672761 3221224544 3221223712 134560983 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.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 3410 0 0 0 106001 16 0 0 25 0 1 0 490881606 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.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 3410 0 0 0 107001 16 0 0 25 0 1 0 490881606 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.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 3410 0 0 0 108002 16 0 0 25 0 1 0 490881606 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+1090.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 3410 0 0 0 109002 16 0 0 25 0 1 0 490881606 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+1100.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 3410 0 0 0 110002 16 0 0 25 0 1 0 490881606 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+1110.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 3410 0 0 0 111002 16 0 0 25 0 1 0 490881606 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+1120.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 3410 0 0 0 112002 16 0 0 25 0 1 0 490881606 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.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 3410 0 0 0 113003 16 0 0 25 0 1 0 490881606 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.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 3410 0 0 0 114003 16 0 0 25 0 1 0 490881606 15654912 3388 4294967295 134512640 134672761 3221224544 3221223648 134554671 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.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 3410 0 0 0 115003 16 0 0 25 0 1 0 490881606 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+1160.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 3411 0 0 0 116003 16 0 0 25 0 1 0 490881606 15654912 3389 4294967295 134512640 134672761 3221224544 3221223680 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3822 3389 603 41 0 3781 0
vsize: 15288
[startup+1170.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 3522 0 0 0 117003 16 0 0 25 0 1 0 490881606 16191488 3500 4294967295 134512640 134672761 3221224544 3221223692 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3953 3500 603 41 0 3912 0
vsize: 15812
[startup+1180.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 3592 0 0 0 118003 17 0 0 25 0 1 0 490881606 16453632 3570 4294967295 134512640 134672761 3221224544 3221223712 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4017 3570 603 41 0 3976 0
vsize: 16068
[startup+1190.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 3598 0 0 0 119003 17 0 0 25 0 1 0 490881606 16453632 3576 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4017 3576 603 41 0 3976 0
vsize: 16068
[startup+1200.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 5315
Raw data (stat): 5315 (minisat+) R 5314 24215 24214 0 -1 0 3598 0 0 0 120003 17 0 0 25 0 1 0 490881606 16453632 3576 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4017 3576 603 41 0 3976 0
vsize: 16068
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 1.00 0.97 0.91 1/54 5315
Raw data (stat): 5315 (minisat+) Z 5314 24215 24214 0 -1 12 3601 0 0 0 120003 18 0 0 25 0 1 0 490881606 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.06
CPU time (s): 1200.22
CPU user time (s): 1200.03
CPU system time (s): 0.181972
CPU usage (%): 100.013
Max. virtual memory (Kb): 16068
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####