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-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-markshare1.opb
MD5SUM	ba87f5dfbaed559dc55bc00bf07dc880
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	3712
Optimality of the best value was proved	NO
Number of terms in the objective function	120
Biggest coefficient in the objective function	524288
Number of bits for the biggest coefficient in the objective function	20
Sum of the numbers in the objective function	6291450
Number of bits of the sum of numbers in the objective function	23
Biggest number in a constraint	524288
Number of bits of the biggest number in a constraint	20
Biggest sum of numbers in a constraint	6291450
Number of bits of the biggest sum of numbers	23
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.68
Number of variables	170
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	70
Trace number 15128

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.220
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        813980 kB
Buffers:         11048 kB
Cached:         189820 kB
SwapCached:        820 kB
Active:          35296 kB
Inactive:       167580 kB
HighTotal:      131008 kB
HighFree:        23688 kB
LowTotal:       903652 kB
LowFree:        790292 kB
SwapTotal:     2097892 kB
SwapFree:      2096248 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5016 kB
Slab:            12216 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 03:18:51 (client local time) WITH STATUS 10 IN 1200.21 SECONDS
stats: 18509 7 1200.21 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: 405119   bits: 20/19
c ---[   8]---> Adder-cost: 314   maxlim: 431743   bits: 20/19
c ---[   6]---> Adder-cost: 348   maxlim: 435327   bits: 20/19
c ---[   4]---> Adder-cost: 318   maxlim: 411775   bits: 20/19
c ---[   2]---> Adder-cost: 312   maxlim: 410751   bits: 20/19
c ---[   0]---> Adder-cost: 314   maxlim: 411135   bits: 20/19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   12820    45524 |    4273       0        0     nan |  0.000 % |
c |       100 |   12820    45524 |    4700     100      583     5.8 | 11.212 % |
c ==============================================================================
c [1mFound solution: 511232[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 110   maxlim: 8288   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       115 |   13523    48038 |    4507     115      713     6.2 | 11.212 % |
c |       215 |   13515    48012 |    4957     214     5912    27.6 | 11.010 % |
c ==============================================================================
c [1mFound solution: 503680[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 8347   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       348 |   13531    48096 |    4510     347    16026    46.2 | 11.010 % |
c |       448 |   13523    48070 |    4961     446    28545    64.0 | 11.207 % |
c |       599 |   13523    48070 |    5457     597    42809    71.7 | 11.207 % |
c |       824 |   13523    48070 |    6002     822    66235    80.6 | 11.207 % |
c ==============================================================================
c [1mFound solution: 456704[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 8714   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1042 |   13535    48141 |    4511    1040    75625    72.7 | 11.207 % |
c ==============================================================================
c [1mFound solution: 455808[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 8721   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1079 |   13538    48164 |    4512    1077    77579    72.0 | 11.207 % |
c |      1179 |   13538    48164 |    4963    1177    88739    75.4 | 11.432 % |
c |      1329 |   13538    48164 |    5459    1327   105274    79.3 | 11.432 % |
c |      1556 |   13538    48164 |    6005    1554   122467    78.8 | 11.432 % |
c |      1894 |   13538    48164 |    6606    1892   144685    76.5 | 11.432 % |
c ==============================================================================
c [1mFound solution: 383232[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 9288   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2069 |   13549    48219 |    4516    2067   159419    77.1 | 11.432 % |
c |      2169 |   13549    48219 |    4967    2167   169791    78.4 | 11.570 % |
c |      2321 |   13549    48219 |    5464    2319   185407    80.0 | 11.570 % |
c |      2548 |   13549    48219 |    6010    2546   200655    78.8 | 11.570 % |
c |      2885 |   13549    48219 |    6611    2883   229403    79.6 | 11.570 % |
c |      3391 |   13549    48219 |    7273    3389   265847    78.4 | 11.570 % |
c |      4150 |   13533    48167 |    8000    4146   321237    77.5 | 11.656 % |
c ==============================================================================
c [1mFound solution: 364288[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 9436   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4517 |   13544    48235 |    4514    4513   356795    79.1 | 11.656 % |
c |      4618 |   13544    48235 |    4965    4614   368915    80.0 | 11.868 % |
c |      4768 |   13544    48235 |    5461    4764   379005    79.6 | 11.868 % |
c |      4994 |   13544    48235 |    6008    4990   390119    78.2 | 11.868 % |
c |      5332 |   13544    48235 |    6608    5328   416527    78.2 | 11.868 % |
c |      5838 |   13544    48235 |    7269    5834   458111    78.5 | 11.868 % |
c |      6597 |   13544    48235 |    7996    6593   514456    78.0 | 11.868 % |
c |      7736 |   13544    48235 |    8796    7732   587098    75.9 | 11.868 % |
c |      9445 |   13536    48209 |    9676    9440   719576    76.2 | 11.911 % |
c |     12009 |   13528    48183 |   10643    6758   492981    72.9 | 11.954 % |
c |     15853 |   13528    48183 |   11708   10602   783975    73.9 | 11.954 % |
c |     21619 |   13514    48143 |   12878    9988   709104    71.0 | 12.082 % |
c ==============================================================================
c [1mFound solution: 335360[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 9662   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     23589 |   13527    48235 |    4509   11958   863512    72.2 | 12.082 % |
c |     23690 |   13527    48235 |    4959    3091   167808    54.3 | 12.377 % |
c |     23842 |   13527    48235 |    5455    3243   175273    54.0 | 12.377 % |
c |     24067 |   13527    48235 |    6001    3468   196191    56.6 | 12.377 % |
c |     24406 |   13527    48235 |    6601    3807   218204    57.3 | 12.377 % |
c |     24912 |   13519    48209 |    7261    4312   254982    59.1 | 12.420 % |
c |     25672 |   13511    48183 |    7987    5071   316388    62.4 | 12.463 % |
c |     26811 |   13503    48157 |    8786    6209   386730    62.3 | 12.505 % |
c ==============================================================================
c [1mFound solution: 310016[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 9860   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27516 |   13500    48167 |    4500    6913   429968    62.2 | 12.505 % |
c |     27617 |   13500    48167 |    4950    3558   171002    48.1 | 12.692 % |
c |     27767 |   13500    48167 |    5445    3708   187587    50.6 | 12.692 % |
c |     27992 |   13500    48167 |    5989    3933   206290    52.5 | 12.692 % |
c |     28330 |   13500    48167 |    6588    4271   228093    53.4 | 12.692 % |
c |     28836 |   13500    48167 |    7247    4777   268210    56.1 | 12.692 % |
c |     29597 |   13500    48167 |    7972    5538   303899    54.9 | 12.692 % |
c |     30738 |   13500    48167 |    8769    6679   359293    53.8 | 12.692 % |
c |     32446 |   13492    48141 |    9646    8386   462548    55.2 | 12.734 % |
c |     35008 |   13492    48141 |   10610    5647   368183    65.2 | 12.734 % |
c ==============================================================================
c [1mFound solution: 267904[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 10189   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     37998 |   13500    48195 |    4500    8637   496764    57.5 | 12.734 % |
c |     38098 |   13500    48195 |    4950    4419   149234    33.8 | 12.946 % |
c |     38248 |   13500    48195 |    5445    4569   163668    35.8 | 12.946 % |
c |     38475 |   13500    48195 |    5989    4796   181974    37.9 | 12.946 % |
c |     38814 |   13500    48195 |    6588    5135   205638    40.0 | 12.946 % |
c |     39321 |   13500    48195 |    7247    5642   238996    42.4 | 12.946 % |
c |     40080 |   13500    48195 |    7972    6401   299534    46.8 | 12.946 % |
c |     41219 |   13500    48195 |    8769    7540   385271    51.1 | 12.946 % |
c |     42928 |   13500    48195 |    9646    9249   523733    56.6 | 12.946 % |
c |     45490 |   13500    48195 |   10610    6515   412888    63.4 | 12.946 % |
c |     49336 |   13492    48173 |   11671   10360   589091    56.9 | 13.031 % |
c |     55102 |   13492    48173 |   12839    9980   406807    40.8 | 13.031 % |
c ==============================================================================
c [1mFound solution: 236544[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 10434   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     55890 |   13459    47854 |    4486   10768   442603    41.1 | 13.031 % |
c |     55990 |   13459    47854 |    4934    2792    75560    27.1 | 13.235 % |
c |     56140 |   13444    47801 |    5428    2934    82471    28.1 | 13.319 % |
c |     56365 |   13444    47801 |    5970    3159    96705    30.6 | 13.319 % |
c |     56702 |   13444    47801 |    6567    3496   115463    33.0 | 13.319 % |
c |     57209 |   13444    47801 |    7224    4003   138314    34.6 | 13.319 % |
c |     57970 |   13444    47801 |    7947    4764   173787    36.5 | 13.319 % |
c ==============================================================================
c [1mFound solution: 186112[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 10828   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     58797 |   13444    47817 |    4481    5586   219549    39.3 | 13.319 % |
c |     58897 |   13444    47817 |    4929    2893    93209    32.2 | 13.564 % |
c |     59048 |   13435    47788 |    5422    3042    97224    32.0 | 13.648 % |
c |     59274 |   13435    47788 |    5964    3268   106868    32.7 | 13.648 % |
c |     59611 |   13429    47770 |    6560    3604   117186    32.5 | 13.690 % |
c |     60117 |   13429    47770 |    7216    4110   131247    31.9 | 13.690 % |
c |     60876 |   13429    47770 |    7938    4869   162338    33.3 | 13.690 % |
c ==============================================================================
c [1mFound solution: 169088[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 10961   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     61287 |   13437    47807 |    4479    5280   193520    36.7 | 13.690 % |
c |     61388 |   13437    47807 |    4926    2741    82723    30.2 | 13.812 % |
c |     61538 |   13437    47807 |    5419    2891    90565    31.3 | 13.812 % |
c |     61765 |   13437    47807 |    5961    3118    97940    31.4 | 13.812 % |
c |     62103 |   13437    47807 |    6557    3456   112599    32.6 | 13.812 % |
c |     62609 |   13437    47807 |    7213    3962   130470    32.9 | 13.812 % |
c |     63368 |   13437    47807 |    7934    4721   176909    37.5 | 13.812 % |
c ==============================================================================
c [1mFound solution: 166400[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 10982   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     63847 |   13443    47851 |    4481    5200   192470    37.0 | 13.812 % |
c |     63950 |   13443    47851 |    4929    2703    77060    28.5 | 13.945 % |
c |     64100 |   13443    47851 |    5422    2853    81016    28.4 | 13.945 % |
c |     64327 |   13443    47851 |    5964    3080    92806    30.1 | 13.945 % |
c |     64664 |   13443    47851 |    6560    3417   104060    30.5 | 13.945 % |
c |     65171 |   13443    47851 |    7216    3924   120099    30.6 | 13.945 % |
c |     65930 |   13443    47851 |    7938    4683   138645    29.6 | 13.945 % |
c |     67070 |   13443    47851 |    8732    5823   220994    38.0 | 13.945 % |
c |     68779 |   13443    47851 |    9605    7532   340196    45.2 | 13.945 % |
c |     71342 |   13443    47851 |   10565   10095   460397    45.6 | 13.945 % |
c |     75186 |   13443    47851 |   11622    8193   314714    38.4 | 13.945 % |
c |     80952 |   13443    47851 |   12784    7850   280319    35.7 | 13.945 % |
c |     89601 |   13443    47851 |   14063    9855   407122    41.3 | 13.945 % |
c ==============================================================================
c [1mFound solution: 134528[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 11231   bits: 14/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     98628 |   13450    47879 |    4483   11452   464871    40.6 | 13.945 % |
c |     98729 |   13450    47879 |    4931    2964    88892    30.0 | 14.071 % |
c |     98879 |   13450    47879 |    5424    3114    91355    29.3 | 14.071 % |
c |     99105 |   13450    47879 |    5966    3340    97831    29.3 | 14.071 % |
c |     99442 |   13450    47879 |    6563    3677   109728    29.8 | 14.071 % |
c |     99949 |   13450    47879 |    7219    4184   125717    30.0 | 14.071 % |
c ==============================================================================
c [1mFound solution: 123392[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 4   maxlim: 5174   bits: 13/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    100664 |   13395    47709 |    4465    4622   130720    28.3 | 14.071 % |
c ==============================================================================
c [1mFound solution: 117760[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 5218   bits: 13/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    100728 |   13402    47743 |    4467    4686   131777    28.1 | 14.071 % |
c |    100828 |   13391    47702 |    4913    4784   134201    28.1 | 14.907 % |
c |    100978 |   13391    47702 |    5405    4934   136219    27.6 | 14.907 % |
c |    101203 |   13391    47702 |    5945    5159   144607    28.0 | 14.907 % |
c |    101542 |   13391    47702 |    6540    5498   155686    28.3 | 14.907 % |
c |    102048 |   13354    47507 |    7194    5601   151869    27.1 | 15.072 % |
c |    102807 |   13354    47507 |    7913    6360   181702    28.6 | 15.072 % |
c |    103948 |   13338    47455 |    8704    7493   219839    29.3 | 15.197 % |
c |    105656 |   13338    47455 |    9575    9201   289083    31.4 | 15.197 % |
c |    108219 |   13338    47455 |   10532    6484   225564    34.8 | 15.197 % |
c |    112064 |   13338    47455 |   11586   10329   392557    38.0 | 15.197 % |
c |    117833 |   13338    47455 |   12744    9964   395569    39.7 | 15.197 % |
c |    126482 |   13338    47455 |   14019   11834   494903    41.8 | 15.197 % |
c ==============================================================================
c [1mFound solution: 91648[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 5422   bits: 13/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    135255 |   13348    47508 |    4449   13259   550001    41.5 | 15.197 % |
c |    135355 |   13348    47508 |    4893    3415    93444    27.4 | 15.381 % |
c |    135505 |   13348    47508 |    5383    3565    97087    27.2 | 15.381 % |
c |    135731 |   13348    47508 |    5921    3791   103170    27.2 | 15.381 % |
c |    136070 |   13348    47508 |    6513    4130   112364    27.2 | 15.381 % |
c |    136577 |   13348    47508 |    7165    4637   129588    27.9 | 15.381 % |
c |    137336 |   13348    47508 |    7881    5396   151242    28.0 | 15.381 % |
c |    138478 |   13348    47508 |    8669    6538   200453    30.7 | 15.381 % |
c |    140187 |   13348    47508 |    9536    8247   252593    30.6 | 15.381 % |
c |    142750 |   13348    47508 |   10490    5608   166009    29.6 | 15.381 % |
c |    146596 |   13348    47508 |   11539    9454   346848    36.7 | 15.381 % |
c |    152363 |   13348    47508 |   12693    9129   346264    37.9 | 15.381 % |
c |    161014 |   13348    47508 |   13962   11122   472397    42.5 | 15.381 % |
c |    173988 |   13348    47508 |   15359    9531   331705    34.8 | 15.381 % |
c ==============================================================================
c [1mFound solution: 89984[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 5435   bits: 13/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    192469 |   13354    47536 |    4451   11937   509956    42.7 | 15.381 % |
c |    192570 |   13354    47536 |    4896    3086    85947    27.9 | 15.467 % |
c |    192720 |   13354    47536 |    5385    3236    90181    27.9 | 15.467 % |
c |    192945 |   13354    47536 |    5924    3461    98564    28.5 | 15.467 % |
c |    193284 |   13354    47536 |    6516    3800   110407    29.1 | 15.467 % |
c |    193790 |   13354    47536 |    7168    4306   125669    29.2 | 15.467 % |
c |    194551 |   13354    47536 |    7885    5067   153749    30.3 | 15.467 % |
c |    195690 |   13354    47536 |    8673    6206   191097    30.8 | 15.467 % |
c |    197399 |   13354    47536 |    9541    7915   250712    31.7 | 15.467 % |
c |    199962 |   13354    47536 |   10495    5375   158830    29.5 | 15.467 % |
c |    203809 |   13354    47536 |   11544    9222   303039    32.9 | 15.467 % |
c |    209575 |   13354    47536 |   12699    8805   337160    38.3 | 15.467 % |
c |    218224 |   13346    47514 |   13969   10753   404450    37.6 | 15.549 % |
c |    231198 |   13346    47514 |   15366    9195   348803    37.9 | 15.549 % |
c |    250659 |   13346    47514 |   16902   12714   512087    40.3 | 15.549 % |
c |    279852 |   13346    47514 |   18592   15680   673771    43.0 | 15.549 % |
c ==============================================================================
c [1mFound solution: 88832[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 5444   bits: 13/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    288212 |   13351    47541 |    4450   14437   674320    46.7 | 15.549 % |
c |    288313 |   13351    47541 |    4895    3711   145326    39.2 | 15.640 % |
c |    288463 |   13351    47541 |    5384    3861   150549    39.0 | 15.640 % |
c |    288688 |   13351    47541 |    5922    4086   157832    38.6 | 15.640 % |
c |    289025 |   13351    47541 |    6515    4423   162657    36.8 | 15.640 % |
c |    289531 |   13351    47541 |    7166    4929   176529    35.8 | 15.640 % |
c |    290290 |   13351    47541 |    7883    5688   198324    34.9 | 15.640 % |
c |    291429 |   13351    47541 |    8671    6827   236374    34.6 | 15.640 % |
c |    293137 |   13351    47541 |    9538    8535   286968    33.6 | 15.640 % |
c |    295700 |   13351    47541 |   10492    6071   161451    26.6 | 15.640 % |
c ==============================================================================
c [1mFound solution: 80256[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 5511   bits: 13/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    297816 |   13355    47556 |    4451    8187   245635    30.0 | 15.640 % |
c |    297916 |   13355    47556 |    4896    4194   117409    28.0 | 15.697 % |
c |    298066 |   13355    47556 |    5385    4344   123164    28.4 | 15.697 % |
c |    298291 |   13355    47556 |    5924    4569   130310    28.5 | 15.697 % |
c |    298628 |   13355    47556 |    6516    4906   136788    27.9 | 15.697 % |
c |    299135 |   13355    47556 |    7168    5413   150881    27.9 | 15.697 % |
c |    299894 |   13355    47556 |    7885    6172   175794    28.5 | 15.697 % |
c |    301033 |   13355    47556 |    8673    7311   210621    28.8 | 15.697 % |
c |    302743 |   13355    47556 |    9541    9021   283371    31.4 | 15.697 % |
c |    305305 |   13355    47556 |   10495    6346   245744    38.7 | 15.697 % |
c |    309149 |   13355    47556 |   11544   10190   400207    39.3 | 15.697 % |
c |    314915 |   13355    47556 |   12699    9896   369446    37.3 | 15.697 % |
c |    323564 |   13355    47556 |   13969   11800   470407    39.9 | 15.697 % |
c ==============================================================================
c [1mFound solution: 77696[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 5531   bits: 13/13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    323896 |   13361    47582 |    4453   12132   482262    39.8 | 15.697 % |
c |    323996 |   13361    47582 |    4898    3133    75277    24.0 | 15.781 % |
c |    324147 |   13361    47582 |    5388    3284    77495    23.6 | 15.781 % |
c |    324372 |   13361    47582 |    5926    3509    85920    24.5 | 15.781 % |
c |    324709 |   13361    47582 |    6519    3846    94916    24.7 | 15.781 % |
c |    325215 |   13361    47582 |    7171    4352   108935    25.0 | 15.781 % |
c |    325974 |   13361    47582 |    7888    5111   130728    25.6 | 15.781 % |
c |    327114 |   13361    47582 |    8677    6251   172348    27.6 | 15.781 % |
c |    328822 |   13361    47582 |    9545    7959   248681    31.2 | 15.781 % |
c |    331385 |   13361    47582 |   10499    5461   166076    30.4 | 15.781 % |
c |    335229 |   13361    47582 |   11549    9305   299126    32.1 | 15.781 % |
c |    340995 |   13361    47582 |   12704    8967   303099    33.8 | 15.781 % |
c ==============================================================================
c [1mFound solution: 60288[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 4   maxlim: 2595   bits: 12/12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    341618 |   13302    47370 |    4434    9558   325905    34.1 | 15.781 % |
c |    341718 |   13302    47370 |    4877    4879   155431    31.9 | 16.334 % |
c |    341868 |   13302    47370 |    5365    5029   156993    31.2 | 16.334 % |
c |    342093 |   13275    47277 |    5901    5242   160804    30.7 | 16.497 % |
c |    342431 |   13275    47277 |    6491    5580   169155    30.3 | 16.497 % |
c |    342937 |   13267    47251 |    7141    6085   179252    29.5 | 16.538 % |
c |    343697 |   13267    47251 |    7855    6845   211486    30.9 | 16.538 % |
c |    344837 |   13259    47225 |    8640    7984   255826    32.0 | 16.578 % |
c |    346545 |   13215    46982 |    9504    4973   144117    29.0 | 16.741 % |
c |    349107 |   13215    46982 |   10455    7535   229056    30.4 | 16.741 % |
c |    352951 |   13215    46982 |   11500    5815   202197    34.8 | 16.741 % |
c |    358719 |   13215    46982 |   12650   11583   441948    38.2 | 16.741 % |
c |    367370 |   13215    46982 |   13915    6787   268985    39.6 | 16.741 % |
c |    380344 |   13215    46982 |   15307   12510   492631    39.4 | 16.741 % |
c |    399806 |   13215    46982 |   16838   15888   743079    46.8 | 16.741 % |
c |    429001 |   13215    46982 |   18521   10073   395146    39.2 | 16.741 % |
c |    472791 |   13215    46982 |   20374   15523   603968    38.9 | 16.741 % |
c ==============================================================================
c [1mFound solution: 56192[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2627   bits: 12/12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    489177 |   13218    46993 |    4406   10691   473881    44.3 | 16.741 % |
c |    489280 |   13218    46993 |    4846    2776    72406    26.1 | 16.802 % |
c |    489432 |   13218    46993 |    5331    2928    74360    25.4 | 16.802 % |
c |    489658 |   13218    46993 |    5864    3154    82687    26.2 | 16.802 % |
c |    489995 |   13218    46993 |    6450    3491    92147    26.4 | 16.802 % |
c |    490502 |   13218    46993 |    7095    3998   106587    26.7 | 16.802 % |
c |    491262 |   13218    46993 |    7805    4758   125654    26.4 | 16.802 % |
c |    492402 |   13218    46993 |    8586    5898   161958    27.5 | 16.802 % |
c |    494111 |   13218    46993 |    9444    7607   224840    29.6 | 16.802 % |
c |    496673 |   13218    46993 |   10389   10169   349191    34.3 | 16.802 % |
c |    500518 |   13218    46993 |   11428    8485   308401    36.3 | 16.802 % |
c |    506284 |   13218    46993 |   12570    8255   288221    34.9 | 16.802 % |
c |    514936 |   13218    46993 |   13827   10266   360206    35.1 | 16.802 % |
c |    527910 |   13218    46993 |   15210    8773   363496    41.4 | 16.802 % |
c |    547372 |   13218    46993 |   16731   12366   499923    40.4 | 16.802 % |
c |    576566 |   13218    46993 |   18404   15245   713837    46.8 | 16.802 % |
c |    620356 |   13218    46993 |   20245   11197   382326    34.1 | 16.802 % |
c ==============================================================================
c [1mFound solution: 49152[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2682   bits: 12/12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    650971 |   13227    47037 |    4409   20824   948231    45.5 | 16.802 % |
c |    651072 |   13227    47037 |    4849    2704    61854    22.9 | 16.944 % |
c |    651224 |   13227    47037 |    5334    2856    64619    22.6 | 16.944 % |
c |    651452 |   13227    47037 |    5868    3084    71938    23.3 | 16.944 % |
c |    651790 |   13227    47037 |    6455    3422    80852    23.6 | 16.944 % |
c |    652297 |   13227    47037 |    7100    3929    97200    24.7 | 16.944 % |
c |    653056 |   13227    47037 |    7810    4688   124393    26.5 | 16.944 % |
c |    654195 |   13227    47037 |    8591    5827   164767    28.3 | 16.944 % |
c |    655903 |   13227    47037 |    9451    7535   259879    34.5 | 16.944 % |
c |    658466 |   13227    47037 |   10396   10098   370855    36.7 | 16.944 % |
c |    662310 |   13227    47037 |   11435    8387   320102    38.2 | 16.944 % |
c |    668076 |   13227    47037 |   12579    8114   267287    32.9 | 16.944 % |
c |    676725 |   13227    47037 |   13837   10194   339745    33.3 | 16.944 % |
c |    689699 |   13227    47037 |   15221    8669   314640    36.3 | 16.944 % |
c |    709160 |   13227    47037 |   16743   12252   577429    47.1 | 16.944 % |
c ==============================================================================
c [1mFound solution: 39040[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2761   bits: 12/12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    718512 |   13233    47060 |    4411   12949   784286    60.6 | 16.944 % |
c |    718613 |   13233    47060 |    4852    3339   142379    42.6 | 17.064 % |
c |    718763 |   13233    47060 |    5337    3489   144681    41.5 | 17.064 % |
c |    718990 |   13233    47060 |    5871    3716   148611    40.0 | 17.064 % |
c |    719327 |   13233    47060 |    6458    4053   160688    39.6 | 17.064 % |
c |    719833 |   13233    47060 |    7103    4559   175624    38.5 | 17.064 % |
c |    720594 |   13233    47060 |    7814    5320   205460    38.6 | 17.064 % |
c |    721736 |   13233    47060 |    8595    6462   247241    38.3 | 17.064 % |
c |    723446 |   13233    47060 |    9455    8172   314461    38.5 | 17.064 % |
c |    726010 |   13233    47060 |   10400    5609   177093    31.6 | 17.064 % |
c |    729855 |   13233    47060 |   11440    9454   320348    33.9 | 17.064 % |
c |    735622 |   13233    47060 |   12585    9147   357511    39.1 | 17.064 % |
c |    744271 |   13233    47060 |   13843   11095   382768    34.5 | 17.064 % |
c |    757247 |   13233    47060 |   15227    9595   364755    38.0 | 17.064 % |
c |    776710 |   13233    47060 |   16750   13144   496887    37.8 | 17.064 % |
c |    805903 |   13233    47060 |   18425   16103   650574    40.4 | 17.064 % |
c ==============================================================================
c [1mFound solution: 37248[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2775   bits: 12/12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    836311 |   13236    47071 |    4412   17786   779424    43.8 | 17.064 % |
c |    836411 |   13236    47071 |    4853    4547   168356    37.0 | 17.124 % |
c |    836561 |   13236    47071 |    5338    4697   172730    36.8 | 17.124 % |
c |    836787 |   13236    47071 |    5872    4923   176195    35.8 | 17.124 % |
c |    837126 |   13236    47071 |    6459    5262   184655    35.1 | 17.124 % |
c |    837632 |   13236    47071 |    7105    5768   201439    34.9 | 17.124 % |
c |    838391 |   13236    47071 |    7816    6527   226199    34.7 | 17.124 % |
c |    839532 |   13236    47071 |    8597    7668   264608    34.5 | 17.124 % |
c |    841240 |   13236    47071 |    9457    9376   352839    37.6 | 17.124 % |
c |    843804 |   13236    47071 |   10403    6839   217236    31.8 | 17.124 % |
c |    847648 |   13236    47071 |   11443   10683   365217    34.2 | 17.124 % |
c |    853416 |   13236    47071 |   12587   10285   433578    42.2 | 17.124 % |
c |    862067 |   13236    47071 |   13846   12301   544350    44.3 | 17.124 % |
c |    875043 |   13236    47071 |   15231   10795   377613    35.0 | 17.124 % |
c |    894505 |   13236    47071 |   16754   14292   546134    38.2 | 17.124 % |
c |    923699 |   13236    47071 |   18430   17330   683018    39.4 | 17.124 % |
c |    967488 |   13236    47071 |   20273   13061   523270    40.1 | 17.124 % |
c |   1033174 |   13236    47071 |   22300   15125   736429    48.7 | 17.124 % |
#### 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.94 0.94 0.92 2/54 28101
Raw data (stat): 28101 (runsolver) R 28100 28099 28098 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 541673341 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+10.0006 s]
Raw data (loadavg): 0.95 0.94 0.92 2/54 28101
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 1162 0 0 0 995 3 0 0 25 0 1 0 541673341 6377472 1140 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1557 1140 603 41 0 1516 0
vsize: 6228
[startup+20.0009 s]
Raw data (loadavg): 0.95 0.94 0.92 2/54 28101
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 1508 0 0 0 1994 4 0 0 25 0 1 0 541673341 7716864 1486 4294967295 134512640 134672761 3221224544 3221223680 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1884 1486 603 41 0 1843 0
vsize: 7536
[startup+30.0011 s]
Raw data (loadavg): 0.96 0.94 0.92 2/54 28101
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 1655 0 0 0 2993 5 0 0 25 0 1 0 541673341 8388608 1633 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2048 1633 603 41 0 2007 0
vsize: 8192
[startup+40.0014 s]
Raw data (loadavg): 0.97 0.94 0.92 2/54 28101
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 1746 0 0 0 3993 5 0 0 25 0 1 0 541673341 8794112 1724 4294967295 134512640 134672761 3221224544 3221223648 134559869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2147 1724 603 41 0 2106 0
vsize: 8588
[startup+50.0017 s]
Raw data (loadavg): 0.97 0.95 0.92 2/54 28101
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 1748 0 0 0 4993 5 0 0 25 0 1 0 541673341 8794112 1726 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2147 1726 603 41 0 2106 0
vsize: 8588
[startup+60.0016 s]
Raw data (loadavg): 0.97 0.95 0.92 2/54 28101
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 1748 0 0 0 5993 5 0 0 25 0 1 0 541673341 8794112 1726 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2147 1726 603 41 0 2106 0
vsize: 8588
[startup+70.0023 s]
Raw data (loadavg): 0.98 0.95 0.92 2/54 28101
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 1755 0 0 0 6993 5 0 0 25 0 1 0 541673341 8794112 1733 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2147 1733 603 41 0 2106 0
vsize: 8588
[startup+80.0016 s]
Raw data (loadavg): 1.06 0.96 0.92 2/54 28155
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 1755 0 0 0 7988 10 0 0 25 0 1 0 541673341 8794112 1733 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2147 1733 603 41 0 2106 0
vsize: 8588
[startup+90.0016 s]
Raw data (loadavg): 1.05 0.97 0.92 2/54 28155
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 1756 0 0 0 8987 11 0 0 25 0 1 0 541673341 8794112 1734 4294967295 134512640 134672761 3221224544 3221223844 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2147 1734 603 41 0 2106 0
vsize: 8588
[startup+100.001 s]
Raw data (loadavg): 1.04 0.97 0.92 2/54 28155
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 1756 0 0 0 9987 11 0 0 25 0 1 0 541673341 8794112 1734 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2147 1734 603 41 0 2106 0
vsize: 8588
[startup+110.001 s]
Raw data (loadavg): 1.04 0.97 0.92 2/54 28155
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 1756 0 0 0 10987 12 0 0 25 0 1 0 541673341 8794112 1734 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2147 1734 603 41 0 2106 0
vsize: 8588
[startup+120.001 s]
Raw data (loadavg): 1.03 0.97 0.92 2/54 28155
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 1758 0 0 0 11987 12 0 0 25 0 1 0 541673341 8794112 1736 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2147 1736 603 41 0 2106 0
vsize: 8588
[startup+130.001 s]
Raw data (loadavg): 1.02 0.97 0.92 2/54 28155
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 1772 0 0 0 12986 12 0 0 25 0 1 0 541673341 8974336 1750 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2191 1750 603 41 0 2150 0
vsize: 8764
[startup+140.001 s]
Raw data (loadavg): 1.02 0.97 0.92 2/54 28155
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 1772 0 0 0 13986 13 0 0 25 0 1 0 541673341 8974336 1750 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2191 1750 603 41 0 2150 0
vsize: 8764
[startup+150.001 s]
Raw data (loadavg): 1.02 0.97 0.92 2/54 28155
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 1772 0 0 0 14986 13 0 0 25 0 1 0 541673341 8974336 1750 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2191 1750 603 41 0 2150 0
vsize: 8764
[startup+160.002 s]
Raw data (loadavg): 1.01 0.97 0.92 2/54 28157
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 1772 0 0 0 15986 14 0 0 25 0 1 0 541673341 8974336 1750 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2191 1750 603 41 0 2150 0
vsize: 8764
[startup+170.003 s]
Raw data (loadavg): 1.01 0.97 0.92 2/54 28157
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 1772 0 0 0 16986 14 0 0 25 0 1 0 541673341 8974336 1750 4294967295 134512640 134672761 3221224544 3221223696 134565083 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2191 1750 603 41 0 2150 0
vsize: 8764
[startup+180.002 s]
Raw data (loadavg): 1.01 0.97 0.92 2/54 28157
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 1772 0 0 0 17986 14 0 0 25 0 1 0 541673341 8974336 1750 4294967295 134512640 134672761 3221224544 3221223712 134561003 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2191 1750 603 41 0 2150 0
vsize: 8764
[startup+190.003 s]
Raw data (loadavg): 1.01 0.97 0.92 2/54 28157
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 1772 0 0 0 18986 14 0 0 25 0 1 0 541673341 8974336 1750 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2191 1750 603 41 0 2150 0
vsize: 8764
[startup+200.003 s]
Raw data (loadavg): 1.01 0.97 0.92 2/54 28157
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 1780 0 0 0 19986 14 0 0 25 0 1 0 541673341 8974336 1758 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2191 1758 603 41 0 2150 0
vsize: 8764
[startup+210.004 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28157
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 1879 0 0 0 20986 14 0 0 25 0 1 0 541673341 9383936 1857 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2291 1857 603 41 0 2250 0
vsize: 9164
[startup+220.004 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28157
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 1879 0 0 0 21986 14 0 0 25 0 1 0 541673341 9383936 1857 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2291 1857 603 41 0 2250 0
vsize: 9164
[startup+230.004 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28157
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 1879 0 0 0 22986 14 0 0 25 0 1 0 541673341 9383936 1857 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2291 1857 603 41 0 2250 0
vsize: 9164
[startup+240.005 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28157
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 1879 0 0 0 23987 14 0 0 25 0 1 0 541673341 9383936 1857 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2291 1857 603 41 0 2250 0
vsize: 9164
[startup+250.004 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28157
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 1879 0 0 0 24987 14 0 0 25 0 1 0 541673341 9383936 1857 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2291 1857 603 41 0 2250 0
vsize: 9164
[startup+260.005 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28157
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 1909 0 0 0 25987 14 0 0 25 0 1 0 541673341 9519104 1887 4294967295 134512640 134672761 3221224544 3221223712 134560906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2324 1887 603 41 0 2283 0
vsize: 9296
[startup+270.006 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28157
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 1950 0 0 0 26987 14 0 0 25 0 1 0 541673341 9674752 1928 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2362 1928 603 41 0 2321 0
vsize: 9448
[startup+280.006 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28157
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 1958 0 0 0 27987 14 0 0 25 0 1 0 541673341 9674752 1936 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2362 1936 603 41 0 2321 0
vsize: 9448
[startup+290.006 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28157
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 2010 0 0 0 28987 15 0 0 25 0 1 0 541673341 9940992 1988 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2427 1988 603 41 0 2386 0
vsize: 9708
[startup+300.005 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28157
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 2181 0 0 0 29987 15 0 0 25 0 1 0 541673341 10608640 2159 4294967295 134512640 134672761 3221224544 3221223648 134559796 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2590 2159 603 41 0 2549 0
vsize: 10360
[startup+310.006 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28157
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 2181 0 0 0 30987 15 0 0 25 0 1 0 541673341 10608640 2159 4294967295 134512640 134672761 3221224544 3221223668 134566118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2590 2159 603 41 0 2549 0
vsize: 10360
[startup+320.006 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28157
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 2181 0 0 0 31987 15 0 0 25 0 1 0 541673341 10608640 2159 4294967295 134512640 134672761 3221224544 3221223728 134558899 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2590 2159 603 41 0 2549 0
vsize: 10360
[startup+330.005 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28157
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 2181 0 0 0 32987 15 0 0 25 0 1 0 541673341 10608640 2159 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2590 2159 603 41 0 2549 0
vsize: 10360
[startup+340.006 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28157
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 2181 0 0 0 33987 15 0 0 25 0 1 0 541673341 10608640 2159 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2590 2159 603 41 0 2549 0
vsize: 10360
[startup+350.006 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28157
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 2183 0 0 0 34987 15 0 0 25 0 1 0 541673341 10608640 2161 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2590 2161 603 41 0 2549 0
vsize: 10360
[startup+360.006 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28157
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 2183 0 0 0 35988 15 0 0 25 0 1 0 541673341 10608640 2161 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2590 2161 603 41 0 2549 0
vsize: 10360
[startup+370.006 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28157
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 2183 0 0 0 36988 15 0 0 25 0 1 0 541673341 10608640 2161 4294967295 134512640 134672761 3221224544 3221223712 134560964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2590 2161 603 41 0 2549 0
vsize: 10360
[startup+380.005 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28157
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 2183 0 0 0 37988 15 0 0 25 0 1 0 541673341 10608640 2161 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2590 2161 603 41 0 2549 0
vsize: 10360
[startup+390.006 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28157
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 2183 0 0 0 38988 15 0 0 25 0 1 0 541673341 10608640 2161 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2590 2161 603 41 0 2549 0
vsize: 10360
[startup+400.006 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28157
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 2331 0 0 0 39987 16 0 0 25 0 1 0 541673341 11276288 2309 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2753 2309 603 41 0 2712 0
vsize: 11012
[startup+410.006 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28157
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 2333 0 0 0 40988 16 0 0 25 0 1 0 541673341 11276288 2311 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2753 2311 603 41 0 2712 0
vsize: 11012
[startup+420.006 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28159
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 2337 0 0 0 41988 16 0 0 25 0 1 0 541673341 11276288 2315 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2753 2315 603 41 0 2712 0
vsize: 11012
[startup+430.006 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28159
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 2350 0 0 0 42988 17 0 0 25 0 1 0 541673341 11276288 2328 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2753 2328 603 41 0 2712 0
vsize: 11012
[startup+440.006 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28159
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 2376 0 0 0 43988 17 0 0 25 0 1 0 541673341 11423744 2354 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2789 2354 603 41 0 2748 0
vsize: 11156
[startup+450.007 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28159
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 2387 0 0 0 44988 17 0 0 25 0 1 0 541673341 11423744 2365 4294967295 134512640 134672761 3221224544 3221223712 134560842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2789 2365 603 41 0 2748 0
vsize: 11156
[startup+460.008 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28159
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 2400 0 0 0 45988 17 0 0 25 0 1 0 541673341 11563008 2378 4294967295 134512640 134672761 3221224544 3221223712 134561212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2823 2378 603 41 0 2782 0
vsize: 11292
[startup+470.008 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28159
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 2400 0 0 0 46988 17 0 0 25 0 1 0 541673341 11563008 2378 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2823 2378 603 41 0 2782 0
vsize: 11292
[startup+480.008 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28159
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 2415 0 0 0 47989 17 0 0 25 0 1 0 541673341 11563008 2393 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2823 2393 603 41 0 2782 0
vsize: 11292
[startup+490.008 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28159
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 2455 0 0 0 48989 17 0 0 25 0 1 0 541673341 11857920 2433 4294967295 134512640 134672761 3221224544 3221223712 134561127 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2895 2433 603 41 0 2854 0
vsize: 11580
[startup+500.008 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28159
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 2552 0 0 0 49989 17 0 0 25 0 1 0 541673341 12120064 2530 4294967295 134512640 134672761 3221224544 3221223680 134560726 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2959 2530 603 41 0 2918 0
vsize: 11836
[startup+510.009 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28159
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 2636 0 0 0 50989 17 0 0 25 0 1 0 541673341 12529664 2614 4294967295 134512640 134672761 3221224544 3221223712 134561003 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3059 2614 603 41 0 3018 0
vsize: 12236
[startup+520.008 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28159
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 2708 0 0 0 51989 17 0 0 25 0 1 0 541673341 12800000 2686 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3125 2686 603 41 0 3084 0
vsize: 12500
[startup+530.008 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28159
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 2708 0 0 0 52989 17 0 0 25 0 1 0 541673341 12800000 2686 4294967295 134512640 134672761 3221224544 3221223680 134560697 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3125 2686 603 41 0 3084 0
vsize: 12500
[startup+540.008 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28159
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 2708 0 0 0 53989 17 0 0 25 0 1 0 541673341 12800000 2686 4294967295 134512640 134672761 3221224544 3221223648 134560350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3125 2686 603 41 0 3084 0
vsize: 12500
[startup+550.009 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28159
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 2708 0 0 0 54989 17 0 0 25 0 1 0 541673341 12800000 2686 4294967295 134512640 134672761 3221224544 3221223712 134560906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3125 2686 603 41 0 3084 0
vsize: 12500
[startup+560.01 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28159
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 2708 0 0 0 55989 17 0 0 25 0 1 0 541673341 12800000 2686 4294967295 134512640 134672761 3221224544 3221223648 134554668 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3125 2686 603 41 0 3084 0
vsize: 12500
[startup+570.009 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28159
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 2708 0 0 0 56990 17 0 0 25 0 1 0 541673341 12800000 2686 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3125 2686 603 41 0 3084 0
vsize: 12500
[startup+580.009 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28159
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 2708 0 0 0 57990 17 0 0 25 0 1 0 541673341 12800000 2686 4294967295 134512640 134672761 3221224544 3221223040 134565768 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3125 2686 603 41 0 3084 0
vsize: 12500
[startup+590.01 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28159
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 2708 0 0 0 58990 18 0 0 25 0 1 0 541673341 12800000 2686 4294967295 134512640 134672761 3221224544 3221223712 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3125 2686 603 41 0 3084 0
vsize: 12500
[startup+600.009 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28159
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 2722 0 0 0 59990 18 0 0 25 0 1 0 541673341 12935168 2700 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3158 2700 603 41 0 3117 0
vsize: 12632
[startup+610.01 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28159
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 2727 0 0 0 60990 18 0 0 25 0 1 0 541673341 12935168 2705 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3158 2705 603 41 0 3117 0
vsize: 12632
[startup+620.009 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28159
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 2730 0 0 0 61990 18 0 0 25 0 1 0 541673341 12935168 2708 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3158 2708 603 41 0 3117 0
vsize: 12632
[startup+630.009 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28159
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 2737 0 0 0 62991 18 0 0 25 0 1 0 541673341 12935168 2715 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3158 2715 603 41 0 3117 0
vsize: 12632
[startup+640.01 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28159
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 2737 0 0 0 63991 18 0 0 25 0 1 0 541673341 12935168 2715 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3158 2715 603 41 0 3117 0
vsize: 12632
[startup+650.01 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28159
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 2737 0 0 0 64991 18 0 0 25 0 1 0 541673341 12935168 2715 4294967295 134512640 134672761 3221224544 3221223712 134561003 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3158 2715 603 41 0 3117 0
vsize: 12632
[startup+660.011 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28159
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 2741 0 0 0 65991 18 0 0 25 0 1 0 541673341 12935168 2719 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3158 2719 603 41 0 3117 0
vsize: 12632
[startup+670.01 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28159
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 2895 0 0 0 66991 19 0 0 25 0 1 0 541673341 13602816 2873 4294967295 134512640 134672761 3221224544 3221223648 134554910 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3321 2873 603 41 0 3280 0
vsize: 13284
[startup+680.01 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28159
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 2899 0 0 0 67991 19 0 0 25 0 1 0 541673341 13602816 2877 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3321 2877 603 41 0 3280 0
vsize: 13284
[startup+690.011 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28159
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 2903 0 0 0 68991 19 0 0 25 0 1 0 541673341 13602816 2881 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3321 2881 603 41 0 3280 0
vsize: 13284
[startup+700.011 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28159
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 2903 0 0 0 69991 19 0 0 25 0 1 0 541673341 13602816 2881 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3321 2881 603 41 0 3280 0
vsize: 13284
[startup+710.011 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28159
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 2903 0 0 0 70991 19 0 0 25 0 1 0 541673341 13602816 2881 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3321 2881 603 41 0 3280 0
vsize: 13284
[startup+720.011 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28159
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 2903 0 0 0 71992 19 0 0 25 0 1 0 541673341 13602816 2881 4294967295 134512640 134672761 3221224544 3221223728 134559572 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3321 2881 603 41 0 3280 0
vsize: 13284
[startup+730.011 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28159
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 2903 0 0 0 72992 19 0 0 25 0 1 0 541673341 13602816 2881 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3321 2881 603 41 0 3280 0
vsize: 13284
[startup+740.012 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28159
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 2903 0 0 0 73992 19 0 0 25 0 1 0 541673341 13602816 2881 4294967295 134512640 134672761 3221224544 3221223648 134560248 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3321 2881 603 41 0 3280 0
vsize: 13284
[startup+750.012 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28159
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 2930 0 0 0 74992 19 0 0 25 0 1 0 541673341 13733888 2908 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3353 2908 603 41 0 3312 0
vsize: 13412
[startup+760.013 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28159
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 2930 0 0 0 75992 19 0 0 25 0 1 0 541673341 13733888 2908 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3353 2908 603 41 0 3312 0
vsize: 13412
[startup+770.014 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28159
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 2930 0 0 0 76992 19 0 0 25 0 1 0 541673341 13733888 2908 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3353 2908 603 41 0 3312 0
vsize: 13412
[startup+780.013 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28159
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 2930 0 0 0 77993 19 0 0 25 0 1 0 541673341 13733888 2908 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3353 2908 603 41 0 3312 0
vsize: 13412
[startup+790.014 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28159
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 2930 0 0 0 78993 19 0 0 25 0 1 0 541673341 13733888 2908 4294967295 134512640 134672761 3221224544 3221223712 134561161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3353 2908 603 41 0 3312 0
vsize: 13412
[startup+800.014 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28159
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 2930 0 0 0 79993 19 0 0 25 0 1 0 541673341 13733888 2908 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3353 2908 603 41 0 3312 0
vsize: 13412
[startup+810.014 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28159
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 2930 0 0 0 80993 19 0 0 25 0 1 0 541673341 13733888 2908 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3353 2908 603 41 0 3312 0
vsize: 13412
[startup+820.015 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28159
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 2930 0 0 0 81993 19 0 0 25 0 1 0 541673341 13733888 2908 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3353 2908 603 41 0 3312 0
vsize: 13412
[startup+830.014 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28159
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 2930 0 0 0 82994 19 0 0 25 0 1 0 541673341 13733888 2908 4294967295 134512640 134672761 3221224544 3221223712 134560926 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3353 2908 603 41 0 3312 0
vsize: 13412
[startup+840.015 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28159
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 2930 0 0 0 83994 19 0 0 25 0 1 0 541673341 13733888 2908 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3353 2908 603 41 0 3312 0
vsize: 13412
[startup+850.016 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28159
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 2930 0 0 0 84994 19 0 0 25 0 1 0 541673341 13733888 2908 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3353 2908 603 41 0 3312 0
vsize: 13412
[startup+860.016 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28159
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 2930 0 0 0 85994 19 0 0 25 0 1 0 541673341 13733888 2908 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3353 2908 603 41 0 3312 0
vsize: 13412
[startup+870.017 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28159
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 2936 0 0 0 86994 19 0 0 25 0 1 0 541673341 13733888 2914 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3353 2914 603 41 0 3312 0
vsize: 13412
[startup+880.017 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28159
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 2939 0 0 0 87995 19 0 0 25 0 1 0 541673341 13733888 2917 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3353 2917 603 41 0 3312 0
vsize: 13412
[startup+890.017 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28159
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 2939 0 0 0 88995 19 0 0 25 0 1 0 541673341 13733888 2917 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3353 2917 603 41 0 3312 0
vsize: 13412
[startup+900.017 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28159
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 2939 0 0 0 89995 19 0 0 25 0 1 0 541673341 13733888 2917 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3353 2917 603 41 0 3312 0
vsize: 13412
[startup+910.017 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28159
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 2939 0 0 0 90995 19 0 0 25 0 1 0 541673341 13733888 2917 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3353 2917 603 41 0 3312 0
vsize: 13412
[startup+920.018 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28159
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 2939 0 0 0 91995 19 0 0 25 0 1 0 541673341 13733888 2917 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3353 2917 603 41 0 3312 0
vsize: 13412
[startup+930.018 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28159
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 2939 0 0 0 92996 19 0 0 25 0 1 0 541673341 13733888 2917 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3353 2917 603 41 0 3312 0
vsize: 13412
[startup+940.018 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28159
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 2939 0 0 0 93996 19 0 0 25 0 1 0 541673341 13733888 2917 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3353 2917 603 41 0 3312 0
vsize: 13412
[startup+950.019 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28159
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 2939 0 0 0 94996 19 0 0 25 0 1 0 541673341 13733888 2917 4294967295 134512640 134672761 3221224544 3221223680 134560590 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3353 2917 603 41 0 3312 0
vsize: 13412
[startup+960.019 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28159
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 2939 0 0 0 95996 19 0 0 25 0 1 0 541673341 13733888 2917 4294967295 134512640 134672761 3221224544 3221223744 134557796 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3353 2917 603 41 0 3312 0
vsize: 13412
[startup+970.019 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28159
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 2939 0 0 0 96996 19 0 0 25 0 1 0 541673341 13733888 2917 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3353 2917 603 41 0 3312 0
vsize: 13412
[startup+980.019 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28159
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 2939 0 0 0 97997 19 0 0 25 0 1 0 541673341 13733888 2917 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3353 2917 603 41 0 3312 0
vsize: 13412
[startup+990.019 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28159
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 2939 0 0 0 98997 19 0 0 25 0 1 0 541673341 13733888 2917 4294967295 134512640 134672761 3221224544 3221223668 134566057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3353 2917 603 41 0 3312 0
vsize: 13412
[startup+1000.02 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28159
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 3042 0 0 0 99997 19 0 0 25 0 1 0 541673341 14274560 3020 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3485 3020 603 41 0 3444 0
vsize: 13940
[startup+1010.02 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28159
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 3077 0 0 0 100997 19 0 0 25 0 1 0 541673341 14405632 3055 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3517 3055 603 41 0 3476 0
vsize: 14068
[startup+1020.02 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28159
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 3080 0 0 0 101997 19 0 0 25 0 1 0 541673341 14405632 3058 4294967295 134512640 134672761 3221224544 3221223712 134560968 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3517 3058 603 41 0 3476 0
vsize: 14068
[startup+1030.02 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28159
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 3100 0 0 0 102997 20 0 0 25 0 1 0 541673341 14405632 3078 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3517 3078 603 41 0 3476 0
vsize: 14068
[startup+1040.02 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28159
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 3165 0 0 0 103997 20 0 0 25 0 1 0 541673341 14671872 3143 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3582 3143 603 41 0 3541 0
vsize: 14328
[startup+1050.02 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28159
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 3364 0 0 0 104996 21 0 0 25 0 1 0 541673341 15466496 3342 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3776 3342 603 41 0 3735 0
vsize: 15104
[startup+1060.02 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28159
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 3397 0 0 0 105996 21 0 0 25 0 1 0 541673341 15601664 3375 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3809 3375 603 41 0 3768 0
vsize: 15236
[startup+1070.02 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28159
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 3477 0 0 0 106996 21 0 0 25 0 1 0 541673341 16015360 3455 4294967295 134512640 134672761 3221224544 3221223712 134561025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3910 3455 603 41 0 3869 0
vsize: 15640
[startup+1080.02 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28159
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 3477 0 0 0 107996 21 0 0 25 0 1 0 541673341 16015360 3455 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3910 3455 603 41 0 3869 0
vsize: 15640
[startup+1090.02 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28159
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 3477 0 0 0 108996 21 0 0 25 0 1 0 541673341 16015360 3455 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3910 3455 603 41 0 3869 0
vsize: 15640
[startup+1100.02 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28159
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 3477 0 0 0 109996 21 0 0 25 0 1 0 541673341 16015360 3455 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3910 3455 603 41 0 3869 0
vsize: 15640
[startup+1110.02 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28159
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 3477 0 0 0 110997 21 0 0 25 0 1 0 541673341 16015360 3455 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3910 3455 603 41 0 3869 0
vsize: 15640
[startup+1120.02 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28159
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 3477 0 0 0 111997 21 0 0 25 0 1 0 541673341 16015360 3455 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3910 3455 603 41 0 3869 0
vsize: 15640
[startup+1130.02 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28159
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 3477 0 0 0 112996 22 0 0 25 0 1 0 541673341 16015360 3455 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3910 3455 603 41 0 3869 0
vsize: 15640
[startup+1140.02 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28159
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 3479 0 0 0 113997 22 0 0 25 0 1 0 541673341 16015360 3457 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3910 3457 603 41 0 3869 0
vsize: 15640
[startup+1150.02 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28159
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 3479 0 0 0 114997 22 0 0 25 0 1 0 541673341 16015360 3457 4294967295 134512640 134672761 3221224544 3221223712 134561220 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3910 3457 603 41 0 3869 0
vsize: 15640
[startup+1160.02 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28159
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 3479 0 0 0 115997 22 0 0 25 0 1 0 541673341 16015360 3457 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3910 3457 603 41 0 3869 0
vsize: 15640
[startup+1170.02 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28159
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 3479 0 0 0 116997 22 0 0 25 0 1 0 541673341 16015360 3457 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3910 3457 603 41 0 3869 0
vsize: 15640
[startup+1180.02 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28159
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 3479 0 0 0 117997 22 0 0 25 0 1 0 541673341 16015360 3457 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3910 3457 603 41 0 3869 0
vsize: 15640
[startup+1190.02 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28159
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 3479 0 0 0 118998 22 0 0 25 0 1 0 541673341 16015360 3457 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3910 3457 603 41 0 3869 0
vsize: 15640
[startup+1200.02 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 28159
Raw data (stat): 28101 (minisat+) R 28100 28099 28098 0 -1 0 3479 0 0 0 119998 22 0 0 25 0 1 0 541673341 16015360 3457 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3910 3457 603 41 0 3869 0
vsize: 15640
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.03 s]
Raw data (loadavg): 1.00 0.97 0.92 1/54 28159
Raw data (stat): 28101 (minisat+) Z 28100 28099 28098 0 -1 12 3482 0 0 0 119998 22 0 0 25 0 1 0 541673341 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.03
CPU time (s): 1200.21
CPU user time (s): 1199.98
CPU system time (s): 0.227965
CPU usage (%): 100.015
Max. virtual memory (Kb): 15640
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####