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-air01.opb
MD5SUM	90db1995bd949fc5ac74143a523f3bcf
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	3398
Optimality of the best value was proved	NO
Number of terms in the objective function	771
Biggest coefficient in the objective function	3698
Number of bits for the biggest coefficient in the objective function	12
Sum of the numbers in the objective function	1192753
Number of bits of the sum of numbers in the objective function	21
Biggest number in a constraint	3698
Number of bits of the biggest number in a constraint	12
Biggest sum of numbers in a constraint	1192753
Number of bits of the biggest sum of numbers	21
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.02884
Number of variables	771
Total number of constraints	794
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	794
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	438
Trace number 15927

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc3 THE 2005-04-21 05:57:52 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=16613 boxname=wulflinc3 idbench=1278 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  90db1995bd949fc5ac74143a523f3bcf  /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-13-7-air01.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-13-7-air01.opb /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-13-7-air01.opb
IDLAUNCH: 16613
/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:        513700 kB
Buffers:         34032 kB
Cached:         463536 kB
SwapCached:         56 kB
Active:          46864 kB
Inactive:       453576 kB
HighTotal:      131008 kB
HighFree:        37464 kB
LowTotal:       903652 kB
LowFree:        476236 kB
SwapTotal:     2097136 kB
SwapFree:      2096992 kB
Dirty:              32 kB
Writeback:           0 kB
Mapped:           6840 kB
Slab:            14904 kB
Committed_AS:    71676 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 06:17:55 (client local time) WITH STATUS 10 IN 1200.53 SECONDS
stats: 16613 7 1200.53 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 46 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #######################
c   -- Clauses(.)/Splits(s): (none)
c ---[  44]---> BDD-cost:   49
c ---[  42]---> BDD-cost:   39
c ---[  40]---> BDD-cost:   41
c ---[  38]---> BDD-cost:   53
c ---[  36]---> BDD-cost:   63
c ---[  34]---> BDD-cost:   61
c ---[  32]---> BDD-cost:   83
c ---[  30]---> BDD-cost:  111
c ---[  28]---> BDD-cost:  139
c ---[  26]---> BDD-cost:  197
c ---[  24]---> BDD-cost:  233
c ---[  22]---> BDD-cost:  273
c ---[  20]---> BDD-cost:  353
c ---[  18]---> BDD-cost:  331
c ---[  16]---> BDD-cost:  527
c ---[  14]---> BDD-cost:  589
c ---[  12]---> BDD-cost:  607
c ---[  10]---> BDD-cost:  559
c ---[   8]---> BDD-cost:  755
c ---[   6]---> BDD-cost:  769
c ---[   4]---> BDD-cost:  741
c ---[   2]---> BDD-cost:  781
c ---[   0]---> BDD-cost:  873
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   20564    53488 |    6854       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 9600[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:405471     Base: 2 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        26 | 1076333  2519033 |  358777      26     1591    61.2 |  0.000 % |
c ==============================================================================
c [1mFound solution: 7246[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        41 | 1081308  2532280 |  360436      41     2258    55.1 |  0.000 % |
c ==============================================================================
c [1mFound solution: 6035[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        49 | 1082093  2535275 |  360697      49     3635    74.2 |  0.000 % |
c |       162 | 1081886  2534808 |  396766     161    34933   217.0 |  0.020 % |
c |       314 | 1081870  2534772 |  436443     312    59302   190.1 |  0.021 % |
c |       539 | 1081556  2534062 |  480087     536   173133   323.0 |  0.042 % |
c |       876 | 1078519  2527142 |  528096     815   192949   236.7 |  0.263 % |
c ==============================================================================
c [1mFound solution: 5928[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       950 | 1080226  2531316 |  360075     889   233545   262.7 |  0.263 % |
c |      1050 | 1079697  2530112 |  396082     987   245138   248.4 |  0.302 % |
c |      1200 | 1079697  2530112 |  435690    1137   260298   228.9 |  0.302 % |
c |      1425 | 1079573  2529830 |  479259    1360   262082   192.7 |  0.311 % |
c |      1765 | 1077094  2524166 |  527185    1659   276840   166.9 |  0.494 % |
c |      2272 | 1073638  2516255 |  579904    2113   391798   185.4 |  0.751 % |
c |      3032 | 1073207  2515277 |  637894    2855  1360522   476.5 |  0.782 % |
c ==============================================================================
c [1mFound solution: 5471[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:305145     Base: 2 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3194 | 1838554  4302735 |  612851    3016  1397590   463.4 |  0.782 % |
c ==============================================================================
c [1mFound solution: 5311[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3218 | 1840124  4308648 |  613374    3040  1418436   466.6 |  0.782 % |
c |      3318 | 1840124  4308648 |  674711    3140  1423590   453.4 |  0.661 % |
c |      3469 | 1839313  4306837 |  742182    3280  1436724   438.0 |  0.697 % |
c |      3696 | 1836198  4299794 |  816400    3466  1459627   421.1 |  0.834 % |
c |      4033 | 1829295  4284035 |  898040    3784  1605079   424.2 |  1.140 % |
c |      4542 | 1829295  4284035 |  987844    4293  1859193   433.1 |  1.140 % |
c |      5304 | 1829295  4284035 | 1086629    5055  2513459   497.2 |  1.140 % |
c ==============================================================================
c [1mFound solution: 4729[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:331342     Base: 2 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6102 | 2652877  6207237 |  884292    5818  3333972   573.0 |  1.140 % |
c |      6202 | 2652020  6205291 |  972721    5915  3359494   568.0 |  1.230 % |
c ==============================================================================
c [1mFound solution: 4607[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:332348     Base: 2 2 3 3 3 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6340 | 3520429  8233160 | 1173476    6000  3368486   561.4 |  1.230 % |
c |      6441 | 3513168  8216645 | 1290823    6079  3370074   554.4 |  1.421 % |
c |      6597 | 3510881  8211423 | 1419905    6233  3506059   562.5 |  1.473 % |
c |      6822 | 3510532  8210636 | 1561896    6457  3537448   547.8 |  1.481 % |
c |      7159 | 3505536  8199254 | 1718086    6711  3570665   532.1 |  1.598 % |
c |      7665 | 3496472  8178540 | 1889894    7107  3686794   518.8 |  1.811 % |
c |      8424 | 3496205  8177935 | 2078884    7865  3920527   498.5 |  1.818 % |
c |      9563 | 3493093  8170815 | 2286772    8994  4433306   492.9 |  1.892 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -CL000001_bit0 -CL000002_bit0 -CL000003_bit0 -CL000004_bit0 CL000005_bit0 -CL000006_bit0 -CL000007_bit0 -CL000008_bit0 -CL000009_bit0 -CL000010_bit0 -CL000011_bit0 -CL000012_bit0 -CL000013_bit0 -CL000014_bit0 -CL000015_bit0 -CL000016_bit0 -CL000017_bit0 -CL000018_bit0 -CL000019_bit0 -CL000020_bit0 -CL000021_bit0 -CL000022_bit0 -CL000023_bit0 -CL000024_bit0 -CL000025_bit0 -CL000026_bit0 -CL000027_bit0 -CL000028_bit0 -CL000029_bit0 -CL000030_bit0 -CL000031_bit0 -CL000032_bit0 -CL000033_bit0 -CL000034_bit0 -CL000035_bit0 -CL000036_bit0 -CL000037_bit0 -CL000038_bit0 -CL000039_bit0 -CL000040_bit0 -CL000041_bit0 -CL000042_bit0 -CL000043_bit0 -CL000044_bit0 -CL000045_bit0 -CL000046_bit0 -CL000047_bit0 -CL000048_bit0 -CL000049_bit0 -CL000050_bit0 -CL000051_bit0 -CL000052_bit0 -CL000053_bit0 -CL000054_bit0 -CL000055_bit0 CL000056_bit0 -CL000057_bit0 -CL000058_bit0 -CL000059_bit0 -CL000060_bit0 -CL000061_bit0 -CL000062_bit0 -CL000063_bit0 -CL000064_bit0 -CL000065_bit0 -CL000066_bit0 -CL000067_bit0 -CL000068_bit0 -CL000069_bit0 -CL000070_bit0 -CL000071_bit0 -CL000072_bit0 -CL000073_bit0 -CL000074_bit0 -CL000075_bit0 -CL000076_bit0 -CL000077_bit0 -CL000078_bit0 -CL000079_bit0 -CL000080_bit0 -CL000081_bit0 -CL000082_bit0 -CL000083_bit0 -CL000084_bit0 -CL000085_bit0 -CL000086_bit0 -CL000087_bit0 -CL000088_bit0 -CL000089_bit0 -CL000090_bit0 -CL000091_bit0 -CL000092_bit0 -CL000093_bit0 -CL000094_bit0 -CL000095_bit0 -CL000096_bit0 -CL000097_bit0 -CL000098_bit0 -CL000099_bit0 -CL000100_bit0 -CL000101_bit0 -CL000102_bit0 -CL000103_bit0 -CL000104_bit0 -CL000105_bit0 -CL000106_bit0 -CL000107_bit0 -CL000108_bit0 -CL000109_bit0 -CL000110_bit0 -CL000111_bit0 -CL000112_bit0 -CL000113_bit0 -CL000114_bit0 -CL000115_bit0 -CL000116_bit0 -CL000117_bit0 -CL000118_bit0 -CL000119_bit0 -CL000120_bit0 -CL000121_bit0 -CL000122_bit0 -CL000123_bit0 -CL000124_bit0 -CL000125_bit0 -CL000126_bit0 -CL000127_bit0 -CL000128_bit0 -CL000129_bit0 -CL000130_bit0 -CL000131_bit0 -CL000132_bit0 -CL000133_bit0 CL000134_bit0 -CL000135_bit0 -CL000136_bit0 -CL000137_bit0 -CL000138_bit0 -CL000139_bit0 -CL000140_bit0 -CL000141_bit0 -CL000142_bit0 -CL000143_bit0 -CL000144_bit0 -CL000145_bit0 -CL000146_bit0 -CL000147_bit0 -CL000148_bit0 -CL000149_bit0 -CL000150_bit0 -CL000151_bit0 -CL000152_bit0 -CL000153_bit0 -CL000154_bit0 -CL000155_bit0 -CL000156_bit0 -CL000157_bit0 -CL000158_bit0 -CL000159_bit0 -CL000160_bit0 -CL000161_bit0 -CL000162_bit0 -CL000163_bit0 -CL000164_bit0 -CL000165_bit0 -CL000166_bit0 -CL000167_bit0 -CL000168_bit0 -CL000169_bit0 -CL000170_bit0 -CL000171_bit0 -CL000172_bit0 -CL000173_bit0 -CL000174_bit0 -CL000175_bit0 -CL000176_bit0 -CL000177_bit0 -CL000178_bit0 -CL000179_bit0 -CL000180_bit0 -CL000181_bit0 -CL000182_bit0 -CL000183_bit0 -CL000184_bit0 -CL000185_bit0 -CL000186_bit0 -CL000187_bit0 -CL000188_bit0 -CL000189_bit0 -CL000190_bit0 -CL000191_bit0 -CL000192_bit0 -CL000193_bit0 -CL000194_bit0 -CL000195_bit0 -CL000196_bit0 -CL000197_bit0 -CL000198_bit0 -CL000199_bit0 -CL000200_bit0 -CL000201_bit0 -CL000202_bit0 -CL000203_bit0 -CL000204_bit0 -CL000205_bit0 -CL000206_bit0 -CL000207_bit0 -CL000208_bit0 -CL000209_bit0 -CL000210_bit0 -CL000211_bit0 -CL000212_bit0 -CL000213_bit0 -CL000214_bit0 -CL000215_bit0 -CL000216_bit0 -CL000217_bit0 -CL000218_bit0 -CL000219_bit0 -CL000220_bit0 -CL000221_bit0 -CL000222_bit0 -CL000223_bit0 -CL000224_bit0 -CL000225_bit0 -CL000226_bit0 -CL000227_bit0 -CL000228_bit0 -CL000229_bit0 -CL000230_bit0 -CL000231_bit0 -CL000232_bit0 -CL000233_bit0 -CL000234_bit0 -CL000235_bit0 -CL000236_bit0 -CL000237_bit0 -CL000238_bit0 -CL000239_bit0 -CL000240_bit0 -CL000241_bit0 -CL000242_bit0 -CL000243_bit0 -CL000244_bit0 -CL000245_bit0 -CL000246_bit0 -CL000247_bit0 -CL000248_bit0 -CL000249_bit0 CL000250_bit0 -CL000251_bit0 -CL000252_bit0 -CL000253_bit0 -CL000254_bit0 -CL000255_bit0 -CL000256_bit0 -CL000257_bit0 -CL000258_bit0 -CL000259_bit0 -CL000260_bit0 -CL000261_bit0 -CL000262_bit0 -CL000263_bit0 -CL000264_bit0 -CL000265_bit0 -CL000266_bit0 -CL000267_bit0 -CL000268_bit0 -CL000269_bit0 -CL000270_bit0 -CL000271_bit0 -CL000272_bit0 -CL000273_bit0 -CL000274_bit0 -CL000275_bit0 -CL000276_bit0 -CL000277_bit0 -CL000278_bit0 -CL000279_bit0 -CL000280_bit0 -CL000281_bit0 -CL000282_bit0 -CL000283_bit0 -CL000284_bit0 -CL000285_bit0 -CL000286_bit0 -CL000287_bit0 -CL000288_bit0 -CL000289_bit0 -CL000290_bit0 -CL000291_bit0 -CL000292_bit0 -CL000293_bit0 -CL000294_bit0 -CL000295_bit0 -CL000296_bit0 -CL000297_bit0 -CL000298_bit0 -CL000299_bit0 -CL000300_bit0 -CL000301_bit0 -CL000302_bit0 -CL000303_bit0 -CL000304_bit0 -CL000305_bit0 -CL000306_bit0 -CL000307_bit0 -CL000308_bit0 -CL000309_bit0 -CL000310_bit0 -CL000311_bit0 -CL000312_bit0 -CL000313_bit0 -CL000314_bit0 -CL000315_bit0 -CL000316_bit0 -CL000317_bit0 -CL000318_bit0 -CL000319_bit0 -CL000320_bit0 -CL000321_bit0 -CL000322_bit0 -CL000323_bit0 -CL000324_bit0 -CL000325_bit0 -CL000326_bit0 -CL000327_bit0 -CL000328_bit0 -CL000329_bit0 -CL000330_bit0 -CL000331_bit0 -CL000332_bit0 -CL000333_bit0 -CL000334_bit0 -CL000335_bit0 -CL000336_bit0 -CL000337_bit0 -CL000338_bit0 -CL000339_bit0 -CL000340_bit0 -CL000341_bit0 -CL000342_bit0 -CL000343_bit0 -CL000344_bit0 -CL000345_bit0 -CL000346_bit0 -CL000347_bit0 -CL000348_bit0 -CL000349_bit0 -CL000350_bit0 -CL000351_bit0 -CL000352_bit0 -CL000353_bit0 -CL000354_bit0 -CL000355_bit0 -CL000356_bit0 -CL000357_bit0 -CL000358_bit0 -CL000359_bit0 -CL000360_bit0 -CL000361_bit0 -CL000362_bit0 -CL000363_bit0 -CL000364_bit0 -CL000365_bit0 -CL000366_bit0 -CL000367_bit0 -CL000368_bit0 -CL000369_bit0 -CL000370_bit0 -CL000371_bit0 -CL000372_bit0 -CL000373_bit0 -CL000374_bit0 -CL000375_bit0 -CL000376_bit0 -CL000377_bit0 -CL000378_bit0 -CL000379_bit0 -CL000380_bit0 -CL000381_bit0 -CL000382_bit0 -CL000383_bit0 -CL000384_bit0 -CL000385_bit0 -CL000386_bit0 -CL000387_bit0 -CL000388_bit0 -CL000389_bit0 -CL000390_bit0 -CL000391_bit0 -CL000392_bit0 -CL000393_bit0 -CL000394_bit0 -CL000395_bit0 -CL000396_bit0 -CL000397_bit0 -CL000398_bit0 -CL000399_bit0 -CL000400_bit0 -CL000401_bit0 -CL000402_bit0 -CL000403_bit0 -CL000404_bit0 -CL000405_bit0 -CL000406_bit0 -CL000407_bit0 -CL000408_bit0 -CL000409_bit0 -CL000410_bit0 -CL000411_bit0 -CL000412_bit0 -CL000413_bit0 -CL000414_bit0 -CL000415_bit0 -CL000416_bit0 -CL000417_bit0 -CL000418_bit0 -CL000419_bit0 -CL000420_bit0 CL000421_bit0 -CL000422_bit0 -CL000423_bit0 -CL000424_bit0 -CL000425_bit0 -CL000426_bit0 -CL000427_bit0 -CL000428_bit0 -CL000429_bit0 -CL000430_bit0 -CL000431_bit0 -CL000432_bit0 -CL000433_bit0 -CL000434_bit0 -CL000435_bit0 -CL000436_bit0 -CL000437_bit0 -CL000438_bit0 -CL000439_bit0 -CL000440_bit0 -CL000441_bit0 -CL000442_bit0 -CL000443_bit0 -CL000444_bit0 -CL000445_bit0 -CL000446_bit0 -CL000447_bit0 -CL000448_bit0 -CL000449_bit0 -CL000450_bit0 -CL000451_bit0 -CL000452_bit0 -CL000453_bit0 -CL000454_bit0 -CL000455_bit0 -CL000456_bit0 -CL000457_bit0 -CL000458_bit0 -CL000459_bit0 -CL000460_bit0 -CL000461_bit0 -CL000462_bit0 -CL000463_bit0 -CL000464_bit0 -CL000465_bit0 -CL000466_bit0 -CL000467_bit0 -CL000468_bit0 -CL000469_bit0 -CL000470_bit0 -CL000471_bit0 -CL000472_bit0 -CL000473_bit0 -CL000474_bit0 -CL000475_bit0 -CL000476_bit0 -CL000477_bit0 -CL000478_bit0 -CL000479_bit0 -CL000480_bit0 -CL000481_bit0 -CL000482_bit0 -CL000483_bit0 -CL000484_bit0 -CL000485_bit0 -CL000486_bit0 -CL000487_bit0 -CL000488_bit0 -CL000489_bit0 -CL000490_bit0 -CL000491_bit0 -CL000492_bit0 -CL000493_bit0 -CL000494_bit0 -CL000495_bit0 -CL000496_bit0 -CL000497_bit0 -CL000498_bit0 -CL000499_bit0 -CL000500_bit0 -CL000501_bit0 -CL000502_bit0 -CL000503_bit0 -CL000504_bit0 -CL000505_bit0 -CL000506_bit0 -CL000507_bit0 -CL000508_bit0 -CL000509_bit0 -CL000510_bit0 -CL000511_bit0 -CL000512_bit0 -CL000513_bit0 -CL000514_bit0 -CL000515_bit0 -CL000516_bit0 -CL000517_bit0 -CL000518_bit0 -CL000519_bit0 -CL000520_bit0 -CL000521_bit0 -CL000522_bit0 -CL000523_bit0 -CL000524_bit0 -CL000525_bit0 -CL000526_bit0 -CL000527_bit0 -CL000528_bit0 -CL000529_bit0 -CL000530_bit0 -CL000531_bit0 -CL000532_bit0 -CL000533_bit0 -CL000534_bit0 -CL000535_bit0 -CL000536_bit0 -CL000537_bit0 -CL000538_bit0 -CL000539_bit0 -CL000540_bit0 -CL000541_bit0 -CL000542_bit0 -CL000543_bit0 -CL000544_bi#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.91 0.95 0.90 2/54 5162
Raw data (stat): 5162 (runsolver) R 5161 10720 10719 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 484511536 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99984 s]
Raw data (loadavg): 0.93 0.95 0.90 2/54 5162
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 32598 0 0 0 921 77 0 0 25 0 1 0 484511536 145518592 31271 4294967295 134512640 134672761 3221224544 3221223392 134597191 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35527 31271 603 41 0 35486 0
vsize: 142108
[startup+20.001 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 5162
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 32921 0 0 0 1920 78 0 0 25 0 1 0 484511536 146423808 31540 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35748 31540 603 41 0 35707 0
vsize: 142992
[startup+30.0017 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 5162
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 32984 0 0 0 2919 79 0 0 25 0 1 0 484511536 146739200 31603 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35825 31603 603 41 0 35784 0
vsize: 143300
[startup+40.0019 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 5162
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 33013 0 0 0 3919 79 0 0 25 0 1 0 484511536 146739200 31632 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35825 31632 603 41 0 35784 0
vsize: 143300
[startup+50.0025 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 5162
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 33099 0 0 0 4919 79 0 0 25 0 1 0 484511536 147156992 31718 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35927 31718 603 41 0 35886 0
vsize: 143708
[startup+60.002 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 5162
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 33128 0 0 0 5918 79 0 0 25 0 1 0 484511536 147292160 31747 4294967295 134512640 134672761 3221224544 3221223680 134560606 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35960 31747 603 41 0 35919 0
vsize: 143840
[startup+70.0077 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 5162
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 33138 0 0 0 6919 79 0 0 25 0 1 0 484511536 147292160 31757 4294967295 134512640 134672761 3221224544 3221223680 134560718 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35960 31757 603 41 0 35919 0
vsize: 143840
[startup+80.008 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 5162
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 33141 0 0 0 7919 79 0 0 25 0 1 0 484511536 147292160 31760 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35960 31760 603 41 0 35919 0
vsize: 143840
[startup+90.0075 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 5162
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 33275 0 0 0 8919 79 0 0 25 0 1 0 484511536 147570688 31862 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36028 31862 603 41 0 35987 0
vsize: 144112
[startup+100.008 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 5162
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 33283 0 0 0 9919 79 0 0 25 0 1 0 484511536 147697664 31870 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36059 31870 603 41 0 36018 0
vsize: 144236
[startup+110.009 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 5162
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 33302 0 0 0 10919 79 0 0 25 0 1 0 484511536 147697664 31889 4294967295 134512640 134672761 3221224544 3221223728 134558656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36059 31889 603 41 0 36018 0
vsize: 144236
[startup+120.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5162
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 33310 0 0 0 11919 79 0 0 25 0 1 0 484511536 147832832 31897 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36092 31897 603 41 0 36051 0
vsize: 144368
[startup+130.113 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5162
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 33392 0 0 0 12929 79 0 0 25 0 1 0 484511536 148103168 31979 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36158 31979 603 41 0 36117 0
vsize: 144632
[startup+140.113 s]
Raw data (loadavg): 1.06 0.98 0.91 2/57 5206
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 33466 0 0 0 13929 80 0 0 25 0 1 0 484511536 148365312 32053 4294967295 134512640 134672761 3221224544 3221223712 134561234 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36222 32053 603 41 0 36181 0
vsize: 144888
[startup+150.122 s]
Raw data (loadavg): 1.13 1.00 0.92 2/54 5215
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 33489 0 0 0 14930 80 0 0 25 0 1 0 484511536 148504576 32076 4294967295 134512640 134672761 3221224544 3221223728 134559542 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36256 32076 603 41 0 36215 0
vsize: 145024
[startup+160.122 s]
Raw data (loadavg): 1.11 1.00 0.92 2/54 5215
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 33542 0 0 0 15930 80 0 0 25 0 1 0 484511536 148717568 32129 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36308 32129 603 41 0 36267 0
vsize: 145232
[startup+170.122 s]
Raw data (loadavg): 1.09 1.00 0.92 2/54 5215
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 33629 0 0 0 16930 80 0 0 25 0 1 0 484511536 149155840 32216 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36415 32216 603 41 0 36374 0
vsize: 145660
[startup+180.122 s]
Raw data (loadavg): 1.08 1.00 0.92 2/54 5215
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 33701 0 0 0 17930 80 0 0 25 0 1 0 484511536 149372928 32288 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36468 32288 603 41 0 36427 0
vsize: 145872
[startup+190.122 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 5215
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 33771 0 0 0 18930 80 0 0 25 0 1 0 484511536 149684224 32358 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36544 32358 603 41 0 36503 0
vsize: 146176
[startup+200.122 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 5215
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 33828 0 0 0 19930 80 0 0 25 0 1 0 484511536 149913600 32415 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36600 32415 603 41 0 36559 0
vsize: 146400
[startup+210.121 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 5215
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 33879 0 0 0 20930 81 0 0 25 0 1 0 484511536 150138880 32466 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36655 32466 603 41 0 36614 0
vsize: 146620
[startup+220.123 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 5217
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 33959 0 0 0 21930 81 0 0 25 0 1 0 484511536 150515712 32546 4294967295 134512640 134672761 3221224544 3221223648 134560250 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36747 32546 603 41 0 36706 0
vsize: 146988
[startup+230.122 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 5217
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 34004 0 0 0 22930 81 0 0 25 0 1 0 484511536 150663168 32591 4294967295 134512640 134672761 3221224544 3221223648 134560381 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36783 32591 603 41 0 36742 0
vsize: 147132
[startup+240.122 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 5217
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 34061 0 0 0 23930 81 0 0 25 0 1 0 484511536 150872064 32648 4294967295 134512640 134672761 3221224544 3221223648 134560048 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36834 32648 603 41 0 36793 0
vsize: 147336
[startup+250.122 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 5217
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 34157 0 0 0 24930 82 0 0 25 0 1 0 484511536 151310336 32744 4294967295 134512640 134672761 3221224544 3221223648 134560212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36941 32744 603 41 0 36900 0
vsize: 147764
[startup+260.123 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 5217
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 34236 0 0 0 25930 82 0 0 25 0 1 0 484511536 151695360 32823 4294967295 134512640 134672761 3221224544 3221223648 134560287 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37035 32823 603 41 0 36994 0
vsize: 148140
[startup+270.122 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 5217
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 34347 0 0 0 26930 82 0 0 25 0 1 0 484511536 152137728 32934 4294967295 134512640 134672761 3221224544 3221223712 134561264 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37143 32934 603 41 0 37102 0
vsize: 148572
[startup+280.123 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 5217
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 34427 0 0 0 27930 82 0 0 25 0 1 0 484511536 152436736 33014 4294967295 134512640 134672761 3221224544 3221223700 134561241 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37216 33014 603 41 0 37175 0
vsize: 148864
[startup+290.123 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 5217
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 43021 0 0 0 28910 101 0 0 25 0 1 0 484511536 184881152 40290 4294967295 134512640 134672761 3221224544 3221164336 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45137 40291 603 41 0 45096 0
vsize: 180548
[startup+300.123 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 5217
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 58073 0 0 0 29875 136 0 0 25 0 1 0 484511536 261095424 55342 4294967295 134512640 134672761 3221224544 3221223684 134560556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63744 55342 603 41 0 63703 0
vsize: 254976
[startup+310.123 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 5217
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 58528 0 0 0 30874 137 0 0 25 0 1 0 484511536 263737344 55771 4294967295 134512640 134672761 3221224544 3221223708 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64389 55771 603 41 0 64348 0
vsize: 257556
[startup+320.124 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5217
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 58536 0 0 0 31875 137 0 0 25 0 1 0 484511536 263737344 55779 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64389 55779 603 41 0 64348 0
vsize: 257556
[startup+330.124 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5217
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 58555 0 0 0 32875 137 0 0 25 0 1 0 484511536 263872512 55798 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64422 55798 603 41 0 64381 0
vsize: 257688
[startup+340.125 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5217
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 58569 0 0 0 33875 137 0 0 25 0 1 0 484511536 263872512 55812 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64422 55812 603 41 0 64381 0
vsize: 257688
[startup+350.125 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5217
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 58583 0 0 0 34875 137 0 0 25 0 1 0 484511536 264007680 55826 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64455 55826 603 41 0 64414 0
vsize: 257820
[startup+360.125 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5217
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 58588 0 0 0 35875 137 0 0 25 0 1 0 484511536 264007680 55831 4294967295 134512640 134672761 3221224544 3221223680 134560654 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64455 55831 603 41 0 64414 0
vsize: 257820
[startup+370.126 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5217
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 58593 0 0 0 36875 137 0 0 25 0 1 0 484511536 264007680 55836 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64455 55836 603 41 0 64414 0
vsize: 257820
[startup+380.127 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5217
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 58616 0 0 0 37875 138 0 0 25 0 1 0 484511536 264146944 55859 4294967295 134512640 134672761 3221224544 3221223648 134559869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64489 55859 603 41 0 64448 0
vsize: 257956
[startup+390.126 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5217
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 58633 0 0 0 38876 138 0 0 25 0 1 0 484511536 264146944 55876 4294967295 134512640 134672761 3221224544 3221223648 134559847 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64489 55876 603 41 0 64448 0
vsize: 257956
[startup+400.128 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5217
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 58646 0 0 0 39876 138 0 0 25 0 1 0 484511536 264146944 55889 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64489 55889 603 41 0 64448 0
vsize: 257956
[startup+410.128 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5217
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 58659 0 0 0 40876 138 0 0 25 0 1 0 484511536 264286208 55902 4294967295 134512640 134672761 3221224544 3221223648 134559916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64523 55902 603 41 0 64482 0
vsize: 258092
[startup+420.128 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5217
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 58670 0 0 0 41876 138 0 0 25 0 1 0 484511536 264286208 55913 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64523 55913 603 41 0 64482 0
vsize: 258092
[startup+430.128 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5217
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 58685 0 0 0 42876 138 0 0 25 0 1 0 484511536 264429568 55928 4294967295 134512640 134672761 3221224544 3221223648 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64558 55928 603 41 0 64517 0
vsize: 258232
[startup+440.128 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5217
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 58693 0 0 0 43877 138 0 0 25 0 1 0 484511536 264429568 55936 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64558 55936 603 41 0 64517 0
vsize: 258232
[startup+450.127 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5217
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 58719 0 0 0 44877 138 0 0 25 0 1 0 484511536 264564736 55962 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64591 55962 603 41 0 64550 0
vsize: 258364
[startup+460.128 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5217
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 58719 0 0 0 45877 138 0 0 25 0 1 0 484511536 264564736 55962 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64591 55962 603 41 0 64550 0
vsize: 258364
[startup+470.129 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5217
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 58747 0 0 0 46877 138 0 0 25 0 1 0 484511536 264564736 55990 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64591 55990 603 41 0 64550 0
vsize: 258364
[startup+480.129 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5217
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 58804 0 0 0 47877 138 0 0 25 0 1 0 484511536 264839168 56047 4294967295 134512640 134672761 3221224544 3221223680 134560726 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64658 56047 603 41 0 64617 0
vsize: 258632
[startup+490.129 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5217
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 58867 0 0 0 48877 138 0 0 25 0 1 0 484511536 265109504 56110 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64724 56110 603 41 0 64683 0
vsize: 258896
[startup+500.13 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5217
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 58964 0 0 0 49877 138 0 0 25 0 1 0 484511536 265502720 56207 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64820 56207 603 41 0 64779 0
vsize: 259280
[startup+510.129 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5217
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 59045 0 0 0 50877 138 0 0 25 0 1 0 484511536 265912320 56288 4294967295 134512640 134672761 3221224544 3221223712 134560842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64920 56288 603 41 0 64879 0
vsize: 259680
[startup+520.13 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5219
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 59045 0 0 0 51877 138 0 0 25 0 1 0 484511536 265912320 56288 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64920 56288 603 41 0 64879 0
vsize: 259680
[startup+530.13 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5219
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 59169 0 0 0 52877 138 0 0 25 0 1 0 484511536 266338304 56412 4294967295 134512640 134672761 3221224544 3221223728 134558656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65024 56412 603 41 0 64983 0
vsize: 260096
[startup+540.13 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5219
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 59263 0 0 0 53877 139 0 0 25 0 1 0 484511536 266993664 56506 4294967295 134512640 134672761 3221224544 3221223648 134559883 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65184 56506 603 41 0 65143 0
vsize: 260736
[startup+550.13 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5219
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 59347 0 0 0 54877 139 0 0 25 0 1 0 484511536 267280384 56590 4294967295 134512640 134672761 3221224544 3221223648 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65254 56590 603 41 0 65213 0
vsize: 261016
[startup+560.13 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5219
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 59439 0 0 0 55877 139 0 0 25 0 1 0 484511536 267702272 56682 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65357 56682 603 41 0 65316 0
vsize: 261428
[startup+570.13 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5219
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 59519 0 0 0 56877 139 0 0 25 0 1 0 484511536 268095488 56762 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65453 56762 603 41 0 65412 0
vsize: 261812
[startup+580.131 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5219
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 59585 0 0 0 57878 139 0 0 25 0 1 0 484511536 268238848 56828 4294967295 134512640 134672761 3221224544 3221223648 134560399 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65488 56828 603 41 0 65447 0
vsize: 261952
[startup+590.13 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5219
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 59666 0 0 0 58878 139 0 0 25 0 1 0 484511536 268591104 56909 4294967295 134512640 134672761 3221224544 3221223648 134559964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65574 56909 603 41 0 65533 0
vsize: 262296
[startup+600.13 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5219
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 59692 0 0 0 59878 139 0 0 25 0 1 0 484511536 268746752 56935 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65612 56935 603 41 0 65571 0
vsize: 262448
[startup+610.13 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5219
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 59694 0 0 0 60878 139 0 0 25 0 1 0 484511536 268746752 56937 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65612 56937 603 41 0 65571 0
vsize: 262448
[startup+620.131 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5219
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 59711 0 0 0 61878 139 0 0 25 0 1 0 484511536 268746752 56954 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65612 56954 603 41 0 65571 0
vsize: 262448
[startup+630.13 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5219
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 59746 0 0 0 62878 139 0 0 25 0 1 0 484511536 269021184 56989 4294967295 134512640 134672761 3221224544 3221223648 134559964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65679 56989 603 41 0 65638 0
vsize: 262716
[startup+640.131 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5219
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 59889 0 0 0 63878 140 0 0 25 0 1 0 484511536 269561856 57132 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65811 57132 603 41 0 65770 0
vsize: 263244
[startup+650.131 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5219
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 60127 0 0 0 64878 140 0 0 25 0 1 0 484511536 270512128 57370 4294967295 134512640 134672761 3221224544 3221223648 134560022 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66043 57370 603 41 0 66002 0
vsize: 264172
[startup+660.131 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5219
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 60287 0 0 0 65878 140 0 0 25 0 1 0 484511536 271155200 57530 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66200 57530 603 41 0 66159 0
vsize: 264800
[startup+670.131 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5219
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 60501 0 0 0 66878 141 0 0 25 0 1 0 484511536 272007168 57744 4294967295 134512640 134672761 3221224544 3221223668 134566049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66408 57744 603 41 0 66367 0
vsize: 265632
[startup+680.132 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5219
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 83070 0 0 0 67832 187 0 0 25 0 1 0 484511536 357527552 80313 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87287 80313 603 41 0 87246 0
vsize: 349148
[startup+690.131 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5219
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 83085 0 0 0 68832 187 0 0 25 0 1 0 484511536 357654528 80328 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87318 80328 603 41 0 87277 0
vsize: 349272
[startup+700.132 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5219
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 83086 0 0 0 69832 187 0 0 25 0 1 0 484511536 357654528 80329 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87318 80329 603 41 0 87277 0
vsize: 349272
[startup+710.132 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5219
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 83800 0 0 0 70831 188 0 0 25 0 1 0 484511536 358244352 81043 4294967295 134512640 134672761 3221224544 3221222528 134597176 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87462 81043 603 41 0 87421 0
vsize: 349848
[startup+720.132 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5219
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 112110 0 0 0 71757 262 0 0 25 0 1 0 484511536 509771776 106671 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 124456 106671 603 41 0 124415 0
vsize: 497824
[startup+730.132 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5219
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 112126 0 0 0 72757 262 0 0 25 0 1 0 484511536 509771776 106687 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 124456 106687 603 41 0 124415 0
vsize: 497824
[startup+740.132 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5219
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 112234 0 0 0 73757 263 0 0 25 0 1 0 484511536 509771776 106795 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 124456 106795 603 41 0 124415 0
vsize: 497824
[startup+750.133 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5219
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 112235 0 0 0 74757 263 0 0 25 0 1 0 484511536 509771776 106796 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 124456 106796 603 41 0 124415 0
vsize: 497824
[startup+760.133 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5219
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 112419 0 0 0 75756 263 0 0 25 0 1 0 484511536 510279680 106980 4294967295 134512640 134672761 3221224544 3221223728 134558687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 124580 106980 603 41 0 124539 0
vsize: 498320
[startup+770.133 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5219
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 112467 0 0 0 76757 264 0 0 25 0 1 0 484511536 510431232 107028 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 124617 107028 603 41 0 124576 0
vsize: 498468
[startup+780.134 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5219
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 112467 0 0 0 77757 264 0 0 25 0 1 0 484511536 510431232 107028 4294967295 134512640 134672761 3221224544 3221223744 134557903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 124617 107028 603 41 0 124576 0
vsize: 498468
[startup+790.134 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5219
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 112472 0 0 0 78757 264 0 0 25 0 1 0 484511536 510431232 107033 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 124617 107033 603 41 0 124576 0
vsize: 498468
[startup+800.135 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5219
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 112485 0 0 0 79757 264 0 0 25 0 1 0 484511536 510431232 107046 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 124617 107046 603 41 0 124576 0
vsize: 498468
[startup+810.135 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5219
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 112493 0 0 0 80757 264 0 0 25 0 1 0 484511536 510566400 107054 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 124650 107054 603 41 0 124609 0
vsize: 498600
[startup+820.136 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5219
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 112499 0 0 0 81757 264 0 0 25 0 1 0 484511536 510566400 107060 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 124650 107060 603 41 0 124609 0
vsize: 498600
[startup+830.136 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5219
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 112515 0 0 0 82757 264 0 0 25 0 1 0 484511536 510566400 107076 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 124650 107076 603 41 0 124609 0
vsize: 498600
[startup+840.136 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5219
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 112527 0 0 0 83758 264 0 0 25 0 1 0 484511536 510701568 107088 4294967295 134512640 134672761 3221224544 3221223648 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 124683 107088 603 41 0 124642 0
vsize: 498732
[startup+850.137 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5219
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 112540 0 0 0 84758 264 0 0 25 0 1 0 484511536 510701568 107101 4294967295 134512640 134672761 3221224544 3221223712 134560833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 124683 107101 603 41 0 124642 0
vsize: 498732
[startup+860.137 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5219
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 112542 0 0 0 85758 264 0 0 25 0 1 0 484511536 510701568 107103 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 124683 107103 603 41 0 124642 0
vsize: 498732
[startup+870.138 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5219
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 112544 0 0 0 86758 264 0 0 25 0 1 0 484511536 510701568 107105 4294967295 134512640 134672761 3221224544 3221223744 134557876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 124683 107105 603 41 0 124642 0
vsize: 498732
[startup+880.139 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5219
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 112598 0 0 0 87759 264 0 0 25 0 1 0 484511536 510701568 107159 4294967295 134512640 134672761 3221224544 3221223692 1074733095 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 124683 107159 603 41 0 124642 0
vsize: 498732
[startup+890.141 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5219
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 112602 0 0 0 88759 264 0 0 25 0 1 0 484511536 510701568 107163 4294967295 134512640 134672761 3221224544 3221223680 134560604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 124683 107163 603 41 0 124642 0
vsize: 498732
[startup+900.141 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5219
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 112640 0 0 0 89759 264 0 0 25 0 1 0 484511536 510926848 107201 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 124738 107201 603 41 0 124697 0
vsize: 498952
[startup+910.141 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5219
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 112676 0 0 0 90759 264 0 0 25 0 1 0 484511536 511062016 107237 4294967295 134512640 134672761 3221224544 3221223712 134560867 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 124771 107237 603 41 0 124730 0
vsize: 499084
[startup+920.142 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5219
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 112693 0 0 0 91759 264 0 0 25 0 1 0 484511536 511062016 107254 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 124771 107254 603 41 0 124730 0
vsize: 499084
[startup+930.142 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5219
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 112693 0 0 0 92759 264 0 0 25 0 1 0 484511536 511062016 107254 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 124771 107254 603 41 0 124730 0
vsize: 499084
[startup+940.142 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5219
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 112711 0 0 0 93760 264 0 0 25 0 1 0 484511536 511209472 107272 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 124807 107272 603 41 0 124766 0
vsize: 499228
[startup+950.15 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5219
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 112714 0 0 0 94761 264 0 0 25 0 1 0 484511536 511209472 107275 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 124807 107275 603 41 0 124766 0
vsize: 499228
[startup+960.158 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5219
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 112715 0 0 0 95762 264 0 0 25 0 1 0 484511536 511209472 107276 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 124807 107276 603 41 0 124766 0
vsize: 499228
[startup+970.159 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5219
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 112716 0 0 0 96762 264 0 0 25 0 1 0 484511536 511209472 107277 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 124807 107277 603 41 0 124766 0
vsize: 499228
[startup+980.159 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5219
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 112716 0 0 0 97762 264 0 0 25 0 1 0 484511536 511209472 107277 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 124807 107277 603 41 0 124766 0
vsize: 499228
[startup+990.159 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5219
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 112718 0 0 0 98762 264 0 0 25 0 1 0 484511536 511209472 107279 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 124807 107279 603 41 0 124766 0
vsize: 499228
[startup+1000.16 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5219
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 112752 0 0 0 99762 264 0 0 25 0 1 0 484511536 511352832 107313 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 124842 107313 603 41 0 124801 0
vsize: 499368
[startup+1010.16 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5219
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 112894 0 0 0 100762 264 0 0 25 0 1 0 484511536 511909888 107455 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 124978 107455 603 41 0 124937 0
vsize: 499912
[startup+1020.16 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5219
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 112895 0 0 0 101762 264 0 0 25 0 1 0 484511536 511909888 107456 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 124978 107456 603 41 0 124937 0
vsize: 499912
[startup+1030.16 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5219
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 112932 0 0 0 102763 264 0 0 25 0 1 0 484511536 512188416 107493 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125046 107493 603 41 0 125005 0
vsize: 500184
[startup+1040.16 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5219
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 112956 0 0 0 103763 264 0 0 25 0 1 0 484511536 512188416 107517 4294967295 134512640 134672761 3221224544 3221223712 134560845 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125046 107517 603 41 0 125005 0
vsize: 500184
[startup+1050.16 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5219
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 112986 0 0 0 104763 265 0 0 25 0 1 0 484511536 512344064 107547 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125084 107547 603 41 0 125043 0
vsize: 500336
[startup+1060.16 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5219
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 113021 0 0 0 105763 265 0 0 25 0 1 0 484511536 512479232 107582 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125117 107582 603 41 0 125076 0
vsize: 500468
[startup+1070.16 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5219
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 113025 0 0 0 106763 265 0 0 25 0 1 0 484511536 512479232 107586 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125117 107586 603 41 0 125076 0
vsize: 500468
[startup+1080.16 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5219
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 113098 0 0 0 107763 265 0 0 25 0 1 0 484511536 513359872 107659 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125332 107659 603 41 0 125291 0
vsize: 501328
[startup+1090.16 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5219
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 113112 0 0 0 108763 265 0 0 25 0 1 0 484511536 513359872 107673 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125332 107673 603 41 0 125291 0
vsize: 501328
[startup+1100.16 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5219
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 113126 0 0 0 109763 265 0 0 25 0 1 0 484511536 513499136 107687 4294967295 134512640 134672761 3221224544 3221223648 134559979 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125366 107687 603 41 0 125325 0
vsize: 501464
[startup+1110.16 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5219
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 113222 0 0 0 110763 265 0 0 25 0 1 0 484511536 513945600 107783 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125475 107783 603 41 0 125434 0
vsize: 501900
[startup+1120.16 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5219
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 113252 0 0 0 111764 265 0 0 25 0 1 0 484511536 514027520 107813 4294967295 134512640 134672761 3221224544 3221223744 134561967 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125495 107813 603 41 0 125454 0
vsize: 501980
[startup+1130.16 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5219
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 113255 0 0 0 112764 265 0 0 25 0 1 0 484511536 514027520 107816 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125495 107816 603 41 0 125454 0
vsize: 501980
[startup+1140.16 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5219
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 113257 0 0 0 113764 265 0 0 25 0 1 0 484511536 514027520 107818 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125495 107818 603 41 0 125454 0
vsize: 501980
[startup+1150.16 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5219
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 113259 0 0 0 114764 265 0 0 25 0 1 0 484511536 514027520 107820 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125495 107820 603 41 0 125454 0
vsize: 501980
[startup+1160.16 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5219
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 113263 0 0 0 115764 265 0 0 25 0 1 0 484511536 514027520 107824 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125495 107824 603 41 0 125454 0
vsize: 501980
[startup+1170.16 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5219
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 113273 0 0 0 116765 265 0 0 25 0 1 0 484511536 514027520 107834 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125495 107834 603 41 0 125454 0
vsize: 501980
[startup+1180.16 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5219
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 113276 0 0 0 117765 265 0 0 25 0 1 0 484511536 514158592 107837 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125527 107837 603 41 0 125486 0
vsize: 502108
[startup+1190.16 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5219
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 113382 0 0 0 118765 265 0 0 25 0 1 0 484511536 514592768 107943 4294967295 134512640 134672761 3221224544 3221223648 134560520 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125633 107943 603 41 0 125592 0
vsize: 502532
[startup+1200.16 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 5219
Raw data (stat): 5162 (minisat+) R 5161 10720 10719 0 -1 0 113520 0 0 0 119764 266 0 0 25 0 1 0 484511536 515031040 108081 4294967295 134512640 134672761 3221224544 3221223680 134560590 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125740 108081 603 41 0 125699 0
vsize: 502960
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.39 s]
Raw data (loadavg): 1.00 1.00 0.92 1/54 5219
Raw data (stat): 5162 (minisat+) Z 5161 10720 10719 0 -1 12 113523 0 0 0 119765 287 0 0 25 0 1 0 484511536 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.38
CPU time (s): 1200.53
CPU user time (s): 1197.65
CPU system time (s): 2.87456
CPU usage (%): 100.012
Max. virtual memory (Kb): 502960
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####