PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-misc07.opb
MD5SUM	54df16ee65da54d5975ffedee80d2bb9
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 15113

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc1 THE 2005-04-21 02:56:09 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18590 boxname=wulflinc1 idbench=1430 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  54df16ee65da54d5975ffedee80d2bb9  /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-13-7-misc07.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-13-7-misc07.opb /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-13-7-misc07.opb
IDLAUNCH: 18590
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.053
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.053
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:        600740 kB
Buffers:         23216 kB
Cached:         383084 kB
SwapCached:          0 kB
Active:         110328 kB
Inactive:       299108 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        600488 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           7220 kB
Slab:            18796 kB
Committed_AS:    92820 kB
PageTables:        344 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 03:16:11 (client local time) WITH STATUS 10 IN 1200.19 SECONDS
stats: 18590 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 % |
c |    378370 |   30220    97756 |   51343   21306  1884108    88.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.85 0.94 0.90 2/56 18443
Raw data (stat): 18443 (runsolver) R 18442 12452 12451 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 426570483 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+9.99967 s]
Raw data (loadavg): 0.87 0.94 0.90 2/56 18443
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 1759 0 0 0 995 4 0 0 25 0 1 0 426570483 8568832 1690 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2092 1690 603 41 0 2051 0
vsize: 8368
[startup+20.0005 s]
Raw data (loadavg): 0.89 0.94 0.90 2/56 18443
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 2319 0 0 0 1994 5 0 0 25 0 1 0 426570483 10862592 2250 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2652 2250 603 41 0 2611 0
vsize: 10608
[startup+30.0013 s]
Raw data (loadavg): 0.91 0.94 0.90 2/56 18443
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 2564 0 0 0 2993 6 0 0 25 0 1 0 426570483 11923456 2495 4294967295 134512640 134672761 3221224544 3221223712 134560903 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.0021 s]
Raw data (loadavg): 0.92 0.94 0.90 2/56 18443
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 2746 0 0 0 3992 7 0 0 25 0 1 0 426570483 12595200 2677 4294967295 134512640 134672761 3221224544 3221223736 134557988 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.0029 s]
Raw data (loadavg): 0.93 0.94 0.90 2/56 18443
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 2746 0 0 0 4993 7 0 0 25 0 1 0 426570483 12595200 2677 4294967295 134512640 134672761 3221224544 3221223744 134557911 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.0031 s]
Raw data (loadavg): 0.94 0.95 0.91 2/56 18443
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 2746 0 0 0 5992 7 0 0 25 0 1 0 426570483 12595200 2677 4294967295 134512640 134672761 3221224544 3221223648 134559877 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.0035 s]
Raw data (loadavg): 0.95 0.95 0.91 2/56 18443
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 3282 0 0 0 6991 8 0 0 25 0 1 0 426570483 14905344 3213 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3639 3213 603 41 0 3598 0
vsize: 14556
[startup+80.0041 s]
Raw data (loadavg): 0.96 0.95 0.91 2/56 18443
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 3395 0 0 0 7990 9 0 0 25 0 1 0 426570483 15310848 3326 4294967295 134512640 134672761 3221224544 3221223648 134560184 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3738 3326 603 41 0 3697 0
vsize: 14952
[startup+90.0049 s]
Raw data (loadavg): 0.96 0.95 0.91 2/56 18443
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 3395 0 0 0 8990 9 0 0 25 0 1 0 426570483 15310848 3326 4294967295 134512640 134672761 3221224544 3221223648 134560381 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3738 3326 603 41 0 3697 0
vsize: 14952
[startup+100.005 s]
Raw data (loadavg): 0.97 0.95 0.91 2/56 18443
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 3855 0 0 0 9990 10 0 0 25 0 1 0 426570483 17166336 3786 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4191 3786 603 41 0 4150 0
vsize: 16764
[startup+110.004 s]
Raw data (loadavg): 0.97 0.95 0.91 2/56 18443
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 4505 0 0 0 10988 11 0 0 25 0 1 0 426570483 19857408 4436 4294967295 134512640 134672761 3221224544 3221223744 134557806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4848 4436 603 41 0 4807 0
vsize: 19392
[startup+120.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/56 18443
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 4884 0 0 0 11988 11 0 0 25 0 1 0 426570483 21467136 4815 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5241 4815 603 41 0 5200 0
vsize: 20964
[startup+130.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/56 18443
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 5232 0 0 0 12987 13 0 0 25 0 1 0 426570483 22806528 5163 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5568 5163 603 41 0 5527 0
vsize: 22272
[startup+140.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/56 18443
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 5232 0 0 0 13987 13 0 0 25 0 1 0 426570483 22806528 5163 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5568 5163 603 41 0 5527 0
vsize: 22272
[startup+150.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/56 18443
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 5232 0 0 0 14987 13 0 0 25 0 1 0 426570483 22806528 5163 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5568 5163 603 41 0 5527 0
vsize: 22272
[startup+160.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 18443
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 5232 0 0 0 15987 13 0 0 25 0 1 0 426570483 22806528 5163 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5568 5163 603 41 0 5527 0
vsize: 22272
[startup+170.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 18443
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 5232 0 0 0 16987 13 0 0 25 0 1 0 426570483 22806528 5163 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5568 5163 603 41 0 5527 0
vsize: 22272
[startup+180.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 18443
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 5232 0 0 0 17988 13 0 0 25 0 1 0 426570483 22806528 5163 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5568 5163 603 41 0 5527 0
vsize: 22272
[startup+190.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 18443
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 5232 0 0 0 18988 13 0 0 25 0 1 0 426570483 22806528 5163 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5568 5163 603 41 0 5527 0
vsize: 22272
[startup+200.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 18443
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 5232 0 0 0 19988 13 0 0 25 0 1 0 426570483 22806528 5163 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5568 5163 603 41 0 5527 0
vsize: 22272
[startup+210.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 18443
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 5351 0 0 0 20988 13 0 0 25 0 1 0 426570483 23474176 5282 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5731 5282 603 41 0 5690 0
vsize: 22924
[startup+220.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 18443
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 5758 0 0 0 21987 14 0 0 25 0 1 0 426570483 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+230.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 18443
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 5758 0 0 0 22987 14 0 0 25 0 1 0 426570483 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+240.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 18498
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 5758 0 0 0 23987 14 0 0 25 0 1 0 426570483 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+250.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 18498
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 5758 0 0 0 24988 14 0 0 25 0 1 0 426570483 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+260.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18498
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 5758 0 0 0 25988 14 0 0 25 0 1 0 426570483 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+270.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18498
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 5872 0 0 0 26988 14 0 0 25 0 1 0 426570483 25485312 5803 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6222 5803 603 41 0 6181 0
vsize: 24888
[startup+280.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18498
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 6411 0 0 0 27986 16 0 0 25 0 1 0 426570483 27758592 6342 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6777 6342 603 41 0 6736 0
vsize: 27108
[startup+290.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18498
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 6529 0 0 0 28986 16 0 0 25 0 1 0 426570483 28299264 6460 4294967295 134512640 134672761 3221224544 3221223704 134561029 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6909 6460 603 41 0 6868 0
vsize: 27636
[startup+300.005 s]
Raw data (loadavg): 1.07 0.99 0.91 2/56 18500
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 6529 0 0 0 29986 17 0 0 25 0 1 0 426570483 28299264 6460 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6909 6460 603 41 0 6868 0
vsize: 27636
[startup+310.005 s]
Raw data (loadavg): 1.06 0.99 0.91 2/56 18500
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 6529 0 0 0 30986 17 0 0 25 0 1 0 426570483 28299264 6460 4294967295 134512640 134672761 3221224544 3221223728 134559622 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6909 6460 603 41 0 6868 0
vsize: 27636
[startup+320.005 s]
Raw data (loadavg): 1.05 0.99 0.91 2/56 18502
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 6529 0 0 0 31986 17 0 0 25 0 1 0 426570483 28299264 6460 4294967295 134512640 134672761 3221224544 3221223712 134561156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6909 6460 603 41 0 6868 0
vsize: 27636
[startup+330.005 s]
Raw data (loadavg): 1.04 0.99 0.91 2/56 18502
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 6529 0 0 0 32986 17 0 0 25 0 1 0 426570483 28299264 6460 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6909 6460 603 41 0 6868 0
vsize: 27636
[startup+340.005 s]
Raw data (loadavg): 1.03 0.99 0.91 2/56 18502
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 6529 0 0 0 33986 17 0 0 25 0 1 0 426570483 28299264 6460 4294967295 134512640 134672761 3221224544 3221223680 134560608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6909 6460 603 41 0 6868 0
vsize: 27636
[startup+350.006 s]
Raw data (loadavg): 1.03 0.99 0.91 2/56 18502
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 6959 0 0 0 34985 18 0 0 25 0 1 0 426570483 30044160 6890 4294967295 134512640 134672761 3221224544 3221223648 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7335 6890 603 41 0 7294 0
vsize: 29340
[startup+360.006 s]
Raw data (loadavg): 1.02 0.99 0.91 2/56 18502
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7140 0 0 0 35984 19 0 0 25 0 1 0 426570483 30711808 7071 4294967295 134512640 134672761 3221224544 3221223728 134558656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7498 7071 603 41 0 7457 0
vsize: 29992
[startup+370.006 s]
Raw data (loadavg): 1.02 0.99 0.91 2/56 18502
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7140 0 0 0 36985 19 0 0 25 0 1 0 426570483 30711808 7071 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7498 7071 603 41 0 7457 0
vsize: 29992
[startup+380.006 s]
Raw data (loadavg): 1.02 0.99 0.91 2/56 18502
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7140 0 0 0 37985 19 0 0 25 0 1 0 426570483 30711808 7071 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7498 7071 603 41 0 7457 0
vsize: 29992
[startup+390.007 s]
Raw data (loadavg): 1.01 0.99 0.91 2/56 18502
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7140 0 0 0 38985 19 0 0 25 0 1 0 426570483 30711808 7071 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7498 7071 603 41 0 7457 0
vsize: 29992
[startup+400.007 s]
Raw data (loadavg): 1.01 0.99 0.91 2/56 18502
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7140 0 0 0 39985 19 0 0 25 0 1 0 426570483 30711808 7071 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7498 7071 603 41 0 7457 0
vsize: 29992
[startup+410.007 s]
Raw data (loadavg): 1.01 0.99 0.91 2/56 18502
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7140 0 0 0 40985 19 0 0 25 0 1 0 426570483 30711808 7071 4294967295 134512640 134672761 3221224544 3221223692 134565030 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7498 7071 603 41 0 7457 0
vsize: 29992
[startup+420.008 s]
Raw data (loadavg): 1.01 0.99 0.91 2/56 18502
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7140 0 0 0 41986 19 0 0 25 0 1 0 426570483 30711808 7071 4294967295 134512640 134672761 3221224544 3221223744 134557900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7498 7071 603 41 0 7457 0
vsize: 29992
[startup+430.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 18502
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7140 0 0 0 42986 19 0 0 25 0 1 0 426570483 30711808 7071 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7498 7071 603 41 0 7457 0
vsize: 29992
[startup+440.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 18502
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7141 0 0 0 43986 19 0 0 25 0 1 0 426570483 30711808 7072 4294967295 134512640 134672761 3221224544 3221223728 134559575 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7498 7072 603 41 0 7457 0
vsize: 29992
[startup+450.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 18502
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7142 0 0 0 44986 19 0 0 25 0 1 0 426570483 30711808 7073 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7498 7073 603 41 0 7457 0
vsize: 29992
[startup+460.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 18502
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7143 0 0 0 45986 19 0 0 25 0 1 0 426570483 30711808 7074 4294967295 134512640 134672761 3221224544 3221223712 134561115 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7498 7074 603 41 0 7457 0
vsize: 29992
[startup+470.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 18502
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7143 0 0 0 46986 19 0 0 25 0 1 0 426570483 30711808 7074 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7498 7074 603 41 0 7457 0
vsize: 29992
[startup+480.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 18502
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7143 0 0 0 47986 19 0 0 25 0 1 0 426570483 30711808 7074 4294967295 134512640 134672761 3221224544 3221223712 134561391 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7498 7074 603 41 0 7457 0
vsize: 29992
[startup+490.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 18502
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7143 0 0 0 48987 19 0 0 25 0 1 0 426570483 30711808 7074 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7498 7074 603 41 0 7457 0
vsize: 29992
[startup+500.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 18502
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7143 0 0 0 49987 19 0 0 25 0 1 0 426570483 30711808 7074 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7498 7074 603 41 0 7457 0
vsize: 29992
[startup+510.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 18502
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7143 0 0 0 50987 19 0 0 25 0 1 0 426570483 30711808 7074 4294967295 134512640 134672761 3221224544 3221223648 134560529 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7498 7074 603 41 0 7457 0
vsize: 29992
[startup+520.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 18502
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7143 0 0 0 51987 19 0 0 25 0 1 0 426570483 30711808 7074 4294967295 134512640 134672761 3221224544 3221223680 134560588 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.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 18502
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7143 0 0 0 52987 19 0 0 25 0 1 0 426570483 30711808 7074 4294967295 134512640 134672761 3221224544 3221223680 134560709 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.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 18504
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7143 0 0 0 53986 20 0 0 25 0 1 0 426570483 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+550.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 18504
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7143 0 0 0 54986 20 0 0 25 0 1 0 426570483 30711808 7074 4294967295 134512640 134672761 3221224544 3221223744 134557895 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.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 18504
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7143 0 0 0 55986 21 0 0 25 0 1 0 426570483 30711808 7074 4294967295 134512640 134672761 3221224544 3221223648 134560410 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.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 18504
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7143 0 0 0 56986 21 0 0 25 0 1 0 426570483 30711808 7074 4294967295 134512640 134672761 3221224544 3221223712 134560830 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.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 18504
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7143 0 0 0 57986 21 0 0 25 0 1 0 426570483 30711808 7074 4294967295 134512640 134672761 3221224544 3221223704 134561029 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.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 18504
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7143 0 0 0 58986 21 0 0 25 0 1 0 426570483 30711808 7074 4294967295 134512640 134672761 3221224544 3221223728 134558662 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.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 18504
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7143 0 0 0 59986 21 0 0 25 0 1 0 426570483 30711808 7074 4294967295 134512640 134672761 3221224544 3221223680 134560588 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.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 18504
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7143 0 0 0 60986 21 0 0 25 0 1 0 426570483 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+620.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 18504
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7144 0 0 0 61986 21 0 0 25 0 1 0 426570483 30711808 7075 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7498 7075 603 41 0 7457 0
vsize: 29992
[startup+630.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 18504
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7144 0 0 0 62986 21 0 0 25 0 1 0 426570483 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.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 18504
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7144 0 0 0 63986 21 0 0 25 0 1 0 426570483 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.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 18504
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7144 0 0 0 64986 22 0 0 25 0 1 0 426570483 30711808 7075 4294967295 134512640 134672761 3221224544 3221223648 134559805 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.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 18504
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7144 0 0 0 65986 22 0 0 25 0 1 0 426570483 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+670.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 18504
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7144 0 0 0 66987 22 0 0 25 0 1 0 426570483 30711808 7075 4294967295 134512640 134672761 3221224544 3221223600 134565092 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.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 18504
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7144 0 0 0 67986 22 0 0 25 0 1 0 426570483 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+690.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 18504
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7144 0 0 0 68987 22 0 0 25 0 1 0 426570483 30711808 7075 4294967295 134512640 134672761 3221224544 3221223648 134560218 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.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 18504
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7144 0 0 0 69987 22 0 0 25 0 1 0 426570483 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+710.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 18504
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7144 0 0 0 70987 22 0 0 25 0 1 0 426570483 30711808 7075 4294967295 134512640 134672761 3221224544 3221223648 134560285 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.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 18504
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7144 0 0 0 71987 22 0 0 25 0 1 0 426570483 30711808 7075 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7498 7075 603 41 0 7457 0
vsize: 29992
[startup+730.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 18504
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7144 0 0 0 72987 22 0 0 25 0 1 0 426570483 30711808 7075 4294967295 134512640 134672761 3221224544 3221223728 134559031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7498 7075 603 41 0 7457 0
vsize: 29992
[startup+740.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 18504
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7144 0 0 0 73987 22 0 0 25 0 1 0 426570483 30711808 7075 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7498 7075 603 41 0 7457 0
vsize: 29992
[startup+750.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 18504
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7144 0 0 0 74987 22 0 0 25 0 1 0 426570483 30711808 7075 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7498 7075 603 41 0 7457 0
vsize: 29992
[startup+760.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 18504
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7144 0 0 0 75988 22 0 0 25 0 1 0 426570483 30711808 7075 4294967295 134512640 134672761 3221224544 3221223728 134559616 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7498 7075 603 41 0 7457 0
vsize: 29992
[startup+770.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 18504
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7144 0 0 0 76988 22 0 0 25 0 1 0 426570483 30711808 7075 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7498 7075 603 41 0 7457 0
vsize: 29992
[startup+780.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 18504
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7144 0 0 0 77988 22 0 0 25 0 1 0 426570483 30711808 7075 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7498 7075 603 41 0 7457 0
vsize: 29992
[startup+790.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 18504
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7144 0 0 0 78988 22 0 0 25 0 1 0 426570483 30711808 7075 4294967295 134512640 134672761 3221224544 3221223712 134560999 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.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 18504
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7144 0 0 0 79988 22 0 0 25 0 1 0 426570483 30711808 7075 4294967295 134512640 134672761 3221224544 3221223648 134560215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7498 7075 603 41 0 7457 0
vsize: 29992
[startup+810.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 18504
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7144 0 0 0 80988 22 0 0 25 0 1 0 426570483 30711808 7075 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7498 7075 603 41 0 7457 0
vsize: 29992
[startup+820.016 s]
Raw data (loadavg): 1.00 0.99 0.91 3/56 18504
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7144 0 0 0 81989 22 0 0 25 0 1 0 426570483 30711808 7075 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7498 7075 603 41 0 7457 0
vsize: 29992
[startup+830.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 18504
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7144 0 0 0 82989 22 0 0 25 0 1 0 426570483 30711808 7075 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7498 7075 603 41 0 7457 0
vsize: 29992
[startup+840.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 18506
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7227 0 0 0 83988 23 0 0 25 0 1 0 426570483 31113216 7158 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7596 7158 603 41 0 7555 0
vsize: 30384
[startup+850.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 18506
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7227 0 0 0 84989 23 0 0 25 0 1 0 426570483 31113216 7158 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7596 7158 603 41 0 7555 0
vsize: 30384
[startup+860.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 18506
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7227 0 0 0 85989 23 0 0 25 0 1 0 426570483 31113216 7158 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7596 7158 603 41 0 7555 0
vsize: 30384
[startup+870.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 18506
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7227 0 0 0 86989 23 0 0 25 0 1 0 426570483 31113216 7158 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7596 7158 603 41 0 7555 0
vsize: 30384
[startup+880.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 18506
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7230 0 0 0 87989 23 0 0 25 0 1 0 426570483 31113216 7161 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7596 7161 603 41 0 7555 0
vsize: 30384
[startup+890.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 18506
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7245 0 0 0 88989 23 0 0 25 0 1 0 426570483 31248384 7176 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7629 7176 603 41 0 7588 0
vsize: 30516
[startup+900.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 18506
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7277 0 0 0 89989 23 0 0 25 0 1 0 426570483 31412224 7208 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7669 7208 603 41 0 7628 0
vsize: 30676
[startup+910.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 18506
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7294 0 0 0 90990 23 0 0 25 0 1 0 426570483 31412224 7225 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7669 7225 603 41 0 7628 0
vsize: 30676
[startup+920.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 18506
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7304 0 0 0 91990 23 0 0 25 0 1 0 426570483 31576064 7235 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7709 7235 603 41 0 7668 0
vsize: 30836
[startup+930.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 18506
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7319 0 0 0 92990 23 0 0 25 0 1 0 426570483 31576064 7250 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7709 7250 603 41 0 7668 0
vsize: 30836
[startup+940.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 18506
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7319 0 0 0 93990 23 0 0 25 0 1 0 426570483 31576064 7250 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7709 7250 603 41 0 7668 0
vsize: 30836
[startup+950.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 18506
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7319 0 0 0 94990 23 0 0 25 0 1 0 426570483 31576064 7250 4294967295 134512640 134672761 3221224544 3221223712 134561193 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.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 18506
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7319 0 0 0 95990 23 0 0 25 0 1 0 426570483 31576064 7250 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7709 7250 603 41 0 7668 0
vsize: 30836
[startup+970.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 18506
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7329 0 0 0 96990 23 0 0 25 0 1 0 426570483 31576064 7260 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7709 7260 603 41 0 7668 0
vsize: 30836
[startup+980.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 18506
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7342 0 0 0 97990 24 0 0 25 0 1 0 426570483 31739904 7273 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7749 7273 603 41 0 7708 0
vsize: 30996
[startup+990.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 18506
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7351 0 0 0 98990 24 0 0 25 0 1 0 426570483 31739904 7282 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7749 7282 603 41 0 7708 0
vsize: 30996
[startup+1000.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 18506
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7356 0 0 0 99990 24 0 0 25 0 1 0 426570483 31739904 7287 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7749 7287 603 41 0 7708 0
vsize: 30996
[startup+1010.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 18506
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7377 0 0 0 100990 24 0 0 25 0 1 0 426570483 31887360 7308 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7785 7308 603 41 0 7744 0
vsize: 31140
[startup+1020.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 18506
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7390 0 0 0 101989 24 0 0 25 0 1 0 426570483 32047104 7321 4294967295 134512640 134672761 3221224544 3221223648 134560229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7824 7321 603 41 0 7783 0
vsize: 31296
[startup+1030.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 18506
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7390 0 0 0 102989 25 0 0 25 0 1 0 426570483 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+1040.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 18506
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7469 0 0 0 103989 25 0 0 25 0 1 0 426570483 32313344 7400 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7889 7400 603 41 0 7848 0
vsize: 31556
[startup+1050.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 18506
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 7960 0 0 0 104987 27 0 0 25 0 1 0 426570483 34299904 7891 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8374 7891 603 41 0 8333 0
vsize: 33496
[startup+1060.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 18506
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 8296 0 0 0 105986 28 0 0 25 0 1 0 426570483 35635200 8227 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8700 8227 603 41 0 8659 0
vsize: 34800
[startup+1070.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 18506
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 8296 0 0 0 106987 28 0 0 25 0 1 0 426570483 35635200 8227 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8700 8227 603 41 0 8659 0
vsize: 34800
[startup+1080.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 18506
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 8296 0 0 0 107987 28 0 0 25 0 1 0 426570483 35635200 8227 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8700 8227 603 41 0 8659 0
vsize: 34800
[startup+1090.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 18506
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 8296 0 0 0 108987 28 0 0 25 0 1 0 426570483 35635200 8227 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8700 8227 603 41 0 8659 0
vsize: 34800
[startup+1100.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 18506
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 8296 0 0 0 109987 28 0 0 25 0 1 0 426570483 35635200 8227 4294967295 134512640 134672761 3221224544 3221223728 134558654 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8700 8227 603 41 0 8659 0
vsize: 34800
[startup+1110.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 18506
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 8296 0 0 0 110987 28 0 0 25 0 1 0 426570483 35635200 8227 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8700 8227 603 41 0 8659 0
vsize: 34800
[startup+1120.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 18506
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 8296 0 0 0 111988 28 0 0 25 0 1 0 426570483 35635200 8227 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8700 8227 603 41 0 8659 0
vsize: 34800
[startup+1130.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 18506
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 8296 0 0 0 112988 28 0 0 25 0 1 0 426570483 35635200 8227 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8700 8227 603 41 0 8659 0
vsize: 34800
[startup+1140.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 18508
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 8300 0 0 0 113988 28 0 0 25 0 1 0 426570483 35635200 8231 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8700 8231 603 41 0 8659 0
vsize: 34800
[startup+1150.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 18508
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 8300 0 0 0 114988 28 0 0 25 0 1 0 426570483 35635200 8231 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8700 8231 603 41 0 8659 0
vsize: 34800
[startup+1160.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 18508
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 8300 0 0 0 115988 28 0 0 25 0 1 0 426570483 35635200 8231 4294967295 134512640 134672761 3221224544 3221223648 134560418 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8700 8231 603 41 0 8659 0
vsize: 34800
[startup+1170.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 18508
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 8300 0 0 0 116989 28 0 0 25 0 1 0 426570483 35635200 8231 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8700 8231 603 41 0 8659 0
vsize: 34800
[startup+1180.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 18508
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 8334 0 0 0 117989 28 0 0 25 0 1 0 426570483 35897344 8265 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8764 8265 603 41 0 8723 0
vsize: 35056
[startup+1190.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 18508
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 8473 0 0 0 118988 28 0 0 25 0 1 0 426570483 36438016 8404 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8896 8404 603 41 0 8855 0
vsize: 35584
[startup+1200.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/56 18508
Raw data (stat): 18443 (minisat+) R 18442 12452 12451 0 -1 0 8473 0 0 0 119988 28 0 0 25 0 1 0 426570483 36438016 8404 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8896 8404 603 41 0 8855 0
vsize: 35584
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 1.00 0.99 0.91 1/56 18508
Raw data (stat): 18443 (minisat+) Z 18442 12452 12451 0 -1 12 8476 0 0 0 119988 30 0 0 25 0 1 0 426570483 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.05
CPU time (s): 1200.19
CPU user time (s): 1199.89
CPU system time (s): 0.302953
CPU usage (%): 100.012
Max. virtual memory (Kb): 35584
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####