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/miplib/normalized-mps-v2-13-7-mod013.opb
MD5SUM	b964292d4197638ce79b3f213e8fe89b
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	5130240
Optimality of the best value was proved	NO
Number of terms in the objective function	1008
Biggest coefficient in the objective function	366477312
Number of bits for the biggest coefficient in the objective function	29
Sum of the numbers in the objective function	12643636975
Number of bits of the sum of numbers in the objective function	34
Biggest number in a constraint	366477312
Number of bits of the biggest number in a constraint	29
Biggest sum of numbers in a constraint	12643636975
Number of bits of the biggest sum of numbers	34
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1189.01
Number of variables	1008
Total number of constraints	110
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	48
Number of constraints which are nor clauses,nor cardinality constraints	62
Minimum length of a constraint	1
Maximum length of a constraint	160
Trace number 19060

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc3 THE 2005-04-21 17:45:11 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=17055 boxname=wulflinc3 idbench=1312 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  b964292d4197638ce79b3f213e8fe89b  /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-13-7-mod013.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-13-7-mod013.opb /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-13-7-mod013.opb
IDLAUNCH: 17055
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.190
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.190
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:        704244 kB
Buffers:         29428 kB
Cached:         278340 kB
SwapCached:          0 kB
Active:          46188 kB
Inactive:       264360 kB
HighTotal:      131008 kB
HighFree:        58072 kB
LowTotal:       903652 kB
LowFree:        646172 kB
SwapTotal:     2097136 kB
SwapFree:      2096992 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6844 kB
Slab:            14052 kB
Committed_AS:    71788 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 18:05:14 (client local time) WITH STATUS 10 IN 1200.21 SECONDS
stats: 17055 7 1200.21 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 76 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ##############
c   -- Clauses(.)/Splits(s): (none)
c ---[  74]---> BDD-cost:  478
c ---[  72]---> BDD-cost:  468
c ---[  70]---> BDD-cost:  437
c ---[  68]---> BDD-cost:  422
c ---[  66]---> BDD-cost:  422
c ---[  64]---> BDD-cost:  373
c ---[  63]---> BDD-cost:   19
c ---[  62]---> BDD-cost:   16
c ---[  61]---> BDD-cost:   17
c ---[  60]---> BDD-cost:   15
c ---[  58]---> BDD-cost:  880
c ---[  57]---> BDD-cost:   15
c ---[  56]---> BDD-cost:   14
c ---[  55]---> BDD-cost:   14
c ---[  54]---> BDD-cost:   13
c ---[  53]---> BDD-cost:   19
c ---[  52]---> BDD-cost:   16
c ---[  51]---> BDD-cost:   17
c ---[  50]---> BDD-cost:   15
c ---[  49]---> BDD-cost:   15
c ---[  48]---> BDD-cost:   14
c ---[  46]---> BDD-cost:  876
c ---[  45]---> BDD-cost:   14
c ---[  44]---> BDD-cost:   13
c ---[  43]---> BDD-cost:   16
c ---[  42]---> BDD-cost:   16
c ---[  41]---> BDD-cost:   17
c ---[  40]---> BDD-cost:   15
c ---[  39]---> BDD-cost:   15
c ---[  38]---> BDD-cost:   14
c ---[  37]---> BDD-cost:   14
c ---[  36]---> BDD-cost:   13
c ---[  34]---> BDD-cost:  838
c ---[  33]---> BDD-cost:   15
c ---[  32]---> BDD-cost:   15
c ---[  31]---> BDD-cost:   15
c ---[  30]---> BDD-cost:   15
c ---[  29]---> BDD-cost:   15
c ---[  28]---> BDD-cost:   14
c ---[  27]---> BDD-cost:   14
c ---[  26]---> BDD-cost:   13
c ---[  25]---> BDD-cost:   14
c ---[  24]---> BDD-cost:   14
c ---[  22]---> BDD-cost:  805
c ---[  21]---> BDD-cost:   14
c ---[  20]---> BDD-cost:   14
c ---[  19]---> BDD-cost:   14
c ---[  18]---> BDD-cost:   14
c ---[  17]---> BDD-cost:   14
c ---[  16]---> BDD-cost:   13
c ---[  15]---> BDD-cost:   13
c ---[  14]---> BDD-cost:   13
c ---[  13]---> BDD-cost:   13
c ---[  12]---> BDD-cost:   13
c ---[  10]---> BDD-cost:  722
c ---[   9]---> BDD-cost:   13
c ---[   8]---> BDD-cost:   13
c ---[   7]---> BDD-cost:   13
c ---[   6]---> BDD-cost:   13
c ---[   4]---> BDD-cost:  632
c ---[   2]---> BDD-cost:  498
c ---[   0]---> BDD-cost:  482
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   23983    68004 |    7994       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 12019804[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:159959     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        10 |  469647  1108111 |  156549      10      136    13.6 |  0.000 % |
c |       110 |  469627  1108066 |  172203     109     4232    38.8 |  0.305 % |
c |       260 |  469627  1108066 |  189424     259    12140    46.9 |  0.305 % |
c |       485 |  469614  1108038 |  208366     483    13344    27.6 |  0.307 % |
c |       822 |  469176  1107049 |  229203     816    17467    21.4 |  0.378 % |
c |      1329 |  469176  1107049 |  252123    1323    37438    28.3 |  0.378 % |
c ==============================================================================
c [1mFound solution: 11314862[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   16     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1501 |  469410  1108891 |  156470    1495    42384    28.4 |  0.378 % |
c |      1601 |  469410  1108891 |  172117    1595    42930    26.9 |  0.379 % |
c |      1752 |  469410  1108891 |  189328    1746    46445    26.6 |  0.379 % |
c |      1977 |  469221  1108460 |  208261    1968    53423    27.1 |  0.412 % |
c |      2315 |  469221  1108460 |  229087    2306    64964    28.2 |  0.412 % |
c |      2821 |  469221  1108460 |  251996    2812    72830    25.9 |  0.412 % |
c |      3582 |  469221  1108460 |  277196    3573    82089    23.0 |  0.412 % |
c |      4724 |  469221  1108460 |  304915    4715   118699    25.2 |  0.412 % |
c |      6432 |  469221  1108460 |  335407    6423   434388    67.6 |  0.412 % |
c |      8994 |  469056  1108088 |  368948    8984  1223464   136.2 |  0.440 % |
c |     12838 |  469056  1108088 |  405842   12828  2279093   177.7 |  0.440 % |
c ==============================================================================
c [1mFound solution: 9440856[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     13702 |  469169  1108398 |  156389   13687  2286159   167.0 |  0.440 % |
c |     13802 |  469169  1108398 |  172027   13787  2286856   165.9 |  0.455 % |
c |     13952 |  469169  1108398 |  189230   13937  2288071   164.2 |  0.455 % |
c |     14177 |  468237  1106277 |  208153   14148  2289542   161.8 |  0.620 % |
c |     14514 |  468237  1106277 |  228969   14485  2292415   158.3 |  0.619 % |
c |     15020 |  468237  1106277 |  251866   14991  2297894   153.3 |  0.619 % |
c |     15779 |  468237  1106277 |  277052   15750  2304434   146.3 |  0.619 % |
c |     16918 |  468237  1106277 |  304757   16889  2314098   137.0 |  0.619 % |
c |     18626 |  468237  1106277 |  335233   18597  2349300   126.3 |  0.619 % |
c |     21190 |  468213  1106223 |  368757   21160  2414872   114.1 |  0.623 % |
c |     25035 |  467698  1105048 |  405632   25001  3781442   151.3 |  0.717 % |
c ==============================================================================
c [1mFound solution: 6936352[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   14     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     29559 |  468307  1106581 |  156102   29500  3951563   134.0 |  0.717 % |
c |     29659 |  468307  1106581 |  171712   29600  3975408   134.3 |  0.750 % |
c |     29810 |  468303  1106572 |  188883   29750  3976507   133.7 |  0.750 % |
c |     30036 |  468299  1106563 |  207771   29972  3979340   132.8 |  0.751 % |
c |     30373 |  468155  1106231 |  228548   30307  3982134   131.4 |  0.779 % |
c |     30879 |  468155  1106231 |  251403   30813  3990096   129.5 |  0.779 % |
c |     31639 |  467372  1104440 |  276544   31548  4218343   133.7 |  0.923 % |
c |     32779 |  467372  1104440 |  304198   32688  4344352   132.9 |  0.923 % |
c |     34487 |  467372  1104440 |  334618   34396  4400897   127.9 |  0.923 % |
c |     37052 |  467372  1104440 |  368080   36961  4480046   121.2 |  0.923 % |
c |     40896 |  467372  1104440 |  404888   40805  4985112   122.2 |  0.923 % |
c ==============================================================================
c [1mFound solution: 5998915[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   17     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     42145 |  467344  1104447 |  155781   42053  5161658   122.7 |  0.923 % |
c |     42245 |  467344  1104447 |  171359   42153  5183997   123.0 |  0.953 % |
c |     42395 |  467344  1104447 |  188495   42303  5185645   122.6 |  0.953 % |
c |     42620 |  467252  1104240 |  207344   42522  5191786   122.1 |  0.968 % |
c |     42957 |  467241  1104217 |  228078   42818  5205397   121.6 |  0.972 % |
c |     43463 |  467241  1104217 |  250886   43324  5212231   120.3 |  0.972 % |
c |     44222 |  467241  1104217 |  275975   44083  5224095   118.5 |  0.972 % |
c |     45361 |  467241  1104217 |  303573   45222  5243505   116.0 |  0.972 % |
c ==============================================================================
c [1mFound solution: 5933491[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   15     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     47060 |  467261  1104269 |  155753   46921  5511609   117.5 |  0.972 % |
c |     47161 |  467261  1104269 |  171328   47022  5517962   117.3 |  0.972 % |
c |     47311 |  467261  1104269 |  188461   47172  5526326   117.2 |  0.972 % |
c |     47536 |  466617  1102787 |  207307   47382  5528015   116.7 |  1.093 % |
c |     47873 |  466012  1101415 |  228037   47700  5530455   115.9 |  1.199 % |
c |     48379 |  465921  1101207 |  250841   48204  5585589   115.9 |  1.215 % |
c |     49138 |  465917  1101199 |  275925   48960  5615925   114.7 |  1.216 % |
c |     50277 |  465917  1101199 |  303518   50099  5991500   119.6 |  1.216 % |
c |     51990 |  465290  1099771 |  333870   51786  6034019   116.5 |  1.325 % |
c |     54555 |  465277  1099743 |  367257   54350  6076631   111.8 |  1.327 % |
c |     58400 |  465087  1099310 |  403983   58192  6698129   115.1 |  1.360 % |
c |     64166 |  464548  1098080 |  444381   63927  9275171   145.1 |  1.460 % |
c |     72816 |  464544  1098071 |  488819   72575 11393116   157.0 |  1.460 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -C1_0x2e__bit_7 -C1_0x2e__bit_6 C1_0x2e__bit_5 C1_0x2e__bit_4 C1_0x2e__bit_3 C1_0x2e__bit_2 C1_0x2e__bit_1 -C1_0x2e__bit0 C1_0x2e__bit1 -C1_0x2e__bit2 -C1_0x2e__bit3 -C1_0x2e__bit4 C1_0x2e__bit5 -C1_0x2e__bit6 -C1_0x2e__bit7 -C1_0x2e__bit8 -C1_0x2e__bit9 -C1_0x2e__bit10 -C1_0x2e__bit11 -C1_0x2e__bit12 -C2_0x2e__bit_7 -C2_0x2e__bit_6 C2_0x2e__bit_5 -C2_0x2e__bit_4 -C2_0x2e__bit_3 -C2_0x2e__bit_2 -C2_0x2e__bit_1 -C2_0x2e__bit0 C2_0x2e__bit1 -C2_0x2e__bit2 C2_0x2e__bit3 -C2_0x2e__bit4 -C2_0x2e__bit5 -C2_0x2e__bit6 -C2_0x2e__bit7 -C2_0x2e__bit8 -C2_0x2e__bit9 -C2_0x2e__bit10 -C2_0x2e__bit11 -C2_0x2e__bit12 -C3_0x2e__bit_7 -C3_0x2e__bit_6 -C3_0x2e__bit_5 -C3_0x2e__bit_4 -C3_0x2e__bit_3 -C3_0x2e__bit_2 -C3_0x2e__bit_1 -C3_0x2e__bit0 -C3_0x2e__bit1 -C3_0x2e__bit2 -C3_0x2e__bit3 -C3_0x2e__bit4 -C3_0x2e__bit5 -C3_0x2e__bit6 -C3_0x2e__bit7 -C3_0x2e__bit8 -C3_0x2e__bit9 -C3_0x2e__bit10 -C3_0x2e__bit11 -C3_0x2e__bit12 -C4_0x2e__bit_7 -C4_0x2e__bit_6 -C4_0x2e__bit_5 -C4_0x2e__bit_4 -C4_0x2e__bit_3 -C4_0x2e__bit_2 -C4_0x2e__bit_1 -C4_0x2e__bit0 -C4_0x2e__bit1 -C4_0x2e__bit2 -C4_0x2e__bit3 -C4_0x2e__bit4 -C4_0x2e__bit5 -C4_0x2e__bit6 -C4_0x2e__bit7 -C4_0x2e__bit8 -C4_0x2e__bit9 -C4_0x2e__bit10 -C4_0x2e__bit11 -C4_0x2e__bit12 -C5_0x2e__bit_7 -C5_0x2e__bit_6 -C5_0x2e__bit_5 -C5_0x2e__bit_4 -C5_0x2e__bit_3 -C5_0x2e__bit_2 -C5_0x2e__bit_1 -C5_0x2e__bit0 -C5_0x2e__bit1 -C5_0x2e__bit2 -C5_0x2e__bit3 -C5_0x2e__bit4 -C5_0x2e__bit5 -C5_0x2e__bit6 -C5_0x2e__bit7 -C5_0x2e__bit8 -C5_0x2e__bit9 -C5_0x2e__bit10 -C5_0x2e__bit11 -C5_0x2e__bit12 -C6_0x2e__bit_7 -C6_0x2e__bit_6 -C6_0x2e__bit_5 -C6_0x2e__bit_4 -C6_0x2e__bit_3 -C6_0x2e__bit_2 -C6_0x2e__bit_1 -C6_0x2e__bit0 -C6_0x2e__bit1 -C6_0x2e__bit2 -C6_0x2e__bit3 -C6_0x2e__bit4 -C6_0x2e__bit5 -C6_0x2e__bit6 -C6_0x2e__bit7 -C6_0x2e__bit8 -C6_0x2e__bit9 -C6_0x2e__bit10 -C6_0x2e__bit11 -C6_0x2e__bit12 -C7_0x2e__bit_7 -C7_0x2e__bit_6 -C7_0x2e__bit_5 -C7_0x2e__bit_4 -C7_0x2e__bit_3 -C7_0x2e__bit_2 -C7_0x2e__bit_1 -C7_0x2e__bit0 -C7_0x2e__bit1 -C7_0x2e__bit2 -C7_0x2e__bit3 -C7_0x2e__bit4 -C7_0x2e__bit5 -C7_0x2e__bit6 -C7_0x2e__bit7 -C7_0x2e__bit8 -C7_0x2e__bit9 -C7_0x2e__bit10 -C7_0x2e__bit11 -C7_0x2e__bit12 -C8_0x2e__bit_7 -C8_0x2e__bit_6 -C8_0x2e__bit_5 -C8_0x2e__bit_4 -C8_0x2e__bit_3 -C8_0x2e__bit_2 -C8_0x2e__bit_1 -C8_0x2e__bit0 -C8_0x2e__bit1 -C8_0x2e__bit2 -C8_0x2e__bit3 -C8_0x2e__bit4 -C8_0x2e__bit5 -C8_0x2e__bit6 -C8_0x2e__bit7 -C8_0x2e__bit8 -C8_0x2e__bit9 -C8_0x2e__bit10 -C8_0x2e__bit11 -C8_0x2e__bit12 -C9_0x2e__bit_7 -C9_0x2e__bit_6 -C9_0x2e__bit_5 -C9_0x2e__bit_4 -C9_0x2e__bit_3 -C9_0x2e__bit_2 -C9_0x2e__bit_1 -C9_0x2e__bit0 -C9_0x2e__bit1 -C9_0x2e__bit2 -C9_0x2e__bit3 -C9_0x2e__bit4 -C9_0x2e__bit5 -C9_0x2e__bit6 -C9_0x2e__bit7 -C9_0x2e__bit8 -C9_0x2e__bit9 -C9_0x2e__bit10 -C9_0x2e__bit11 -C9_0x2e__bit12 -C10_0x2e__bit_7 -C10_0x2e__bit_6 -C10_0x2e__bit_5 -C10_0x2e__bit_4 -C10_0x2e__bit_3 -C10_0x2e__bit_2 -C10_0x2e__bit_1 -C10_0x2e__bit0 -C10_0x2e__bit1 -C10_0x2e__bit2 -C10_0x2e__bit3 -C10_0x2e__bit4 -C10_0x2e__bit5 -C10_0x2e__bit6 -C10_0x2e__bit7 -C10_0x2e__bit8 -C10_0x2e__bit9 -C10_0x2e__bit10 -C10_0x2e__bit11 -C10_0x2e__bit12 C11_0x2e__bit_7 -C11_0x2e__bit_6 C11_0x2e__bit_5 -C11_0x2e__bit_4 -C11_0x2e__bit_3 -C11_0x2e__bit_2 -C11_0x2e__bit_1 -C11_0x2e__bit0 -C11_0x2e__bit1 C11_0x2e__bit2 -C11_0x2e__bit3 C11_0x2e__bit4 -C11_0x2e__bit5 -C11_0x2e__bit6 -C11_0x2e__bit7 -C11_0x2e__bit8 -C11_0x2e__bit9 -C11_0x2e__bit10 -C11_0x2e__bit11 -C11_0x2e__bit12 -C12_0x2e__bit_7 -C12_0x2e__bit_6 -C12_0x2e__bit_5 -C12_0x2e__bit_4 C12_0x2e__bit_3 C12_0x2e__bit_2 -C12_0x2e__bit_1 -C12_0x2e__bit0 -C12_0x2e__bit1 -C12_0x2e__bit2 -C12_0x2e__bit3 C12_0x2e__bit4 -C12_0x2e__bit5 -C12_0x2e__bit6 -C12_0x2e__bit7 -C12_0x2e__bit8 -C12_0x2e__bit9 -C12_0x2e__bit10 -C12_0x2e__bit11 -C12_0x2e__bit12 C13_0x2e__bit_7 C13_0x2e__bit_6 -C13_0x2e__bit_5 C13_0x2e__bit_4 -C13_0x2e__bit_3 -C13_0x2e__bit_2 C13_0x2e__bit_1 C13_0x2e__bit0 C13_0x2e__bit1 -C13_0x2e__bit2 -C13_0x2e__bit3 -C13_0x2e__bit4 -C13_0x2e__bit5 -C13_0x2e__bit6 -C13_0x2e__bit7 -C13_0x2e__bit8 -C13_0x2e__bit9 -C13_0x2e__bit10 -C13_0x2e__bit11 -C13_0x2e__bit12 -C14_0x2e__bit_7 -C14_0x2e__bit_6 -C14_0x2e__bit_5 -C14_0x2e__bit_4 -C14_0x2e__bit_3 -C14_0x2e__bit_2 -C14_0x2e__bit_1 -C14_0x2e__bit0 -C14_0x2e__bit1 -C14_0x2e__bit2 -C14_0x2e__bit3 -C14_0x2e__bit4 -C14_0x2e__bit5 -C14_0x2e__bit6 -C14_0x2e__bit7 -C14_0x2e__bit8 -C14_0x2e__bit9 -C14_0x2e__bit10 -C14_0x2e__bit11 -C14_0x2e__bit12 -C15_0x2e__bit_7 -C15_0x2e__bit_6 -C15_0x2e__bit_5 -C15_0x2e__bit_4 -C15_0x2e__bit_3 -C15_0x2e__bit_2 -C15_0x2e__bit_1 -C15_0x2e__bit0 -C15_0x2e__bit1 -C15_0x2e__bit2 -C15_0x2e__bit3 -C15_0x2e__bit4 -C15_0x2e__bit5 -C15_0x2e__bit6 -C15_0x2e__bit7 -C15_0x2e__bit8 -C15_0x2e__bit9 -C15_0x2e__bit10 -C15_0x2e__bit11 -C15_0x2e__bit12 -C16_0x2e__bit_7 -C16_0x2e__bit_6 -C16_0x2e__bit_5 -C16_0x2e__bit_4 -C16_0x2e__bit_3 -C16_0x2e__bit_2 -C16_0x2e__bit_1 -C16_0x2e__bit0 -C16_0x2e__bit1 -C16_0x2e__bit2 -C16_0x2e__bit3 -C16_0x2e__bit4 -C16_0x2e__bit5 -C16_0x2e__bit6 -C16_0x2e__bit7 -C16_0x2e__bit8 -C16_0x2e__bit9 -C16_0x2e__bit10 -C16_0x2e__bit11 -C16_0x2e__bit12 -C17_0x2e__bit_7 -C17_0x2e__bit_6 -C17_0x2e__bit_5 -C17_0x2e__bit_4 -C17_0x2e__bit_3 -C17_0x2e__bit_2 -C17_0x2e__bit_1 -C17_0x2e__bit0 -C17_0x2e__bit1 -C17_0x2e__bit2 -C17_0x2e__bit3 -C17_0x2e__bit4 -C17_0x2e__bit5 -C17_0x2e__bit6 -C17_0x2e__bit7 -C17_0x2e__bit8 -C17_0x2e__bit9 -C17_0x2e__bit10 -C17_0x2e__bit11 -C17_0x2e__bit12 -C18_0x2e__bit_7 C18_0x2e__bit_6 -C18_0x2e__bit_5 -C18_0x2e__bit_4 -C18_0x2e__bit_3 C18_0x2e__bit_2 -C18_0x2e__bit_1 -C18_0x2e__bit0 C18_0x2e__bit1 -C18_0x2e__bit2 -C18_0x2e__bit3 C18_0x2e__bit4 -C18_0x2e__bit5 -C18_0x2e__bit6 -C18_0x2e__bit7 -C18_0x2e__bit8 -C18_0x2e__bit9 -C18_0x2e__bit10 -C18_0x2e__bit11 -C18_0x2e__bit12 C19_0x2e__bit_7 C19_0x2e__bit_6 C19_0x2e__bit_5 C19_0x2e__bit_4 C19_0x2e__bit_3 -C19_0x2e__bit_2 -C19_0x2e__bit_1 -C19_0x2e__bit0 C19_0x2e__bit1 -C19_0x2e__bit2 -C19_0x2e__bit3 -C19_0x2e__bit4 -C19_0x2e__bit5 -C19_0x2e__bit6 -C19_0x2e__bit7 -C19_0x2e__bit8 -C19_0x2e__bit9 -C19_0x2e__bit10 -C19_0x2e__bit11 -C19_0x2e__bit12 -C20_0x2e__bit_7 -C20_0x2e__bit_6 -C20_0x2e__bit_5 -C20_0x2e__bit_4 -C20_0x2e__bit_3 -C20_0x2e__bit_2 -C20_0x2e__bit_1 -C20_0x2e__bit0 -C20_0x2e__bit1 -C20_0x2e__bit2 -C20_0x2e__bit3 -C20_0x2e__bit4 -C20_0x2e__bit5 -C20_0x2e__bit6 -C20_0x2e__bit7 -C20_0x2e__bit8 -C20_0x2e__bit9 -C20_0x2e__bit10 -C20_0x2e__bit11 -C20_0x2e__bit12 C21_0x2e__bit_7 C21_0x2e__bit_6 C21_0x2e__bit_5 C21_0x2e__bit_4 C21_0x2e__bit_3 C21_0x2e__bit_2 -C21_0x2e__bit_1 C21_0x2e__bit0 C21_0x2e__bit1 C21_0x2e__bit2 -C21_0x2e__bit3 -C21_0x2e__bit4 -C21_0x2e__bit5 -C21_0x2e__bit6 -C21_0x2e__bit7 -C21_0x2e__bit8 -C21_0x2e__bit9 -C21_0x2e__bit10 -C21_0x2e__bit11 -C21_0x2e__bit12 -C22_0x2e__bit_7 -C22_0x2e__bit_6 -C22_0x2e__bit_5 -C22_0x2e__bit_4 -C22_0x2e__bit_3 -C22_0x2e__bit_2 -C22_0x2e__bit_1 -C22_0x2e__bit0 C22_0x2e__bit1 -C22_0x2e__bit2 -C22_0x2e__bit3 -C22_0x2e__bit4 -C22_0x2e__bit5 -C22_0x2e__bit6 -C22_0x2e__bit7 -C22_0x2e__bit8 -C22_0x2e__bit9 -C22_0x2e__bit10 -C22_0x2e__bit11 -C22_0x2e__bit12 -C23_0x2e__bit_7 -C23_0x2e__bit_6 -C23_0x2e__bit_5 -C23_0x2e__bit_4 -C23_0x2e__bit_3 -C23_0x2e__bit_2 -C23_0x2e__bit_1 -C23_0x2e__bit0 -C23_0x2e__bit1 -C23_0x2e__bit2 -C23_0x2e__bit3 -C23_0x2e__bit4 -C23_0x2e__bit5 -C23_0x2e__bit6 -C23_0x2e__bit7 -C23_0x2e__bit8 -C23_0x2e__bit9 -C23_0x2e__bit10 -C23_0x2e__bit11 -C23_0x2e__bit12 -C24_0x2e__bit_7 -C24_0x2e__bit_6 -C24_0x2e__bit_5 -C24_0x2e__bit_4 -C24_0x2e__bit_3 -C24_0x2e__bit_2 -C24_0x2e__bit_1 -C24_0x2e__bit0 -C24_0x2e__bit1 -C24_0x2e__bit2 -C24_0x2e__bit3 -C24_0x2e__bit4 -C24_0x2e__bit5 -C24_0x2e__bit6 -C24_0x2e__bit7 -C24_0x2e__bit8 -C24_0x2e__bit9 -C24_0x2e__bit10 -C24_0x2e__bit11 -C24_0x2e__bit12 -C25_0x2e__bit_7 -C25_0x2e__bit_6 C25_0x2e__bit_5 -C25_0x2e__bit_4 -C25_0x2e__bit_3 -C25_0x2e__bit_2 -C25_0x2e__bit_1 -C25_0x2e__bit0 -C25_0x2e__bit1 -C25_0x2e__bit2 -C25_0x2e__bit3 -C25_0x2e__bit4 -C25_0x2e__bit5 -C25_0x2e__bit6 -C25_0x2e__bit7 -C25_0x2e__bit8 -C25_0x2e__bit9 -C25_0x2e__bit10 -C25_0x2e__bit11 -C25_0x2e__bit12 -C26_0x2e__bit_7 -C26_0x2e__bit_6 -C26_0x2e__bit_5 -C26_0x2e__bit_4 -C26_0x2e__bit_3 -C26_0x2e__bit_2 -C26_0x2e__bit_1 -C26_0x2e__bit0 -C26_0x2e__bit1 -C26_0x2e__bit2 -C26_0x2e__bit3 -C26_0x2e__bit4 -C26_0x2e__bit5 -C26_0x2e__bit6 -C26_0x2e__bit7 -C26_0x2e__bit8 -C26_0x2e__bit9 -C26_0x2e__bit10 -C26_0x2e__bit11 -C26_0x2e__bit12 -C27_0x2e__bit_7 -C27_0x2e__bit_6 -C27_0x2e__bit_5 -C27_0x2e__bit_4 -C27_0x2e__bit_3 -C27_0x2e__bit_2 -C27_0x2e__bit_1 -C27_0x2e__bit0 -C27_0x2e__bit1 -C27_0x2e__bit2 -C27_0x2e__bit3 -C27_0x2e__bit4 -C27_0x2e__bit5 -C27_0x2e__bit6 -C27_0x2e__bit7 -C27_0x2e__bit8 -C27_0x2e__bit9 -C27_0x2e__bit10 -C27_0x2e__bit11 -C27_0x2e__bit12 C28_0x2e__bit_7 C28_0x2e__bit_6 -C28_0x2e__bit_5 -C28_0x2e__bit_4 -C28_0x2e__bit_3 -C28_0x2e__bit_2 -C28_0x2e__bit_1 -C28_0x2e__bit0 -C28_0x2e__bit1 -C28_0x2e__bit2 -C28_0x2e__bit3 -C28_0x2e__bit4 -C28_0x2e__bit5 -C28_0x2e__bit6 -C28_0x2e__bit7 -C28_0x2e__bit8 -C28_0x2e__bit9 -C28_0x2e__bit10 -C28_0x2e__bit11 -C28_0x2e__bit12 C29_0x2e__bit_7 C29_0x2e__bit_6 C29_0x2e__bit_5 C29_0x2e__bit_4 C29_0x2e__bit_3 -C29_0x2e__bit_2 C29_0x2e__bit_1 C29_0x2e__bit0 C29_0x2e__bit1 -C29_0x2e__bit2 -C29_0x2e__bit3 -C29_0x2e__bit4 -C29_0x2e__bit5 -C29_0x2e__bit6 -C29_0x2e__bit7 -C29_0x2e__bit8 -C29_0x2e__bit9 -C29_0x2e__bit10 -C29_0x2e__bit11 -C29_0x2e__bit12 -C30_0x2e__bit_7 -C30_0x2e__bit_6 -C30_0x2e__bit_5 -C30_0x2e__bit_4 -C30_0x2e__bit_3 -C30_0x2e__bit_2 -C30_0x2e__bit_1 -C30_0x2e__bit0 -C30_0x2e__bit1 -C30_0x2e__bit2 C30_0x2e__bit3 -C30_0x2e__bit4 -C30_0x2e__bit5 -C30_0x2e__bit6 -C30_0x2e__bit7 -C30_0x2e__bit8 -C30_0x2e__bit9 -C30_0x2e__bit10 -C30_0x2e__bit11 -C30_0x2e__bit12 C31_0x2e__bit_7 C31_0x2e__bit_6 -C31_0x2e__bit_5 -C31_0x2e__bit_4 -C31_0x2e__bit_3 -C31_0x2e__bit_2 -C31_0x2e__bit_1 -C31_0x2e__bit0 -C31_0x2e__bit1 -C31_0x2e__bit2 C31_0x2e__bit3 -C31_0x2e__bit4 -C31_0x2e__bit5 -C31_0x2e__bit6 -C31_0x2e__bit7 -C31_0x2e__bit8 -C31_0x2e__bit9 -C31_0x2e__bit10 -C31_0x2e__bit11 -C31_0x2e__bit12 C32_0x2e__bit_7 C32_0x2e__bit_6 C32_0x2e__bit_5 -C32_0x2e__bit_4 C32_0x2e__bit_3 -C32_0x2e__bit_2 -C32_0x2e__bit_1 -C32_0x2e__bit0 -C32_0x2e__bit1 -C32_0x2e__bit2 -C32_0x2e__bit3 -C32_0x2e__bit4 -C32_0x2e__bit5 -C32_0x2e__bit6 -C32_0x2e__bit7 -C32_0x2e__bit8 -C32_0x2e__bit9 -C32_0x2e__bit10 -C32_0x2e__bit11 -C32_0x2e__bit12 -C33_0x2e__bit_7 -C33_0x2e__bit_6 -C33_0x2e__bit_5 -C33_0x2e__bit_4 -C33_0x2e__bit_3 -C33_0x2e__bit_2 -C33_0x2e__bit_1 -C33_0x2e__bit0 -C33_0x2e__bit1 -C33_0x2e__bit2 -C33_0x2e__bit3 -C33_0x2e__bit4 -C33_0x2e__bit5 -C33_0x2e__bit6 -C33_0x2e__bit7 -C33_0x2e__bit8 -C33_0x2e__bit9 -C33_0x2e__bit10 -C33_0x2e__bit11 -C33_0x2e__bit12 -C34_0x2e__bit_7 C34_0x2e__bit_6 -C34_0x2e__bit_5 C34_0x2e__bit_4 C34_0x2e__bit_3 -C34_0x2e__bit_2 C34_0x2e__bit_1 C34_0x2e__bit0 -C34_0x2e__bit1 -C34_0x2e__bit2 -C34_0x2e__bit3 -C34_0x2e__bit4 -C34_0x2e__bit5 -C34_0x2e__bit6 -C34_0x2e__bit7 -C34_0x2e__bit8 -C34_0x2e__bit9 -C34_0x2e__bit10 -C34_0x2e__bit11 -C34_0x2e__bit12 -C35_0x2e__bit_7 -C35_0x2e__bit_6 C35_0x2e__bit_5 C35_0x2e__bit_4 C35_0x2e__bit_3 -C35_0x2e__bit_2 C35_0x2e__bit_1 -C35_0x2e__bit0 C35_0x2e__bit1 -C35_0x2e__bit2 -C35_0x2e__bit3 -C35_0x2e__bit4 -C35_0x2e__bit5 -C35_0x2e__bit6 -C35_0x2e__bit7 -C35_0x2e__bit8 -C35_0x2e__bit9 -C35_0x2e__bit10 -C35_0x2e__bit11 -C35_0x2e__bit12 C36_0x2e__bit_7 -C36_0x2e__bit_6 C36_0x2e__bit_5 C36_0x2e__bit_4 -C36_0x2e__bit_3 -C36_0x2e__bit_2 C36_0x2e__bit_1 C36_0x2e__bit0 C36_0x2e__bit1 -C36_0x2e__bit2 -C36_0x2e__bit3 -C36_0x2e__bit4 -C36_0x2e__bit5 -C36_0x2e__bit6 -C36_0x2e__bit7 -C36_0x2e__bit8 -C36_0x2e__bit9 -C36_0x2e__bit10 -C36_0x2e__bit11 -C36_0x2e__bit12 -C37_0x2e__bit_7 -C37_0x2e__bit_6 -C37_0x2e__bit_5 -C37_0x2e__bit_4 -C37_0x2e__bit_3 -C37_0x2e__bit_2 -C37_0x2e__bit_1 -C37_0x2e__bit0 -C37_0x2e__bit1 -C37_0x2e__bit2 -C37_0x2e__bit3 -C37_0x2e__bit4 -C37_0x2e__bit5 -C37_0x2e__bit6 -C37_0x2e__bit7 -C37_0x2e__bit8 -C37_0x2e__bit9 -C37_0x2e__bit10 -C37_0x2e__bit11 -C37_0x2e__bit12 -C38_0x2e__bit_7 -C38_0x2e__bit_6 -C38_0x2e__bit_5 -C38_0x2e__bit_4 -C38_0x2e__bit_3 -C38_0x2e__bit_2 -C38_0x2e__bit_1 -C38_0x2e__bit0 -C38_0x2e__bit1 -C38_0x2e__bit2 -C38_0x2e__bit3 -C38_0x2e__bit4 -C38_0x2e__bit5 -C38_0x2e__bit6 -C38_0x2e__bit7 -C38_0x2e__bit8 -C38_0x2e__bit9 -C38_0x2e__bit10 #### 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.65 0.88 0.88 2/54 15479
Raw data (stat): 15479 (runsolver) R 15478 10720 10719 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 488755958 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.0007 s]
Raw data (loadavg): 0.71 0.88 0.88 2/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 14114 0 0 0 965 33 0 0 25 0 1 0 488755958 64847872 13437 4294967295 134512640 134672761 3221224544 3221223680 134560642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15832 13437 603 41 0 15791 0
vsize: 63328
[startup+20.002 s]
Raw data (loadavg): 0.75 0.89 0.88 2/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 14379 0 0 0 1964 35 0 0 25 0 1 0 488755958 66256896 13690 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16176 13690 603 41 0 16135 0
vsize: 64704
[startup+30.0038 s]
Raw data (loadavg): 0.79 0.89 0.88 2/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 14432 0 0 0 2963 35 0 0 25 0 1 0 488755958 66527232 13743 4294967295 134512640 134672761 3221224544 3221223500 1075350084 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16242 13743 603 41 0 16201 0
vsize: 64968
[startup+40.0041 s]
Raw data (loadavg): 0.82 0.89 0.88 2/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 14747 0 0 0 3963 36 0 0 25 0 1 0 488755958 67866624 14058 4294967295 134512640 134672761 3221224544 3221223648 134560148 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16569 14058 603 41 0 16528 0
vsize: 66276
[startup+50.0045 s]
Raw data (loadavg): 0.85 0.90 0.89 2/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 14906 0 0 0 4962 37 0 0 25 0 1 0 488755958 68538368 14217 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16733 14217 603 41 0 16692 0
vsize: 66932
[startup+60.0053 s]
Raw data (loadavg): 0.87 0.90 0.89 2/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 15163 0 0 0 5961 38 0 0 25 0 1 0 488755958 69480448 14474 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16963 14474 603 41 0 16922 0
vsize: 67852
[startup+70.0057 s]
Raw data (loadavg): 0.89 0.90 0.89 2/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 15367 0 0 0 6960 38 0 0 25 0 1 0 488755958 70389760 14678 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17185 14678 603 41 0 17144 0
vsize: 68740
[startup+80.007 s]
Raw data (loadavg): 0.91 0.90 0.89 2/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 15584 0 0 0 7960 39 0 0 25 0 1 0 488755958 71327744 14895 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17414 14895 603 41 0 17373 0
vsize: 69656
[startup+90.0079 s]
Raw data (loadavg): 0.92 0.91 0.89 2/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 15771 0 0 0 8959 40 0 0 25 0 1 0 488755958 71983104 15082 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17574 15082 603 41 0 17533 0
vsize: 70296
[startup+100.007 s]
Raw data (loadavg): 0.93 0.91 0.89 2/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 16053 0 0 0 9958 41 0 0 25 0 1 0 488755958 73183232 15364 4294967295 134512640 134672761 3221224544 3221223648 134560350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17867 15364 603 41 0 17826 0
vsize: 71468
[startup+110.008 s]
Raw data (loadavg): 0.94 0.91 0.89 2/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 16321 0 0 0 10957 42 0 0 25 0 1 0 488755958 74264576 15632 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18131 15632 603 41 0 18090 0
vsize: 72524
[startup+120.009 s]
Raw data (loadavg): 0.95 0.91 0.89 2/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 16647 0 0 0 11956 43 0 0 25 0 1 0 488755958 75612160 15958 4294967295 134512640 134672761 3221224544 3221223648 134560048 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18460 15958 603 41 0 18419 0
vsize: 73840
[startup+130.01 s]
Raw data (loadavg): 0.96 0.92 0.89 2/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 16705 0 0 0 12955 44 0 0 25 0 1 0 488755958 75694080 15995 4294967295 134512640 134672761 3221224544 3221223680 134560673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18480 15995 603 41 0 18439 0
vsize: 73920
[startup+140.011 s]
Raw data (loadavg): 0.96 0.92 0.89 2/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 16743 0 0 0 13954 45 0 0 25 0 1 0 488755958 75968512 16033 4294967295 134512640 134672761 3221224544 3221223680 134560619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18547 16033 603 41 0 18506 0
vsize: 74188
[startup+150.011 s]
Raw data (loadavg): 0.97 0.92 0.90 2/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 16773 0 0 0 14954 45 0 0 25 0 1 0 488755958 76103680 16063 4294967295 134512640 134672761 3221224544 3221223712 134561391 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18580 16063 603 41 0 18539 0
vsize: 74320
[startup+160.012 s]
Raw data (loadavg): 0.97 0.92 0.90 2/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 16831 0 0 0 15954 46 0 0 25 0 1 0 488755958 76369920 16121 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18645 16121 603 41 0 18604 0
vsize: 74580
[startup+170.012 s]
Raw data (loadavg): 0.98 0.92 0.90 2/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 16975 0 0 0 16953 47 0 0 25 0 1 0 488755958 76902400 16265 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18775 16265 603 41 0 18734 0
vsize: 75100
[startup+180.014 s]
Raw data (loadavg): 0.98 0.93 0.90 2/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 17319 0 0 0 17952 48 0 0 25 0 1 0 488755958 78249984 16609 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19104 16609 603 41 0 19063 0
vsize: 76416
[startup+190.015 s]
Raw data (loadavg): 0.98 0.93 0.90 2/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 17873 0 0 0 18951 49 0 0 25 0 1 0 488755958 80646144 17163 4294967295 134512640 134672761 3221224544 3221223728 134558831 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19689 17163 603 41 0 19648 0
vsize: 78756
[startup+200.015 s]
Raw data (loadavg): 0.98 0.93 0.90 2/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 18223 0 0 0 19950 50 0 0 25 0 1 0 488755958 81944576 17513 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20006 17513 603 41 0 19965 0
vsize: 80024
[startup+210.016 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 18387 0 0 0 20949 51 0 0 25 0 1 0 488755958 82616320 17677 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20170 17677 603 41 0 20129 0
vsize: 80680
[startup+220.017 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 18483 0 0 0 21948 52 0 0 25 0 1 0 488755958 82956288 17753 4294967295 134512640 134672761 3221224544 3221223744 134557913 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20253 17753 603 41 0 20212 0
vsize: 81012
[startup+230.018 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 18699 0 0 0 22947 53 0 0 25 0 1 0 488755958 83787776 17969 4294967295 134512640 134672761 3221224544 3221223744 134557900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20456 17969 603 41 0 20415 0
vsize: 81824
[startup+240.018 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 18739 0 0 0 23947 53 0 0 25 0 1 0 488755958 83922944 18009 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20489 18009 603 41 0 20448 0
vsize: 81956
[startup+250.019 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 18894 0 0 0 24947 54 0 0 25 0 1 0 488755958 84733952 18164 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20687 18164 603 41 0 20646 0
vsize: 82748
[startup+260.02 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 18894 0 0 0 25947 54 0 0 25 0 1 0 488755958 84733952 18164 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20687 18164 603 41 0 20646 0
vsize: 82748
[startup+270.021 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 18905 0 0 0 26946 54 0 0 25 0 1 0 488755958 84733952 18175 4294967295 134512640 134672761 3221224544 3221223712 134560855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20687 18175 603 41 0 20646 0
vsize: 82748
[startup+280.023 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 18929 0 0 0 27946 55 0 0 25 0 1 0 488755958 84865024 18199 4294967295 134512640 134672761 3221224544 3221223712 134560864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20719 18199 603 41 0 20678 0
vsize: 82876
[startup+290.024 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 18956 0 0 0 28946 55 0 0 25 0 1 0 488755958 85000192 18226 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20752 18226 603 41 0 20711 0
vsize: 83008
[startup+300.023 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 18982 0 0 0 29945 56 0 0 25 0 1 0 488755958 85135360 18252 4294967295 134512640 134672761 3221224544 3221223744 134557828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20785 18252 603 41 0 20744 0
vsize: 83140
[startup+310.024 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 18997 0 0 0 30945 56 0 0 25 0 1 0 488755958 85135360 18267 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20785 18267 603 41 0 20744 0
vsize: 83140
[startup+320.025 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 19017 0 0 0 31945 56 0 0 25 0 1 0 488755958 85266432 18287 4294967295 134512640 134672761 3221224544 3221223712 134560833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20817 18287 603 41 0 20776 0
vsize: 83268
[startup+330.026 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 19039 0 0 0 32945 57 0 0 25 0 1 0 488755958 85266432 18309 4294967295 134512640 134672761 3221224544 3221223712 134561391 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20817 18309 603 41 0 20776 0
vsize: 83268
[startup+340.027 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 19098 0 0 0 33944 57 0 0 25 0 1 0 488755958 85536768 18368 4294967295 134512640 134672761 3221224544 3221223688 134560630 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20883 18368 603 41 0 20842 0
vsize: 83532
[startup+350.028 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 19225 0 0 0 34944 58 0 0 25 0 1 0 488755958 86200320 18495 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21045 18495 603 41 0 21004 0
vsize: 84180
[startup+360.028 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 19347 0 0 0 35943 59 0 0 25 0 1 0 488755958 86585344 18617 4294967295 134512640 134672761 3221224544 3221223680 134560598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21139 18617 603 41 0 21098 0
vsize: 84556
[startup+370.028 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 19449 0 0 0 36943 59 0 0 25 0 1 0 488755958 86990848 18719 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21238 18719 603 41 0 21197 0
vsize: 84952
[startup+380.029 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 19588 0 0 0 37942 60 0 0 25 0 1 0 488755958 87519232 18858 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21367 18858 603 41 0 21326 0
vsize: 85468
[startup+390.029 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 19699 0 0 0 38941 61 0 0 25 0 1 0 488755958 88072192 18969 4294967295 134512640 134672761 3221224544 3221223712 134561378 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21502 18969 603 41 0 21461 0
vsize: 86008
[startup+400.03 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 19793 0 0 0 39941 62 0 0 25 0 1 0 488755958 88346624 19063 4294967295 134512640 134672761 3221224544 3221223248 134597018 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21569 19063 603 41 0 21528 0
vsize: 86276
[startup+410.031 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 19842 0 0 0 40940 62 0 0 25 0 1 0 488755958 88535040 19091 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21615 19091 603 41 0 21574 0
vsize: 86460
[startup+420.031 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 19923 0 0 0 41940 63 0 0 25 0 1 0 488755958 88801280 19172 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21680 19172 603 41 0 21639 0
vsize: 86720
[startup+430.032 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 20026 0 0 0 42940 63 0 0 25 0 1 0 488755958 89198592 19275 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21777 19275 603 41 0 21736 0
vsize: 87108
[startup+440.032 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 20140 0 0 0 43939 64 0 0 25 0 1 0 488755958 89726976 19389 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21906 19389 603 41 0 21865 0
vsize: 87624
[startup+450.031 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 20236 0 0 0 44939 64 0 0 25 0 1 0 488755958 89956352 19467 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21962 19467 603 41 0 21921 0
vsize: 87848
[startup+460.033 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 20247 0 0 0 45939 64 0 0 25 0 1 0 488755958 90087424 19478 4294967295 134512640 134672761 3221224544 3221223712 134561378 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21994 19478 603 41 0 21953 0
vsize: 87976
[startup+470.034 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 20302 0 0 0 46939 65 0 0 25 0 1 0 488755958 90222592 19533 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22027 19533 603 41 0 21986 0
vsize: 88108
[startup+480.034 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 20340 0 0 0 47938 65 0 0 25 0 1 0 488755958 90492928 19571 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22093 19571 603 41 0 22052 0
vsize: 88372
[startup+490.035 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 20512 0 0 0 48938 66 0 0 25 0 1 0 488755958 91181056 19743 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22261 19743 603 41 0 22220 0
vsize: 89044
[startup+500.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 20641 0 0 0 49937 66 0 0 25 0 1 0 488755958 91717632 19872 4294967295 134512640 134672761 3221224544 3221223648 134560529 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22392 19872 603 41 0 22351 0
vsize: 89568
[startup+510.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 20724 0 0 0 50937 67 0 0 25 0 1 0 488755958 91983872 19955 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22457 19955 603 41 0 22416 0
vsize: 89828
[startup+520.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 20774 0 0 0 51937 67 0 0 25 0 1 0 488755958 92254208 20005 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22523 20005 603 41 0 22482 0
vsize: 90092
[startup+530.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 20799 0 0 0 52937 67 0 0 25 0 1 0 488755958 92254208 20030 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22523 20030 603 41 0 22482 0
vsize: 90092
[startup+540.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 20816 0 0 0 53936 68 0 0 25 0 1 0 488755958 92389376 20047 4294967295 134512640 134672761 3221224544 3221223680 134560718 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22556 20047 603 41 0 22515 0
vsize: 90224
[startup+550.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 21060 0 0 0 54934 70 0 0 25 0 1 0 488755958 93323264 20291 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22784 20291 603 41 0 22743 0
vsize: 91136
[startup+560.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 21142 0 0 0 55934 70 0 0 25 0 1 0 488755958 93724672 20373 4294967295 134512640 134672761 3221224544 3221223728 134559161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22882 20373 603 41 0 22841 0
vsize: 91528
[startup+570.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 21274 0 0 0 56934 71 0 0 25 0 1 0 488755958 94265344 20505 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23014 20505 603 41 0 22973 0
vsize: 92056
[startup+580.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 21391 0 0 0 57933 71 0 0 25 0 1 0 488755958 94670848 20622 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23113 20622 603 41 0 23072 0
vsize: 92452
[startup+590.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 21483 0 0 0 58933 72 0 0 25 0 1 0 488755958 95084544 20714 4294967295 134512640 134672761 3221224544 3221223712 134561025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23214 20714 603 41 0 23173 0
vsize: 92856
[startup+600.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 21821 0 0 0 59932 73 0 0 25 0 1 0 488755958 96468992 21052 4294967295 134512640 134672761 3221224544 3221223712 134561264 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23552 21052 603 41 0 23511 0
vsize: 94208
[startup+610.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 22048 0 0 0 60931 74 0 0 25 0 1 0 488755958 97402880 21279 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23780 21279 603 41 0 23739 0
vsize: 95120
[startup+620.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 22203 0 0 0 61931 74 0 0 25 0 1 0 488755958 98062336 21434 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23941 21434 603 41 0 23900 0
vsize: 95764
[startup+630.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 22316 0 0 0 62931 75 0 0 25 0 1 0 488755958 98615296 21547 4294967295 134512640 134672761 3221224544 3221223648 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24076 21547 603 41 0 24035 0
vsize: 96304
[startup+640.044 s]
Raw data (loadavg): 0.99 0.97 0.91 3/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 22380 0 0 0 63930 75 0 0 25 0 1 0 488755958 98750464 21611 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24109 21611 603 41 0 24068 0
vsize: 96436
[startup+650.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 22417 0 0 0 64930 75 0 0 25 0 1 0 488755958 99024896 21648 4294967295 134512640 134672761 3221224544 3221223648 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24176 21648 603 41 0 24135 0
vsize: 96704
[startup+660.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 22497 0 0 0 65930 76 0 0 25 0 1 0 488755958 99291136 21728 4294967295 134512640 134672761 3221224544 3221223648 134560226 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24241 21728 603 41 0 24200 0
vsize: 96964
[startup+670.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 22549 0 0 0 66931 76 0 0 25 0 1 0 488755958 99426304 21780 4294967295 134512640 134672761 3221224544 3221223648 134560031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24274 21780 603 41 0 24233 0
vsize: 97096
[startup+680.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 22602 0 0 0 67931 76 0 0 25 0 1 0 488755958 99688448 21833 4294967295 134512640 134672761 3221224544 3221223680 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24338 21833 603 41 0 24297 0
vsize: 97352
[startup+690.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 22785 0 0 0 68930 76 0 0 25 0 1 0 488755958 100630528 22016 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24568 22016 603 41 0 24527 0
vsize: 98272
[startup+700.047 s]
Raw data (loadavg): 0.99 0.97 0.91 3/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 22871 0 0 0 69930 76 0 0 25 0 1 0 488755958 101031936 22102 4294967295 134512640 134672761 3221224544 3221223648 134560279 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24666 22102 603 41 0 24625 0
vsize: 98664
[startup+710.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 22880 0 0 0 70931 76 0 0 25 0 1 0 488755958 101031936 22111 4294967295 134512640 134672761 3221224544 3221223648 134560350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24666 22111 603 41 0 24625 0
vsize: 98664
[startup+720.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 23009 0 0 0 71930 77 0 0 25 0 1 0 488755958 101572608 22240 4294967295 134512640 134672761 3221224544 3221223728 134559542 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24798 22240 603 41 0 24757 0
vsize: 99192
[startup+730.049 s]
Raw data (loadavg): 0.99 0.97 0.91 3/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 23063 0 0 0 72931 77 0 0 25 0 1 0 488755958 101842944 22294 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24864 22294 603 41 0 24823 0
vsize: 99456
[startup+740.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 23289 0 0 0 73930 78 0 0 25 0 1 0 488755958 102641664 22520 4294967295 134512640 134672761 3221224544 3221223648 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25059 22520 603 41 0 25018 0
vsize: 100236
[startup+750.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 23524 0 0 0 74930 78 0 0 25 0 1 0 488755958 103604224 22755 4294967295 134512640 134672761 3221224544 3221223712 134561256 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25294 22755 603 41 0 25253 0
vsize: 101176
[startup+760.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 23719 0 0 0 75929 79 0 0 25 0 1 0 488755958 104517632 22950 4294967295 134512640 134672761 3221224544 3221223648 134559929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25517 22950 603 41 0 25476 0
vsize: 102068
[startup+770.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 23843 0 0 0 76929 79 0 0 25 0 1 0 488755958 104996864 23074 4294967295 134512640 134672761 3221224544 3221223648 134559995 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25634 23074 603 41 0 25593 0
vsize: 102536
[startup+780.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 24043 0 0 0 77928 80 0 0 25 0 1 0 488755958 105734144 23274 4294967295 134512640 134672761 3221224544 3221223728 134558694 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25814 23274 603 41 0 25773 0
vsize: 103256
[startup+790.05 s]
Raw data (loadavg): 0.99 0.97 0.91 3/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 24104 0 0 0 78927 81 0 0 25 0 1 0 488755958 106000384 23335 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25879 23335 603 41 0 25838 0
vsize: 103516
[startup+800.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 24193 0 0 0 79927 81 0 0 25 0 1 0 488755958 106401792 23424 4294967295 134512640 134672761 3221224544 3221223648 134560025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25977 23424 603 41 0 25936 0
vsize: 103908
[startup+810.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 24316 0 0 0 80927 82 0 0 25 0 1 0 488755958 106917888 23547 4294967295 134512640 134672761 3221224544 3221223648 134560002 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26103 23547 603 41 0 26062 0
vsize: 104412
[startup+820.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 24413 0 0 0 81927 83 0 0 25 0 1 0 488755958 107585536 23644 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26266 23644 603 41 0 26225 0
vsize: 105064
[startup+830.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 24558 0 0 0 82926 83 0 0 25 0 1 0 488755958 108113920 23789 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26395 23789 603 41 0 26354 0
vsize: 105580
[startup+840.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 24659 0 0 0 83926 83 0 0 25 0 1 0 488755958 108523520 23890 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26495 23890 603 41 0 26454 0
vsize: 105980
[startup+850.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 24759 0 0 0 84925 84 0 0 25 0 1 0 488755958 108998656 23990 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26611 23990 603 41 0 26570 0
vsize: 106444
[startup+860.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 24858 0 0 0 85926 84 0 0 25 0 1 0 488755958 109387776 24089 4294967295 134512640 134672761 3221224544 3221223648 134559835 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26706 24089 603 41 0 26665 0
vsize: 106824
[startup+870.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 24969 0 0 0 86926 84 0 0 25 0 1 0 488755958 109772800 24200 4294967295 134512640 134672761 3221224544 3221223648 134560169 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26800 24200 603 41 0 26759 0
vsize: 107200
[startup+880.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 25066 0 0 0 87926 84 0 0 25 0 1 0 488755958 110186496 24297 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26901 24297 603 41 0 26860 0
vsize: 107604
[startup+890.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15479
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 25176 0 0 0 88925 85 0 0 25 0 1 0 488755958 110694400 24407 4294967295 134512640 134672761 3221224544 3221223648 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27025 24407 603 41 0 26984 0
vsize: 108100
[startup+900.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15532
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 25290 0 0 0 89921 88 0 0 25 0 1 0 488755958 111099904 24521 4294967295 134512640 134672761 3221224544 3221223648 134560158 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27124 24521 603 41 0 27083 0
vsize: 108496
[startup+910.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15532
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 25470 0 0 0 90921 89 0 0 25 0 1 0 488755958 111915008 24701 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27323 24701 603 41 0 27282 0
vsize: 109292
[startup+920.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15532
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 25611 0 0 0 91921 89 0 0 25 0 1 0 488755958 112451584 24842 4294967295 134512640 134672761 3221224544 3221223648 134560326 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27454 24842 603 41 0 27413 0
vsize: 109816
[startup+930.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15532
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 25713 0 0 0 92921 89 0 0 25 0 1 0 488755958 112852992 24944 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27552 24944 603 41 0 27511 0
vsize: 110208
[startup+940.063 s]
Raw data (loadavg): 0.99 0.97 0.91 3/54 15532
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 25845 0 0 0 93921 89 0 0 25 0 1 0 488755958 113393664 25076 4294967295 134512640 134672761 3221224544 3221223648 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27684 25076 603 41 0 27643 0
vsize: 110736
[startup+950.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15532
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 25979 0 0 0 94921 90 0 0 25 0 1 0 488755958 113913856 25210 4294967295 134512640 134672761 3221224544 3221223648 134560207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27811 25210 603 41 0 27770 0
vsize: 111244
[startup+960.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15532
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 26147 0 0 0 95921 90 0 0 25 0 1 0 488755958 114589696 25378 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27976 25378 603 41 0 27935 0
vsize: 111904
[startup+970.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15534
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 26187 0 0 0 96921 90 0 0 25 0 1 0 488755958 114728960 25418 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28010 25418 603 41 0 27969 0
vsize: 112040
[startup+980.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15534
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 26252 0 0 0 97920 90 0 0 25 0 1 0 488755958 114995200 25483 4294967295 134512640 134672761 3221224544 3221223712 134561378 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28075 25483 603 41 0 28034 0
vsize: 112300
[startup+990.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15534
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 26321 0 0 0 98920 91 0 0 25 0 1 0 488755958 115384320 25552 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28170 25552 603 41 0 28129 0
vsize: 112680
[startup+1000.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15534
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 26439 0 0 0 99920 91 0 0 25 0 1 0 488755958 115789824 25670 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28269 25670 603 41 0 28228 0
vsize: 113076
[startup+1010.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15534
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 26671 0 0 0 100920 92 0 0 25 0 1 0 488755958 116719616 25902 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28496 25902 603 41 0 28455 0
vsize: 113984
[startup+1020.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15534
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 26789 0 0 0 101920 92 0 0 25 0 1 0 488755958 117264384 26020 4294967295 134512640 134672761 3221224544 3221223648 134560191 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28629 26020 603 41 0 28588 0
vsize: 114516
[startup+1030.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15534
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 26978 0 0 0 102919 93 0 0 25 0 1 0 488755958 117948416 26209 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28796 26209 603 41 0 28755 0
vsize: 115184
[startup+1040.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15534
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 27178 0 0 0 103919 93 0 0 25 0 1 0 488755958 118898688 26409 4294967295 134512640 134672761 3221224544 3221223728 134558687 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29028 26409 603 41 0 28987 0
vsize: 116112
[startup+1050.06 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 15534
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 27424 0 0 0 104918 94 0 0 25 0 1 0 488755958 119824384 26655 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29254 26655 603 41 0 29213 0
vsize: 117016
[startup+1060.06 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 15534
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 27657 0 0 0 105918 95 0 0 25 0 1 0 488755958 120750080 26888 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29480 26888 603 41 0 29439 0
vsize: 117920
[startup+1070.06 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 15534
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 27917 0 0 0 106917 96 0 0 25 0 1 0 488755958 121892864 27148 4294967295 134512640 134672761 3221224544 3221223728 134559622 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29759 27148 603 41 0 29718 0
vsize: 119036
[startup+1080.06 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 15534
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 28089 0 0 0 107916 96 0 0 25 0 1 0 488755958 122531840 27320 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29915 27320 603 41 0 29874 0
vsize: 119660
[startup+1090.06 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 15534
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 28276 0 0 0 108916 97 0 0 25 0 1 0 488755958 123338752 27507 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30112 27507 603 41 0 30071 0
vsize: 120448
[startup+1100.06 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 15534
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 28389 0 0 0 109915 97 0 0 25 0 1 0 488755958 123744256 27620 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30211 27620 603 41 0 30170 0
vsize: 120844
[startup+1110.06 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 15534
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 28547 0 0 0 110915 98 0 0 25 0 1 0 488755958 124411904 27778 4294967295 134512640 134672761 3221224544 3221223728 134559031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30374 27778 603 41 0 30333 0
vsize: 121496
[startup+1120.06 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 15534
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 28679 0 0 0 111915 98 0 0 25 0 1 0 488755958 124948480 27910 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30505 27910 603 41 0 30464 0
vsize: 122020
[startup+1130.06 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 15534
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 28727 0 0 0 112915 99 0 0 25 0 1 0 488755958 125202432 27958 4294967295 134512640 134672761 3221224544 3221223648 134559979 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30567 27958 603 41 0 30526 0
vsize: 122268
[startup+1140.06 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 15534
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 28822 0 0 0 113915 99 0 0 25 0 1 0 488755958 125579264 28053 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30659 28053 603 41 0 30618 0
vsize: 122636
[startup+1150.06 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 15534
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 28912 0 0 0 114914 100 0 0 25 0 1 0 488755958 125931520 28143 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30745 28143 603 41 0 30704 0
vsize: 122980
[startup+1160.06 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 15534
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 29007 0 0 0 115914 100 0 0 25 0 1 0 488755958 126332928 28238 4294967295 134512640 134672761 3221224544 3221223648 134560399 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30843 28238 603 41 0 30802 0
vsize: 123372
[startup+1170.06 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 15534
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 29152 0 0 0 116914 100 0 0 25 0 1 0 488755958 126889984 28383 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30979 28383 603 41 0 30938 0
vsize: 123916
[startup+1180.06 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 15534
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 29271 0 0 0 117914 100 0 0 25 0 1 0 488755958 127311872 28502 4294967295 134512640 134672761 3221224544 3221223648 134560373 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31082 28502 603 41 0 31041 0
vsize: 124328
[startup+1190.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15534
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 29377 0 0 0 118914 101 0 0 25 0 1 0 488755958 127848448 28608 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31213 28608 603 41 0 31172 0
vsize: 124852
[startup+1200.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15536
Raw data (stat): 15479 (minisat+) R 15478 10720 10719 0 -1 0 29512 0 0 0 119914 101 0 0 25 0 1 0 488755958 128323584 28743 4294967295 134512640 134672761 3221224544 3221223680 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31329 28743 603 41 0 31288 0
vsize: 125316
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.13 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 15536
Raw data (stat): 15479 (minisat+) Z 15478 10720 10719 0 -1 12 29515 0 0 0 119914 106 0 0 25 0 1 0 488755958 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.13
CPU time (s): 1200.21
CPU user time (s): 1199.14
CPU system time (s): 1.06884
CPU usage (%): 100.007
Max. virtual memory (Kb): 125316
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####