PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-p0282.opb
MD5SUM	a733e9fa1e4e3ac90baf85249f7c3e9a
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.01984
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 16963

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc2 THE 2005-04-21 09:13:07 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=12139 boxname=wulflinc2 idbench=934 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  a733e9fa1e4e3ac90baf85249f7c3e9a  /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-20-10-p0282.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-20-10-p0282.opb /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-20-10-p0282.opb
IDLAUNCH: 12139
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.191
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.191
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:        842620 kB
Buffers:          4684 kB
Cached:         166240 kB
SwapCached:        504 kB
Active:          27932 kB
Inactive:       145240 kB
HighTotal:      131008 kB
HighFree:        93184 kB
LowTotal:       903652 kB
LowFree:        749436 kB
SwapTotal:     2097136 kB
SwapFree:      2095900 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           5712 kB
Slab:            13088 kB
Committed_AS:    71784 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 09:33:09 (client local time) WITH STATUS 10 IN 1200.14 SECONDS
stats: 12139 7 1200.14 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.92 0.98 0.98 2/54 24711
Raw data (stat): 24711 (runsolver) R 24710 20937 20936 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 485689644 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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.0012 s]
Raw data (loadavg): 0.93 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 2033 0 0 0 992 6 0 0 25 0 1 0 485689644 10092544 2010 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2464 2010 603 41 0 2423 0
vsize: 9856
[startup+20.0013 s]
Raw data (loadavg): 0.94 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 2548 0 0 0 1991 7 0 0 25 0 1 0 485689644 12214272 2525 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2982 2525 603 41 0 2941 0
vsize: 11928
[startup+30.0016 s]
Raw data (loadavg): 0.95 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 3463 0 0 0 2988 10 0 0 25 0 1 0 485689644 16101376 3440 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3931 3440 603 41 0 3890 0
vsize: 15724
[startup+40.002 s]
Raw data (loadavg): 0.96 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 3995 0 0 0 3985 12 0 0 25 0 1 0 485689644 18247680 3972 4294967295 134512640 134672761 3221224544 3221223712 134560806 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.0024 s]
Raw data (loadavg): 0.96 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 3995 0 0 0 4986 12 0 0 25 0 1 0 485689644 18247680 3972 4294967295 134512640 134672761 3221224544 3221223712 134560858 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.0034 s]
Raw data (loadavg): 0.97 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 3995 0 0 0 5986 12 0 0 25 0 1 0 485689644 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+70.0041 s]
Raw data (loadavg): 0.97 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 4296 0 0 0 6985 13 0 0 25 0 1 0 485689644 19451904 4273 4294967295 134512640 134672761 3221224544 3221223728 134559392 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4749 4273 603 41 0 4708 0
vsize: 18996
[startup+80.0035 s]
Raw data (loadavg): 0.98 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 4693 0 0 0 7984 15 0 0 25 0 1 0 485689644 21061632 4670 4294967295 134512640 134672761 3221224544 3221223712 134560869 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.0036 s]
Raw data (loadavg): 0.98 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 4693 0 0 0 8984 15 0 0 25 0 1 0 485689644 21061632 4670 4294967295 134512640 134672761 3221224544 3221223728 134559356 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.003 s]
Raw data (loadavg): 0.98 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 4693 0 0 0 9984 15 0 0 25 0 1 0 485689644 21061632 4670 4294967295 134512640 134672761 3221224544 3221223648 134560174 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.004 s]
Raw data (loadavg): 0.98 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 5117 0 0 0 10983 16 0 0 25 0 1 0 485689644 22806528 5094 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5568 5094 603 41 0 5527 0
vsize: 22272
[startup+120.005 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 5883 0 0 0 11980 19 0 0 25 0 1 0 485689644 25903104 5860 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6324 5860 603 41 0 6283 0
vsize: 25296
[startup+130.005 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 6176 0 0 0 12979 20 0 0 25 0 1 0 485689644 27111424 6153 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6619 6153 603 41 0 6578 0
vsize: 26476
[startup+140.005 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 6176 0 0 0 13978 20 0 0 25 0 1 0 485689644 27111424 6153 4294967295 134512640 134672761 3221224544 3221223712 134561378 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6619 6153 603 41 0 6578 0
vsize: 26476
[startup+150.006 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 6177 0 0 0 14978 21 0 0 25 0 1 0 485689644 27111424 6154 4294967295 134512640 134672761 3221224544 3221223696 134561035 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6619 6154 603 41 0 6578 0
vsize: 26476
[startup+160.007 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 6178 0 0 0 15978 21 0 0 25 0 1 0 485689644 27111424 6155 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6619 6155 603 41 0 6578 0
vsize: 26476
[startup+170.007 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 6178 0 0 0 16977 22 0 0 25 0 1 0 485689644 27111424 6155 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6619 6155 603 41 0 6578 0
vsize: 26476
[startup+180.007 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 6178 0 0 0 17977 22 0 0 25 0 1 0 485689644 27111424 6155 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6619 6155 603 41 0 6578 0
vsize: 26476
[startup+190.008 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 6178 0 0 0 18977 22 0 0 25 0 1 0 485689644 27111424 6155 4294967295 134512640 134672761 3221224544 3221223728 134558941 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6619 6155 603 41 0 6578 0
vsize: 26476
[startup+200.008 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 6178 0 0 0 19976 23 0 0 25 0 1 0 485689644 27111424 6155 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6619 6155 603 41 0 6578 0
vsize: 26476
[startup+210.009 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 6178 0 0 0 20976 23 0 0 25 0 1 0 485689644 27111424 6155 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6619 6155 603 41 0 6578 0
vsize: 26476
[startup+220.01 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 6179 0 0 0 21976 24 0 0 25 0 1 0 485689644 27111424 6156 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6619 6156 603 41 0 6578 0
vsize: 26476
[startup+230.009 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 6179 0 0 0 22976 24 0 0 25 0 1 0 485689644 27111424 6156 4294967295 134512640 134672761 3221224544 3221223744 134557913 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6619 6156 603 41 0 6578 0
vsize: 26476
[startup+240.01 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 6179 0 0 0 23976 24 0 0 25 0 1 0 485689644 27111424 6156 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6619 6156 603 41 0 6578 0
vsize: 26476
[startup+250.011 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 6179 0 0 0 24976 24 0 0 25 0 1 0 485689644 27111424 6156 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6619 6156 603 41 0 6578 0
vsize: 26476
[startup+260.012 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 6179 0 0 0 25976 25 0 0 25 0 1 0 485689644 27111424 6156 4294967295 134512640 134672761 3221224544 3221223620 134553578 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6619 6156 603 41 0 6578 0
vsize: 26476
[startup+270.012 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 6179 0 0 0 26976 25 0 0 25 0 1 0 485689644 27111424 6156 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6619 6156 603 41 0 6578 0
vsize: 26476
[startup+280.012 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 6179 0 0 0 27975 25 0 0 25 0 1 0 485689644 27111424 6156 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6619 6156 603 41 0 6578 0
vsize: 26476
[startup+290.012 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 6179 0 0 0 28975 26 0 0 25 0 1 0 485689644 27111424 6156 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6619 6156 603 41 0 6578 0
vsize: 26476
[startup+300.013 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 6179 0 0 0 29975 26 0 0 25 0 1 0 485689644 27111424 6156 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6619 6156 603 41 0 6578 0
vsize: 26476
[startup+310.013 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 6179 0 0 0 30974 26 0 0 25 0 1 0 485689644 27111424 6156 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6619 6156 603 41 0 6578 0
vsize: 26476
[startup+320.014 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 6179 0 0 0 31974 27 0 0 25 0 1 0 485689644 27111424 6156 4294967295 134512640 134672761 3221224544 3221223712 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6619 6156 603 41 0 6578 0
vsize: 26476
[startup+330.015 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 6180 0 0 0 32974 27 0 0 25 0 1 0 485689644 27111424 6157 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6619 6157 603 41 0 6578 0
vsize: 26476
[startup+340.015 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 6180 0 0 0 33974 27 0 0 25 0 1 0 485689644 27111424 6157 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6619 6157 603 41 0 6578 0
vsize: 26476
[startup+350.016 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 6180 0 0 0 34974 28 0 0 25 0 1 0 485689644 27111424 6157 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6619 6157 603 41 0 6578 0
vsize: 26476
[startup+360.017 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 6180 0 0 0 35974 28 0 0 25 0 1 0 485689644 27111424 6157 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6619 6157 603 41 0 6578 0
vsize: 26476
[startup+370.017 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 6180 0 0 0 36973 28 0 0 25 0 1 0 485689644 27111424 6157 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6619 6157 603 41 0 6578 0
vsize: 26476
[startup+380.017 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 6283 0 0 0 37973 29 0 0 25 0 1 0 485689644 27516928 6260 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6718 6260 603 41 0 6677 0
vsize: 26872
[startup+390.018 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 6790 0 0 0 38971 31 0 0 25 0 1 0 485689644 29536256 6767 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7211 6767 603 41 0 7170 0
vsize: 28844
[startup+400.019 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 7230 0 0 0 39969 33 0 0 25 0 1 0 485689644 31686656 7207 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7736 7207 603 41 0 7695 0
vsize: 30944
[startup+410.019 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 7795 0 0 0 40968 34 0 0 25 0 1 0 485689644 33980416 7772 4294967295 134512640 134672761 3221224544 3221223728 134559327 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8296 7772 603 41 0 8255 0
vsize: 33184
[startup+420.019 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 7848 0 0 0 41967 35 0 0 25 0 1 0 485689644 34246656 7825 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8361 7825 603 41 0 8320 0
vsize: 33444
[startup+430.02 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 7848 0 0 0 42967 35 0 0 25 0 1 0 485689644 34246656 7825 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8361 7825 603 41 0 8320 0
vsize: 33444
[startup+440.02 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 7848 0 0 0 43967 35 0 0 25 0 1 0 485689644 34246656 7825 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8361 7825 603 41 0 8320 0
vsize: 33444
[startup+450.021 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 7848 0 0 0 44967 36 0 0 25 0 1 0 485689644 34246656 7825 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8361 7825 603 41 0 8320 0
vsize: 33444
[startup+460.022 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 7848 0 0 0 45967 36 0 0 25 0 1 0 485689644 34246656 7825 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8361 7825 603 41 0 8320 0
vsize: 33444
[startup+470.022 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 7848 0 0 0 46967 36 0 0 25 0 1 0 485689644 34246656 7825 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8361 7825 603 41 0 8320 0
vsize: 33444
[startup+480.022 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 8378 0 0 0 47965 38 0 0 25 0 1 0 485689644 36401152 8355 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8887 8355 603 41 0 8846 0
vsize: 35548
[startup+490.022 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 8928 0 0 0 48963 40 0 0 25 0 1 0 485689644 38674432 8905 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9442 8905 603 41 0 9401 0
vsize: 37768
[startup+500.024 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 9096 0 0 0 49962 41 0 0 25 0 1 0 485689644 39350272 9073 4294967295 134512640 134672761 3221224544 3221223696 134561035 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9607 9073 603 41 0 9566 0
vsize: 38428
[startup+510.024 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 9096 0 0 0 50962 41 0 0 25 0 1 0 485689644 39350272 9073 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9607 9073 603 41 0 9566 0
vsize: 38428
[startup+520.024 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 9096 0 0 0 51962 42 0 0 25 0 1 0 485689644 39350272 9073 4294967295 134512640 134672761 3221224544 3221223648 134560523 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9607 9073 603 41 0 9566 0
vsize: 38428
[startup+530.025 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 9096 0 0 0 52962 42 0 0 25 0 1 0 485689644 39350272 9073 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9607 9073 603 41 0 9566 0
vsize: 38428
[startup+540.025 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 9097 0 0 0 53961 42 0 0 25 0 1 0 485689644 39350272 9074 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9607 9074 603 41 0 9566 0
vsize: 38428
[startup+550.026 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 9097 0 0 0 54961 43 0 0 25 0 1 0 485689644 39350272 9074 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9607 9074 603 41 0 9566 0
vsize: 38428
[startup+560.027 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 9097 0 0 0 55960 43 0 0 25 0 1 0 485689644 39350272 9074 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9607 9074 603 41 0 9566 0
vsize: 38428
[startup+570.028 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 9097 0 0 0 56960 44 0 0 25 0 1 0 485689644 39350272 9074 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9607 9074 603 41 0 9566 0
vsize: 38428
[startup+580.028 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 9097 0 0 0 57960 44 0 0 25 0 1 0 485689644 39350272 9074 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9607 9074 603 41 0 9566 0
vsize: 38428
[startup+590.029 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 9097 0 0 0 58960 44 0 0 25 0 1 0 485689644 39350272 9074 4294967295 134512640 134672761 3221224544 3221223728 134559161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9607 9074 603 41 0 9566 0
vsize: 38428
[startup+600.029 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 9097 0 0 0 59959 45 0 0 25 0 1 0 485689644 39350272 9074 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9607 9074 603 41 0 9566 0
vsize: 38428
[startup+610.031 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 9097 0 0 0 60959 45 0 0 25 0 1 0 485689644 39350272 9074 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9607 9074 603 41 0 9566 0
vsize: 38428
[startup+620.031 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 9097 0 0 0 61959 45 0 0 25 0 1 0 485689644 39350272 9074 4294967295 134512640 134672761 3221224544 3221223712 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9607 9074 603 41 0 9566 0
vsize: 38428
[startup+630.032 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 9097 0 0 0 62959 45 0 0 25 0 1 0 485689644 39350272 9074 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9607 9074 603 41 0 9566 0
vsize: 38428
[startup+640.032 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 9097 0 0 0 63959 45 0 0 25 0 1 0 485689644 39350272 9074 4294967295 134512640 134672761 3221224544 3221223728 134558885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9607 9074 603 41 0 9566 0
vsize: 38428
[startup+650.032 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 9097 0 0 0 64959 46 0 0 25 0 1 0 485689644 39350272 9074 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9607 9074 603 41 0 9566 0
vsize: 38428
[startup+660.033 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 9097 0 0 0 65959 46 0 0 25 0 1 0 485689644 39350272 9074 4294967295 134512640 134672761 3221224544 3221223712 134560979 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9607 9074 603 41 0 9566 0
vsize: 38428
[startup+670.033 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 9097 0 0 0 66959 46 0 0 25 0 1 0 485689644 39350272 9074 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9607 9074 603 41 0 9566 0
vsize: 38428
[startup+680.033 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 9097 0 0 0 67959 46 0 0 25 0 1 0 485689644 39350272 9074 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9607 9074 603 41 0 9566 0
vsize: 38428
[startup+690.034 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 9098 0 0 0 68959 47 0 0 25 0 1 0 485689644 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+700.034 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 9098 0 0 0 69959 47 0 0 25 0 1 0 485689644 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9607 9075 603 41 0 9566 0
vsize: 38428
[startup+710.036 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 9098 0 0 0 70958 47 0 0 25 0 1 0 485689644 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+720.036 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 9098 0 0 0 71958 48 0 0 25 0 1 0 485689644 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+730.036 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 9098 0 0 0 72958 48 0 0 25 0 1 0 485689644 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134561161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9607 9075 603 41 0 9566 0
vsize: 38428
[startup+740.036 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 9098 0 0 0 73958 48 0 0 25 0 1 0 485689644 39350272 9075 4294967295 134512640 134672761 3221224544 3221223680 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9607 9075 603 41 0 9566 0
vsize: 38428
[startup+750.037 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 9098 0 0 0 74958 48 0 0 25 0 1 0 485689644 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+760.038 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 9098 0 0 0 75958 48 0 0 25 0 1 0 485689644 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+770.038 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 9098 0 0 0 76958 49 0 0 25 0 1 0 485689644 39350272 9075 4294967295 134512640 134672761 3221224544 3221223648 134560198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9607 9075 603 41 0 9566 0
vsize: 38428
[startup+780.038 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 9098 0 0 0 77957 49 0 0 25 0 1 0 485689644 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+790.039 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 9098 0 0 0 78957 49 0 0 25 0 1 0 485689644 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9607 9075 603 41 0 9566 0
vsize: 38428
[startup+800.039 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 9098 0 0 0 79957 49 0 0 25 0 1 0 485689644 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+810.04 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 9098 0 0 0 80957 49 0 0 25 0 1 0 485689644 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.041 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 9098 0 0 0 81957 49 0 0 25 0 1 0 485689644 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+830.04 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 9098 0 0 0 82957 50 0 0 25 0 1 0 485689644 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.041 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 9098 0 0 0 83957 50 0 0 25 0 1 0 485689644 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.042 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 9098 0 0 0 84957 50 0 0 25 0 1 0 485689644 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.043 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 9098 0 0 0 85957 50 0 0 25 0 1 0 485689644 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+870.043 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 9098 0 0 0 86957 50 0 0 25 0 1 0 485689644 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+880.043 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 9098 0 0 0 87957 51 0 0 25 0 1 0 485689644 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+890.043 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 9098 0 0 0 88956 51 0 0 25 0 1 0 485689644 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+900.043 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 9098 0 0 0 89957 51 0 0 25 0 1 0 485689644 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134561205 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.044 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 9098 0 0 0 90956 52 0 0 25 0 1 0 485689644 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134561008 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.045 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 9098 0 0 0 91956 52 0 0 25 0 1 0 485689644 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560929 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.045 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 9098 0 0 0 92956 52 0 0 25 0 1 0 485689644 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.045 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 9098 0 0 0 93956 52 0 0 25 0 1 0 485689644 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560895 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.045 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 9098 0 0 0 94956 52 0 0 25 0 1 0 485689644 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+960.047 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 9098 0 0 0 95956 53 0 0 25 0 1 0 485689644 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560882 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): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 9098 0 0 0 96956 53 0 0 25 0 1 0 485689644 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+980.047 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 9098 0 0 0 97956 53 0 0 25 0 1 0 485689644 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+990.048 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 9098 0 0 0 98956 53 0 0 25 0 1 0 485689644 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+1000.05 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 9098 0 0 0 99955 53 0 0 25 0 1 0 485689644 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): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 9098 0 0 0 100955 54 0 0 25 0 1 0 485689644 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560903 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): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 9098 0 0 0 101955 54 0 0 25 0 1 0 485689644 39350272 9075 4294967295 134512640 134672761 3221224544 3221223648 134560218 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): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 9098 0 0 0 102955 54 0 0 25 0 1 0 485689644 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134560882 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): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 9098 0 0 0 103955 54 0 0 25 0 1 0 485689644 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+1050.05 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 9098 0 0 0 104955 55 0 0 25 0 1 0 485689644 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+1060.05 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 9098 0 0 0 105954 55 0 0 25 0 1 0 485689644 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): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 9098 0 0 0 106954 56 0 0 25 0 1 0 485689644 39350272 9075 4294967295 134512640 134672761 3221224544 3221223648 134560350 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): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 9098 0 0 0 107954 56 0 0 25 0 1 0 485689644 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134561008 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): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 9098 0 0 0 108954 56 0 0 25 0 1 0 485689644 39350272 9075 4294967295 134512640 134672761 3221224544 3221223648 134554910 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): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 9098 0 0 0 109954 56 0 0 25 0 1 0 485689644 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+1110.06 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 9098 0 0 0 110954 57 0 0 25 0 1 0 485689644 39350272 9075 4294967295 134512640 134672761 3221224544 3221223648 134560504 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.06 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 9098 0 0 0 111954 57 0 0 25 0 1 0 485689644 39350272 9075 4294967295 134512640 134672761 3221224544 3221223712 134561164 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.06 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 9098 0 0 0 112954 57 0 0 25 0 1 0 485689644 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.06 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 9098 0 0 0 113953 57 0 0 25 0 1 0 485689644 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+1150.06 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 9098 0 0 0 114953 57 0 0 25 0 1 0 485689644 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+1160.06 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 9098 0 0 0 115954 57 0 0 25 0 1 0 485689644 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+1170.06 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 9098 0 0 0 116953 58 0 0 25 0 1 0 485689644 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.06 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 9098 0 0 0 117953 59 0 0 25 0 1 0 485689644 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+1190.06 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 9098 0 0 0 118953 59 0 0 25 0 1 0 485689644 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.06 s]
Raw data (loadavg): 0.99 0.98 0.98 2/54 24711
Raw data (stat): 24711 (minisat+) R 24710 20937 20936 0 -1 0 9098 0 0 0 119952 59 0 0 25 0 1 0 485689644 39350272 9075 4294967295 134512640 134672761 3221224544 3221223680 134560688 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.08 s]
Raw data (loadavg): 0.99 0.98 0.98 1/54 24711
Raw data (stat): 24711 (minisat+) Z 24710 20937 20936 0 -1 12 9101 0 0 0 119952 61 0 0 25 0 1 0 485689644 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.08
CPU time (s): 1200.14
CPU user time (s): 1199.53
CPU system time (s): 0.612906
CPU usage (%): 100.005
Max. virtual memory (Kb): 38428
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####