PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-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	3684
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.3
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 15665

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        791824 kB
Buffers:         33448 kB
Cached:         187376 kB
SwapCached:        176 kB
Active:          58584 kB
Inactive:       164980 kB
HighTotal:      131008 kB
HighFree:         4956 kB
LowTotal:       903652 kB
LowFree:        786868 kB
SwapTotal:     2097136 kB
SwapFree:      2096860 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6808 kB
Slab:            13688 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 05:46:48 (client local time) WITH STATUS 10 IN 1200.27 SECONDS
stats: 16912 7 1200.27 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): 0.79 0.92 0.91 2/54 31196
Raw data (stat): 31196 (runsolver) R 31195 30701 30700 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 484333426 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0003 s]
Raw data (loadavg): 0.82 0.93 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 28233 0 0 0 936 63 0 0 25 0 1 0 484333426 127602688 26782 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31153 26782 603 41 0 31112 0
vsize: 124612
[startup+20.0013 s]
Raw data (loadavg): 0.85 0.93 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 28311 0 0 0 1935 63 0 0 25 0 1 0 484333426 127602688 26860 4294967295 134512640 134672761 3221224544 3221223668 134566034 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.002 s]
Raw data (loadavg): 0.87 0.93 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 28399 0 0 0 2934 63 0 0 25 0 1 0 484333426 127733760 26948 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31185 26948 603 41 0 31144 0
vsize: 124740
[startup+40.002 s]
Raw data (loadavg): 0.89 0.93 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 28425 0 0 0 3935 63 0 0 25 0 1 0 484333426 127733760 26974 4294967295 134512640 134672761 3221224544 3221223716 134556653 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.0023 s]
Raw data (loadavg): 0.91 0.93 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 28546 0 0 0 4934 65 0 0 25 0 1 0 484333426 128262144 27095 4294967295 134512640 134672761 3221224544 3221223680 134560647 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31314 27095 603 41 0 31273 0
vsize: 125256
[startup+60.0023 s]
Raw data (loadavg): 0.92 0.93 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 28699 0 0 0 5933 65 0 0 25 0 1 0 484333426 128925696 27248 4294967295 134512640 134672761 3221224544 3221223712 134561025 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.0029 s]
Raw data (loadavg): 0.93 0.94 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 29091 0 0 0 6933 66 0 0 25 0 1 0 484333426 131272704 27613 4294967295 134512640 134672761 3221224544 3221223712 134561385 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.0036 s]
Raw data (loadavg): 0.94 0.94 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 29092 0 0 0 7933 66 0 0 25 0 1 0 484333426 131272704 27614 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32049 27614 603 41 0 32008 0
vsize: 128196
[startup+90.0032 s]
Raw data (loadavg): 0.95 0.94 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 29195 0 0 0 8933 66 0 0 25 0 1 0 484333426 131629056 27694 4294967295 134512640 134672761 3221224544 3221223712 134561164 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.004 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 29202 0 0 0 9933 66 0 0 25 0 1 0 484333426 131629056 27701 4294967295 134512640 134672761 3221224544 3221223744 134557830 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.004 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 29244 0 0 0 10933 66 0 0 25 0 1 0 484333426 131764224 27743 4294967295 134512640 134672761 3221224544 3221223696 134561244 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32169 27743 603 41 0 32128 0
vsize: 128676
[startup+120.005 s]
Raw data (loadavg): 0.97 0.94 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 29319 0 0 0 11933 66 0 0 25 0 1 0 484333426 132034560 27818 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32235 27818 603 41 0 32194 0
vsize: 128940
[startup+130.006 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 29417 0 0 0 12933 66 0 0 25 0 1 0 484333426 132440064 27916 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32334 27916 603 41 0 32293 0
vsize: 129336
[startup+140.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 29528 0 0 0 13933 67 0 0 25 0 1 0 484333426 132706304 27996 4294967295 134512640 134672761 3221224544 3221223680 134560619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32399 27996 603 41 0 32358 0
vsize: 129596
[startup+150.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 29568 0 0 0 14933 67 0 0 25 0 1 0 484333426 132976640 28036 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32465 28036 603 41 0 32424 0
vsize: 129860
[startup+160.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 29646 0 0 0 15933 67 0 0 25 0 1 0 484333426 133328896 28114 4294967295 134512640 134672761 3221224544 3221223760 134561948 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.007 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 29786 0 0 0 16933 67 0 0 25 0 1 0 484333426 133836800 28254 4294967295 134512640 134672761 3221224544 3221223648 134560002 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32675 28254 603 41 0 32634 0
vsize: 130700
[startup+180.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 29874 0 0 0 17933 67 0 0 25 0 1 0 484333426 134119424 28342 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32744 28342 603 41 0 32703 0
vsize: 130976
[startup+190.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 29902 0 0 0 18934 67 0 0 25 0 1 0 484333426 134262784 28370 4294967295 134512640 134672761 3221224544 3221223648 134559964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32779 28370 603 41 0 32738 0
vsize: 131116
[startup+200.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 30032 0 0 0 19934 67 0 0 25 0 1 0 484333426 134795264 28500 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32909 28500 603 41 0 32868 0
vsize: 131636
[startup+210.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 30094 0 0 0 20933 68 0 0 25 0 1 0 484333426 135061504 28562 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32974 28562 603 41 0 32933 0
vsize: 131896
[startup+220.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 30140 0 0 0 21934 68 0 0 25 0 1 0 484333426 135458816 28608 4294967295 134512640 134672761 3221224544 3221223648 134559887 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33071 28608 603 41 0 33030 0
vsize: 132284
[startup+230.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 30175 0 0 0 22934 68 0 0 25 0 1 0 484333426 135598080 28643 4294967295 134512640 134672761 3221224544 3221223648 134560022 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33105 28643 603 41 0 33064 0
vsize: 132420
[startup+240.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 30192 0 0 0 23934 68 0 0 25 0 1 0 484333426 135733248 28660 4294967295 134512640 134672761 3221224544 3221223648 134560148 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33138 28660 603 41 0 33097 0
vsize: 132552
[startup+250.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 30210 0 0 0 24934 68 0 0 25 0 1 0 484333426 135733248 28678 4294967295 134512640 134672761 3221224544 3221223648 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33138 28678 603 41 0 33097 0
vsize: 132552
[startup+260.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 30220 0 0 0 25934 68 0 0 25 0 1 0 484333426 135872512 28688 4294967295 134512640 134672761 3221224544 3221223648 134560154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33172 28688 603 41 0 33131 0
vsize: 132688
[startup+270.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 30238 0 0 0 26935 68 0 0 25 0 1 0 484333426 135872512 28706 4294967295 134512640 134672761 3221224544 3221223648 134560355 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33172 28706 603 41 0 33131 0
vsize: 132688
[startup+280.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 30242 0 0 0 27935 68 0 0 25 0 1 0 484333426 135872512 28710 4294967295 134512640 134672761 3221224544 3221223648 134560264 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33172 28710 603 41 0 33131 0
vsize: 132688
[startup+290.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 30248 0 0 0 28935 68 0 0 25 0 1 0 484333426 135872512 28716 4294967295 134512640 134672761 3221224544 3221223648 134560224 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33172 28716 603 41 0 33131 0
vsize: 132688
[startup+300.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 30272 0 0 0 29935 68 0 0 25 0 1 0 484333426 136003584 28740 4294967295 134512640 134672761 3221224544 3221223648 134559927 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33204 28740 603 41 0 33163 0
vsize: 132816
[startup+310.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 30277 0 0 0 30935 68 0 0 25 0 1 0 484333426 136003584 28745 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33204 28745 603 41 0 33163 0
vsize: 132816
[startup+320.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 30277 0 0 0 31935 68 0 0 25 0 1 0 484333426 136003584 28745 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33204 28745 603 41 0 33163 0
vsize: 132816
[startup+330.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 30282 0 0 0 32936 68 0 0 25 0 1 0 484333426 136003584 28750 4294967295 134512640 134672761 3221224544 3221223648 134560410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33204 28750 603 41 0 33163 0
vsize: 132816
[startup+340.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 30287 0 0 0 33936 68 0 0 25 0 1 0 484333426 136151040 28755 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33240 28755 603 41 0 33199 0
vsize: 132960
[startup+350.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 30292 0 0 0 34936 68 0 0 25 0 1 0 484333426 136151040 28760 4294967295 134512640 134672761 3221224544 3221223648 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33240 28760 603 41 0 33199 0
vsize: 132960
[startup+360.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 30297 0 0 0 35936 68 0 0 25 0 1 0 484333426 136151040 28765 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33240 28765 603 41 0 33199 0
vsize: 132960
[startup+370.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 30297 0 0 0 36936 68 0 0 25 0 1 0 484333426 136151040 28765 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33240 28765 603 41 0 33199 0
vsize: 132960
[startup+380.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 30302 0 0 0 37937 68 0 0 25 0 1 0 484333426 136151040 28770 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33240 28770 603 41 0 33199 0
vsize: 132960
[startup+390.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 30307 0 0 0 38937 68 0 0 25 0 1 0 484333426 136151040 28775 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33240 28775 603 41 0 33199 0
vsize: 132960
[startup+400.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 30312 0 0 0 39937 68 0 0 25 0 1 0 484333426 136151040 28780 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33240 28780 603 41 0 33199 0
vsize: 132960
[startup+410.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 30317 0 0 0 40937 68 0 0 25 0 1 0 484333426 136151040 28785 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33240 28785 603 41 0 33199 0
vsize: 132960
[startup+420.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 30322 0 0 0 41937 68 0 0 25 0 1 0 484333426 136294400 28790 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33275 28790 603 41 0 33234 0
vsize: 133100
[startup+430.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 30322 0 0 0 42937 68 0 0 25 0 1 0 484333426 136294400 28790 4294967295 134512640 134672761 3221224544 3221223648 134559916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33275 28790 603 41 0 33234 0
vsize: 133100
[startup+440.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 30327 0 0 0 43938 68 0 0 25 0 1 0 484333426 136294400 28795 4294967295 134512640 134672761 3221224544 3221223648 134560002 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33275 28795 603 41 0 33234 0
vsize: 133100
[startup+450.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 30332 0 0 0 44938 68 0 0 25 0 1 0 484333426 136294400 28800 4294967295 134512640 134672761 3221224544 3221223648 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33275 28800 603 41 0 33234 0
vsize: 133100
[startup+460.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 30337 0 0 0 45938 68 0 0 25 0 1 0 484333426 136294400 28805 4294967295 134512640 134672761 3221224544 3221223648 134559927 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33275 28805 603 41 0 33234 0
vsize: 133100
[startup+470.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 30342 0 0 0 46938 68 0 0 25 0 1 0 484333426 136294400 28810 4294967295 134512640 134672761 3221224544 3221223648 134560396 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33275 28810 603 41 0 33234 0
vsize: 133100
[startup+480.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 30342 0 0 0 47939 68 0 0 25 0 1 0 484333426 136294400 28810 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33275 28810 603 41 0 33234 0
vsize: 133100
[startup+490.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 30347 0 0 0 48939 68 0 0 25 0 1 0 484333426 136294400 28815 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33275 28815 603 41 0 33234 0
vsize: 133100
[startup+500.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 30351 0 0 0 49939 68 0 0 25 0 1 0 484333426 136294400 28819 4294967295 134512640 134672761 3221224544 3221223648 134560418 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33275 28819 603 41 0 33234 0
vsize: 133100
[startup+510.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 30356 0 0 0 50939 68 0 0 25 0 1 0 484333426 136433664 28824 4294967295 134512640 134672761 3221224544 3221223648 134559941 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33309 28824 603 41 0 33268 0
vsize: 133236
[startup+520.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 30361 0 0 0 51939 68 0 0 25 0 1 0 484333426 136433664 28829 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33309 28829 603 41 0 33268 0
vsize: 133236
[startup+530.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 30366 0 0 0 52939 68 0 0 25 0 1 0 484333426 136433664 28834 4294967295 134512640 134672761 3221224544 3221223648 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33309 28834 603 41 0 33268 0
vsize: 133236
[startup+540.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 30366 0 0 0 53940 68 0 0 25 0 1 0 484333426 136433664 28834 4294967295 134512640 134672761 3221224544 3221223648 134559979 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33309 28834 603 41 0 33268 0
vsize: 133236
[startup+550.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 30371 0 0 0 54940 68 0 0 25 0 1 0 484333426 136433664 28839 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33309 28839 603 41 0 33268 0
vsize: 133236
[startup+560.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 30376 0 0 0 55940 68 0 0 25 0 1 0 484333426 136433664 28844 4294967295 134512640 134672761 3221224544 3221223648 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33309 28844 603 41 0 33268 0
vsize: 133236
[startup+570.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 30381 0 0 0 56940 68 0 0 25 0 1 0 484333426 136433664 28849 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33309 28849 603 41 0 33268 0
vsize: 133236
[startup+580.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 30386 0 0 0 57940 68 0 0 25 0 1 0 484333426 136433664 28854 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33309 28854 603 41 0 33268 0
vsize: 133236
[startup+590.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 30391 0 0 0 58941 68 0 0 25 0 1 0 484333426 136577024 28859 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33344 28859 603 41 0 33303 0
vsize: 133376
[startup+600.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 30391 0 0 0 59941 68 0 0 25 0 1 0 484333426 136577024 28859 4294967295 134512640 134672761 3221224544 3221223648 134560198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33344 28859 603 41 0 33303 0
vsize: 133376
[startup+610.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 30396 0 0 0 60941 68 0 0 25 0 1 0 484333426 136577024 28864 4294967295 134512640 134672761 3221224544 3221223648 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33344 28864 603 41 0 33303 0
vsize: 133376
[startup+620.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 30401 0 0 0 61941 68 0 0 25 0 1 0 484333426 136577024 28869 4294967295 134512640 134672761 3221224544 3221223648 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33344 28869 603 41 0 33303 0
vsize: 133376
[startup+630.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 30406 0 0 0 62941 68 0 0 25 0 1 0 484333426 136577024 28874 4294967295 134512640 134672761 3221224544 3221223648 134559985 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33344 28874 603 41 0 33303 0
vsize: 133376
[startup+640.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 30411 0 0 0 63942 68 0 0 25 0 1 0 484333426 136577024 28879 4294967295 134512640 134672761 3221224544 3221223648 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33344 28879 603 41 0 33303 0
vsize: 133376
[startup+650.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 30411 0 0 0 64942 68 0 0 25 0 1 0 484333426 136577024 28879 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33344 28879 603 41 0 33303 0
vsize: 133376
[startup+660.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 30416 0 0 0 65942 68 0 0 25 0 1 0 484333426 136577024 28884 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33344 28884 603 41 0 33303 0
vsize: 133376
[startup+670.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 30421 0 0 0 66942 68 0 0 25 0 1 0 484333426 136577024 28889 4294967295 134512640 134672761 3221224544 3221223648 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33344 28889 603 41 0 33303 0
vsize: 133376
[startup+680.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 30426 0 0 0 67942 68 0 0 25 0 1 0 484333426 136720384 28894 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33379 28894 603 41 0 33338 0
vsize: 133516
[startup+690.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 30430 0 0 0 68943 68 0 0 25 0 1 0 484333426 136720384 28898 4294967295 134512640 134672761 3221224544 3221223648 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33379 28898 603 41 0 33338 0
vsize: 133516
[startup+700.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 30430 0 0 0 69943 68 0 0 25 0 1 0 484333426 136720384 28898 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33379 28898 603 41 0 33338 0
vsize: 133516
[startup+710.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 30435 0 0 0 70943 68 0 0 25 0 1 0 484333426 136720384 28903 4294967295 134512640 134672761 3221224544 3221223648 134559887 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33379 28903 603 41 0 33338 0
vsize: 133516
[startup+720.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 30440 0 0 0 71943 68 0 0 25 0 1 0 484333426 136720384 28908 4294967295 134512640 134672761 3221224544 3221223648 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33379 28908 603 41 0 33338 0
vsize: 133516
[startup+730.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 30466 0 0 0 72943 68 0 0 25 0 1 0 484333426 136884224 28934 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33419 28934 603 41 0 33378 0
vsize: 133676
[startup+740.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 30499 0 0 0 73943 68 0 0 25 0 1 0 484333426 136953856 28967 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33436 28967 603 41 0 33395 0
vsize: 133744
[startup+750.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 30504 0 0 0 74944 68 0 0 25 0 1 0 484333426 136953856 28972 4294967295 134512640 134672761 3221224544 3221223648 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33436 28972 603 41 0 33395 0
vsize: 133744
[startup+760.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 30517 0 0 0 75944 68 0 0 25 0 1 0 484333426 137035776 28985 4294967295 134512640 134672761 3221224544 3221223648 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33456 28985 603 41 0 33415 0
vsize: 133824
[startup+770.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 30520 0 0 0 76944 68 0 0 25 0 1 0 484333426 137035776 28988 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33456 28988 603 41 0 33415 0
vsize: 133824
[startup+780.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 30523 0 0 0 77944 68 0 0 25 0 1 0 484333426 137035776 28991 4294967295 134512640 134672761 3221224544 3221223648 134560408 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33456 28991 603 41 0 33415 0
vsize: 133824
[startup+790.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 30527 0 0 0 78944 68 0 0 25 0 1 0 484333426 137035776 28995 4294967295 134512640 134672761 3221224544 3221223648 134560514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33456 28995 603 41 0 33415 0
vsize: 133824
[startup+800.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 30544 0 0 0 79945 68 0 0 25 0 1 0 484333426 137175040 29012 4294967295 134512640 134672761 3221224544 3221223648 134560243 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33490 29012 603 41 0 33449 0
vsize: 133960
[startup+810.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 30582 0 0 0 80945 69 0 0 25 0 1 0 484333426 137256960 29050 4294967295 134512640 134672761 3221224544 3221223648 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33510 29050 603 41 0 33469 0
vsize: 134040
[startup+820.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 30588 0 0 0 81945 69 0 0 25 0 1 0 484333426 137256960 29056 4294967295 134512640 134672761 3221224544 3221223648 134560316 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33510 29056 603 41 0 33469 0
vsize: 134040
[startup+830.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 30611 0 0 0 82945 69 0 0 25 0 1 0 484333426 137396224 29079 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33544 29079 603 41 0 33503 0
vsize: 134176
[startup+840.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 30620 0 0 0 83945 69 0 0 25 0 1 0 484333426 137396224 29088 4294967295 134512640 134672761 3221224544 3221223648 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33544 29088 603 41 0 33503 0
vsize: 134176
[startup+850.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 30624 0 0 0 84945 69 0 0 25 0 1 0 484333426 137396224 29092 4294967295 134512640 134672761 3221224544 3221223648 134560025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33544 29092 603 41 0 33503 0
vsize: 134176
[startup+860.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 30633 0 0 0 85945 69 0 0 25 0 1 0 484333426 137535488 29101 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33578 29101 603 41 0 33537 0
vsize: 134312
[startup+870.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 30638 0 0 0 86945 69 0 0 25 0 1 0 484333426 137535488 29106 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33578 29106 603 41 0 33537 0
vsize: 134312
[startup+880.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 30638 0 0 0 87946 69 0 0 25 0 1 0 484333426 137535488 29106 4294967295 134512640 134672761 3221224544 3221223648 134560506 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.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 30642 0 0 0 88946 69 0 0 25 0 1 0 484333426 137535488 29110 4294967295 134512640 134672761 3221224544 3221223648 134560520 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.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 30691 0 0 0 89945 69 0 0 25 0 1 0 484333426 137662464 29159 4294967295 134512640 134672761 3221224544 3221223648 134560347 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33609 29159 603 41 0 33568 0
vsize: 134436
[startup+910.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 30748 0 0 0 90945 69 0 0 25 0 1 0 484333426 137932800 29216 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33675 29216 603 41 0 33634 0
vsize: 134700
[startup+920.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 30759 0 0 0 91945 69 0 0 25 0 1 0 484333426 138063872 29227 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33707 29227 603 41 0 33666 0
vsize: 134828
[startup+930.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 30964 0 0 0 92945 70 0 0 25 0 1 0 484333426 138940416 29432 4294967295 134512640 134672761 3221224544 3221223648 134559908 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33921 29432 603 41 0 33880 0
vsize: 135684
[startup+940.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 31081 0 0 0 93945 70 0 0 25 0 1 0 484333426 139382784 29549 4294967295 134512640 134672761 3221224544 3221223712 134560855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34029 29549 603 41 0 33988 0
vsize: 136116
[startup+950.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 31176 0 0 0 94945 70 0 0 25 0 1 0 484333426 139665408 29644 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34098 29644 603 41 0 34057 0
vsize: 136392
[startup+960.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 31278 0 0 0 95945 71 0 0 25 0 1 0 484333426 140193792 29746 4294967295 134512640 134672761 3221224544 3221223648 134560316 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34227 29746 603 41 0 34186 0
vsize: 136908
[startup+970.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 31370 0 0 0 96945 71 0 0 25 0 1 0 484333426 140505088 29838 4294967295 134512640 134672761 3221224544 3221223648 134560191 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34303 29838 603 41 0 34262 0
vsize: 137212
[startup+980.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 31564 0 0 0 97944 71 0 0 25 0 1 0 484333426 141365248 30032 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34513 30032 603 41 0 34472 0
vsize: 138052
[startup+990.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 31626 0 0 0 98944 72 0 0 25 0 1 0 484333426 141524992 30094 4294967295 134512640 134672761 3221224544 3221223648 134560019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34552 30094 603 41 0 34511 0
vsize: 138208
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 31678 0 0 0 99944 72 0 0 25 0 1 0 484333426 141807616 30146 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34621 30146 603 41 0 34580 0
vsize: 138484
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 31731 0 0 0 100944 72 0 0 25 0 1 0 484333426 141942784 30199 4294967295 134512640 134672761 3221224544 3221223648 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34654 30199 603 41 0 34613 0
vsize: 138616
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 31775 0 0 0 101945 72 0 0 25 0 1 0 484333426 142102528 30243 4294967295 134512640 134672761 3221224544 3221223648 134559887 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34693 30243 603 41 0 34652 0
vsize: 138772
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 31842 0 0 0 102945 72 0 0 25 0 1 0 484333426 142389248 30310 4294967295 134512640 134672761 3221224544 3221223648 134560506 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34763 30310 603 41 0 34722 0
vsize: 139052
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 31904 0 0 0 103945 72 0 0 25 0 1 0 484333426 142671872 30372 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34832 30372 603 41 0 34791 0
vsize: 139328
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 31951 0 0 0 104945 72 0 0 25 0 1 0 484333426 142946304 30419 4294967295 134512640 134672761 3221224544 3221223648 134560191 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34899 30419 603 41 0 34858 0
vsize: 139596
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 31988 0 0 0 105945 72 0 0 25 0 1 0 484333426 143015936 30456 4294967295 134512640 134672761 3221224544 3221223648 134559966 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34916 30456 603 41 0 34875 0
vsize: 139664
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 32036 0 0 0 106945 73 0 0 25 0 1 0 484333426 143273984 30504 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34979 30504 603 41 0 34938 0
vsize: 139916
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 32084 0 0 0 107945 73 0 0 25 0 1 0 484333426 143417344 30552 4294967295 134512640 134672761 3221224544 3221223648 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35014 30552 603 41 0 34973 0
vsize: 140056
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 32112 0 0 0 108945 73 0 0 25 0 1 0 484333426 143564800 30580 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35050 30580 603 41 0 35009 0
vsize: 140200
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 32155 0 0 0 109945 73 0 0 25 0 1 0 484333426 143724544 30623 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35089 30623 603 41 0 35048 0
vsize: 140356
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 32168 0 0 0 110946 73 0 0 25 0 1 0 484333426 143724544 30636 4294967295 134512640 134672761 3221224544 3221223648 134560370 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35089 30636 603 41 0 35048 0
vsize: 140356
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 32187 0 0 0 111946 73 0 0 25 0 1 0 484333426 143867904 30655 4294967295 134512640 134672761 3221224544 3221223648 134559941 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35124 30655 603 41 0 35083 0
vsize: 140496
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 32219 0 0 0 112946 73 0 0 25 0 1 0 484333426 144015360 30687 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35160 30687 603 41 0 35119 0
vsize: 140640
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 32268 0 0 0 113946 73 0 0 25 0 1 0 484333426 144211968 30736 4294967295 134512640 134672761 3221224544 3221223648 134559835 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35208 30736 603 41 0 35167 0
vsize: 140832
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 32332 0 0 0 114946 73 0 0 25 0 1 0 484333426 144494592 30800 4294967295 134512640 134672761 3221224544 3221223648 134560514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35277 30800 603 41 0 35236 0
vsize: 141108
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 32424 0 0 0 115946 73 0 0 25 0 1 0 484333426 144773120 30892 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35345 30892 603 41 0 35304 0
vsize: 141380
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 32459 0 0 0 116946 73 0 0 25 0 1 0 484333426 144908288 30927 4294967295 134512640 134672761 3221224544 3221223648 134560514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35378 30927 603 41 0 35337 0
vsize: 141512
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 32524 0 0 0 117946 73 0 0 25 0 1 0 484333426 145203200 30992 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35450 30992 603 41 0 35409 0
vsize: 141800
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 32556 0 0 0 118947 73 0 0 25 0 1 0 484333426 145346560 31024 4294967295 134512640 134672761 3221224544 3221223648 134559985 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35485 31024 603 41 0 35444 0
vsize: 141940
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31196
Raw data (stat): 31196 (minisat+) R 31195 30701 30700 0 -1 0 32580 0 0 0 119947 73 0 0 25 0 1 0 484333426 145498112 31048 4294967295 134512640 134672761 3221224544 3221223648 134559902 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35522 31048 603 41 0 35481 0
vsize: 142088
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.09 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 31196
Raw data (stat): 31196 (minisat+) Z 31195 30701 30700 0 -1 12 32583 0 0 0 119947 79 0 0 25 0 1 0 484333426 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.09
CPU time (s): 1200.27
CPU user time (s): 1199.47
CPU system time (s): 0.798878
CPU usage (%): 100.015
Max. virtual memory (Kb): 142088
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####