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-lp4l.opb
MD5SUM	3c39e3c2b993ee2185e2a1a3e73b9723
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	3744
Optimality of the best value was proved	NO
Number of terms in the objective function	1086
Biggest coefficient in the objective function	283
Number of bits for the biggest coefficient in the objective function	9
Sum of the numbers in the objective function	197191
Number of bits of the sum of numbers in the objective function	18
Biggest number in a constraint	283
Number of bits of the biggest number in a constraint	9
Biggest sum of numbers in a constraint	197191
Number of bits of the biggest sum of numbers	18
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.09
Number of variables	1086
Total number of constraints	1171
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	1170
Number of constraints which are nor clauses,nor cardinality constraints	1
Minimum length of a constraint	1
Maximum length of a constraint	1086
Trace number 22271

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc21 THE 2005-04-22 02:34:09 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=11920 boxname=wulflinc21 idbench=917 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  3c39e3c2b993ee2185e2a1a3e73b9723  /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-20-10-lp4l.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-20-10-lp4l.opb /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-20-10-lp4l.opb
IDLAUNCH: 11920
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.161
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	: 3
cpu MHz		: 451.161
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:        812084 kB
Buffers:          1960 kB
Cached:         200800 kB
SwapCached:       1444 kB
Active:          41344 kB
Inactive:       163752 kB
HighTotal:      131008 kB
HighFree:        40180 kB
LowTotal:       903652 kB
LowFree:        771904 kB
SwapTotal:     2097892 kB
SwapFree:      2095700 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           4940 kB
Slab:            11916 kB
Committed_AS:    63792 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-22 02:54:11 (client local time) WITH STATUS 10 IN 1200.34 SECONDS
stats: 11920 7 1200.34 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 169 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ####################################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 168]---> BDD-cost: 1386
c ---[ 166]---> BDD-cost:   41
c ---[ 164]---> BDD-cost:   67
c ---[ 162]---> BDD-cost:   99
c ---[ 160]---> BDD-cost:   79
c ---[ 158]---> BDD-cost:   45
c ---[ 156]---> BDD-cost:   69
c ---[ 154]---> BDD-cost:   55
c ---[ 152]---> BDD-cost:   37
c ---[ 150]---> BDD-cost:   27
c ---[ 148]---> BDD-cost:   77
c ---[ 146]---> BDD-cost:   79
c ---[ 144]---> BDD-cost:   23
c ---[ 142]---> BDD-cost:   75
c ---[ 140]---> BDD-cost:   77
c ---[ 138]---> BDD-cost:   41
c ---[ 136]---> BDD-cost:   75
c ---[ 134]---> BDD-cost:  107
c ---[ 132]---> BDD-cost:   91
c ---[ 130]---> BDD-cost:  127
c ---[ 128]---> BDD-cost:  123
c ---[ 126]---> BDD-cost:   89
c ---[ 124]---> BDD-cost:   57
c ---[ 122]---> BDD-cost:   89
c ---[ 120]---> BDD-cost:   71
c ---[ 118]---> BDD-cost:  103
c ---[ 116]---> BDD-cost:  117
c ---[ 114]---> BDD-cost:  125
c ---[ 112]---> BDD-cost:   91
c ---[ 110]---> BDD-cost:   59
c ---[ 108]---> BDD-cost:   89
c ---[ 106]---> BDD-cost:   71
c ---[ 104]---> BDD-cost:  129
c ---[ 102]---> BDD-cost:  113
c ---[ 100]---> BDD-cost:  123
c ---[  98]---> BDD-cost:   89
c ---[  96]---> BDD-cost:   61
c ---[  94]---> BDD-cost:   59
c ---[  92]---> BDD-cost:   33
c ---[  90]---> BDD-cost:  123
c ---[  88]---> BDD-cost:  121
c ---[  86]---> BDD-cost:   99
c ---[  84]---> BDD-cost:   45
c ---[  82]---> BDD-cost:   69
c ---[  80]---> BDD-cost:   59
c ---[  78]---> BDD-cost:   33
c ---[  76]---> BDD-cost:   73
c ---[  74]---> BDD-cost:   69
c ---[  72]---> BDD-cost:   47
c ---[  70]---> BDD-cost:   67
c ---[  68]---> BDD-cost:   95
c ---[  66]---> BDD-cost:   85
c ---[  64]---> BDD-cost:  107
c ---[  62]---> BDD-cost:   97
c ---[  60]---> BDD-cost:   33
c ---[  58]---> BDD-cost:   79
c ---[  56]---> BDD-cost:   87
c ---[  54]---> BDD-cost:   75
c ---[  52]---> BDD-cost:   67
c ---[  50]---> BDD-cost:   43
c ---[  48]---> BDD-cost:   75
c ---[  46]---> BDD-cost:  105
c ---[  44]---> BDD-cost:   87
c ---[  42]---> BDD-cost:   77
c ---[  40]---> BDD-cost:   63
c ---[  38]---> BDD-cost:   39
c ---[  36]---> BDD-cost:   77
c ---[  34]---> BDD-cost:   63
c ---[  32]---> BDD-cost:    5
c ---[  30]---> BDD-cost:  169
c ---[  28]---> BDD-cost:  155
c ---[  26]---> BDD-cost:  115
c ---[  24]---> BDD-cost:   77
c ---[  22]---> BDD-cost:   83
c ---[  20]---> BDD-cost:  111
c ---[  18]---> BDD-cost:  107
c ---[  16]---> BDD-cost:  161
c ---[  14]---> BDD-cost:  151
c ---[  12]---> BDD-cost:  117
c ---[  10]---> BDD-cost:   57
c ---[   8]---> BDD-cost:   85
c ---[   6]---> BDD-cost:   71
c ---[   4]---> BDD-cost:   25
c ---[   2]---> BDD-cost:   37
c ---[   0]---> BDD-cost:29667
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  107492   312738 |   35830       0        0     nan |  0.000 % |
c |       100 |  107492   312738 |   39413     100     4465    44.6 |  0.222 % |
c |       251 |  107492   312738 |   43354     251    37605   149.8 |  0.222 % |
c ==============================================================================
c [1mFound solution: 5035[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:315675     Base: 2 3 2 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       414 |  916094  2200760 |  305364     414    45311   109.4 |  0.222 % |
c |       514 |  911090  2189333 |  335900     490    52212   106.6 |  0.468 % |
c |       670 |  905071  2175504 |  369490     610    63952   104.8 |  1.008 % |
c |       899 |  898479  2160303 |  406439     802    88234   110.0 |  1.627 % |
c |      1237 |  894046  2150106 |  447083    1091   119391   109.4 |  2.039 % |
c |      1744 |  893934  2149845 |  491791    1597   335790   210.3 |  2.049 % |
c ==============================================================================
c [1mFound solution: 4778[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 3 2 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2008 |  887974  2136702 |  295991    1810   352746   194.9 |  2.049 % |
c |      2108 |  886071  2132312 |  325590    1904   363180   190.7 |  2.847 % |
c |      2258 |  884992  2129827 |  358149    2047   363994   177.8 |  2.947 % |
c |      2483 |  880934  2120477 |  393964    2183   367424   168.3 |  3.323 % |
c ==============================================================================
c [1mFound solution: 4771[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 3 2 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2819 |  883205  2126094 |  294401    2518   391720   155.6 |  3.323 % |
c |      2920 |  879470  2117466 |  323841    2601   393557   151.3 |  3.707 % |
c |      3072 |  876691  2111053 |  356225    2733   405917   148.5 |  3.966 % |
c |      3297 |  875756  2108904 |  391847    2952   410875   139.2 |  4.052 % |
c |      3637 |  875471  2108250 |  431032    3290   450495   136.9 |  4.078 % |
c |      4143 |  875471  2108250 |  474135    3796   526034   138.6 |  4.078 % |
c ==============================================================================
c [1mFound solution: 4173[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 3 2 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4753 |  877284  2113499 |  292428    4406   622669   141.3 |  4.078 % |
c |      4853 |  875917  2110365 |  321670    4493   624475   139.0 |  4.248 % |
c |      5003 |  874920  2108078 |  353837    4639   636657   137.2 |  4.283 % |
c |      5228 |  874284  2106615 |  389221    4860   656054   135.0 |  4.339 % |
c |      5566 |  874284  2106615 |  428143    5198   709299   136.5 |  4.339 % |
c |      6073 |  870087  2096931 |  470958    5681   924330   162.7 |  4.731 % |
c |      6832 |  862749  2079977 |  518054    6383  1054938   165.3 |  5.422 % |
c |      7973 |  859832  2073236 |  569859    7507  1676924   223.4 |  5.695 % |
c |      9682 |  853862  2059449 |  626845    9155  2108307   230.3 |  6.258 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v CO100001_bit0 -CO100002_bit0 -CO100003_bit0 -CO100004_bit0 -CO100005_bit0 -CO100006_bit0 -CO100007_bit0 -CO100008_bit0 -CO100009_bit0 -CO100010_bit0 -CO100011_bit0 -CO100012_bit0 -CO100013_bit0 -CO100014_bit0 -CO100015_bit0 -CO100016_bit0 -CO100017_bit0 -CO100018_bit0 -CO100019_bit0 -CO100020_bit0 -CO100021_bit0 -CO100022_bit0 -CO100023_bit0 -CO100024_bit0 -CO100025_bit0 -CO100026_bit0 CO100027_bit0 -CO100028_bit0 -CO100029_bit0 -CO100030_bit0 -CO100031_bit0 -CO100032_bit0 -CO100033_bit0 -CO100034_bit0 -CO100035_bit0 -CO100036_bit0 -CO100037_bit0 -CO100038_bit0 -CO100039_bit0 -CO100040_bit0 -CO100041_bit0 -CO100042_bit0 -CO100043_bit0 -CO100044_bit0 -CO100045_bit0 -CO100046_bit0 -CO100047_bit0 -CO100048_bit0 -CO100049_bit0 -CO100050_bit0 -CO100051_bit0 -CO100052_bit0 -CO100053_bit0 CO100054_bit0 -CO100055_bit0 -CO100056_bit0 -CO100057_bit0 -CO100058_bit0 -CO100059_bit0 -CO100060_bit0 -CO100061_bit0 -CO100062_bit0 -CO100063_bit0 -CO100064_bit0 -CO100065_bit0 -CO100066_bit0 -CO100067_bit0 -CO100068_bit0 -CO100069_bit0 -CO100070_bit0 -CO100071_bit0 -CO100072_bit0 -CO100073_bit0 -CO100074_bit0 -CO100075_bit0 CO100076_bit0 -CO100077_bit0 -CO100078_bit0 -CO100079_bit0 -CO100080_bit0 -CO100081_bit0 -CO100082_bit0 -CO100083_bit0 -CO100084_bit0 -CO100085_bit0 -CO100086_bit0 -CO100087_bit0 -CO100088_bit0 -CO100089_bit0 CO100090_bit0 -CO100091_bit0 -CO100092_bit0 -CO100093_bit0 -CO100094_bit0 -CO100095_bit0 -CO100096_bit0 -CO100097_bit0 -CO100098_bit0 -CO100099_bit0 -CO100100_bit0 -CO100101_bit0 -CO100102_bit0 -CO100103_bit0 -CO100104_bit0 -CO100105_bit0 -CO100106_bit0 -CO100107_bit0 CO100108_bit0 -CO100109_bit0 -CO100110_bit0 -CO100111_bit0 -CO100112_bit0 -CO100113_bit0 -CO100114_bit0 -CO100115_bit0 -CO100116_bit0 -CO100117_bit0 -CO100118_bit0 -CO100119_bit0 -CO100120_bit0 -CO100121_bit0 -CO100122_bit0 -CO100123_bit0 -CO100124_bit0 -CO100125_bit0 -CO100126_bit0 -CO100127_bit0 -CO100128_bit0 -CO100129_bit0 -CO100130_bit0 -CO100131_bit0 -CO100132_bit0 -CO100133_bit0 -CO100134_bit0 -CO100135_bit0 -CO100136_bit0 -CO100137_bit0 CO100138_bit0 -CO100139_bit0 -CO100140_bit0 -CO100141_bit0 -CO100142_bit0 -CO100143_bit0 -CO100144_bit0 -CO100145_bit0 -CO100146_bit0 -CO100147_bit0 -CO100148_bit0 -CO100149_bit0 -CO100150_bit0 CO100151_bit0 -CO100152_bit0 -CO100153_bit0 -CO100154_bit0 -CO100155_bit0 -CO100156_bit0 -CO100157_bit0 -CO100158_bit0 -CO100159_bit0 -CO100160_bit0 -CO100161_bit0 -CO100162_bit0 -CO100163_bit0 -CO100164_bit0 -CO100165_bit0 CO100166_bit0 -CO100167_bit0 -CO100168_bit0 -CO100169_bit0 -CO100170_bit0 -CO100171_bit0 -CO100172_bit0 -CO100173_bit0 -CO100174_bit0 -CO100175_bit0 -CO100176_bit0 -CO100177_bit0 -CO100178_bit0 CO100179_bit0 -CO100180_bit0 -CO100181_bit0 -CO100182_bit0 -CO100183_bit0 -CO100184_bit0 -CO100185_bit0 -CO100186_bit0 -CO100187_bit0 -CO100188_bit0 -CO100189_bit0 -CO100190_bit0 -CO100191_bit0 -CO100192_bit0 -CO100193_bit0 -CO100194_bit0 -CO100195_bit0 -CO100196_bit0 -CO100197_bit0 -CO100198_bit0 -CO100199_bit0 -CO100200_bit0 -CO100201_bit0 -CO100202_bit0 -CO100203_bit0 -CO100204_bit0 -CO100205_bit0 -CO100206_bit0 -CO100207_bit0 -CO100208_bit0 -CO100209_bit0 -CO100210_bit0 -CO100211_bit0 -CO100212_bit0 -CO100213_bit0 -CO100214_bit0 -CO100215_bit0 -CO100216_bit0 -CO100217_bit0 -CO100218_bit0 -CO100219_bit0 -CO100220_bit0 -CO100221_bit0 -CO100222_bit0 -CO100223_bit0 -CO100224_bit0 -CO100225_bit0 -CO100226_bit0 -CO100227_bit0 -CO100228_bit0 -CO100229_bit0 CO100230_bit0 -CO100231_bit0 -CO100232_bit0 -CO100233_bit0 -CO100234_bit0 -CO100235_bit0 -CO100236_bit0 -CO100237_bit0 -CO100238_bit0 -CO100239_bit0 -CO100240_bit0 -CO100241_bit0 -CO100242_bit0 -CO100243_bit0 -CO100244_bit0 -CO100245_bit0 -CO100246_bit0 -CO100247_bit0 -CO100248_bit0 -CO100249_bit0 -CO100250_bit0 -CO100251_bit0 -CO100252_bit0 -CO100253_bit0 -CO100254_bit0 -CO100255_bit0 -CO100256_bit0 -CO100257_bit0 -CO100258_bit0 -CO100259_bit0 -CO100260_bit0 -CO100261_bit0 -CO100262_bit0 -CO100263_bit0 -CO100264_bit0 -CO100265_bit0 -CO100266_bit0 -CO100267_bit0 -CO100268_bit0 -CO100269_bit0 -CO100270_bit0 -CO100271_bit0 -CO100272_bit0 -CO100273_bit0 -CO100274_bit0 -CO100275_bit0 -CO100276_bit0 -CO100277_bit0 -CO100278_bit0 -CO100279_bit0 -CO100280_bit0 -CO100281_bit0 -CO100282_bit0 -CO100283_bit0 -CO100284_bit0 -CO100285_bit0 -CO100286_bit0 -CO100287_bit0 -CO100288_bit0 -CO100289_bit0 -CO100290_bit0 -CO100291_bit0 -CO100292_bit0 -CO100293_bit0 -CO100294_bit0 -CO100295_bit0 -CO100296_bit0 CO100297_bit0 -CO100298_bit0 -CO100299_bit0 -CO100300_bit0 -CO100301_bit0 -CO100302_bit0 -CO100303_bit0 -CO100304_bit0 -CO100305_bit0 -CO100306_bit0 -CO100307_bit0 -CO100308_bit0 -CO100309_bit0 -CO100310_bit0 -CO100311_bit0 -CO100312_bit0 -CO100313_bit0 -CO100314_bit0 -CO100315_bit0 -CO100316_bit0 -CO100317_bit0 -CO100318_bit0 -CO100319_bit0 -CO100320_bit0 -CO100321_bit0 -CO100322_bit0 -CO100323_bit0 -CO100324_bit0 -CO100325_bit0 -CO100326_bit0 -CO100327_bit0 -CO100328_bit0 -CO100329_bit0 -CO100330_bit0 -CO100331_bit0 -CO100332_bit0 -CO100333_bit0 -CO100334_bit0 -CO100335_bit0 -CO100336_bit0 -CO100337_bit0 -CO100338_bit0 -CO100339_bit0 -CO100340_bit0 -CO100341_bit0 -CO100342_bit0 -CO100343_bit0 -CO100344_bit0 -CO100345_bit0 -CO100346_bit0 CO100347_bit0 -CO100348_bit0 -CO100349_bit0 -CO100350_bit0 -CO100351_bit0 -CO100352_bit0 -CO100353_bit0 -CO100354_bit0 -CO100355_bit0 -CO100356_bit0 -CO100357_bit0 -CO100358_bit0 -CO100359_bit0 -CO100360_bit0 -CO100361_bit0 -CO100362_bit0 -CO100363_bit0 -CO100364_bit0 -CO100365_bit0 -CO100366_bit0 -CO100367_bit0 -CO100368_bit0 -CO100369_bit0 -CO100370_bit0 -CO100371_bit0 -CO100372_bit0 -CO100373_bit0 -CO100374_bit0 -CO100375_bit0 -CO100376_bit0 -CO100377_bit0 -CO100378_bit0 -CO100379_bit0 -CO100380_bit0 -CO100381_bit0 -CO100382_bit0 -CO100383_bit0 -CO100384_bit0 -CO100385_bit0 -CO100386_bit0 -CO100387_bit0 -CO100388_bit0 -CO100389_bit0 -CO100390_bit0 -CO100391_bit0 -CO100392_bit0 -CO100393_bit0 -CO100394_bit0 -CO100395_bit0 -CO100396_bit0 -CO100397_bit0 -CO100398_bit0 -CO100399_bit0 -CO100400_bit0 -CO100401_bit0 -CO100402_bit0 -CO100403_bit0 -CO100404_bit0 -CO100405_bit0 -CO100406_bit0 -CO100407_bit0 -CO100408_bit0 -CO100409_bit0 -CO100410_bit0 -CO100411_bit0 -CO100412_bit0 -CO100413_bit0 -CO100414_bit0 -CO100415_bit0 -CO100416_bit0 -CO100417_bit0 -CO100418_bit0 -CO100419_bit0 -CO100420_bit0 -CO100421_bit0 -CO100422_bit0 -CO100423_bit0 -CO100424_bit0 -CO100425_bit0 -CO100426_bit0 -CO100427_bit0 -CO100428_bit0 CO100429_bit0 -CO100430_bit0 -CO100431_bit0 -CO100432_bit0 -CO100433_bit0 -CO100434_bit0 -CO100435_bit0 -CO100436_bit0 -CO100437_bit0 -CO100438_bit0 -CO100439_bit0 -CO100440_bit0 -CO100441_bit0 -CO100442_bit0 -CO100443_bit0 -CO100444_bit0 -CO100445_bit0 -CO100446_bit0 -CO100447_bit0 -CO100448_bit0 -CO100449_bit0 -CO100450_bit0 -CO100451_bit0 -CO100452_bit0 -CO100453_bit0 -CO100454_bit0 -CO100455_bit0 -CO100456_bit0 CO100457_bit0 -CO100458_bit0 -CO100459_bit0 -CO100460_bit0 -CO100461_bit0 -CO100462_bit0 -CO100463_bit0 -CO100464_bit0 -CO100465_bit0 -CO100466_bit0 -CO100467_bit0 -CO100468_bit0 -CO100469_bit0 -CO100470_bit0 -CO100471_bit0 -CO100472_bit0 -CO100473_bit0 -CO100474_bit0 -CO100475_bit0 -CO100476_bit0 -CO100477_bit0 -CO100478_bit0 -CO100479_bit0 -CO100480_bit0 -CO100481_bit0 -CO100482_bit0 -CO100483_bit0 -CO100484_bit0 -CO100485_bit0 -CO100486_bit0 -CO100487_bit0 -CO100488_bit0 -CO100489_bit0 -CO100490_bit0 -CO100491_bit0 -CO100492_bit0 -CO100493_bit0 -CO100494_bit0 -CO100495_bit0 -CO100496_bit0 -CO100497_bit0 -CO100498_bit0 -CO100499_bit0 -CO100500_bit0 -CO100501_bit0 -CO100502_bit0 -CO100503_bit0 -CO100504_bit0 -CO100505_bit0 -CO100506_bit0 -CO100507_bit0 -CO100508_bit0 CO100509_bit0 -CO100510_bit0 -CO100511_bit0 -CO100512_bit0 -CO100513_bit0 -CO100514_bit0 -CO100515_bit0 -CO100516_bit0 -CO100517_bit0 -CO100518_bit0 -CO100519_bit0 -CO100520_bit0 -CO100521_bit0 -CO100522_bit0 -CO100523_bit0 -CO100524_bit0 -CO100525_bit0 -CO100526_bit0 -CO100527_bit0 -CO100528_bit0 -CO100529_bit0 -CO100530_bit0 -CO100531_bit0 -CO100532_bit0 -CO100533_bit0 -CO100534_bit0 -CO100535_bit0 -CO100536_bit0 -CO100537_bit0 -CO100538_bit0 -CO100539_bit0 -CO100540_bit0 -CO100541_bit0 -CO100542_bit0 -CO100543_bit0 -CO100544_bit0 -CO100545_bit0 -CO100546_bit0 -CO100547_bit0 -CO100548_bit0 -CO100549_bit0 -CO100550_bit0 -CO100551_bit0 -CO100552_bit0 -CO100553_bit0 -CO100554_bit0 -CO100555_bit0 CO100556_bit0 -CO100557_bit0 -CO100558_bit0 -CO100559_bit0 -CO100560_bit0 -CO100561_bit0 -CO100562_bit0 -CO100563_bit0 -CO100564_bit0 -CO100565_bit0 -CO100566_bit0 -CO100567_bit0 -CO100568_bit0 -CO100569_bit0 -CO100570_bit0 -CO100571_bit0 -CO100572_bit0 -CO100573_bit0 -CO100574_bit0 -CO100575_bit0 -CO100576_bit0 -CO100577_bit0 -CO100578_bit0 -CO100579_bit0 -CO100580_bit0 -CO100581_bit0 -CO100582_bit0 -CO100583_bit0 -CO100584_bit0 -CO100585_bit0 -CO100586_bit0 -CO100587_bit0 -CO100588_bit0 -CO100589_bit0 -CO100590_bit0 -CO100591_bit0 -CO100592_bit0 -CO100593_bit0 -CO100594_bit0 -CO100595_bit0 -CO100596_bit0 -CO100597_bit0 -CO100598_bit0 -CO100599_bit0 -CO100600_bit0 -CO100601_bit0 -CO100602_bit0 -CO100603_bit0 -CO100604_bit0 -CO100605_bit0 -CO100606_bit0 -CO100607_bit0 -CO100608_bit0 -CO100609_bit0 -CO100610_bit0 -CO100611_bit0 -CO100612_bit0 -CO100613_bit0 -CO100614_bit0 -CO100615_bit0 -CO100616_bit0 -CO100617_bit0 -CO100618_bit0 -CO100619_bit0 -CO100620_bit0 -CO100621_bit0 -CO100622_bit0 -CO100623_bit0 -CO100624_bit0 -CO100625_bit0 -CO100626_bit0 -CO100627_bit0 -CO100628_bit0 -CO100629_bit0 -CO100630_bit0 CO100631_bit0 -CO100632_bit0 -CO100633_bit0 -CO100634_bit0 -CO100635_bit0 -CO100636_bit0 -CO100637_bit0 -CO100638_bit0 -CO100639_bit0 CO100640_bit0 -CO100641_bit0 -CO100642_bit0 -CO100643_bit0 -CO100644_bit0 -CO100645_bit0 -CO100646_bit0 -CO100647_bit0 -CO100648_bit0 -CO100649_bit0 -CO100650_bit0 -CO100651_bit0 -CO100652_bit0 -CO100653_bit0 -CO100654_bit0 -CO100655_bit0 -CO100656_bit0 -CO100657_bit0 -CO100658_bit0 -CO100659_bit0 -CO100660_bit0 -CO100661_bit0 -CO100662_bit0 -CO100663_bit0 -CO100664_bit0 -CO100665_bit0 -CO100666_bit0 -CO100667_bit0 -CO100668_bit0 -CO100669_bit0 -CO100670_bit0 -CO100671_bit0 -CO100672_bit0 -CO100673_bit0 -CO100674_bit0 -CO100675_bit0 -CO100676_bit0 -CO100677_bit0 -CO100678_bit0 -CO100679_bit0 -CO100680_bit0 -CO100681_bit0 -CO100682_bit0 -CO100683_bit0 -CO100684_bit0 -CO100685_bit0 -CO100686_bit0 -CO100687_bit0 -CO100688_bit0 -CO100689_bit0 -CO100690_bit0 -CO100691_bit0 -CO100692_bit0 -CO100693_bit0 -CO100694_bit0 -CO100695_bit0 -CO100696_bit0 -CO100697_bit0 -CO100698_bit0 -CO100699_bit0 -CO100700_bit0 -CO100701_bit0 -CO100702_bit0 -CO100703_bit0 -CO100704_bit0 -CO100705_bit0 -CO100706_bit0 -CO100707_bit0 -CO100708_bit0 -CO100709_bit0 -CO100710_bit0 -CO100711_bit0 -CO100712_bit0 -CO100713_bit0 -CO100714_bit0 -CO100715_bit0 -CO100716_bit0 -CO100717_bit0 -CO100718_bit0 -CO100719_bit0 -CO100720_bit0 -CO100721_bit0 -CO100722_bit0 -CO100723_bit0 -CO100724_bit0 -CO100725_bit0 -CO100726_bit0 -CO100727_bit0 -CO100728_bit0 -CO100729_bit0 -CO100730_bit0 -CO100731_bit0 -CO100732_bit0 -CO100733_bit0 -CO100734_bit0 -CO100735_bit0 -CO100736_bit0 CO100737_bit0 -CO100738_bit0 -CO100739_bit0 -CO100740_bit0 -CO100741_bit0 -CO100742_bit0 -CO100743_bit0 -CO100744_bit0 -CO100745_bit0 -CO100746_bit0 -CO100747_bit0 -CO100748_bit0 -CO100749_bit0 -CO100750_bit0 -CO100751_bit0 -CO100752_bit0 -CO100753_bit0 -CO100754_bit0 -CO100755_bit0 -CO100756_bit0 -CO100757_bit0 -CO100758_bit0 -CO100759_bit0 -CO100760_bit0 -CO100761_bit0 -CO100762_bit0 -CO100763_bit0 -CO100764_bit0 -CO100765_bit0 -CO100766_bit0 -CO100767_bit0 -CO100768_bit0 -CO100769_bit0 -CO100770_bit0 -CO100771_bit0 -CO100772_bit0 -CO100773_bit0 -CO100774_bit0 -CO100775_bit0 -CO100776_bit0 -CO100777_bit0 -CO100778_bit0 -CO100779_bit0 -CO100780_bit0 -CO100781_bit0 -CO100782_bit0 -CO100783_bit0 -CO100784_bit0 -CO100785_bit0 -CO100786_bit0 -CO100787_bit0 -CO100788_bit0 -CO100789_bit0 -CO100790_bit0 -CO100791_bit0 -CO100792_bit0 -CO100793_bit0 -CO100794_bit0 -CO100795_bit0 -CO100796_bit0 -CO100797_bit0 -CO100798_bit0 -CO100799_bit0 -CO100800_bit0 -CO100801_bit0 -CO100802_bit0 -CO100803_bit0 -CO100804_bit0 -CO100805_bit0 -CO100806_bit0 -CO100807_bit0 -CO100808_bit0 -CO100809_bit0 -CO100810_bit0 -CO100811_bit0 -CO100812_bit0 CO100813_bit0 -CO100814_bit0 -CO100815_bit0 -CO100816_bit0 -CO100817_bit0 -CO100818_bit0#### 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): 1.07 1.02 0.94 2/55 27737
Raw data (stat): 27737 (runsolver) R 27736 30927 30926 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 427419646 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.99978 s]
Raw data (loadavg): 1.06 1.01 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 28209 0 0 0 934 65 0 0 25 0 1 0 427419646 127602688 26758 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31153 26758 603 41 0 31112 0
vsize: 124612
[startup+20.0005 s]
Raw data (loadavg): 1.05 1.01 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 28311 0 0 0 1934 65 0 0 25 0 1 0 427419646 127602688 26860 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31153 26860 603 41 0 31112 0
vsize: 124612
[startup+30.0012 s]
Raw data (loadavg): 1.04 1.01 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 28397 0 0 0 2933 66 0 0 25 0 1 0 427419646 127733760 26946 4294967295 134512640 134672761 3221224544 3221223712 134560808 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31185 26946 603 41 0 31144 0
vsize: 124740
[startup+40.0018 s]
Raw data (loadavg): 1.03 1.01 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 28425 0 0 0 3933 66 0 0 25 0 1 0 427419646 127733760 26974 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31185 26974 603 41 0 31144 0
vsize: 124740
[startup+50.0095 s]
Raw data (loadavg): 1.03 1.01 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 28531 0 0 0 4934 66 0 0 25 0 1 0 427419646 128262144 27080 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31314 27080 603 41 0 31273 0
vsize: 125256
[startup+60.0095 s]
Raw data (loadavg): 1.02 1.01 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 28699 0 0 0 5933 67 0 0 25 0 1 0 427419646 128925696 27248 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31476 27248 603 41 0 31435 0
vsize: 125904
[startup+70.0098 s]
Raw data (loadavg): 1.02 1.01 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 29091 0 0 0 6932 68 0 0 25 0 1 0 427419646 131272704 27613 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32049 27613 603 41 0 32008 0
vsize: 128196
[startup+80.0097 s]
Raw data (loadavg): 1.02 1.01 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 29091 0 0 0 7932 68 0 0 25 0 1 0 427419646 131272704 27613 4294967295 134512640 134672761 3221224544 3221223712 134560833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32049 27613 603 41 0 32008 0
vsize: 128196
[startup+90.0103 s]
Raw data (loadavg): 1.01 1.01 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 29195 0 0 0 8932 68 0 0 25 0 1 0 427419646 131629056 27694 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32136 27694 603 41 0 32095 0
vsize: 128544
[startup+100.01 s]
Raw data (loadavg): 1.01 1.01 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 29202 0 0 0 9932 69 0 0 25 0 1 0 427419646 131629056 27701 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32136 27701 603 41 0 32095 0
vsize: 128544
[startup+110.01 s]
Raw data (loadavg): 1.01 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 29228 0 0 0 10932 69 0 0 25 0 1 0 427419646 131764224 27727 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32169 27727 603 41 0 32128 0
vsize: 128676
[startup+120.011 s]
Raw data (loadavg): 1.01 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 29316 0 0 0 11931 70 0 0 25 0 1 0 427419646 132034560 27815 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32235 27815 603 41 0 32194 0
vsize: 128940
[startup+130.011 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 29403 0 0 0 12931 70 0 0 25 0 1 0 427419646 132440064 27902 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32334 27902 603 41 0 32293 0
vsize: 129336
[startup+140.012 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 29522 0 0 0 13931 70 0 0 25 0 1 0 427419646 132706304 27990 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32399 27990 603 41 0 32358 0
vsize: 129596
[startup+150.012 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 29563 0 0 0 14931 70 0 0 25 0 1 0 427419646 132841472 28031 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32432 28031 603 41 0 32391 0
vsize: 129728
[startup+160.012 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 29646 0 0 0 15931 71 0 0 25 0 1 0 427419646 133328896 28114 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32551 28114 603 41 0 32510 0
vsize: 130204
[startup+170.013 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 29786 0 0 0 16931 71 0 0 25 0 1 0 427419646 133836800 28254 4294967295 134512640 134672761 3221224544 3221223648 134559905 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32675 28254 603 41 0 32634 0
vsize: 130700
[startup+180.013 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 29873 0 0 0 17930 71 0 0 25 0 1 0 427419646 134119424 28341 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32744 28341 603 41 0 32703 0
vsize: 130976
[startup+190.013 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 29889 0 0 0 18931 71 0 0 25 0 1 0 427419646 134262784 28357 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32779 28357 603 41 0 32738 0
vsize: 131116
[startup+200.013 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 30007 0 0 0 19931 71 0 0 25 0 1 0 427419646 134660096 28475 4294967295 134512640 134672761 3221224544 3221223680 134560585 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32876 28475 603 41 0 32835 0
vsize: 131504
[startup+210.012 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 30060 0 0 0 20931 71 0 0 25 0 1 0 427419646 134930432 28528 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32942 28528 603 41 0 32901 0
vsize: 131768
[startup+220.013 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 30140 0 0 0 21931 72 0 0 25 0 1 0 427419646 135458816 28608 4294967295 134512640 134672761 3221224544 3221223648 134559853 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33071 28608 603 41 0 33030 0
vsize: 132284
[startup+230.013 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 30172 0 0 0 22931 72 0 0 25 0 1 0 427419646 135598080 28640 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33105 28640 603 41 0 33064 0
vsize: 132420
[startup+240.013 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 30192 0 0 0 23931 72 0 0 25 0 1 0 427419646 135733248 28660 4294967295 134512640 134672761 3221224544 3221223648 134560514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33138 28660 603 41 0 33097 0
vsize: 132552
[startup+250.012 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 30210 0 0 0 24931 72 0 0 25 0 1 0 427419646 135733248 28678 4294967295 134512640 134672761 3221224544 3221223648 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33138 28678 603 41 0 33097 0
vsize: 132552
[startup+260.012 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 30217 0 0 0 25931 72 0 0 25 0 1 0 427419646 135872512 28685 4294967295 134512640 134672761 3221224544 3221223648 134560148 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33172 28685 603 41 0 33131 0
vsize: 132688
[startup+270.011 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 30238 0 0 0 26931 72 0 0 25 0 1 0 427419646 135872512 28706 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33172 28706 603 41 0 33131 0
vsize: 132688
[startup+280.011 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 30242 0 0 0 27931 72 0 0 25 0 1 0 427419646 135872512 28710 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33172 28710 603 41 0 33131 0
vsize: 132688
[startup+290.012 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 30247 0 0 0 28931 72 0 0 25 0 1 0 427419646 135872512 28715 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33172 28715 603 41 0 33131 0
vsize: 132688
[startup+300.012 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 30272 0 0 0 29932 72 0 0 25 0 1 0 427419646 136003584 28740 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33204 28740 603 41 0 33163 0
vsize: 132816
[startup+310.011 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 30272 0 0 0 30932 72 0 0 25 0 1 0 427419646 136003584 28740 4294967295 134512640 134672761 3221224544 3221223648 134559887 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33204 28740 603 41 0 33163 0
vsize: 132816
[startup+320.011 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 30277 0 0 0 31932 72 0 0 25 0 1 0 427419646 136003584 28745 4294967295 134512640 134672761 3221224544 3221223648 134559887 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33204 28745 603 41 0 33163 0
vsize: 132816
[startup+330.01 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 30282 0 0 0 32932 72 0 0 25 0 1 0 427419646 136003584 28750 4294967295 134512640 134672761 3221224544 3221223648 134560529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33204 28750 603 41 0 33163 0
vsize: 132816
[startup+340.01 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 30287 0 0 0 33932 72 0 0 25 0 1 0 427419646 136151040 28755 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33240 28755 603 41 0 33199 0
vsize: 132960
[startup+350.01 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 30292 0 0 0 34932 72 0 0 25 0 1 0 427419646 136151040 28760 4294967295 134512640 134672761 3221224544 3221223648 134560031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33240 28760 603 41 0 33199 0
vsize: 132960
[startup+360.01 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 30292 0 0 0 35932 72 0 0 25 0 1 0 427419646 136151040 28760 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33240 28760 603 41 0 33199 0
vsize: 132960
[startup+370.01 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 30297 0 0 0 36933 72 0 0 25 0 1 0 427419646 136151040 28765 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33240 28765 603 41 0 33199 0
vsize: 132960
[startup+380.01 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 30302 0 0 0 37933 72 0 0 25 0 1 0 427419646 136151040 28770 4294967295 134512640 134672761 3221224544 3221223648 134560212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33240 28770 603 41 0 33199 0
vsize: 132960
[startup+390.01 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 30307 0 0 0 38933 72 0 0 25 0 1 0 427419646 136151040 28775 4294967295 134512640 134672761 3221224544 3221223648 134559875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33240 28775 603 41 0 33199 0
vsize: 132960
[startup+400.009 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 30312 0 0 0 39933 72 0 0 25 0 1 0 427419646 136151040 28780 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33240 28780 603 41 0 33199 0
vsize: 132960
[startup+410.009 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 30312 0 0 0 40933 72 0 0 25 0 1 0 427419646 136151040 28780 4294967295 134512640 134672761 3221224544 3221223648 134560396 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33240 28780 603 41 0 33199 0
vsize: 132960
[startup+420.009 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 30317 0 0 0 41933 72 0 0 25 0 1 0 427419646 136151040 28785 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33240 28785 603 41 0 33199 0
vsize: 132960
[startup+430.008 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 30322 0 0 0 42933 72 0 0 25 0 1 0 427419646 136294400 28790 4294967295 134512640 134672761 3221224544 3221223648 134559835 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33275 28790 603 41 0 33234 0
vsize: 133100
[startup+440.008 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 30327 0 0 0 43934 72 0 0 25 0 1 0 427419646 136294400 28795 4294967295 134512640 134672761 3221224544 3221223648 134560344 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33275 28795 603 41 0 33234 0
vsize: 133100
[startup+450.008 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 30332 0 0 0 44934 72 0 0 25 0 1 0 427419646 136294400 28800 4294967295 134512640 134672761 3221224544 3221223648 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33275 28800 603 41 0 33234 0
vsize: 133100
[startup+460.007 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 30337 0 0 0 45934 72 0 0 25 0 1 0 427419646 136294400 28805 4294967295 134512640 134672761 3221224544 3221223648 134560376 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33275 28805 603 41 0 33234 0
vsize: 133100
[startup+470.007 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 30337 0 0 0 46934 72 0 0 25 0 1 0 427419646 136294400 28805 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33275 28805 603 41 0 33234 0
vsize: 133100
[startup+480.109 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 30342 0 0 0 47944 72 0 0 25 0 1 0 427419646 136294400 28810 4294967295 134512640 134672761 3221224544 3221223648 134560379 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33275 28810 603 41 0 33234 0
vsize: 133100
[startup+490.109 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 30347 0 0 0 48945 72 0 0 25 0 1 0 427419646 136294400 28815 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33275 28815 603 41 0 33234 0
vsize: 133100
[startup+500.11 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 30351 0 0 0 49945 72 0 0 25 0 1 0 427419646 136294400 28819 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33275 28819 603 41 0 33234 0
vsize: 133100
[startup+510.11 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 30356 0 0 0 50945 72 0 0 25 0 1 0 427419646 136433664 28824 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33309 28824 603 41 0 33268 0
vsize: 133236
[startup+520.109 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 30361 0 0 0 51945 72 0 0 25 0 1 0 427419646 136433664 28829 4294967295 134512640 134672761 3221224544 3221223648 134560313 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33309 28829 603 41 0 33268 0
vsize: 133236
[startup+530.109 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 30361 0 0 0 52945 72 0 0 25 0 1 0 427419646 136433664 28829 4294967295 134512640 134672761 3221224544 3221223648 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33309 28829 603 41 0 33268 0
vsize: 133236
[startup+540.109 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 30366 0 0 0 53945 72 0 0 25 0 1 0 427419646 136433664 28834 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33309 28834 603 41 0 33268 0
vsize: 133236
[startup+550.109 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 30371 0 0 0 54946 72 0 0 25 0 1 0 427419646 136433664 28839 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33309 28839 603 41 0 33268 0
vsize: 133236
[startup+560.108 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 30376 0 0 0 55946 72 0 0 25 0 1 0 427419646 136433664 28844 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33309 28844 603 41 0 33268 0
vsize: 133236
[startup+570.108 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 30381 0 0 0 56946 72 0 0 25 0 1 0 427419646 136433664 28849 4294967295 134512640 134672761 3221224544 3221223648 134560212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33309 28849 603 41 0 33268 0
vsize: 133236
[startup+580.107 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 30381 0 0 0 57946 72 0 0 25 0 1 0 427419646 136433664 28849 4294967295 134512640 134672761 3221224544 3221223648 134560529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33309 28849 603 41 0 33268 0
vsize: 133236
[startup+590.108 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 30386 0 0 0 58946 72 0 0 25 0 1 0 427419646 136433664 28854 4294967295 134512640 134672761 3221224544 3221223648 134560291 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33309 28854 603 41 0 33268 0
vsize: 133236
[startup+600.108 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 30391 0 0 0 59946 72 0 0 25 0 1 0 427419646 136577024 28859 4294967295 134512640 134672761 3221224544 3221223648 134559853 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33344 28859 603 41 0 33303 0
vsize: 133376
[startup+610.108 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 30396 0 0 0 60946 72 0 0 25 0 1 0 427419646 136577024 28864 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33344 28864 603 41 0 33303 0
vsize: 133376
[startup+620.11 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 30401 0 0 0 61947 72 0 0 25 0 1 0 427419646 136577024 28869 4294967295 134512640 134672761 3221224544 3221223648 134560379 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33344 28869 603 41 0 33303 0
vsize: 133376
[startup+630.11 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 30401 0 0 0 62947 72 0 0 25 0 1 0 427419646 136577024 28869 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33344 28869 603 41 0 33303 0
vsize: 133376
[startup+640.11 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 30406 0 0 0 63947 72 0 0 25 0 1 0 427419646 136577024 28874 4294967295 134512640 134672761 3221224544 3221223648 134560184 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33344 28874 603 41 0 33303 0
vsize: 133376
[startup+650.109 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 30411 0 0 0 64947 72 0 0 25 0 1 0 427419646 136577024 28879 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33344 28879 603 41 0 33303 0
vsize: 133376
[startup+660.109 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 30416 0 0 0 65947 72 0 0 25 0 1 0 427419646 136577024 28884 4294967295 134512640 134672761 3221224544 3221223648 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33344 28884 603 41 0 33303 0
vsize: 133376
[startup+670.11 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 30421 0 0 0 66948 72 0 0 25 0 1 0 427419646 136577024 28889 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33344 28889 603 41 0 33303 0
vsize: 133376
[startup+680.109 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 30421 0 0 0 67948 72 0 0 25 0 1 0 427419646 136577024 28889 4294967295 134512640 134672761 3221224544 3221223648 134560008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33344 28889 603 41 0 33303 0
vsize: 133376
[startup+690.109 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 30426 0 0 0 68948 72 0 0 25 0 1 0 427419646 136720384 28894 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33379 28894 603 41 0 33338 0
vsize: 133516
[startup+700.109 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 30430 0 0 0 69948 72 0 0 25 0 1 0 427419646 136720384 28898 4294967295 134512640 134672761 3221224544 3221223648 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33379 28898 603 41 0 33338 0
vsize: 133516
[startup+710.108 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 30435 0 0 0 70948 72 0 0 25 0 1 0 427419646 136720384 28903 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33379 28903 603 41 0 33338 0
vsize: 133516
[startup+720.108 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 30440 0 0 0 71948 72 0 0 25 0 1 0 427419646 136720384 28908 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33379 28908 603 41 0 33338 0
vsize: 133516
[startup+730.108 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 30445 0 0 0 72949 72 0 0 25 0 1 0 427419646 136720384 28913 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33379 28913 603 41 0 33338 0
vsize: 133516
[startup+740.107 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 30495 0 0 0 73949 72 0 0 25 0 1 0 427419646 136953856 28963 4294967295 134512640 134672761 3221224544 3221223648 134559937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33436 28963 603 41 0 33395 0
vsize: 133744
[startup+750.108 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 30499 0 0 0 74949 72 0 0 25 0 1 0 427419646 136953856 28967 4294967295 134512640 134672761 3221224544 3221223648 134560013 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33436 28967 603 41 0 33395 0
vsize: 133744
[startup+760.108 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 30504 0 0 0 75949 72 0 0 25 0 1 0 427419646 136953856 28972 4294967295 134512640 134672761 3221224544 3221223648 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33436 28972 603 41 0 33395 0
vsize: 133744
[startup+770.108 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 30517 0 0 0 76949 72 0 0 25 0 1 0 427419646 137035776 28985 4294967295 134512640 134672761 3221224544 3221223648 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33456 28985 603 41 0 33415 0
vsize: 133824
[startup+780.108 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 30520 0 0 0 77949 72 0 0 25 0 1 0 427419646 137035776 28988 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33456 28988 603 41 0 33415 0
vsize: 133824
[startup+790.108 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 30523 0 0 0 78950 72 0 0 25 0 1 0 427419646 137035776 28991 4294967295 134512640 134672761 3221224544 3221223648 134560264 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33456 28991 603 41 0 33415 0
vsize: 133824
[startup+800.108 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 30544 0 0 0 79950 72 0 0 25 0 1 0 427419646 137175040 29012 4294967295 134512640 134672761 3221224544 3221223648 134560344 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33490 29012 603 41 0 33449 0
vsize: 133960
[startup+810.107 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 30570 0 0 0 80950 72 0 0 25 0 1 0 427419646 137322496 29038 4294967295 134512640 134672761 3221224544 3221223648 134560303 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33526 29038 603 41 0 33485 0
vsize: 134104
[startup+820.108 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 30585 0 0 0 81950 73 0 0 25 0 1 0 427419646 137256960 29053 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33510 29053 603 41 0 33469 0
vsize: 134040
[startup+830.108 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 30595 0 0 0 82950 73 0 0 25 0 1 0 427419646 137256960 29063 4294967295 134512640 134672761 3221224544 3221223648 134559869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33510 29063 603 41 0 33469 0
vsize: 134040
[startup+840.108 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 30616 0 0 0 83950 73 0 0 25 0 1 0 427419646 137396224 29084 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33544 29084 603 41 0 33503 0
vsize: 134176
[startup+850.108 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 30620 0 0 0 84950 73 0 0 25 0 1 0 427419646 137396224 29088 4294967295 134512640 134672761 3221224544 3221223648 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33544 29088 603 41 0 33503 0
vsize: 134176
[startup+860.108 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 30624 0 0 0 85950 73 0 0 25 0 1 0 427419646 137396224 29092 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33544 29092 603 41 0 33503 0
vsize: 134176
[startup+870.108 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 30633 0 0 0 86950 73 0 0 25 0 1 0 427419646 137535488 29101 4294967295 134512640 134672761 3221224544 3221223648 134560514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33578 29101 603 41 0 33537 0
vsize: 134312
[startup+880.107 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 30638 0 0 0 87951 73 0 0 25 0 1 0 427419646 137535488 29106 4294967295 134512640 134672761 3221224544 3221223648 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33578 29106 603 41 0 33537 0
vsize: 134312
[startup+890.108 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 30642 0 0 0 88951 73 0 0 25 0 1 0 427419646 137535488 29110 4294967295 134512640 134672761 3221224544 3221223648 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33578 29110 603 41 0 33537 0
vsize: 134312
[startup+900.108 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 30647 0 0 0 89950 74 0 0 25 0 1 0 427419646 137535488 29115 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33578 29115 603 41 0 33537 0
vsize: 134312
[startup+910.107 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 30704 0 0 0 90950 74 0 0 25 0 1 0 427419646 137797632 29172 4294967295 134512640 134672761 3221224544 3221223712 134561269 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33642 29172 603 41 0 33601 0
vsize: 134568
[startup+920.108 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 30756 0 0 0 91950 74 0 0 25 0 1 0 427419646 137932800 29224 4294967295 134512640 134672761 3221224544 3221223712 134561272 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33675 29224 603 41 0 33634 0
vsize: 134700
[startup+930.108 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 30781 0 0 0 92950 74 0 0 25 0 1 0 427419646 138063872 29249 4294967295 134512640 134672761 3221224544 3221223648 134560492 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33707 29249 603 41 0 33666 0
vsize: 134828
[startup+940.108 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 31058 0 0 0 93949 75 0 0 25 0 1 0 427419646 139247616 29526 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33996 29526 603 41 0 33955 0
vsize: 135984
[startup+950.108 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 31110 0 0 0 94949 76 0 0 25 0 1 0 427419646 139382784 29578 4294967295 134512640 134672761 3221224544 3221223648 134559866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34029 29578 603 41 0 33988 0
vsize: 136116
[startup+960.108 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 31205 0 0 0 95948 76 0 0 25 0 1 0 427419646 139792384 29673 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34129 29673 603 41 0 34088 0
vsize: 136516
[startup+970.108 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 31309 0 0 0 96948 76 0 0 25 0 1 0 427419646 140193792 29777 4294967295 134512640 134672761 3221224544 3221223648 134560248 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34227 29777 603 41 0 34186 0
vsize: 136908
[startup+980.108 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 31423 0 0 0 97948 77 0 0 25 0 1 0 427419646 140775424 29891 4294967295 134512640 134672761 3221224544 3221223648 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34369 29891 603 41 0 34328 0
vsize: 137476
[startup+990.109 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 31583 0 0 0 98948 77 0 0 25 0 1 0 427419646 141365248 30051 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34513 30051 603 41 0 34472 0
vsize: 138052
[startup+1000.11 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 31638 0 0 0 99948 77 0 0 25 0 1 0 427419646 141660160 30106 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34585 30106 603 41 0 34544 0
vsize: 138340
[startup+1010.11 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 31691 0 0 0 100948 77 0 0 25 0 1 0 427419646 141807616 30159 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34621 30159 603 41 0 34580 0
vsize: 138484
[startup+1020.11 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 31744 0 0 0 101948 77 0 0 25 0 1 0 427419646 142102528 30212 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34693 30212 603 41 0 34652 0
vsize: 138772
[startup+1030.11 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 31794 0 0 0 102948 77 0 0 25 0 1 0 427419646 142254080 30262 4294967295 134512640 134672761 3221224544 3221223648 134559835 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34730 30262 603 41 0 34689 0
vsize: 138920
[startup+1040.11 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 31855 0 0 0 103948 77 0 0 25 0 1 0 427419646 142528512 30323 4294967295 134512640 134672761 3221224544 3221223728 134559332 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34797 30323 603 41 0 34756 0
vsize: 139188
[startup+1050.11 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 31927 0 0 0 104947 78 0 0 25 0 1 0 427419646 142807040 30395 4294967295 134512640 134672761 3221224544 3221223648 134560410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34865 30395 603 41 0 34824 0
vsize: 139460
[startup+1060.11 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 31964 0 0 0 105948 78 0 0 25 0 1 0 427419646 142946304 30432 4294967295 134512640 134672761 3221224544 3221223648 134560352 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34899 30432 603 41 0 34858 0
vsize: 139596
[startup+1070.11 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 32019 0 0 0 106947 78 0 0 25 0 1 0 427419646 143122432 30487 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34942 30487 603 41 0 34901 0
vsize: 139768
[startup+1080.11 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 32052 0 0 0 107947 78 0 0 25 0 1 0 427419646 143273984 30520 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34979 30520 603 41 0 34938 0
vsize: 139916
[startup+1090.11 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 32089 0 0 0 108947 78 0 0 25 0 1 0 427419646 143417344 30557 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35014 30557 603 41 0 34973 0
vsize: 140056
[startup+1100.11 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 32112 0 0 0 109948 78 0 0 25 0 1 0 427419646 143564800 30580 4294967295 134512640 134672761 3221224544 3221223648 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35050 30580 603 41 0 35009 0
vsize: 140200
[startup+1110.11 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 32155 0 0 0 110948 79 0 0 25 0 1 0 427419646 143724544 30623 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35089 30623 603 41 0 35048 0
vsize: 140356
[startup+1120.11 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 32173 0 0 0 111948 79 0 0 25 0 1 0 427419646 143867904 30641 4294967295 134512640 134672761 3221224544 3221223648 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35124 30641 603 41 0 35083 0
vsize: 140496
[startup+1130.11 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 32187 0 0 0 112947 79 0 0 25 0 1 0 427419646 143867904 30655 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35124 30655 603 41 0 35083 0
vsize: 140496
[startup+1140.11 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 32219 0 0 0 113947 79 0 0 25 0 1 0 427419646 144015360 30687 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35160 30687 603 41 0 35119 0
vsize: 140640
[startup+1150.11 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 32274 0 0 0 114947 79 0 0 25 0 1 0 427419646 144211968 30742 4294967295 134512640 134672761 3221224544 3221223648 134560237 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35208 30742 603 41 0 35167 0
vsize: 140832
[startup+1160.11 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 32335 0 0 0 115947 79 0 0 25 0 1 0 427419646 144494592 30803 4294967295 134512640 134672761 3221224544 3221223648 134559835 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35277 30803 603 41 0 35236 0
vsize: 141108
[startup+1170.11 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 32425 0 0 0 116947 80 0 0 25 0 1 0 427419646 144773120 30893 4294967295 134512640 134672761 3221224544 3221223648 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35345 30893 603 41 0 35304 0
vsize: 141380
[startup+1180.11 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 32469 0 0 0 117947 80 0 0 25 0 1 0 427419646 145055744 30937 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35414 30937 603 41 0 35373 0
vsize: 141656
[startup+1190.11 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 32533 0 0 0 118947 80 0 0 25 0 1 0 427419646 145346560 31001 4294967295 134512640 134672761 3221224544 3221223648 134560224 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35485 31001 603 41 0 35444 0
vsize: 141940
[startup+1200.11 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 27737
Raw data (stat): 27737 (minisat+) R 27736 30927 30926 0 -1 0 32561 0 0 0 119947 80 0 0 25 0 1 0 427419646 145346560 31029 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35485 31029 603 41 0 35444 0
vsize: 141940
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.18 s]
Raw data (loadavg): 1.00 1.00 0.94 1/55 27737
Raw data (stat): 27737 (minisat+) Z 27736 30927 30926 0 -1 12 32564 0 0 0 119947 86 0 0 25 0 1 0 427419646 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.18
CPU time (s): 1200.34
CPU user time (s): 1199.48
CPU system time (s): 0.865868
CPU usage (%): 100.014
Max. virtual memory (Kb): 141940
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####