PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-misc07.opb
MD5SUM	9cc94d1db4d494288ef67a8d5ad5d77e
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	1408128
Optimality of the best value was proved	NO
Number of terms in the objective function	21
Biggest coefficient in the objective function	1048576
Number of bits for the biggest coefficient in the objective function	21
Sum of the numbers in the objective function	2097151
Number of bits of the sum of numbers in the objective function	21
Biggest number in a constraint	1048576
Number of bits of the biggest number in a constraint	21
Biggest sum of numbers in a constraint	11486079
Number of bits of the biggest sum of numbers	24
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1189.01
Number of variables	280
Total number of constraints	471
Number of constraints which are clauses	127
Number of constraints which are cardinality constraints (but not clauses)	272
Number of constraints which are nor clauses,nor cardinality constraints	72
Minimum length of a constraint	1
Maximum length of a constraint	253
Trace number 19122

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc27 THE 2005-04-21 18:00:57 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=17017 boxname=wulflinc27 idbench=1309 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  9cc94d1db4d494288ef67a8d5ad5d77e  /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-13-7-misc07.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-13-7-misc07.opb /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-13-7-misc07.opb
IDLAUNCH: 17017
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.169
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	: 3
cpu MHz		: 451.169
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:        786156 kB
Buffers:         14048 kB
Cached:         210928 kB
SwapCached:        512 kB
Active:          26228 kB
Inactive:       200720 kB
HighTotal:      131008 kB
HighFree:         9352 kB
LowTotal:       903652 kB
LowFree:        776804 kB
SwapTotal:     2097892 kB
SwapFree:      2096468 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           5092 kB
Slab:            15856 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 18:20:59 (client local time) WITH STATUS 10 IN 1200.19 SECONDS
stats: 17017 7 1200.19 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 247 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ###################################
c   -- Clauses(.)/Splits(s): ...............................................................................................................................
c ---[ 245]---> Adder-cost: 1695   maxlim: 1048703   bits: 22/21
c ---[ 243]---> BDD-cost:   51
c ---[ 241]---> BDD-cost:   51
c ---[ 239]---> BDD-cost:   51
c ---[ 237]---> BDD-cost:   51
c ---[ 235]---> BDD-cost:   51
c ---[ 233]---> BDD-cost:   51
c ---[ 231]---> BDD-cost:   51
c ---[ 230]---> BDD-cost:  239
c ---[ 229]---> BDD-cost:  239
c ---[ 228]---> BDD-cost:  239
c ---[  99]---> Sorter-cost:  127     Base:
c ---[  97]---> Sorter-cost:  127     Base:
c ---[  95]---> Sorter-cost:  127     Base:
c ---[  93]---> Sorter-cost:  127     Base:
c ---[  91]---> Sorter-cost:  127     Base:
c ---[  89]---> Sorter-cost:  127     Base:
c ---[  87]---> Sorter-cost:  127     Base:
c ---[  85]---> Sorter-cost:  127     Base:
c ---[  83]---> Sorter-cost:  127     Base:
c ---[  81]---> Sorter-cost:  127     Base:
c ---[  79]---> Sorter-cost:  127     Base:
c ---[  77]---> Sorter-cost:  127     Base:
c ---[  75]---> Sorter-cost:  127     Base:
c ---[  73]---> Sorter-cost:  127     Base:
c ---[  71]---> Sorter-cost:  127     Base:
c ---[  69]---> Sorter-cost:  127     Base:
c ---[  67]---> Sorter-cost:  127     Base:
c ---[  65]---> Sorter-cost:  127     Base:
c ---[  63]---> Sorter-cost:  127     Base:
c ---[  61]---> Sorter-cost:  127     Base:
c ---[  59]---> Sorter-cost:  127     Base:
c ---[  57]---> Sorter-cost:  127     Base:
c ---[  55]---> Sorter-cost:  127     Base:
c ---[  53]---> Sorter-cost:  127     Base:
c ---[  51]---> Sorter-cost:  127     Base:
c ---[  49]---> Sorter-cost:  127     Base:
c ---[  47]---> Sorter-cost:  127     Base:
c ---[  46]---> BDD-cost:   23
c ---[  45]---> BDD-cost:   23
c ---[  44]---> BDD-cost:   23
c ---[  43]---> BDD-cost:    7
c ---[  42]---> BDD-cost:    7
c ---[  41]---> BDD-cost:   27
c ---[  40]---> BDD-cost:   27
c ---[  39]---> BDD-cost:   27
c ---[  38]---> BDD-cost:   27
c ---[  37]---> BDD-cost:   27
c ---[  36]---> BDD-cost:   27
c ---[  35]---> BDD-cost:   50
c ---[  34]---> BDD-cost:   50
c ---[  33]---> BDD-cost:   50
c ---[  32]---> BDD-cost:   27
c ---[  31]---> BDD-cost:   27
c ---[  30]---> BDD-cost:   27
c ---[  29]---> BDD-cost:   48
c ---[  28]---> BDD-cost:   48
c ---[  27]---> BDD-cost:   48
c ---[  26]---> BDD-cost:   27
c ---[  25]---> BDD-cost:   27
c ---[  24]---> BDD-cost:   27
c ---[  23]---> BDD-cost:   50
c ---[  22]---> BDD-cost:   50
c ---[  21]---> BDD-cost:   50
c ---[  20]---> BDD-cost:   27
c ---[  19]---> BDD-cost:   27
c ---[  18]---> BDD-cost:   27
c ---[  17]---> BDD-cost:   48
c ---[  16]---> BDD-cost:   48
c ---[  15]---> BDD-cost:   48
c ---[  14]---> BDD-cost:   27
c ---[  13]---> BDD-cost:   27
c ---[  12]---> BDD-cost:   27
c ---[  11]---> BDD-cost:   50
c ---[  10]---> BDD-cost:   50
c ---[   9]---> BDD-cost:   50
c ---[   8]---> BDD-cost:   27
c ---[   7]---> BDD-cost:   27
c ---[   6]---> BDD-cost:   27
c ---[   5]---> BDD-cost:   48
c ---[   4]---> BDD-cost:   48
c ---[   3]---> BDD-cost:   48
c ---[   2]---> BDD-cost:   27
c ---[   1]---> BDD-cost:   27
c ---[   0]---> BDD-cost:   27
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   31883   102562 |   10627       0        0     nan |  0.000 % |
c |       101 |   31878   102547 |   11689      94     1234    13.1 |  2.691 % |
c ==============================================================================
c [1mFound solution: 1584768[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       147 |   31900   102604 |   10633     140     2787    19.9 |  2.691 % |
c |       247 |   31900   102604 |   11696     240     5379    22.4 |  2.703 % |
c |       397 |   31886   102568 |   12865     389     8513    21.9 |  2.746 % |
c ==============================================================================
c [1mFound solution: 1549568[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       449 |   31901   102608 |   10633     440     9803    22.3 |  2.746 % |
c |       550 |   31901   102608 |   11696     541    14876    27.5 |  2.801 % |
c |       702 |   31901   102608 |   12865     693    25057    36.2 |  2.801 % |
c ==============================================================================
c [1mFound solution: 1548928[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       785 |   31897   102606 |   10632     774    25868    33.4 |  2.801 % |
c |       885 |   31897   102606 |   11695     874    39547    45.2 |  2.928 % |
c |      1035 |   31879   102561 |   12864    1020    40842    40.0 |  2.986 % |
c |      1262 |   31838   102470 |   14151    1242    64042    51.6 |  3.159 % |
c |      1599 |   31713   102156 |   15566    1562    76214    48.8 |  3.621 % |
c |      2106 |   31713   102156 |   17122    2069   137467    66.4 |  3.620 % |
c |      2866 |   31713   102156 |   18835    2829   192760    68.1 |  3.620 % |
c ==============================================================================
c [1mFound solution: 1539968[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3731 |   31734   102211 |   10578    3694   264070    71.5 |  3.620 % |
c |      3832 |   31734   102211 |   11635    3795   265017    69.8 |  3.632 % |
c |      3982 |   31734   102211 |   12799    3945   269841    68.4 |  3.632 % |
c |      4208 |   31723   102187 |   14079    4169   287123    68.9 |  3.675 % |
c |      4547 |   31667   102062 |   15487    4483   316090    70.5 |  3.920 % |
c |      5055 |   31643   101978 |   17035    4985   326816    65.6 |  3.949 % |
c ==============================================================================
c [1mFound solution: 1534208[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5130 |   31668   102039 |   10556    5060   332463    65.7 |  3.949 % |
c |      5230 |   31668   102039 |   11611    5160   334136    64.8 |  3.959 % |
c |      5382 |   31668   102039 |   12772    5312   349661    65.8 |  3.959 % |
c |      5607 |   31663   102024 |   14050    5534   369608    66.8 |  3.974 % |
c ==============================================================================
c [1mFound solution: 1524608[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5726 |   31688   102087 |   10562    5653   383232    67.8 |  3.974 % |
c |      5826 |   31688   102087 |   11618    5753   384170    66.8 |  3.984 % |
c |      5976 |   31677   102063 |   12780    5901   387603    65.7 |  4.027 % |
c ==============================================================================
c [1mFound solution: 1518848[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6078 |   31699   102117 |   10566    6003   389713    64.9 |  4.027 % |
c |      6178 |   31699   102117 |   11622    6103   402553    66.0 |  4.037 % |
c |      6330 |   31699   102117 |   12784    6255   405201    64.8 |  4.037 % |
c |      6555 |   31699   102117 |   14063    6480   426150    65.8 |  4.037 % |
c |      6895 |   31656   101968 |   15469    6812   459916    67.5 |  4.080 % |
c |      7401 |   31640   101929 |   17016    7316   506490    69.2 |  4.138 % |
c |      8160 |   31640   101929 |   18718    8075   572320    70.9 |  4.138 % |
c ==============================================================================
c [1mFound solution: 1517568[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9071 |   31652   101961 |   10550    8985   664695    74.0 |  4.138 % |
c |      9171 |   31652   101961 |   11605    9085   666938    73.4 |  4.177 % |
c |      9322 |   31652   101961 |   12765    9236   686356    74.3 |  4.177 % |
c |      9548 |   31641   101937 |   14042    9461   696613    73.6 |  4.221 % |
c |      9886 |   31641   101937 |   15446    9799   734384    74.9 |  4.221 % |
c |     10392 |   31611   101870 |   16990   10301   781995    75.9 |  4.350 % |
c |     11151 |   31611   101870 |   18689   11060   858090    77.6 |  4.350 % |
c ==============================================================================
c [1mFound solution: 1509888[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11735 |   31632   101923 |   10544   11644   936880    80.5 |  4.350 % |
c |     11836 |   31632   101923 |   11598    5923   443128    74.8 |  4.360 % |
c |     11986 |   31632   101923 |   12758    6073   456585    75.2 |  4.360 % |
c |     12212 |   31632   101923 |   14034    6299   491256    78.0 |  4.360 % |
c |     12549 |   31632   101923 |   15437    6636   503437    75.9 |  4.360 % |
c |     13055 |   31632   101923 |   16981    7142   583352    81.7 |  4.360 % |
c |     13816 |   31605   101826 |   18679    7900   658907    83.4 |  4.375 % |
c ==============================================================================
c [1mFound solution: 1462528[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     13891 |   31629   101884 |   10543    7975   665132    83.4 |  4.375 % |
c |     13992 |   31594   101803 |   11597    8072   675547    83.7 |  4.513 % |
c |     14143 |   31594   101803 |   12757    8223   678501    82.5 |  4.513 % |
c |     14370 |   31594   101803 |   14032    8450   700849    82.9 |  4.513 % |
c |     14707 |   31594   101803 |   15436    8787   737874    84.0 |  4.513 % |
c |     15213 |   31594   101803 |   16979    9293   810649    87.2 |  4.513 % |
c |     15974 |   31568   101734 |   18677   10048   902841    89.9 |  4.570 % |
c |     17115 |   31479   101485 |   20545   11176  1000404    89.5 |  4.828 % |
c |     18823 |   31461   101440 |   22599   12865  1179286    91.7 |  4.885 % |
c ==============================================================================
c [1mFound solution: 1459328[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20846 |   31466   101450 |   10488   14878  1319253    88.7 |  4.885 % |
c |     20947 |   31466   101450 |   11536    7540   475839    63.1 |  4.966 % |
c |     21098 |   31466   101450 |   12690    7691   494129    64.2 |  4.966 % |
c |     21323 |   31466   101450 |   13959    7916   502860    63.5 |  4.966 % |
c |     21665 |   31466   101450 |   15355    8258   524942    63.6 |  4.966 % |
c |     22172 |   31466   101450 |   16891    8765   605766    69.1 |  4.966 % |
c |     22931 |   31445   101403 |   18580    9522   697081    73.2 |  5.052 % |
c |     24073 |   31427   101364 |   20438   10662   798004    74.8 |  5.123 % |
c |     25782 |   31427   101364 |   22481   12371  1035789    83.7 |  5.123 % |
c ==============================================================================
c [1mFound solution: 1435008[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27602 |   31434   101367 |   10478   14188  1191101    84.0 |  5.123 % |
c |     27706 |   31434   101367 |   11525    7198   525874    73.1 |  5.174 % |
c |     27857 |   31434   101367 |   12678    7349   535217    72.8 |  5.174 % |
c |     28082 |   31434   101367 |   13946    7574   563543    74.4 |  5.174 % |
c |     28420 |   31405   101303 |   15340    7907   587243    74.3 |  5.302 % |
c |     28927 |   31405   101303 |   16874    8414   653045    77.6 |  5.302 % |
c |     29687 |   31405   101303 |   18562    9174   714479    77.9 |  5.302 % |
c |     30826 |   31380   101242 |   20418   10307   854322    82.9 |  5.417 % |
c |     32534 |   31353   101147 |   22460   12012  1062524    88.5 |  5.446 % |
c |     35097 |   31353   101147 |   24706   14575  1401051    96.1 |  5.445 % |
c ==============================================================================
c [1mFound solution: 1424768[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     38417 |   31375   101201 |   10458   17895  1877121   104.9 |  5.445 % |
c |     38518 |   31375   101201 |   11503    9049   861399    95.2 |  5.454 % |
c |     38672 |   31364   101177 |   12654    9200   886480    96.4 |  5.497 % |
c |     38898 |   31343   101102 |   13919    9422   912731    96.9 |  5.511 % |
c |     39239 |   31343   101102 |   15311    9763   926282    94.9 |  5.511 % |
c |     39745 |   31343   101102 |   16842   10269   998183    97.2 |  5.511 % |
c |     40504 |   31291   100937 |   18526   11020  1090759    99.0 |  5.611 % |
c |     41644 |   31291   100937 |   20379   12160  1204458    99.1 |  5.611 % |
c |     43352 |   31291   100937 |   22417   13868  1428447   103.0 |  5.611 % |
c |     45915 |   31286   100922 |   24659   16425  1616181    98.4 |  5.625 % |
c |     49759 |   31268   100863 |   27125   20265  1973613    97.4 |  5.654 % |
c |     55527 |   31263   100848 |   29837   26030  2815258   108.2 |  5.668 % |
c |     64177 |   31202   100673 |   32821   18908  1944788   102.9 |  5.825 % |
c ==============================================================================
c [1mFound solution: 1419008[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     67181 |   31230   100741 |   10410   21912  2405516   109.8 |  5.825 % |
c |     67284 |   31203   100644 |   11451    5578   422494    75.7 |  5.846 % |
c |     67435 |   31203   100644 |   12596    5729   447484    78.1 |  5.846 % |
c |     67663 |   31181   100591 |   13855    5954   457168    76.8 |  5.932 % |
c |     68001 |   31181   100591 |   15241    6292   519450    82.6 |  5.932 % |
c |     68508 |   31181   100591 |   16765    6799   568748    83.7 |  5.932 % |
c |     69272 |   31100   100306 |   18441    7549   638121    84.5 |  6.017 % |
c |     70412 |   31100   100306 |   20286    8689   731156    84.1 |  6.017 % |
c |     72122 |   31100   100306 |   22314   10399   969149    93.2 |  6.017 % |
c |     74686 |   31063   100224 |   24546   12955  1268954    98.0 |  6.174 % |
c |     78530 |   31052   100200 |   27000   16797  1605700    95.6 |  6.217 % |
c |     84297 |   30861    99720 |   29700   22542  2247613    99.7 |  6.930 % |
c |     92947 |   30784    99505 |   32671   31175  3241750   104.0 |  7.158 % |
c |    105921 |   30635    98984 |   35938   24584  2712666   110.3 |  7.358 % |
c |    125383 |   30535    98701 |   39531   23565  2441955   103.6 |  7.629 % |
c |    154579 |   30491    98601 |   43485   27859  3077771   110.5 |  7.786 % |
c ==============================================================================
c [1mFound solution: 1408128[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    181498 |   30474    98559 |   10158   27308  2501698    91.6 |  7.786 % |
c |    181599 |   30474    98559 |   11173    6928   259313    37.4 |  7.963 % |
c |    181749 |   30474    98559 |   12291    7078   282906    40.0 |  7.963 % |
c |    181974 |   30474    98559 |   13520    7303   308135    42.2 |  7.963 % |
c |    182313 |   30474    98559 |   14872    7642   353208    46.2 |  7.963 % |
c |    182825 |   30474    98559 |   16359    8154   420914    51.6 |  7.963 % |
c |    183589 |   30474    98559 |   17995    8918   518007    58.1 |  7.963 % |
c |    184728 |   30474    98559 |   19795   10057   662739    65.9 |  7.963 % |
c |    186437 |   30474    98559 |   21774   11766   873251    74.2 |  7.963 % |
c |    188999 |   30463    98526 |   23952   14327  1242894    86.8 |  7.991 % |
c |    192844 |   30463    98526 |   26347   18172  1737435    95.6 |  7.991 % |
c |    198610 |   30463    98526 |   28981   23938  2530725   105.7 |  7.991 % |
c |    207260 |   30357    98178 |   31880   17155  1579892    92.1 |  8.219 % |
c |    220239 |   30251    97839 |   35068   30111  3210953   106.6 |  8.433 % |
c |    239703 |   30251    97839 |   38574   26455  2695906   101.9 |  8.433 % |
c |    268895 |   30251    97839 |   42432   30474  3344315   109.7 |  8.433 % |
c |    312686 |   30220    97756 |   46675   22390  1823582    81.4 |  8.519 % |
#### 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.74 0.91 0.89 2/54 23074
Raw data (stat): 23074 (runsolver) R 23073 18865 18864 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 547073540 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.0014 s]
Raw data (loadavg): 0.78 0.91 0.89 2/54 23074
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 1760 0 0 0 994 5 0 0 25 0 1 0 547073540 8568832 1691 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2092 1691 603 41 0 2051 0
vsize: 8368
[startup+20.0023 s]
Raw data (loadavg): 0.81 0.91 0.89 2/54 23076
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 2319 0 0 0 1991 7 0 0 25 0 1 0 547073540 10862592 2250 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2652 2250 603 41 0 2611 0
vsize: 10608
[startup+30.0025 s]
Raw data (loadavg): 0.84 0.92 0.89 2/54 23076
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 2564 0 0 0 2991 8 0 0 25 0 1 0 547073540 11923456 2495 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2911 2495 603 41 0 2870 0
vsize: 11644
[startup+40.0026 s]
Raw data (loadavg): 0.86 0.92 0.89 2/54 23076
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 2746 0 0 0 3990 8 0 0 25 0 1 0 547073540 12595200 2677 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3075 2677 603 41 0 3034 0
vsize: 12300
[startup+50.0034 s]
Raw data (loadavg): 0.88 0.92 0.89 2/54 23076
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 2746 0 0 0 4990 9 0 0 25 0 1 0 547073540 12595200 2677 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3075 2677 603 41 0 3034 0
vsize: 12300
[startup+60.0039 s]
Raw data (loadavg): 0.90 0.92 0.90 2/54 23076
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 2746 0 0 0 5990 9 0 0 25 0 1 0 547073540 12595200 2677 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3075 2677 603 41 0 3034 0
vsize: 12300
[startup+70.0041 s]
Raw data (loadavg): 0.92 0.92 0.90 2/54 23076
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 3223 0 0 0 6989 10 0 0 25 0 1 0 547073540 14639104 3154 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3574 3154 603 41 0 3533 0
vsize: 14296
[startup+80.0039 s]
Raw data (loadavg): 0.93 0.93 0.90 2/54 23076
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 3395 0 0 0 7988 11 0 0 25 0 1 0 547073540 15310848 3326 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3738 3326 603 41 0 3697 0
vsize: 14952
[startup+90.0045 s]
Raw data (loadavg): 0.94 0.93 0.90 2/54 23076
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 3395 0 0 0 8989 11 0 0 25 0 1 0 547073540 15310848 3326 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3738 3326 603 41 0 3697 0
vsize: 14952
[startup+100.005 s]
Raw data (loadavg): 0.95 0.93 0.90 2/54 23076
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 3752 0 0 0 9987 12 0 0 25 0 1 0 547073540 16764928 3683 4294967295 134512640 134672761 3221224544 3221223560 1075353072 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4093 3683 603 41 0 4052 0
vsize: 16372
[startup+110.005 s]
Raw data (loadavg): 0.96 0.93 0.90 2/54 23076
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 4439 0 0 0 10985 15 0 0 25 0 1 0 547073540 19587072 4370 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4782 4370 603 41 0 4741 0
vsize: 19128
[startup+120.005 s]
Raw data (loadavg): 0.96 0.93 0.90 2/54 23076
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 4785 0 0 0 11984 16 0 0 25 0 1 0 547073540 20934656 4716 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5111 4716 603 41 0 5070 0
vsize: 20444
[startup+130.005 s]
Raw data (loadavg): 0.97 0.94 0.90 2/54 23076
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 5232 0 0 0 12984 16 0 0 25 0 1 0 547073540 22806528 5163 4294967295 134512640 134672761 3221224544 3221223648 134560051 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5568 5163 603 41 0 5527 0
vsize: 22272
[startup+140.006 s]
Raw data (loadavg): 0.97 0.94 0.90 2/54 23076
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 5232 0 0 0 13984 16 0 0 25 0 1 0 547073540 22806528 5163 4294967295 134512640 134672761 3221224544 3221223712 134561406 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5568 5163 603 41 0 5527 0
vsize: 22272
[startup+150.006 s]
Raw data (loadavg): 0.98 0.94 0.90 2/54 23076
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 5232 0 0 0 14984 16 0 0 25 0 1 0 547073540 22806528 5163 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5568 5163 603 41 0 5527 0
vsize: 22272
[startup+160.007 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 23076
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 5232 0 0 0 15984 16 0 0 25 0 1 0 547073540 22806528 5163 4294967295 134512640 134672761 3221224544 3221223728 134559542 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5568 5163 603 41 0 5527 0
vsize: 22272
[startup+170.007 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 23076
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 5232 0 0 0 16984 16 0 0 25 0 1 0 547073540 22806528 5163 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5568 5163 603 41 0 5527 0
vsize: 22272
[startup+180.007 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 23076
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 5232 0 0 0 17985 16 0 0 25 0 1 0 547073540 22806528 5163 4294967295 134512640 134672761 3221224544 3221223728 134559388 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5568 5163 603 41 0 5527 0
vsize: 22272
[startup+190.007 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 23076
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 5232 0 0 0 18985 16 0 0 25 0 1 0 547073540 22806528 5163 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5568 5163 603 41 0 5527 0
vsize: 22272
[startup+200.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 23076
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 5232 0 0 0 19985 16 0 0 25 0 1 0 547073540 22806528 5163 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5568 5163 603 41 0 5527 0
vsize: 22272
[startup+210.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 23076
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 5233 0 0 0 20985 16 0 0 25 0 1 0 547073540 22806528 5164 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5568 5164 603 41 0 5527 0
vsize: 22272
[startup+220.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 23076
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 5752 0 0 0 21983 18 0 0 25 0 1 0 547073540 25083904 5683 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6124 5683 603 41 0 6083 0
vsize: 24496
[startup+230.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 23076
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 5758 0 0 0 22984 18 0 0 25 0 1 0 547073540 25083904 5689 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6124 5689 603 41 0 6083 0
vsize: 24496
[startup+240.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 23076
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 5758 0 0 0 23984 18 0 0 25 0 1 0 547073540 25083904 5689 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6124 5689 603 41 0 6083 0
vsize: 24496
[startup+250.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 23076
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 5758 0 0 0 24984 18 0 0 25 0 1 0 547073540 25083904 5689 4294967295 134512640 134672761 3221224544 3221223712 134560970 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6124 5689 603 41 0 6083 0
vsize: 24496
[startup+260.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 23076
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 5758 0 0 0 25984 18 0 0 25 0 1 0 547073540 25083904 5689 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6124 5689 603 41 0 6083 0
vsize: 24496
[startup+270.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 23076
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 5758 0 0 0 26984 18 0 0 25 0 1 0 547073540 25083904 5689 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6124 5689 603 41 0 6083 0
vsize: 24496
[startup+280.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 23076
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 6106 0 0 0 27982 20 0 0 25 0 1 0 547073540 26562560 6037 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6485 6037 603 41 0 6444 0
vsize: 25940
[startup+290.011 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 6529 0 0 0 28981 21 0 0 25 0 1 0 547073540 28299264 6460 4294967295 134512640 134672761 3221224544 3221223712 134561220 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6909 6460 603 41 0 6868 0
vsize: 27636
[startup+300.011 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 6529 0 0 0 29981 21 0 0 25 0 1 0 547073540 28299264 6460 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6909 6460 603 41 0 6868 0
vsize: 27636
[startup+310.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 6529 0 0 0 30981 21 0 0 25 0 1 0 547073540 28299264 6460 4294967295 134512640 134672761 3221224544 3221223648 134560237 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6909 6460 603 41 0 6868 0
vsize: 27636
[startup+320.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 6529 0 0 0 31982 21 0 0 25 0 1 0 547073540 28299264 6460 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6909 6460 603 41 0 6868 0
vsize: 27636
[startup+330.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 6529 0 0 0 32982 21 0 0 25 0 1 0 547073540 28299264 6460 4294967295 134512640 134672761 3221224544 3221223648 134560408 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6909 6460 603 41 0 6868 0
vsize: 27636
[startup+340.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 6529 0 0 0 33982 21 0 0 25 0 1 0 547073540 28299264 6460 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6909 6460 603 41 0 6868 0
vsize: 27636
[startup+350.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 6612 0 0 0 34981 22 0 0 25 0 1 0 547073540 28569600 6543 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6975 6543 603 41 0 6934 0
vsize: 27900
[startup+360.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 7127 0 0 0 35980 24 0 0 25 0 1 0 547073540 30711808 7058 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7498 7058 603 41 0 7457 0
vsize: 29992
[startup+370.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 7140 0 0 0 36980 24 0 0 25 0 1 0 547073540 30711808 7071 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7498 7071 603 41 0 7457 0
vsize: 29992
[startup+380.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 7140 0 0 0 37980 24 0 0 25 0 1 0 547073540 30711808 7071 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7498 7071 603 41 0 7457 0
vsize: 29992
[startup+390.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 7140 0 0 0 38980 24 0 0 25 0 1 0 547073540 30711808 7071 4294967295 134512640 134672761 3221224544 3221223728 134559327 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7498 7071 603 41 0 7457 0
vsize: 29992
[startup+400.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 7140 0 0 0 39980 24 0 0 25 0 1 0 547073540 30711808 7071 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7498 7071 603 41 0 7457 0
vsize: 29992
[startup+410.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 7140 0 0 0 40981 24 0 0 25 0 1 0 547073540 30711808 7071 4294967295 134512640 134672761 3221224544 3221223712 134560813 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7498 7071 603 41 0 7457 0
vsize: 29992
[startup+420.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 7140 0 0 0 41981 24 0 0 25 0 1 0 547073540 30711808 7071 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7498 7071 603 41 0 7457 0
vsize: 29992
[startup+430.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 7140 0 0 0 42981 24 0 0 25 0 1 0 547073540 30711808 7071 4294967295 134512640 134672761 3221224544 3221223728 134559045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7498 7071 603 41 0 7457 0
vsize: 29992
[startup+440.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 7140 0 0 0 43981 24 0 0 25 0 1 0 547073540 30711808 7071 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7498 7071 603 41 0 7457 0
vsize: 29992
[startup+450.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 7141 0 0 0 44981 24 0 0 25 0 1 0 547073540 30711808 7072 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7498 7072 603 41 0 7457 0
vsize: 29992
[startup+460.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 7143 0 0 0 45982 24 0 0 25 0 1 0 547073540 30711808 7074 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7498 7074 603 41 0 7457 0
vsize: 29992
[startup+470.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 7143 0 0 0 46982 24 0 0 25 0 1 0 547073540 30711808 7074 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7498 7074 603 41 0 7457 0
vsize: 29992
[startup+480.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 7143 0 0 0 47982 24 0 0 25 0 1 0 547073540 30711808 7074 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7498 7074 603 41 0 7457 0
vsize: 29992
[startup+490.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 7143 0 0 0 48982 24 0 0 25 0 1 0 547073540 30711808 7074 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7498 7074 603 41 0 7457 0
vsize: 29992
[startup+500.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 7143 0 0 0 49982 24 0 0 25 0 1 0 547073540 30711808 7074 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7498 7074 603 41 0 7457 0
vsize: 29992
[startup+510.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 7143 0 0 0 50982 24 0 0 25 0 1 0 547073540 30711808 7074 4294967295 134512640 134672761 3221224544 3221223728 134559254 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7498 7074 603 41 0 7457 0
vsize: 29992
[startup+520.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 7143 0 0 0 51983 24 0 0 25 0 1 0 547073540 30711808 7074 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7498 7074 603 41 0 7457 0
vsize: 29992
[startup+530.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 7143 0 0 0 52982 24 0 0 25 0 1 0 547073540 30711808 7074 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7498 7074 603 41 0 7457 0
vsize: 29992
[startup+540.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 7143 0 0 0 53982 24 0 0 25 0 1 0 547073540 30711808 7074 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7498 7074 603 41 0 7457 0
vsize: 29992
[startup+550.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 7143 0 0 0 54983 24 0 0 25 0 1 0 547073540 30711808 7074 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7498 7074 603 41 0 7457 0
vsize: 29992
[startup+560.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 7143 0 0 0 55983 24 0 0 25 0 1 0 547073540 30711808 7074 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7498 7074 603 41 0 7457 0
vsize: 29992
[startup+570.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 7143 0 0 0 56983 24 0 0 25 0 1 0 547073540 30711808 7074 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7498 7074 603 41 0 7457 0
vsize: 29992
[startup+580.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 7143 0 0 0 57983 24 0 0 25 0 1 0 547073540 30711808 7074 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7498 7074 603 41 0 7457 0
vsize: 29992
[startup+590.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 7143 0 0 0 58983 24 0 0 25 0 1 0 547073540 30711808 7074 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7498 7074 603 41 0 7457 0
vsize: 29992
[startup+600.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 7143 0 0 0 59983 24 0 0 25 0 1 0 547073540 30711808 7074 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7498 7074 603 41 0 7457 0
vsize: 29992
[startup+610.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 7143 0 0 0 60984 24 0 0 25 0 1 0 547073540 30711808 7074 4294967295 134512640 134672761 3221224544 3221223712 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7498 7074 603 41 0 7457 0
vsize: 29992
[startup+620.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 7143 0 0 0 61984 24 0 0 25 0 1 0 547073540 30711808 7074 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7498 7074 603 41 0 7457 0
vsize: 29992
[startup+630.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 7144 0 0 0 62984 24 0 0 25 0 1 0 547073540 30711808 7075 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7498 7075 603 41 0 7457 0
vsize: 29992
[startup+640.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 7144 0 0 0 63984 24 0 0 25 0 1 0 547073540 30711808 7075 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7498 7075 603 41 0 7457 0
vsize: 29992
[startup+650.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 7144 0 0 0 64984 24 0 0 25 0 1 0 547073540 30711808 7075 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7498 7075 603 41 0 7457 0
vsize: 29992
[startup+660.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 7144 0 0 0 65984 24 0 0 25 0 1 0 547073540 30711808 7075 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7498 7075 603 41 0 7457 0
vsize: 29992
[startup+670.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 7144 0 0 0 66985 24 0 0 25 0 1 0 547073540 30711808 7075 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7498 7075 603 41 0 7457 0
vsize: 29992
[startup+680.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 7144 0 0 0 67985 24 0 0 25 0 1 0 547073540 30711808 7075 4294967295 134512640 134672761 3221224544 3221223712 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7498 7075 603 41 0 7457 0
vsize: 29992
[startup+690.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 7144 0 0 0 68985 24 0 0 25 0 1 0 547073540 30711808 7075 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7498 7075 603 41 0 7457 0
vsize: 29992
[startup+700.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 7144 0 0 0 69985 24 0 0 25 0 1 0 547073540 30711808 7075 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7498 7075 603 41 0 7457 0
vsize: 29992
[startup+710.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 7144 0 0 0 70985 24 0 0 25 0 1 0 547073540 30711808 7075 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7498 7075 603 41 0 7457 0
vsize: 29992
[startup+720.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 7144 0 0 0 71985 24 0 0 25 0 1 0 547073540 30711808 7075 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7498 7075 603 41 0 7457 0
vsize: 29992
[startup+730.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 7144 0 0 0 72985 24 0 0 25 0 1 0 547073540 30711808 7075 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7498 7075 603 41 0 7457 0
vsize: 29992
[startup+740.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 7144 0 0 0 73986 24 0 0 25 0 1 0 547073540 30711808 7075 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7498 7075 603 41 0 7457 0
vsize: 29992
[startup+750.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 7144 0 0 0 74986 24 0 0 25 0 1 0 547073540 30711808 7075 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7498 7075 603 41 0 7457 0
vsize: 29992
[startup+760.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 7144 0 0 0 75986 24 0 0 25 0 1 0 547073540 30711808 7075 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7498 7075 603 41 0 7457 0
vsize: 29992
[startup+770.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 7144 0 0 0 76986 24 0 0 25 0 1 0 547073540 30711808 7075 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7498 7075 603 41 0 7457 0
vsize: 29992
[startup+780.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 7144 0 0 0 77986 24 0 0 25 0 1 0 547073540 30711808 7075 4294967295 134512640 134672761 3221224544 3221223712 134561115 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7498 7075 603 41 0 7457 0
vsize: 29992
[startup+790.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 7144 0 0 0 78986 24 0 0 25 0 1 0 547073540 30711808 7075 4294967295 134512640 134672761 3221224544 3221223728 134559116 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7498 7075 603 41 0 7457 0
vsize: 29992
[startup+800.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 7144 0 0 0 79986 24 0 0 25 0 1 0 547073540 30711808 7075 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7498 7075 603 41 0 7457 0
vsize: 29992
[startup+810.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 7144 0 0 0 80986 24 0 0 25 0 1 0 547073540 30711808 7075 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7498 7075 603 41 0 7457 0
vsize: 29992
[startup+820.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 7144 0 0 0 81986 24 0 0 25 0 1 0 547073540 30711808 7075 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7498 7075 603 41 0 7457 0
vsize: 29992
[startup+830.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 7144 0 0 0 82986 24 0 0 25 0 1 0 547073540 30711808 7075 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7498 7075 603 41 0 7457 0
vsize: 29992
[startup+840.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 7144 0 0 0 83986 24 0 0 25 0 1 0 547073540 30711808 7075 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7498 7075 603 41 0 7457 0
vsize: 29992
[startup+850.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 7194 0 0 0 84986 25 0 0 25 0 1 0 547073540 30978048 7125 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7563 7125 603 41 0 7522 0
vsize: 30252
[startup+860.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 7227 0 0 0 85986 25 0 0 25 0 1 0 547073540 31113216 7158 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7596 7158 603 41 0 7555 0
vsize: 30384
[startup+870.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 7227 0 0 0 86986 25 0 0 25 0 1 0 547073540 31113216 7158 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7596 7158 603 41 0 7555 0
vsize: 30384
[startup+880.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 7227 0 0 0 87987 25 0 0 25 0 1 0 547073540 31113216 7158 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7596 7158 603 41 0 7555 0
vsize: 30384
[startup+890.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 7227 0 0 0 88987 25 0 0 25 0 1 0 547073540 31113216 7158 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7596 7158 603 41 0 7555 0
vsize: 30384
[startup+900.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 7234 0 0 0 89987 25 0 0 25 0 1 0 547073540 31113216 7165 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7596 7165 603 41 0 7555 0
vsize: 30384
[startup+910.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 7251 0 0 0 90987 25 0 0 25 0 1 0 547073540 31248384 7182 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7629 7182 603 41 0 7588 0
vsize: 30516
[startup+920.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 7277 0 0 0 91987 25 0 0 25 0 1 0 547073540 31412224 7208 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7669 7208 603 41 0 7628 0
vsize: 30676
[startup+930.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 7294 0 0 0 92987 25 0 0 25 0 1 0 547073540 31412224 7225 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7669 7225 603 41 0 7628 0
vsize: 30676
[startup+940.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 7313 0 0 0 93988 25 0 0 25 0 1 0 547073540 31576064 7244 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7709 7244 603 41 0 7668 0
vsize: 30836
[startup+950.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 7319 0 0 0 94988 25 0 0 25 0 1 0 547073540 31576064 7250 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7709 7250 603 41 0 7668 0
vsize: 30836
[startup+960.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 7319 0 0 0 95988 25 0 0 25 0 1 0 547073540 31576064 7250 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7709 7250 603 41 0 7668 0
vsize: 30836
[startup+970.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 7319 0 0 0 96987 25 0 0 25 0 1 0 547073540 31576064 7250 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7709 7250 603 41 0 7668 0
vsize: 30836
[startup+980.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 7319 0 0 0 97987 25 0 0 25 0 1 0 547073540 31576064 7250 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7709 7250 603 41 0 7668 0
vsize: 30836
[startup+990.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 7339 0 0 0 98987 25 0 0 25 0 1 0 547073540 31739904 7270 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7749 7270 603 41 0 7708 0
vsize: 30996
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 7342 0 0 0 99988 25 0 0 25 0 1 0 547073540 31739904 7273 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7749 7273 603 41 0 7708 0
vsize: 30996
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 7351 0 0 0 100988 25 0 0 25 0 1 0 547073540 31739904 7282 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7749 7282 603 41 0 7708 0
vsize: 30996
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 7358 0 0 0 101988 25 0 0 25 0 1 0 547073540 31739904 7289 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7749 7289 603 41 0 7708 0
vsize: 30996
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 7383 0 0 0 102988 25 0 0 25 0 1 0 547073540 31887360 7314 4294967295 134512640 134672761 3221224544 3221223712 134561054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7785 7314 603 41 0 7744 0
vsize: 31140
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 7390 0 0 0 103988 25 0 0 25 0 1 0 547073540 32047104 7321 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7824 7321 603 41 0 7783 0
vsize: 31296
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 7390 0 0 0 104988 25 0 0 25 0 1 0 547073540 32047104 7321 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7824 7321 603 41 0 7783 0
vsize: 31296
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 7549 0 0 0 105988 26 0 0 25 0 1 0 547073540 32583680 7480 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7955 7480 603 41 0 7914 0
vsize: 31820
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 8016 0 0 0 106987 27 0 0 25 0 1 0 547073540 34566144 7947 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8439 7947 603 41 0 8398 0
vsize: 33756
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 8296 0 0 0 107986 28 0 0 25 0 1 0 547073540 35635200 8227 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8700 8227 603 41 0 8659 0
vsize: 34800
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 8296 0 0 0 108986 28 0 0 25 0 1 0 547073540 35635200 8227 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8700 8227 603 41 0 8659 0
vsize: 34800
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 8296 0 0 0 109986 28 0 0 25 0 1 0 547073540 35635200 8227 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8700 8227 603 41 0 8659 0
vsize: 34800
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 8296 0 0 0 110986 28 0 0 25 0 1 0 547073540 35635200 8227 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8700 8227 603 41 0 8659 0
vsize: 34800
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 8296 0 0 0 111986 28 0 0 25 0 1 0 547073540 35635200 8227 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8700 8227 603 41 0 8659 0
vsize: 34800
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 8296 0 0 0 112987 28 0 0 25 0 1 0 547073540 35635200 8227 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8700 8227 603 41 0 8659 0
vsize: 34800
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 8296 0 0 0 113987 28 0 0 25 0 1 0 547073540 35635200 8227 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8700 8227 603 41 0 8659 0
vsize: 34800
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 8296 0 0 0 114987 28 0 0 25 0 1 0 547073540 35635200 8227 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8700 8227 603 41 0 8659 0
vsize: 34800
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 8300 0 0 0 115987 28 0 0 25 0 1 0 547073540 35635200 8231 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8700 8231 603 41 0 8659 0
vsize: 34800
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 8300 0 0 0 116987 28 0 0 25 0 1 0 547073540 35635200 8231 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8700 8231 603 41 0 8659 0
vsize: 34800
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 8300 0 0 0 117987 28 0 0 25 0 1 0 547073540 35635200 8231 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8700 8231 603 41 0 8659 0
vsize: 34800
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 8300 0 0 0 118988 28 0 0 25 0 1 0 547073540 35635200 8231 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8700 8231 603 41 0 8659 0
vsize: 34800
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23078
Raw data (stat): 23074 (minisat+) R 23073 18865 18864 0 -1 0 8302 0 0 0 119988 28 0 0 25 0 1 0 547073540 35766272 8233 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8732 8233 603 41 0 8691 0
vsize: 34928
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 23078
Raw data (stat): 23074 (minisat+) Z 23073 18865 18864 0 -1 12 8305 0 0 0 119988 30 0 0 25 0 1 0 547073540 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.04
CPU time (s): 1200.19
CPU user time (s): 1199.88
CPU system time (s): 0.301954
CPU usage (%): 100.012
Max. virtual memory (Kb): 34928
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####