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/miplib3/normalized-mps-v2-13-7-p0282.opb
MD5SUM	1a8deb577df7e72871b7e1004c098336
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	258411
Optimality of the best value was proved	NO
Number of terms in the objective function	282
Biggest coefficient in the objective function	160646
Number of bits for the biggest coefficient in the objective function	18
Sum of the numbers in the objective function	1302615
Number of bits of the sum of numbers in the objective function	21
Biggest number in a constraint	160646
Number of bits of the biggest number in a constraint	18
Biggest sum of numbers in a constraint	1302615
Number of bits of the biggest sum of numbers	21
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.02084
Number of variables	282
Total number of constraints	523
Number of constraints which are clauses	177
Number of constraints which are cardinality constraints (but not clauses)	282
Number of constraints which are nor clauses,nor cardinality constraints	64
Minimum length of a constraint	1
Maximum length of a constraint	57
Trace number 18005

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        538536 kB
Buffers:         34656 kB
Cached:         439680 kB
SwapCached:        440 kB
Active:         155844 kB
Inactive:       320672 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        538284 kB
SwapTotal:     2097136 kB
SwapFree:      2095984 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5360 kB
Slab:            13932 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 13:26:33 (client local time) WITH STATUS 10 IN 1200.2 SECONDS
stats: 18717 7 1200.2 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 221 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): sss.................................................................................................................................................................................
c ---[ 223]---> Adder-cost: 124   maxlim: 245   bits: 9/8
c ---[ 222]---> Adder-cost: 104   maxlim: 265   bits: 10/9
c ---[ 221]---> Adder-cost: 126   maxlim: 182   bits: 9/8
c ---[ 220]---> Adder-cost: 98   maxlim: 202   bits: 9/8
c ---[ 219]---> Adder-cost: 114   maxlim: 168   bits: 9/8
c ---[ 218]---> Adder-cost: 100   maxlim: 188   bits: 9/8
c ---[ 217]---> Adder-cost: 98   maxlim: 192   bits: 9/8
c ---[ 216]---> Adder-cost: 98   maxlim: 212   bits: 9/8
c ---[ 215]---> Adder-cost: 106   maxlim: 178   bits: 9/8
c ---[ 214]---> Adder-cost: 98   maxlim: 198   bits: 9/8
c ---[ 213]---> Adder-cost: 127   maxlim: 321   bits: 10/9
c ---[ 211]---> Adder-cost: 115   maxlim: 341   bits: 10/9
c ---[ 209]---> Adder-cost: 112   maxlim: 529   bits: 10/10
c ---[ 208]---> Adder-cost: 98   maxlim: 249   bits: 9/8
c ---[ 207]---> Adder-cost: 108   maxlim: 198   bits: 9/8
c ---[ 206]---> Adder-cost: 104   maxlim: 218   bits: 9/8
c ---[ 205]---> Adder-cost: 100   maxlim: 155   bits: 9/8
c ---[ 204]---> Adder-cost: 98   maxlim: 175   bits: 9/8
c ---[ 203]---> Adder-cost: 104   maxlim: 118   bits: 8/7
c ---[ 202]---> Adder-cost: 98   maxlim: 138   bits: 9/8
c ---[ 201]---> Adder-cost: 104   maxlim: 267   bits: 10/9
c ---[ 199]---> Adder-cost: 98   maxlim: 204   bits: 9/8
c ---[ 198]---> Adder-cost: 98   maxlim: 224   bits: 9/8
c ---[ 197]---> Adder-cost: 96   maxlim: 167   bits: 9/8
c ---[ 196]---> Adder-cost: 102   maxlim: 187   bits: 9/8
c ---[ 195]---> Adder-cost: 106   maxlim: 234   bits: 9/8
c ---[ 194]---> Adder-cost: 100   maxlim: 254   bits: 9/8
c ---[ 193]---> Adder-cost: 100   maxlim: 442   bits: 10/9
c ---[ 192]---> Adder-cost: 110   maxlim: 182   bits: 9/8
c ---[ 191]---> Adder-cost: 119   maxlim: 401   bits: 10/9
c ---[ 190]---> Adder-cost: 117   maxlim: 141   bits: 9/8
c ---[ 189]---> Adder-cost: 115   maxlim: 421   bits: 10/9
c ---[ 188]---> Adder-cost: 117   maxlim: 161   bits: 9/8
c ---[ 187]---> Adder-cost: 112   maxlim: 55   bits: 7/6
c ---[ 186]---> Adder-cost: 20   maxlim: 9   bits: 5/4
c ---[ 185]---> Adder-cost: 112   maxlim: 55   bits: 7/6
c ---[ 184]---> Adder-cost: 112   maxlim: 55   bits: 7/6
c ---[ 183]---> Adder-cost: 31   maxlim: 15   bits: 5/4
c ---[ 182]---> Adder-cost: 52   maxlim: 25   bits: 6/5
c ---[ 181]---> Adder-cost: 15   maxlim: 7   bits: 4/3
c ---[ 180]---> Adder-cost: 7   maxlim: 3   bits: 3/2
c ---[   2]---> Adder-cost: 83   maxlim: 61   bits: 7/6
c ---[   1]---> Adder-cost: 81   maxlim: 81   bits: 8/7
c ---[   0]---> Adder-cost: 21   maxlim: 7   bits: 4/3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   27042    96123 |    9014       0        0     nan |  0.000 % |
c |       100 |   27042    96123 |    9915     100      368     3.7 |  4.011 % |
c |       251 |   27042    96123 |   10906     251     2323     9.3 |  4.011 % |
c |       477 |   27042    96123 |   11997     477     5125    10.7 |  4.011 % |
c |       816 |   27042    96123 |   13197     816     9603    11.8 |  4.011 % |
c |      1322 |   27042    96123 |   14517    1322    17051    12.9 |  4.011 % |
c |      2082 |   27042    96123 |   15968    2082    27819    13.4 |  4.012 % |
c ==============================================================================
c [1mFound solution: 530574[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 2436   maxlim: 772041   bits: 21/20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2861 |   44003   156729 |   14667    2861    38547    13.5 |  4.012 % |
c |      2963 |   44003   156729 |   16133    2963    39359    13.3 |  2.778 % |
c |      3113 |   44003   156729 |   17747    3113    41738    13.4 |  2.778 % |
c |      3338 |   44003   156729 |   19521    3338    44844    13.4 |  2.778 % |
c |      3675 |   44003   156729 |   21473    3675    49558    13.5 |  2.778 % |
c |      4182 |   44003   156729 |   23621    4182    57396    13.7 |  2.778 % |
c ==============================================================================
c [1mFound solution: 495924[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 806691   bits: 21/20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4705 |   44018   156848 |   14672    4705    65230    13.9 |  2.778 % |
c |      4805 |   44018   156848 |   16139    4805    66630    13.9 |  2.889 % |
c |      4955 |   44018   156848 |   17753    4955    68220    13.8 |  2.889 % |
c |      5181 |   44018   156848 |   19528    5181    71423    13.8 |  2.889 % |
c |      5518 |   44018   156848 |   21481    5518    78404    14.2 |  2.889 % |
c |      6024 |   44018   156848 |   23629    6024    83049    13.8 |  2.889 % |
c |      6783 |   44018   156848 |   25992    6783    95959    14.1 |  2.889 % |
c |      7923 |   44018   156848 |   28591    7923   111884    14.1 |  2.889 % |
c |      9632 |   44018   156848 |   31450    9632   165118    17.1 |  2.889 % |
c |     12197 |   44018   156848 |   34595   12197   226674    18.6 |  2.889 % |
c |     16041 |   44018   156848 |   38055   16041   388131    24.2 |  2.889 % |
c |     21808 |   44018   156848 |   41860   21808   728993    33.4 |  2.889 % |
c ==============================================================================
c [1mFound solution: 471827[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 830788   bits: 21/20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     23958 |   44040   157011 |   14680   23958   760593    31.7 |  2.889 % |
c |     24058 |   44040   157011 |   16148   12079   471606    39.0 |  2.998 % |
c |     24208 |   44040   157011 |   17762   12229   472810    38.7 |  2.998 % |
c |     24433 |   44040   157011 |   19539   12454   475232    38.2 |  2.998 % |
c |     24771 |   44040   157011 |   21492   12792   478852    37.4 |  2.998 % |
c |     25277 |   44040   157011 |   23642   13298   487049    36.6 |  2.998 % |
c |     26036 |   44040   157011 |   26006   14057   525090    37.4 |  2.998 % |
c |     27175 |   44040   157011 |   28607   15196   557070    36.7 |  2.998 % |
c |     28885 |   44040   157011 |   31467   16906   604692    35.8 |  2.998 % |
c |     31447 |   44040   157011 |   34614   19468   657782    33.8 |  2.998 % |
c |     35291 |   44040   157011 |   38076   23312   941858    40.4 |  2.998 % |
c |     41059 |   44040   157011 |   41883   29080  1285083    44.2 |  2.998 % |
c |     49709 |   44040   157011 |   46072   37730  1885618    50.0 |  2.998 % |
c |     62683 |   44040   157011 |   50679   17242   857024    49.7 |  2.998 % |
c |     82144 |   44040   157011 |   55747   36703  1910978    52.1 |  2.998 % |
c |    111336 |   44040   157011 |   61322   24666  1025240    41.6 |  2.998 % |
c ==============================================================================
c [1mFound solution: 471639[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 830976   bits: 21/20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    147661 |   44043   157048 |   14681   60991  4210897    69.0 |  2.998 % |
c |    147761 |   44043   157048 |   16149   14692  1336667    91.0 |  3.026 % |
c |    147911 |   44043   157048 |   17764   14842  1338047    90.2 |  3.026 % |
c |    148136 |   44043   157048 |   19540   15067  1340176    88.9 |  3.026 % |
c |    148475 |   44043   157048 |   21494   15406  1344108    87.2 |  3.026 % |
c |    148981 |   44043   157048 |   23643   15912  1350334    84.9 |  3.026 % |
c |    149740 |   44043   157048 |   26008   16671  1367099    82.0 |  3.026 % |
c |    150879 |   44037   157031 |   28609   17809  1380340    77.5 |  3.040 % |
c |    152587 |   44037   157031 |   31470   19517  1422609    72.9 |  3.040 % |
c |    155150 |   44037   157031 |   34617   22080  1515797    68.7 |  3.040 % |
c |    158994 |   44037   157031 |   38078   25924  1738296    67.1 |  3.040 % |
c |    164762 |   44037   157031 |   41886   31692  1976844    62.4 |  3.040 % |
c ==============================================================================
c [1mFound solution: 464210[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 838405   bits: 21/20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    167831 |   44045   157121 |   14681   34761  2081464    59.9 |  3.040 % |
c |    167933 |   44045   157121 |   16149   13823   525799    38.0 |  3.122 % |
c |    168083 |   44045   157121 |   17764   13973   527131    37.7 |  3.122 % |
c |    168309 |   44045   157121 |   19540   14199   530316    37.3 |  3.122 % |
c |    168646 |   44045   157121 |   21494   14536   539546    37.1 |  3.122 % |
c |    169152 |   44045   157121 |   23643   15042   546548    36.3 |  3.122 % |
c |    169911 |   44045   157121 |   26008   15801   564733    35.7 |  3.122 % |
c |    171052 |   44045   157121 |   28609   16942   591764    34.9 |  3.122 % |
c |    172760 |   44045   157121 |   31470   18650   675261    36.2 |  3.122 % |
c |    175323 |   44045   157121 |   34617   21213   750053    35.4 |  3.122 % |
c |    179167 |   44045   157121 |   38078   25057   899368    35.9 |  3.122 % |
c ==============================================================================
c [1mFound solution: 428395[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 874220   bits: 21/20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    184012 |   44060   157289 |   14686   29902  1218066    40.7 |  3.122 % |
c |    184112 |   44060   157289 |   16154   13979   555675    39.8 |  3.273 % |
c |    184263 |   44060   157289 |   17770   14130   557655    39.5 |  3.273 % |
c |    184489 |   44060   157289 |   19547   14356   562583    39.2 |  3.273 % |
c |    184826 |   44060   157289 |   21501   14693   569455    38.8 |  3.273 % |
c |    185332 |   44060   157289 |   23651   15199   581093    38.2 |  3.273 % |
c |    186092 |   44060   157289 |   26017   15959   610267    38.2 |  3.273 % |
c |    187232 |   44060   157289 |   28618   17099   641313    37.5 |  3.273 % |
c |    188940 |   44060   157289 |   31480   18807   722381    38.4 |  3.273 % |
c |    191502 |   44060   157289 |   34628   21369   836978    39.2 |  3.273 % |
c |    195346 |   44060   157289 |   38091   25213   996388    39.5 |  3.273 % |
c ==============================================================================
c [1mFound solution: 423988[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 878627   bits: 21/20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    200841 |   44067   157351 |   14689   30708  1247484    40.6 |  3.273 % |
c |    200941 |   44067   157351 |   16157   14363   512857    35.7 |  3.326 % |
c |    201092 |   44067   157351 |   17773   14514   514356    35.4 |  3.326 % |
c |    201321 |   44067   157351 |   19551   14743   519060    35.2 |  3.326 % |
c |    201659 |   44067   157351 |   21506   15081   529211    35.1 |  3.326 % |
c |    202165 |   44067   157351 |   23656   15587   539280    34.6 |  3.326 % |
c |    202924 |   44067   157351 |   26022   16346   561699    34.4 |  3.326 % |
c |    204063 |   44067   157351 |   28624   17485   587857    33.6 |  3.326 % |
c |    205771 |   44067   157351 |   31487   19193   640102    33.4 |  3.326 % |
c |    208334 |   44067   157351 |   34635   21756   708768    32.6 |  3.326 % |
c |    212178 |   44067   157351 |   38099   25600   904857    35.3 |  3.326 % |
c |    217944 |   44067   157351 |   41909   31366  1130671    36.0 |  3.326 % |
c |    226594 |   44067   157351 |   46100   40016  1847353    46.2 |  3.326 % |
c |    239568 |   44067   157351 |   50710   19765  1007280    51.0 |  3.326 % |
c ==============================================================================
c [1mFound solution: 423588[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 879027   bits: 21/20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    241573 |   44076   157451 |   14692   21770  1052056    48.3 |  3.326 % |
c |    241673 |   44076   157451 |   16161   10985   450938    41.1 |  3.395 % |
c |    241823 |   44076   157451 |   17777   11135   452162    40.6 |  3.395 % |
c |    242048 |   44076   157451 |   19555   11360   454485    40.0 |  3.395 % |
c |    242385 |   44076   157451 |   21510   11697   460353    39.4 |  3.395 % |
c |    242891 |   44076   157451 |   23661   12203   472355    38.7 |  3.395 % |
c |    243653 |   44076   157451 |   26027   12965   488582    37.7 |  3.395 % |
c |    244793 |   44076   157451 |   28630   14105   531048    37.6 |  3.395 % |
c |    246502 |   44076   157451 |   31493   15814   591619    37.4 |  3.395 % |
c |    249064 |   44076   157451 |   34642   18376   691318    37.6 |  3.395 % |
c |    252908 |   44076   157451 |   38107   22220   842012    37.9 |  3.395 % |
c |    258674 |   44076   157451 |   41917   27986  1189161    42.5 |  3.395 % |
c ==============================================================================
c [1mFound solution: 420872[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 881743   bits: 21/20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    266993 |   44081   157509 |   14693   36305  1679287    46.3 |  3.395 % |
c |    267093 |   44081   157509 |   16162   14483   703373    48.6 |  3.449 % |
c |    267243 |   44081   157509 |   17778   14633   706227    48.3 |  3.449 % |
c |    267468 |   44081   157509 |   19556   14858   710085    47.8 |  3.449 % |
c |    267806 |   44081   157509 |   21512   15196   719828    47.4 |  3.449 % |
c |    268312 |   44081   157509 |   23663   15702   728727    46.4 |  3.449 % |
c |    269071 |   44081   157509 |   26029   16461   742697    45.1 |  3.449 % |
c |    270214 |   44081   157509 |   28632   17604   770239    43.8 |  3.449 % |
c |    271923 |   44081   157509 |   31495   19313   837394    43.4 |  3.449 % |
c |    274486 |   44081   157509 |   34645   21876   955364    43.7 |  3.449 % |
c |    278330 |   44081   157509 |   38109   25720  1074152    41.8 |  3.449 % |
c |    284096 |   44081   157509 |   41920   31486  1413971    44.9 |  3.449 % |
c |    292747 |   44081   157509 |   46112   40137  2027122    50.5 |  3.449 % |
c |    305721 |   44081   157509 |   50724   20385  1125855    55.2 |  3.449 % |
c |    325184 |   44081   157509 |   55796   39848  1921718    48.2 |  3.449 % |
c |    354376 |   44081   157509 |   61376   25261  1965083    77.8 |  3.449 % |
c |    398166 |   44081   157509 |   67513   23312   949324    40.7 |  3.449 % |
c |    463850 |   44081   157509 |   74265   35145  3672852   104.5 |  3.449 % |
c ==============================================================================
c [1mFound solution: 419359[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 883256   bits: 21/20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    495971 |   44091   157616 |   14697   67266  6262844    93.1 |  3.449 % |
c |    496071 |   44091   157616 |   16166    7789   286020    36.7 |  3.529 % |
c |    496221 |   44091   157616 |   17783    7939   286976    36.1 |  3.529 % |
c |    496446 |   44091   157616 |   19561    8164   289013    35.4 |  3.529 % |
c |    496783 |   44091   157616 |   21517    8501   292292    34.4 |  3.529 % |
c |    497289 |   44091   157616 |   23669    9007   299722    33.3 |  3.529 % |
c |    498049 |   44091   157616 |   26036    9767   315837    32.3 |  3.529 % |
c |    499193 |   44091   157616 |   28640   10911   342383    31.4 |  3.529 % |
c |    500902 |   44091   157616 |   31504   12620   401810    31.8 |  3.529 % |
c |    503466 |   44091   157616 |   34654   15184   535017    35.2 |  3.529 % |
c |    507310 |   44091   157616 |   38120   19028   733279    38.5 |  3.529 % |
c |    513076 |   44091   157616 |   41932   24794  1087774    43.9 |  3.529 % |
c |    521726 |   44091   157616 |   46125   33444  1359557    40.7 |  3.529 % |
c |    534700 |   44091   157616 |   50738   46418  2128951    45.9 |  3.529 % |
c ==============================================================================
c [1mFound solution: 400558[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 902057   bits: 21/20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    551634 |   44105   157742 |   14701   26955  1310918    48.6 |  3.529 % |
c |    551734 |   44105   157742 |   16171   12906   680313    52.7 |  3.636 % |
c |    551884 |   44105   157742 |   17788   13056   681395    52.2 |  3.636 % |
c |    552110 |   44105   157742 |   19567   13282   683676    51.5 |  3.636 % |
c |    552448 |   44105   157742 |   21523   13620   688067    50.5 |  3.636 % |
c |    552954 |   44105   157742 |   23676   14126   695245    49.2 |  3.636 % |
c |    553713 |   44105   157742 |   26043   14885   708403    47.6 |  3.636 % |
c |    554852 |   44105   157742 |   28648   16024   739185    46.1 |  3.636 % |
c |    556560 |   44105   157742 |   31512   17732   810601    45.7 |  3.636 % |
c |    559123 |   44105   157742 |   34664   20295   891067    43.9 |  3.636 % |
c |    562969 |   44105   157742 |   38130   24141  1078799    44.7 |  3.636 % |
c |    568736 |   44105   157742 |   41943   29908  1401672    46.9 |  3.636 % |
c |    577385 |   44105   157742 |   46138   38557  1755814    45.5 |  3.636 % |
c |    590359 |   44105   157742 |   50751   17722  1304581    73.6 |  3.636 % |
c ==============================================================================
c [1mFound solution: 400552[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 902063   bits: 21/20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    596280 |   44107   157761 |   14702   23643  1639743    69.4 |  3.636 % |
c |    596380 |   44107   157761 |   16172   11922   759686    63.7 |  3.649 % |
c |    596530 |   44107   157761 |   17789   12072   761740    63.1 |  3.649 % |
c |    596755 |   44107   157761 |   19568   12297   766189    62.3 |  3.649 % |
c |    597093 |   44107   157761 |   21525   12635   769597    60.9 |  3.649 % |
c |    597599 |   44107   157761 |   23677   13141   779266    59.3 |  3.649 % |
c |    598358 |   44107   157761 |   26045   13900   798213    57.4 |  3.649 % |
c |    599497 |   44107   157761 |   28650   15039   819921    54.5 |  3.649 % |
c |    601205 |   44107   157761 |   31515   16747   861156    51.4 |  3.649 % |
c |    603767 |   44107   157761 |   34666   19309  1006094    52.1 |  3.649 % |
c |    607614 |   44107   157761 |   38133   23156  1229444    53.1 |  3.649 % |
c |    613380 |   44107   157761 |   41946   28922  1467188    50.7 |  3.649 % |
c |    622029 |   44107   157761 |   46141   37571  1745722    46.5 |  3.649 % |
c |    635005 |   44107   157761 |   50755   15986   842613    52.7 |  3.649 % |
c |    654469 |   44107   157761 |   55830   35450  1990931    56.2 |  3.649 % |
c |    683661 |   44107   157761 |   61413   21176  1289814    60.9 |  3.649 % |
c |    727450 |   44107   157761 |   67555   17370   812244    46.8 |  3.649 % |
c ==============================================================================
c [1mFound solution: 400545[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 902070   bits: 21/20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    758106 |   44116   157844 |   14705   48026  3409727    71.0 |  3.649 % |
c |    758207 |   44116   157844 |   16175   14788  1211145    81.9 |  3.689 % |
c |    758357 |   44116   157844 |   17793   14938  1212847    81.2 |  3.689 % |
c |    758582 |   44116   157844 |   19572   15163  1215427    80.2 |  3.689 % |
c |    758919 |   44116   157844 |   21529   15500  1219018    78.6 |  3.689 % |
c |    759426 |   44116   157844 |   23682   16007  1225623    76.6 |  3.689 % |
c |    760185 |   44116   157844 |   26050   16766  1238051    73.8 |  3.689 % |
c |    761327 |   44116   157844 |   28655   17908  1276581    71.3 |  3.689 % |
c |    763040 |   44116   157844 |   31521   19621  1334077    68.0 |  3.689 % |
c |    765602 |   44116   157844 |   34673   22183  1427366    64.3 |  3.689 % |
c |    769446 |   44116   157844 |   38140   26027  1568726    60.3 |  3.689 % |
c |    775212 |   44116   157844 |   41955   31793  2017974    63.5 |  3.689 % |
c |    783861 |   44116   157844 |   46150   40442  2388298    59.1 |  3.689 % |
c |    796836 |   44116   157844 |   50765   21038   923926    43.9 |  3.689 % |
c |    816297 |   44116   157844 |   55842   40499  2224951    54.9 |  3.689 % |
c |    845489 |   44116   157844 |   61426   26709  1524041    57.1 |  3.689 % |
c |    889278 |   44116   157844 |   67569   20958  1209785    57.7 |  3.689 % |
c |    954965 |   44116   157844 |   74325   33870  2294974    67.8 |  3.689 % |
c ==============================================================================
c [1mFound solution: 400544[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 902071   bits: 21/20
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    958755 |   44118   157865 |   14706   37660  2484804    66.0 |  3.689 % |
c |    958855 |   44118   157865 |   16176    8107   304431    37.6 |  3.702 % |
c |    959005 |   44118   157865 |   17794    8257   305937    37.1 |  3.702 % |
c |    959230 |   44118   157865 |   19573    8482   307906    36.3 |  3.702 % |
c |    959567 |   44118   157865 |   21531    8819   312077    35.4 |  3.702 % |
c |    960074 |   44118   157865 |   23684    9326   326001    35.0 |  3.702 % |
c |    960833 |   44118   157865 |   26052   10085   339354    33.6 |  3.702 % |
c |    961972 |   44118   157865 |   28657   11224   381255    34.0 |  3.702 % |
c |    963680 |   44118   157865 |   31523   12932   495253    38.3 |  3.702 % |
c |    966243 |   44118   157865 |   34675   15495   610073    39.4 |  3.702 % |
c |    970087 |   44118   157865 |   38143   19339   855510    44.2 |  3.702 % |
c |    975854 |   44118   157865 |   41957   25106  1134303    45.2 |  3.702 % |
c |    984503 |   44118   157865 |   46153   33755  1532699    45.4 |  3.702 % |
c |    997478 |   44118   157865 |   50769   46730  2208226    47.3 |  3.702 % |
c |   1016942 |   44118   157865 |   55846   29853  1326820    44.4 |  3.702 % |
c |   1046137 |   44118   157865 |   61430   14560   911721    62.6 |  3.702 % |
c |   1089927 |   44118   157865 |   67573   58350  4936560    84.6 |  3.702 % |
#### 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.99 1.00 0.93 2/54 8607
Raw data (stat): 8607 (runsolver) R 8606 29151 29150 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 487084683 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0009 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 2050 0 0 0 993 5 0 0 25 0 1 0 487084683 10227712 2027 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2497 2027 603 41 0 2456 0
vsize: 9988
[startup+20.0012 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 2598 0 0 0 1992 6 0 0 25 0 1 0 487084683 12484608 2575 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3048 2575 603 41 0 3007 0
vsize: 12192
[startup+30.0015 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 3505 0 0 0 2989 10 0 0 25 0 1 0 487084683 16236544 3482 4294967295 134512640 134672761 3221224544 3221223664 134542718 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3964 3482 603 41 0 3923 0
vsize: 15856
[startup+40.0024 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 3995 0 0 0 3987 11 0 0 25 0 1 0 487084683 18247680 3972 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4455 3972 603 41 0 4414 0
vsize: 17820
[startup+50.0027 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 3995 0 0 0 4987 12 0 0 25 0 1 0 487084683 18247680 3972 4294967295 134512640 134672761 3221224544 3221223712 134560845 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4455 3972 603 41 0 4414 0
vsize: 17820
[startup+60.004 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 3995 0 0 0 5987 12 0 0 25 0 1 0 487084683 18247680 3972 4294967295 134512640 134672761 3221224544 3221223728 134559330 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4455 3972 603 41 0 4414 0
vsize: 17820
[startup+70.0048 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 4339 0 0 0 6986 13 0 0 25 0 1 0 487084683 19582976 4316 4294967295 134512640 134672761 3221224544 3221223712 134560882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4781 4316 603 41 0 4740 0
vsize: 19124
[startup+80.0052 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 4693 0 0 0 7985 14 0 0 25 0 1 0 487084683 21061632 4670 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5142 4670 603 41 0 5101 0
vsize: 20568
[startup+90.0065 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 4693 0 0 0 8985 14 0 0 25 0 1 0 487084683 21061632 4670 4294967295 134512640 134672761 3221224544 3221223712 134559675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5142 4670 603 41 0 5101 0
vsize: 20568
[startup+100.007 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 4693 0 0 0 9985 15 0 0 25 0 1 0 487084683 21061632 4670 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5142 4670 603 41 0 5101 0
vsize: 20568
[startup+110.009 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 5255 0 0 0 10983 16 0 0 25 0 1 0 487084683 23351296 5232 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5701 5232 603 41 0 5660 0
vsize: 22804
[startup+120.01 s]
Raw data (loadavg): 0.99 1.00 0.93 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 6022 0 0 0 11981 18 0 0 25 0 1 0 487084683 26439680 5999 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6455 5999 603 41 0 6414 0
vsize: 25820
[startup+130.011 s]
Raw data (loadavg): 1.07 1.02 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 6176 0 0 0 12981 19 0 0 25 0 1 0 487084683 27111424 6153 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6619 6153 603 41 0 6578 0
vsize: 26476
[startup+140.011 s]
Raw data (loadavg): 1.14 1.03 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 6176 0 0 0 13981 19 0 0 25 0 1 0 487084683 27111424 6153 4294967295 134512640 134672761 3221224544 3221223648 134560477 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6619 6153 603 41 0 6578 0
vsize: 26476
[startup+150.012 s]
Raw data (loadavg): 1.11 1.03 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 6177 0 0 0 14981 19 0 0 25 0 1 0 487084683 27111424 6154 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6619 6154 603 41 0 6578 0
vsize: 26476
[startup+160.013 s]
Raw data (loadavg): 1.10 1.03 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 6178 0 0 0 15981 19 0 0 25 0 1 0 487084683 27111424 6155 4294967295 134512640 134672761 3221224544 3221223712 134560882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6619 6155 603 41 0 6578 0
vsize: 26476
[startup+170.014 s]
Raw data (loadavg): 1.08 1.03 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 6178 0 0 0 16981 19 0 0 25 0 1 0 487084683 27111424 6155 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6619 6155 603 41 0 6578 0
vsize: 26476
[startup+180.014 s]
Raw data (loadavg): 1.07 1.03 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 6178 0 0 0 17981 20 0 0 25 0 1 0 487084683 27111424 6155 4294967295 134512640 134672761 3221224544 3221223712 134561391 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6619 6155 603 41 0 6578 0
vsize: 26476
[startup+190.016 s]
Raw data (loadavg): 1.06 1.03 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 6178 0 0 0 18980 20 0 0 25 0 1 0 487084683 27111424 6155 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6619 6155 603 41 0 6578 0
vsize: 26476
[startup+200.016 s]
Raw data (loadavg): 1.05 1.02 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 6178 0 0 0 19980 21 0 0 25 0 1 0 487084683 27111424 6155 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6619 6155 603 41 0 6578 0
vsize: 26476
[startup+210.017 s]
Raw data (loadavg): 1.04 1.02 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 6179 0 0 0 20980 21 0 0 25 0 1 0 487084683 27111424 6156 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6619 6156 603 41 0 6578 0
vsize: 26476
[startup+220.018 s]
Raw data (loadavg): 1.03 1.02 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 6179 0 0 0 21980 21 0 0 25 0 1 0 487084683 27111424 6156 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6619 6156 603 41 0 6578 0
vsize: 26476
[startup+230.018 s]
Raw data (loadavg): 1.03 1.02 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 6179 0 0 0 22979 21 0 0 25 0 1 0 487084683 27111424 6156 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6619 6156 603 41 0 6578 0
vsize: 26476
[startup+240.019 s]
Raw data (loadavg): 1.02 1.02 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 6179 0 0 0 23980 22 0 0 25 0 1 0 487084683 27111424 6156 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6619 6156 603 41 0 6578 0
vsize: 26476
[startup+250.02 s]
Raw data (loadavg): 1.02 1.02 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 6179 0 0 0 24979 22 0 0 25 0 1 0 487084683 27111424 6156 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6619 6156 603 41 0 6578 0
vsize: 26476
[startup+260.021 s]
Raw data (loadavg): 1.02 1.02 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 6179 0 0 0 25979 23 0 0 25 0 1 0 487084683 27111424 6156 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6619 6156 603 41 0 6578 0
vsize: 26476
[startup+270.021 s]
Raw data (loadavg): 1.01 1.02 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 6179 0 0 0 26979 23 0 0 25 0 1 0 487084683 27111424 6156 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6619 6156 603 41 0 6578 0
vsize: 26476
[startup+280.021 s]
Raw data (loadavg): 1.01 1.02 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 6179 0 0 0 27978 24 0 0 25 0 1 0 487084683 27111424 6156 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6619 6156 603 41 0 6578 0
vsize: 26476
[startup+290.022 s]
Raw data (loadavg): 1.01 1.02 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 6179 0 0 0 28978 24 0 0 25 0 1 0 487084683 27111424 6156 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6619 6156 603 41 0 6578 0
vsize: 26476
[startup+300.023 s]
Raw data (loadavg): 1.01 1.01 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 6179 0 0 0 29978 24 0 0 25 0 1 0 487084683 27111424 6156 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6619 6156 603 41 0 6578 0
vsize: 26476
[startup+310.023 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 6179 0 0 0 30978 24 0 0 25 0 1 0 487084683 27111424 6156 4294967295 134512640 134672761 3221224544 3221223712 134561226 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6619 6156 603 41 0 6578 0
vsize: 26476
[startup+320.023 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 6180 0 0 0 31978 25 0 0 25 0 1 0 487084683 27111424 6157 4294967295 134512640 134672761 3221224544 3221223680 134560706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6619 6157 603 41 0 6578 0
vsize: 26476
[startup+330.024 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 6180 0 0 0 32977 25 0 0 25 0 1 0 487084683 27111424 6157 4294967295 134512640 134672761 3221224544 3221223728 134559161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6619 6157 603 41 0 6578 0
vsize: 26476
[startup+340.025 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 6180 0 0 0 33977 25 0 0 25 0 1 0 487084683 27111424 6157 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6619 6157 603 41 0 6578 0
vsize: 26476
[startup+350.025 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 6180 0 0 0 34977 26 0 0 25 0 1 0 487084683 27111424 6157 4294967295 134512640 134672761 3221224544 3221223728 134558899 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6619 6157 603 41 0 6578 0
vsize: 26476
[startup+360.027 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 6180 0 0 0 35977 26 0 0 25 0 1 0 487084683 27111424 6157 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6619 6157 603 41 0 6578 0
vsize: 26476
[startup+370.027 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 6204 0 0 0 36977 26 0 0 25 0 1 0 487084683 27246592 6181 4294967295 134512640 134672761 3221224544 3221223600 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6652 6181 603 41 0 6611 0
vsize: 26608
[startup+380.027 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 6741 0 0 0 37975 28 0 0 25 0 1 0 487084683 29401088 6718 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7178 6718 603 41 0 7137 0
vsize: 28712
[startup+390.028 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 7206 0 0 0 38974 29 0 0 25 0 1 0 487084683 31551488 7183 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7703 7183 603 41 0 7662 0
vsize: 30812
[startup+400.029 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 7776 0 0 0 39972 31 0 0 25 0 1 0 487084683 33845248 7753 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8263 7753 603 41 0 8222 0
vsize: 33052
[startup+410.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 7848 0 0 0 40972 32 0 0 25 0 1 0 487084683 34246656 7825 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8361 7825 603 41 0 8320 0
vsize: 33444
[startup+420.031 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 7848 0 0 0 41972 32 0 0 25 0 1 0 487084683 34246656 7825 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8361 7825 603 41 0 8320 0
vsize: 33444
[startup+430.031 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 7848 0 0 0 42972 32 0 0 25 0 1 0 487084683 34246656 7825 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8361 7825 603 41 0 8320 0
vsize: 33444
[startup+440.031 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 7848 0 0 0 43971 32 0 0 25 0 1 0 487084683 34246656 7825 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8361 7825 603 41 0 8320 0
vsize: 33444
[startup+450.031 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 7848 0 0 0 44971 33 0 0 25 0 1 0 487084683 34246656 7825 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8361 7825 603 41 0 8320 0
vsize: 33444
[startup+460.03 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 7848 0 0 0 45971 33 0 0 25 0 1 0 487084683 34246656 7825 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8361 7825 603 41 0 8320 0
vsize: 33444
[startup+470.032 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 8485 0 0 0 46969 35 0 0 25 0 1 0 487084683 36802560 8462 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8985 8462 603 41 0 8944 0
vsize: 35940
[startup+480.032 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 9028 0 0 0 47968 37 0 0 25 0 1 0 487084683 39079936 9005 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9541 9005 603 41 0 9500 0
vsize: 38164
[startup+490.032 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 9096 0 0 0 48967 37 0 0 25 0 1 0 487084683 39350272 9073 4294967295 134512640 134672761 3221224544 3221223680 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9607 9073 603 41 0 9566 0
vsize: 38428
[startup+500.033 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 9096 0 0 0 49967 38 0 0 25 0 1 0 487084683 39350272 9073 4294967295 134512640 134672761 3221224544 3221223648 134560299 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9607 9073 603 41 0 9566 0
vsize: 38428
[startup+510.033 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 9096 0 0 0 50967 38 0 0 25 0 1 0 487084683 39350272 9073 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9607 9073 603 41 0 9566 0
vsize: 38428
[startup+520.033 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 9096 0 0 0 51967 38 0 0 25 0 1 0 487084683 39350272 9073 4294967295 134512640 134672761 3221224544 3221223700 134559752 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9607 9073 603 41 0 9566 0
vsize: 38428
[startup+530.034 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 9097 0 0 0 52967 38 0 0 25 0 1 0 487084683 39350272 9074 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9607 9074 603 41 0 9566 0
vsize: 38428
[startup+540.035 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 9097 0 0 0 53967 39 0 0 25 0 1 0 487084683 39350272 9074 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9607 9074 603 41 0 9566 0
vsize: 38428
[startup+550.035 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 9097 0 0 0 54967 39 0 0 25 0 1 0 487084683 39350272 9074 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9607 9074 603 41 0 9566 0
vsize: 38428
[startup+560.035 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 9097 0 0 0 55966 39 0 0 25 0 1 0 487084683 39350272 9074 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9607 9074 603 41 0 9566 0
vsize: 38428
[startup+570.036 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 9097 0 0 0 56967 39 0 0 25 0 1 0 487084683 39350272 9074 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9607 9074 603 41 0 9566 0
vsize: 38428
[startup+580.035 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 9097 0 0 0 57966 40 0 0 25 0 1 0 487084683 39350272 9074 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9607 9074 603 41 0 9566 0
vsize: 38428
[startup+590.035 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 9097 0 0 0 58966 40 0 0 25 0 1 0 487084683 39350272 9074 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9607 9074 603 41 0 9566 0
vsize: 38428
[startup+600.036 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 9097 0 0 0 59966 41 0 0 25 0 1 0 487084683 39350272 9074 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9607 9074 603 41 0 9566 0
vsize: 38428
[startup+610.036 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 9097 0 0 0 60966 41 0 0 25 0 1 0 487084683 39350272 9074 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9607 9074 603 41 0 9566 0
vsize: 38428
[startup+620.036 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 9097 0 0 0 61965 41 0 0 25 0 1 0 487084683 39350272 9074 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9607 9074 603 41 0 9566 0
vsize: 38428
[startup+630.036 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 9097 0 0 0 62965 41 0 0 25 0 1 0 487084683 39350272 9074 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9607 9074 603 41 0 9566 0
vsize: 38428
[startup+640.036 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 9097 0 0 0 63965 42 0 0 25 0 1 0 487084683 39350272 9074 4294967295 134512640 134672761 3221224544 3221223680 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9607 9074 603 41 0 9566 0
vsize: 38428
[startup+650.037 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 9097 0 0 0 64965 42 0 0 25 0 1 0 487084683 39350272 9074 4294967295 134512640 134672761 3221224544 3221223712 134560833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9607 9074 603 41 0 9566 0
vsize: 38428
[startup+660.036 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 9097 0 0 0 65965 42 0 0 25 0 1 0 487084683 39350272 9074 4294967295 134512640 134672761 3221224544 3221223712 134560806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9607 9074 603 41 0 9566 0
vsize: 38428
[startup+670.037 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 9098 0 0 0 66965 43 0 0 25 0 1 0 487084683 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9607 9075 603 41 0 9566 0
vsize: 38428
[startup+680.038 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 9098 0 0 0 67964 43 0 0 25 0 1 0 487084683 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9607 9075 603 41 0 9566 0
vsize: 38428
[startup+690.038 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 9098 0 0 0 68965 43 0 0 25 0 1 0 487084683 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9607 9075 603 41 0 9566 0
vsize: 38428
[startup+700.039 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 9098 0 0 0 69964 43 0 0 25 0 1 0 487084683 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9607 9075 603 41 0 9566 0
vsize: 38428
[startup+710.038 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 9098 0 0 0 70964 44 0 0 25 0 1 0 487084683 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9607 9075 603 41 0 9566 0
vsize: 38428
[startup+720.039 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 9098 0 0 0 71964 44 0 0 25 0 1 0 487084683 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9607 9075 603 41 0 9566 0
vsize: 38428
[startup+730.039 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 9098 0 0 0 72964 44 0 0 25 0 1 0 487084683 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9607 9075 603 41 0 9566 0
vsize: 38428
[startup+740.04 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 9098 0 0 0 73964 45 0 0 25 0 1 0 487084683 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9607 9075 603 41 0 9566 0
vsize: 38428
[startup+750.04 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 9098 0 0 0 74964 45 0 0 25 0 1 0 487084683 39350272 9075 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9607 9075 603 41 0 9566 0
vsize: 38428
[startup+760.041 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 9098 0 0 0 75964 45 0 0 25 0 1 0 487084683 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9607 9075 603 41 0 9566 0
vsize: 38428
[startup+770.041 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 9098 0 0 0 76964 45 0 0 25 0 1 0 487084683 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9607 9075 603 41 0 9566 0
vsize: 38428
[startup+780.042 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 9098 0 0 0 77964 46 0 0 25 0 1 0 487084683 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9607 9075 603 41 0 9566 0
vsize: 38428
[startup+790.043 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 9098 0 0 0 78964 46 0 0 25 0 1 0 487084683 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9607 9075 603 41 0 9566 0
vsize: 38428
[startup+800.043 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 9098 0 0 0 79964 46 0 0 25 0 1 0 487084683 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134564448 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9607 9075 603 41 0 9566 0
vsize: 38428
[startup+810.042 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 9098 0 0 0 80964 46 0 0 25 0 1 0 487084683 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9607 9075 603 41 0 9566 0
vsize: 38428
[startup+820.043 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 9098 0 0 0 81964 46 0 0 25 0 1 0 487084683 39350272 9075 4294967295 134512640 134672761 3221224544 3221223728 134558883 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9607 9075 603 41 0 9566 0
vsize: 38428
[startup+830.043 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 9098 0 0 0 82964 46 0 0 25 0 1 0 487084683 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9607 9075 603 41 0 9566 0
vsize: 38428
[startup+840.044 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 9098 0 0 0 83964 46 0 0 25 0 1 0 487084683 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9607 9075 603 41 0 9566 0
vsize: 38428
[startup+850.045 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 9098 0 0 0 84964 46 0 0 25 0 1 0 487084683 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9607 9075 603 41 0 9566 0
vsize: 38428
[startup+860.045 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 9098 0 0 0 85965 46 0 0 25 0 1 0 487084683 39350272 9075 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9607 9075 603 41 0 9566 0
vsize: 38428
[startup+870.045 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 9098 0 0 0 86965 46 0 0 25 0 1 0 487084683 39350272 9075 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9607 9075 603 41 0 9566 0
vsize: 38428
[startup+880.045 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 9098 0 0 0 87965 46 0 0 25 0 1 0 487084683 39350272 9075 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9607 9075 603 41 0 9566 0
vsize: 38428
[startup+890.046 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 9098 0 0 0 88965 46 0 0 25 0 1 0 487084683 39350272 9075 4294967295 134512640 134672761 3221224544 3221223648 134554642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9607 9075 603 41 0 9566 0
vsize: 38428
[startup+900.046 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 9098 0 0 0 89965 46 0 0 25 0 1 0 487084683 39350272 9075 4294967295 134512640 134672761 3221224544 3221223728 134559516 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9607 9075 603 41 0 9566 0
vsize: 38428
[startup+910.045 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 9098 0 0 0 90966 46 0 0 25 0 1 0 487084683 39350272 9075 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9607 9075 603 41 0 9566 0
vsize: 38428
[startup+920.047 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 9098 0 0 0 91966 46 0 0 25 0 1 0 487084683 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9607 9075 603 41 0 9566 0
vsize: 38428
[startup+930.047 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 9098 0 0 0 92966 46 0 0 25 0 1 0 487084683 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9607 9075 603 41 0 9566 0
vsize: 38428
[startup+940.047 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 9098 0 0 0 93966 46 0 0 25 0 1 0 487084683 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9607 9075 603 41 0 9566 0
vsize: 38428
[startup+950.047 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 9098 0 0 0 94966 46 0 0 25 0 1 0 487084683 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9607 9075 603 41 0 9566 0
vsize: 38428
[startup+960.047 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 9098 0 0 0 95967 46 0 0 25 0 1 0 487084683 39350272 9075 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9607 9075 603 41 0 9566 0
vsize: 38428
[startup+970.047 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 9098 0 0 0 96967 46 0 0 25 0 1 0 487084683 39350272 9075 4294967295 134512640 134672761 3221224544 3221223648 134560057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9607 9075 603 41 0 9566 0
vsize: 38428
[startup+980.048 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 9098 0 0 0 97967 46 0 0 25 0 1 0 487084683 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9607 9075 603 41 0 9566 0
vsize: 38428
[startup+990.048 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 9098 0 0 0 98967 46 0 0 25 0 1 0 487084683 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9607 9075 603 41 0 9566 0
vsize: 38428
[startup+1000.05 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 9098 0 0 0 99967 46 0 0 25 0 1 0 487084683 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9607 9075 603 41 0 9566 0
vsize: 38428
[startup+1010.05 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 9098 0 0 0 100967 46 0 0 25 0 1 0 487084683 39350272 9075 4294967295 134512640 134672761 3221224544 3221223680 134560654 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9607 9075 603 41 0 9566 0
vsize: 38428
[startup+1020.05 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 9098 0 0 0 101968 46 0 0 25 0 1 0 487084683 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9607 9075 603 41 0 9566 0
vsize: 38428
[startup+1030.05 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 9098 0 0 0 102967 46 0 0 25 0 1 0 487084683 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9607 9075 603 41 0 9566 0
vsize: 38428
[startup+1040.05 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 9098 0 0 0 103968 46 0 0 25 0 1 0 487084683 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9607 9075 603 41 0 9566 0
vsize: 38428
[startup+1050.05 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 9098 0 0 0 104968 47 0 0 25 0 1 0 487084683 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560968 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9607 9075 603 41 0 9566 0
vsize: 38428
[startup+1060.05 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 9098 0 0 0 105968 47 0 0 25 0 1 0 487084683 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9607 9075 603 41 0 9566 0
vsize: 38428
[startup+1070.05 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 9098 0 0 0 106968 47 0 0 25 0 1 0 487084683 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9607 9075 603 41 0 9566 0
vsize: 38428
[startup+1080.05 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 9098 0 0 0 107968 47 0 0 25 0 1 0 487084683 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560994 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9607 9075 603 41 0 9566 0
vsize: 38428
[startup+1090.05 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 9098 0 0 0 108968 47 0 0 25 0 1 0 487084683 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9607 9075 603 41 0 9566 0
vsize: 38428
[startup+1100.05 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 9098 0 0 0 109968 47 0 0 25 0 1 0 487084683 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9607 9075 603 41 0 9566 0
vsize: 38428
[startup+1110.05 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 9098 0 0 0 110969 47 0 0 25 0 1 0 487084683 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9607 9075 603 41 0 9566 0
vsize: 38428
[startup+1120.05 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 9098 0 0 0 111969 47 0 0 25 0 1 0 487084683 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9607 9075 603 41 0 9566 0
vsize: 38428
[startup+1130.05 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 9098 0 0 0 112969 47 0 0 25 0 1 0 487084683 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9607 9075 603 41 0 9566 0
vsize: 38428
[startup+1140.05 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 9098 0 0 0 113969 47 0 0 25 0 1 0 487084683 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9607 9075 603 41 0 9566 0
vsize: 38428
[startup+1150.05 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 9098 0 0 0 114969 47 0 0 25 0 1 0 487084683 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9607 9075 603 41 0 9566 0
vsize: 38428
[startup+1160.05 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 9098 0 0 0 115970 47 0 0 25 0 1 0 487084683 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134561212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9607 9075 603 41 0 9566 0
vsize: 38428
[startup+1170.05 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 9098 0 0 0 116970 47 0 0 25 0 1 0 487084683 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9607 9075 603 41 0 9566 0
vsize: 38428
[startup+1180.05 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 9098 0 0 0 117970 47 0 0 25 0 1 0 487084683 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9607 9075 603 41 0 9566 0
vsize: 38428
[startup+1190.05 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 9098 0 0 0 118970 47 0 0 25 0 1 0 487084683 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9607 9075 603 41 0 9566 0
vsize: 38428
[startup+1200.05 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8607
Raw data (stat): 8607 (minisat+) R 8606 29151 29150 0 -1 0 9098 0 0 0 119970 47 0 0 25 0 1 0 487084683 39350272 9075 4294967295 134512640 134672761 3221224544 3221223728 134558851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9607 9075 603 41 0 9566 0
vsize: 38428
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 1.00 1.00 0.94 1/54 8607
Raw data (stat): 8607 (minisat+) Z 8606 29151 29150 0 -1 12 9101 0 0 0 119970 48 0 0 25 0 1 0 487084683 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.07
CPU time (s): 1200.2
CPU user time (s): 1199.71
CPU system time (s): 0.488925
CPU usage (%): 100.011
Max. virtual memory (Kb): 38428
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####