PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

Name	normalized-opb/mps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-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.03384
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 22512

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc15 THE 2005-04-22 03:15:25 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=11621 boxname=wulflinc15 idbench=894 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  90db1995bd949fc5ac74143a523f3bcf  /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-20-10-air01.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-20-10-air01.opb /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-20-10-air01.opb
IDLAUNCH: 11621
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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		: 450.999
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:        617216 kB
Buffers:         29604 kB
Cached:         366336 kB
SwapCached:        432 kB
Active:          60540 kB
Inactive:       337576 kB
HighTotal:      131008 kB
HighFree:        41300 kB
LowTotal:       903652 kB
LowFree:        575916 kB
SwapTotal:     2097136 kB
SwapFree:      2095984 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5364 kB
Slab:            13616 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-22 03:35:28 (client local time) WITH STATUS 10 IN 1200.54 SECONDS
stats: 11621 7 1200.54 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 
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.92 0.95 0.90 2/54 23707
Raw data (stat): 23707 (runsolver) R 23706 29151 29150 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 492178728 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99984 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 32598 0 0 0 918 80 0 0 25 0 1 0 492178728 145518592 31271 4294967295 134512640 134672761 3221224544 3221222816 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35527 31271 603 41 0 35486 0
vsize: 142108
[startup+20.0011 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 32921 0 0 0 1916 81 0 0 25 0 1 0 492178728 146423808 31540 4294967295 134512640 134672761 3221224544 3221223716 134556598 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.0021 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 32984 0 0 0 2915 81 0 0 25 0 1 0 492178728 146739200 31603 4294967295 134512640 134672761 3221224544 3221223744 134557885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35825 31603 603 41 0 35784 0
vsize: 143300
[startup+40.0012 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 33013 0 0 0 3915 81 0 0 25 0 1 0 492178728 146739200 31632 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35825 31632 603 41 0 35784 0
vsize: 143300
[startup+50.0024 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 33096 0 0 0 4916 81 0 0 25 0 1 0 492178728 147156992 31715 4294967295 134512640 134672761 3221224544 3221223712 134560806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35927 31715 603 41 0 35886 0
vsize: 143708
[startup+60.0022 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 33127 0 0 0 5915 81 0 0 25 0 1 0 492178728 147156992 31746 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35927 31746 603 41 0 35886 0
vsize: 143708
[startup+70.0027 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 33138 0 0 0 6916 81 0 0 25 0 1 0 492178728 147292160 31757 4294967295 134512640 134672761 3221224544 3221223680 134560619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35960 31757 603 41 0 35919 0
vsize: 143840
[startup+80.0038 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 33141 0 0 0 7916 81 0 0 25 0 1 0 492178728 147292160 31760 4294967295 134512640 134672761 3221224544 3221223716 134556602 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35960 31760 603 41 0 35919 0
vsize: 143840
[startup+90.0039 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 33248 0 0 0 8916 81 0 0 25 0 1 0 492178728 147689472 31867 4294967295 134512640 134672761 3221224544 3221221744 134522942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36057 31867 603 41 0 36016 0
vsize: 144228
[startup+100.004 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 33283 0 0 0 9916 82 0 0 25 0 1 0 492178728 147697664 31870 4294967295 134512640 134672761 3221224544 3221223712 134560885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36059 31870 603 41 0 36018 0
vsize: 144236
[startup+110.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 33302 0 0 0 10916 82 0 0 25 0 1 0 492178728 147697664 31889 4294967295 134512640 134672761 3221224544 3221223716 134556627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36059 31889 603 41 0 36018 0
vsize: 144236
[startup+120.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 33310 0 0 0 11916 82 0 0 25 0 1 0 492178728 147832832 31897 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36092 31897 603 41 0 36051 0
vsize: 144368
[startup+130.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 33376 0 0 0 12916 82 0 0 25 0 1 0 492178728 148103168 31963 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36158 31963 603 41 0 36117 0
vsize: 144632
[startup+140.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 33463 0 0 0 13915 82 0 0 25 0 1 0 492178728 148365312 32050 4294967295 134512640 134672761 3221224544 3221223712 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36222 32050 603 41 0 36181 0
vsize: 144888
[startup+150.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 33487 0 0 0 14916 82 0 0 25 0 1 0 492178728 148504576 32074 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36256 32074 603 41 0 36215 0
vsize: 145024
[startup+160.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 33541 0 0 0 15916 83 0 0 25 0 1 0 492178728 148717568 32128 4294967295 134512640 134672761 3221224544 3221223704 134561240 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36308 32128 603 41 0 36267 0
vsize: 145232
[startup+170.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 33615 0 0 0 16915 83 0 0 25 0 1 0 492178728 149000192 32202 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36377 32202 603 41 0 36336 0
vsize: 145508
[startup+180.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 33688 0 0 0 17915 84 0 0 25 0 1 0 492178728 149372928 32275 4294967295 134512640 134672761 3221224544 3221223648 134560250 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36468 32275 603 41 0 36427 0
vsize: 145872
[startup+190.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 33758 0 0 0 18915 84 0 0 25 0 1 0 492178728 149684224 32345 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36544 32345 603 41 0 36503 0
vsize: 146176
[startup+200.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 33814 0 0 0 19915 84 0 0 25 0 1 0 492178728 149913600 32401 4294967295 134512640 134672761 3221224544 3221223648 134560410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36600 32401 603 41 0 36559 0
vsize: 146400
[startup+210.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 33863 0 0 0 20915 84 0 0 25 0 1 0 492178728 150052864 32450 4294967295 134512640 134672761 3221224544 3221223648 134560376 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36634 32450 603 41 0 36593 0
vsize: 146536
[startup+220.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 33919 0 0 0 21915 84 0 0 25 0 1 0 492178728 150278144 32506 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36689 32506 603 41 0 36648 0
vsize: 146756
[startup+230.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 33995 0 0 0 22915 84 0 0 25 0 1 0 492178728 150663168 32582 4294967295 134512640 134672761 3221224544 3221223648 134560350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36783 32582 603 41 0 36742 0
vsize: 147132
[startup+240.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 34042 0 0 0 23915 84 0 0 25 0 1 0 492178728 150736896 32629 4294967295 134512640 134672761 3221224544 3221223648 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36801 32629 603 41 0 36760 0
vsize: 147204
[startup+250.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 34139 0 0 0 24915 84 0 0 25 0 1 0 492178728 151375872 32726 4294967295 134512640 134672761 3221224544 3221223648 134560529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36957 32726 603 41 0 36916 0
vsize: 147828
[startup+260.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 34209 0 0 0 25916 85 0 0 25 0 1 0 492178728 151592960 32796 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37010 32796 603 41 0 36969 0
vsize: 148040
[startup+270.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 34304 0 0 0 26916 85 0 0 25 0 1 0 492178728 151986176 32891 4294967295 134512640 134672761 3221224544 3221223648 134560399 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37106 32891 603 41 0 37065 0
vsize: 148424
[startup+280.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 34396 0 0 0 27917 85 0 0 25 0 1 0 492178728 152285184 32983 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37179 32983 603 41 0 37138 0
vsize: 148716
[startup+290.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 34451 0 0 0 28916 85 0 0 25 0 1 0 492178728 152571904 33038 4294967295 134512640 134672761 3221224544 3221223668 134566057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37249 33038 603 41 0 37208 0
vsize: 148996
[startup+300.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 57992 0 0 0 29861 140 0 0 25 0 1 0 492178728 260960256 55261 4294967295 134512640 134672761 3221224544 3221223712 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63711 55261 603 41 0 63670 0
vsize: 254844
[startup+310.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 58521 0 0 0 30860 141 0 0 25 0 1 0 492178728 263737344 55764 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64389 55764 603 41 0 64348 0
vsize: 257556
[startup+320.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 58534 0 0 0 31859 141 0 0 25 0 1 0 492178728 263737344 55777 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64389 55777 603 41 0 64348 0
vsize: 257556
[startup+330.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 58545 0 0 0 32863 141 0 0 25 0 1 0 492178728 263737344 55788 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64389 55788 603 41 0 64348 0
vsize: 257556
[startup+340.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 58563 0 0 0 33863 142 0 0 25 0 1 0 492178728 263872512 55806 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64422 55806 603 41 0 64381 0
vsize: 257688
[startup+350.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 58578 0 0 0 34864 142 0 0 25 0 1 0 492178728 263872512 55821 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64422 55821 603 41 0 64381 0
vsize: 257688
[startup+360.075 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 58583 0 0 0 35865 142 0 0 25 0 1 0 492178728 264007680 55826 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64455 55826 603 41 0 64414 0
vsize: 257820
[startup+370.095 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 58588 0 0 0 36867 142 0 0 25 0 1 0 492178728 264007680 55831 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64455 55831 603 41 0 64414 0
vsize: 257820
[startup+380.104 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 58608 0 0 0 37865 142 0 0 25 0 1 0 492178728 264007680 55851 4294967295 134512640 134672761 3221224544 3221223648 134560229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64455 55851 603 41 0 64414 0
vsize: 257820
[startup+390.111 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 58625 0 0 0 38866 142 0 0 25 0 1 0 492178728 264146944 55868 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64489 55868 603 41 0 64448 0
vsize: 257956
[startup+400.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 58638 0 0 0 39867 142 0 0 25 0 1 0 492178728 264146944 55881 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64489 55881 603 41 0 64448 0
vsize: 257956
[startup+410.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 58650 0 0 0 40868 142 0 0 25 0 1 0 492178728 264286208 55893 4294967295 134512640 134672761 3221224544 3221223648 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64523 55893 603 41 0 64482 0
vsize: 258092
[startup+420.121 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 58669 0 0 0 41868 142 0 0 25 0 1 0 492178728 264286208 55912 4294967295 134512640 134672761 3221224544 3221223648 134560326 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64523 55912 603 41 0 64482 0
vsize: 258092
[startup+430.121 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 58680 0 0 0 42868 142 0 0 25 0 1 0 492178728 264286208 55923 4294967295 134512640 134672761 3221224544 3221223648 134559869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64523 55923 603 41 0 64482 0
vsize: 258092
[startup+440.123 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 58689 0 0 0 43868 142 0 0 25 0 1 0 492178728 264429568 55932 4294967295 134512640 134672761 3221224544 3221223648 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64558 55932 603 41 0 64517 0
vsize: 258232
[startup+450.123 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 58693 0 0 0 44868 142 0 0 25 0 1 0 492178728 264429568 55936 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64558 55936 603 41 0 64517 0
vsize: 258232
[startup+460.131 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 58719 0 0 0 45869 142 0 0 25 0 1 0 492178728 264564736 55962 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64591 55962 603 41 0 64550 0
vsize: 258364
[startup+470.15 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 58734 0 0 0 46871 142 0 0 25 0 1 0 492178728 264564736 55977 4294967295 134512640 134672761 3221224544 3221223648 134560031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64591 55977 603 41 0 64550 0
vsize: 258364
[startup+480.15 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 58748 0 0 0 47872 142 0 0 25 0 1 0 492178728 264564736 55991 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64591 55991 603 41 0 64550 0
vsize: 258364
[startup+490.151 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 58819 0 0 0 48872 142 0 0 25 0 1 0 492178728 264974336 56062 4294967295 134512640 134672761 3221224544 3221223680 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64691 56062 603 41 0 64650 0
vsize: 258764
[startup+500.151 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 58899 0 0 0 49872 143 0 0 25 0 1 0 492178728 265232384 56142 4294967295 134512640 134672761 3221224544 3221223692 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64754 56142 603 41 0 64713 0
vsize: 259016
[startup+510.155 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 58999 0 0 0 50872 143 0 0 25 0 1 0 492178728 265633792 56242 4294967295 134512640 134672761 3221224544 3221223800 134562565 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64852 56242 603 41 0 64811 0
vsize: 259408
[startup+520.156 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 59045 0 0 0 51872 143 0 0 25 0 1 0 492178728 265912320 56288 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64920 56288 603 41 0 64879 0
vsize: 259680
[startup+530.165 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 59056 0 0 0 52873 143 0 0 25 0 1 0 492178728 265912320 56299 4294967295 134512640 134672761 3221224544 3221223648 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64920 56299 603 41 0 64879 0
vsize: 259680
[startup+540.165 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 59183 0 0 0 53873 143 0 0 25 0 1 0 492178728 266473472 56426 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65057 56426 603 41 0 65016 0
vsize: 260228
[startup+550.165 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 59277 0 0 0 54873 144 0 0 25 0 1 0 492178728 266993664 56520 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65184 56520 603 41 0 65143 0
vsize: 260736
[startup+560.165 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 59368 0 0 0 55873 144 0 0 25 0 1 0 492178728 267415552 56611 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65287 56611 603 41 0 65246 0
vsize: 261148
[startup+570.167 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 59455 0 0 0 56873 144 0 0 25 0 1 0 492178728 267841536 56698 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65391 56698 603 41 0 65350 0
vsize: 261564
[startup+580.174 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 59541 0 0 0 57874 144 0 0 25 0 1 0 492178728 268095488 56784 4294967295 134512640 134672761 3221224544 3221223648 134560191 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65453 56784 603 41 0 65412 0
vsize: 261812
[startup+590.174 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 59605 0 0 0 58873 144 0 0 25 0 1 0 492178728 268394496 56848 4294967295 134512640 134672761 3221224544 3221223648 134560424 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65526 56848 603 41 0 65485 0
vsize: 262104
[startup+600.175 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 59682 0 0 0 59874 144 0 0 25 0 1 0 492178728 268746752 56925 4294967295 134512640 134672761 3221224544 3221223648 134560031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65612 56925 603 41 0 65571 0
vsize: 262448
[startup+610.176 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 59692 0 0 0 60874 144 0 0 25 0 1 0 492178728 268746752 56935 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65612 56935 603 41 0 65571 0
vsize: 262448
[startup+620.176 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 59694 0 0 0 61874 144 0 0 25 0 1 0 492178728 268746752 56937 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65612 56937 603 41 0 65571 0
vsize: 262448
[startup+630.177 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 59711 0 0 0 62874 144 0 0 25 0 1 0 492178728 268746752 56954 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65612 56954 603 41 0 65571 0
vsize: 262448
[startup+640.177 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 59769 0 0 0 63874 145 0 0 25 0 1 0 492178728 269021184 57012 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65679 57012 603 41 0 65638 0
vsize: 262716
[startup+650.178 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 59947 0 0 0 64874 145 0 0 25 0 1 0 492178728 269852672 57190 4294967295 134512640 134672761 3221224544 3221223648 134559877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65882 57190 603 41 0 65841 0
vsize: 263528
[startup+660.178 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 60147 0 0 0 65874 145 0 0 25 0 1 0 492178728 270643200 57390 4294967295 134512640 134672761 3221224544 3221223680 134560634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66075 57390 603 41 0 66034 0
vsize: 264300
[startup+670.178 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 60323 0 0 0 66874 146 0 0 25 0 1 0 492178728 271294464 57566 4294967295 134512640 134672761 3221224544 3221223712 134560968 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66234 57566 603 41 0 66193 0
vsize: 264936
[startup+680.178 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 60501 0 0 0 67873 146 0 0 25 0 1 0 492178728 272007168 57744 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66408 57744 603 41 0 66367 0
vsize: 265632
[startup+690.178 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 83070 0 0 0 68826 194 0 0 25 0 1 0 492178728 357527552 80313 4294967295 134512640 134672761 3221224544 3221223728 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 87287 80313 603 41 0 87246 0
vsize: 349148
[startup+700.179 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 83085 0 0 0 69826 194 0 0 25 0 1 0 492178728 357654528 80328 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 87318 80328 603 41 0 87277 0
vsize: 349272
[startup+710.185 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 83086 0 0 0 70827 194 0 0 25 0 1 0 492178728 357654528 80329 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 87318 80329 603 41 0 87277 0
vsize: 349272
[startup+720.186 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 84108 0 0 0 71825 196 0 0 25 0 1 0 492178728 358920192 81351 4294967295 134512640 134672761 3221224544 3221222536 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 87627 81353 603 41 0 87586 0
vsize: 350508
[startup+730.185 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 112110 0 0 0 72758 263 0 0 25 0 1 0 492178728 509771776 106671 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 124456 106671 603 41 0 124415 0
vsize: 497824
[startup+740.185 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 112234 0 0 0 73758 263 0 0 25 0 1 0 492178728 509771776 106795 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 124456 106795 603 41 0 124415 0
vsize: 497824
[startup+750.189 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 112234 0 0 0 74759 263 0 0 25 0 1 0 492178728 509771776 106795 4294967295 134512640 134672761 3221224544 3221223736 134556585 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 124456 106795 603 41 0 124415 0
vsize: 497824
[startup+760.189 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 112235 0 0 0 75759 263 0 0 25 0 1 0 492178728 509771776 106796 4294967295 134512640 134672761 3221224544 3221223712 134560822 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 124456 106796 603 41 0 124415 0
vsize: 497824
[startup+770.19 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 112426 0 0 0 76759 264 0 0 25 0 1 0 492178728 510279680 106987 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 124580 106987 603 41 0 124539 0
vsize: 498320
[startup+780.19 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 112467 0 0 0 77759 264 0 0 25 0 1 0 492178728 510431232 107028 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 124617 107028 603 41 0 124576 0
vsize: 498468
[startup+790.189 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 112467 0 0 0 78759 264 0 0 25 0 1 0 492178728 510431232 107028 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 124617 107028 603 41 0 124576 0
vsize: 498468
[startup+800.189 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 112472 0 0 0 79759 264 0 0 25 0 1 0 492178728 510431232 107033 4294967295 134512640 134672761 3221224544 3221223680 134560611 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 124617 107033 603 41 0 124576 0
vsize: 498468
[startup+810.19 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 112485 0 0 0 80759 264 0 0 25 0 1 0 492178728 510431232 107046 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 124617 107046 603 41 0 124576 0
vsize: 498468
[startup+820.191 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 112491 0 0 0 81759 264 0 0 25 0 1 0 492178728 510566400 107052 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 124650 107052 603 41 0 124609 0
vsize: 498600
[startup+830.193 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 112499 0 0 0 82760 264 0 0 25 0 1 0 492178728 510566400 107060 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 124650 107060 603 41 0 124609 0
vsize: 498600
[startup+840.199 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 112515 0 0 0 83760 264 0 0 25 0 1 0 492178728 510566400 107076 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 124650 107076 603 41 0 124609 0
vsize: 498600
[startup+850.2 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 112527 0 0 0 84761 264 0 0 25 0 1 0 492178728 510701568 107088 4294967295 134512640 134672761 3221224544 3221223648 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 124683 107088 603 41 0 124642 0
vsize: 498732
[startup+860.2 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 112539 0 0 0 85761 264 0 0 25 0 1 0 492178728 510701568 107100 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 124683 107100 603 41 0 124642 0
vsize: 498732
[startup+870.201 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 112542 0 0 0 86761 264 0 0 25 0 1 0 492178728 510701568 107103 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 124683 107103 603 41 0 124642 0
vsize: 498732
[startup+880.201 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 112544 0 0 0 87761 264 0 0 25 0 1 0 492178728 510701568 107105 4294967295 134512640 134672761 3221224544 3221223744 134557885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 124683 107105 603 41 0 124642 0
vsize: 498732
[startup+890.202 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 112598 0 0 0 88761 264 0 0 25 0 1 0 492178728 510701568 107159 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 124683 107159 603 41 0 124642 0
vsize: 498732
[startup+900.202 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 112602 0 0 0 89762 264 0 0 25 0 1 0 492178728 510701568 107163 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 124683 107163 603 41 0 124642 0
vsize: 498732
[startup+910.203 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 112640 0 0 0 90762 264 0 0 25 0 1 0 492178728 510926848 107201 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 124738 107201 603 41 0 124697 0
vsize: 498952
[startup+920.204 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 112661 0 0 0 91762 264 0 0 25 0 1 0 492178728 511062016 107222 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 124771 107222 603 41 0 124730 0
vsize: 499084
[startup+930.205 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 112692 0 0 0 92762 264 0 0 25 0 1 0 492178728 511062016 107253 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 124771 107253 603 41 0 124730 0
vsize: 499084
[startup+940.204 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 112693 0 0 0 93762 264 0 0 25 0 1 0 492178728 511062016 107254 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 124771 107254 603 41 0 124730 0
vsize: 499084
[startup+950.206 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 112708 0 0 0 94762 264 0 0 25 0 1 0 492178728 511209472 107269 4294967295 134512640 134672761 3221224544 3221223712 134561264 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 124807 107269 603 41 0 124766 0
vsize: 499228
[startup+960.205 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 112711 0 0 0 95763 264 0 0 25 0 1 0 492178728 511209472 107272 4294967295 134512640 134672761 3221224544 3221223712 134560785 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 124807 107272 603 41 0 124766 0
vsize: 499228
[startup+970.206 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 112715 0 0 0 96763 264 0 0 25 0 1 0 492178728 511209472 107276 4294967295 134512640 134672761 3221224544 3221223712 134560885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 124807 107276 603 41 0 124766 0
vsize: 499228
[startup+980.207 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 112716 0 0 0 97763 264 0 0 25 0 1 0 492178728 511209472 107277 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 124807 107277 603 41 0 124766 0
vsize: 499228
[startup+990.207 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 112716 0 0 0 98763 264 0 0 25 0 1 0 492178728 511209472 107277 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 124807 107277 603 41 0 124766 0
vsize: 499228
[startup+1000.21 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 112718 0 0 0 99763 264 0 0 25 0 1 0 492178728 511209472 107279 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 124807 107279 603 41 0 124766 0
vsize: 499228
[startup+1010.21 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 112752 0 0 0 100763 265 0 0 25 0 1 0 492178728 511352832 107313 4294967295 134512640 134672761 3221224544 3221223680 134560642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 124842 107313 603 41 0 124801 0
vsize: 499368
[startup+1020.21 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 112833 0 0 0 101762 265 0 0 25 0 1 0 492178728 511631360 107394 4294967295 134512640 134672761 3221224544 3221223728 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 124910 107394 603 41 0 124869 0
vsize: 499640
[startup+1030.21 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 112894 0 0 0 102762 265 0 0 25 0 1 0 492178728 511909888 107455 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 124978 107455 603 41 0 124937 0
vsize: 499912
[startup+1040.21 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 112916 0 0 0 103762 265 0 0 25 0 1 0 492178728 512045056 107477 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125011 107477 603 41 0 124970 0
vsize: 500044
[startup+1050.21 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 112943 0 0 0 104762 266 0 0 25 0 1 0 492178728 512188416 107504 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125046 107504 603 41 0 125005 0
vsize: 500184
[startup+1060.21 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 112976 0 0 0 105763 266 0 0 25 0 1 0 492178728 512344064 107537 4294967295 134512640 134672761 3221224544 3221223648 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125084 107537 603 41 0 125043 0
vsize: 500336
[startup+1070.21 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 113009 0 0 0 106763 266 0 0 25 0 1 0 492178728 512479232 107570 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125117 107570 603 41 0 125076 0
vsize: 500468
[startup+1080.21 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 113021 0 0 0 107763 266 0 0 25 0 1 0 492178728 512479232 107582 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125117 107582 603 41 0 125076 0
vsize: 500468
[startup+1090.21 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 113098 0 0 0 108763 266 0 0 25 0 1 0 492178728 513359872 107659 4294967295 134512640 134672761 3221224544 3221223648 134560410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125332 107659 603 41 0 125291 0
vsize: 501328
[startup+1100.21 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 113111 0 0 0 109763 266 0 0 25 0 1 0 492178728 513359872 107672 4294967295 134512640 134672761 3221224544 3221223712 134560806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125332 107672 603 41 0 125291 0
vsize: 501328
[startup+1110.21 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 113112 0 0 0 110763 266 0 0 25 0 1 0 492178728 513359872 107673 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125332 107673 603 41 0 125291 0
vsize: 501328
[startup+1120.21 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 113202 0 0 0 111763 266 0 0 25 0 1 0 492178728 513810432 107763 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125442 107763 603 41 0 125401 0
vsize: 501768
[startup+1130.21 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 113252 0 0 0 112763 267 0 0 25 0 1 0 492178728 514027520 107813 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125495 107813 603 41 0 125454 0
vsize: 501980
[startup+1140.21 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 113252 0 0 0 113763 267 0 0 25 0 1 0 492178728 514027520 107813 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125495 107813 603 41 0 125454 0
vsize: 501980
[startup+1150.21 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 113257 0 0 0 114764 267 0 0 25 0 1 0 492178728 514027520 107818 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125495 107818 603 41 0 125454 0
vsize: 501980
[startup+1160.21 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 113258 0 0 0 115764 267 0 0 25 0 1 0 492178728 514027520 107819 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125495 107819 603 41 0 125454 0
vsize: 501980
[startup+1170.22 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 113261 0 0 0 116764 267 0 0 25 0 1 0 492178728 514027520 107822 4294967295 134512640 134672761 3221224544 3221223712 134560806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125495 107822 603 41 0 125454 0
vsize: 501980
[startup+1180.22 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 113266 0 0 0 117764 267 0 0 25 0 1 0 492178728 514027520 107827 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125495 107827 603 41 0 125454 0
vsize: 501980
[startup+1190.22 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 113276 0 0 0 118764 267 0 0 25 0 1 0 492178728 514158592 107837 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125527 107837 603 41 0 125486 0
vsize: 502108
[startup+1200.22 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23707
Raw data (stat): 23707 (minisat+) R 23706 29151 29150 0 -1 0 113314 0 0 0 119764 267 0 0 25 0 1 0 492178728 514310144 107875 4294967295 134512640 134672761 3221224544 3221223648 134560198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125564 107875 603 41 0 125523 0
vsize: 502256
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.44 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 23707
Raw data (stat): 23707 (minisat+) Z 23706 29151 29150 0 -1 12 113317 0 0 0 119764 288 0 0 25 0 1 0 492178728 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.44
CPU time (s): 1200.54
CPU user time (s): 1197.65
CPU system time (s): 2.88856
CPU usage (%): 100.008
Max. virtual memory (Kb): 502256
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####