PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-sentoy.opb
MD5SUM	4df3e7eb358d27d446e34b975724a6c1
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-7772
Optimality of the best value was proved	NO
Number of terms in the objective function	60
Biggest coefficient in the objective function	974
Number of bits for the biggest coefficient in the objective function	10
Sum of the numbers in the objective function	9460
Number of bits of the sum of numbers in the objective function	14
Biggest number in a constraint	6000
Number of bits of the biggest number in a constraint	13
Biggest sum of numbers in a constraint	26162
Number of bits of the biggest sum of numbers	15
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.01784
Number of variables	60
Total number of constraints	90
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	60
Number of constraints which are nor clauses,nor cardinality constraints	30
Minimum length of a constraint	1
Maximum length of a constraint	60
Trace number 21983

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc30 THE 2005-04-22 01:43:00 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=12271 boxname=wulflinc30 idbench=944 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  4df3e7eb358d27d446e34b975724a6c1  /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-20-10-sentoy.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-20-10-sentoy.opb /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-20-10-sentoy.opb
IDLAUNCH: 12271
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
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.072
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        719996 kB
Buffers:         14968 kB
Cached:         274700 kB
SwapCached:        352 kB
Active:          22820 kB
Inactive:       269488 kB
HighTotal:      131008 kB
HighFree:        16492 kB
LowTotal:       903652 kB
LowFree:        703504 kB
SwapTotal:     2097892 kB
SwapFree:      2097328 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5980 kB
Slab:            16752 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-22 02:03:02 (client local time) WITH STATUS 10 IN 1200.49 SECONDS
stats: 12271 7 1200.49 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 30 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[  29]---> BDD-cost:72336
c ---[  28]---> BDD-cost:37152
c ---[  27]---> BDD-cost:65344
c ---[  26]---> BDD-cost:70690
c ---[  25]---> BDD-cost:61701
c ---[  24]---> BDD-cost:69736
c ---[  23]---> BDD-cost:70681
c ---[  22]---> BDD-cost:60569
c ---[  21]---> BDD-cost:59590
c ---[  20]---> BDD-cost:68898
c ---[  19]---> BDD-cost:51292
c ---[  18]---> BDD-cost:68218
c ---[  17]---> BDD-cost:44969
c ---[  16]---> BDD-cost:66420
c ---[  15]---> BDD-cost:66330
c ---[  14]---> BDD-cost:57913
c ---[  13]---> BDD-cost:62873
c ---[  12]---> BDD-cost:56928
c ---[  11]---> BDD-cost:71330
c ---[  10]---> BDD-cost:72214
c ---[   9]---> BDD-cost:59705
c ---[   8]---> BDD-cost:66833
c ---[   7]---> BDD-cost:69775
c ---[   6]---> BDD-cost:33741
c ---[   5]---> BDD-cost:61412
c ---[   4]---> BDD-cost:55558
c ---[   3]---> BDD-cost:67780
c ---[   2]---> BDD-cost:57716
c ---[   1]---> BDD-cost:60300
c ---[   0]---> BDD-cost:58322
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 | 5120745 15004487 | 1706915       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: -74[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): s
c ---[   0]---> Sorter-cost: 2593     Base: 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 | 5126850 15018822 | 1708950       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: -353[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): s
c ---[   0]---> Sorter-cost: 4313     Base: 3 2 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        56 | 5136457 15041357 | 1712152      28      327    11.7 |  0.000 % |
c ==============================================================================
c [1mFound solution: -421[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): s
c ---[   0]---> Sorter-cost: 2957     Base: 3 2 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        56 | 5142781 15056217 | 1714260      28      327    11.7 |  0.000 % |
c ==============================================================================
c [1mFound solution: -1393[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 5135     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        59 | 5155573 15086175 | 1718524      31      526    17.0 |  0.000 % |
c ==============================================================================
c [1mFound solution: -1451[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        70 | 5155665 15086448 | 1718555      42     1191    28.4 |  0.000 % |
c ==============================================================================
c [1mFound solution: -4026[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        71 | 5156017 15087323 | 1718672      43     1193    27.7 |  0.000 % |
c ==============================================================================
c [1mFound solution: -4960[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        74 | 5156067 15087474 | 1718689      46     1713    37.2 |  0.000 % |
c ==============================================================================
c [1mFound solution: -5044[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       105 | 5156144 15087660 | 1718714      77     3673    47.7 |  0.000 % |
c |       207 | 5156144 15087660 | 1890585     179     7398    41.3 |  0.002 % |
c ==============================================================================
c [1mFound solution: -5464[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       314 | 5156175 15087740 | 1718725     286    10797    37.8 |  0.002 % |
c |       414 | 5156175 15087740 | 1890597     386    15092    39.1 |  0.002 % |
c ==============================================================================
c [1mFound solution: -5665[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       446 | 5156181 15087753 | 1718727     418    15956    38.2 |  0.002 % |
c ==============================================================================
c [1mFound solution: -5701[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       447 | 5156202 15087807 | 1718734     419    16091    38.4 |  0.002 % |
c ==============================================================================
c [1mFound solution: -5709[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       453 | 5156213 15087852 | 1718737     425    16594    39.0 |  0.002 % |
c |       554 | 5156213 15087852 | 1890610     526    20052    38.1 |  0.002 % |
c ==============================================================================
c [1mFound solution: -5831[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       560 | 5156217 15087862 | 1718739     532    20307    38.2 |  0.002 % |
c ==============================================================================
c [1mFound solution: -5900[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       560 | 5156224 15087878 | 1718741     532    20307    38.2 |  0.002 % |
c ==============================================================================
c [1mFound solution: -5908[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       562 | 5156228 15087887 | 1718742     534    20500    38.4 |  0.002 % |
c ==============================================================================
c [1mFound solution: -6193[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       565 | 5156237 15087910 | 1718745     537    20825    38.8 |  0.002 % |
c |       665 | 5156237 15087910 | 1890619     637    25652    40.3 |  0.003 % |
c ==============================================================================
c [1mFound solution: -6641[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       688 | 5156262 15087974 | 1718754     660    26164    39.6 |  0.003 % |
c ==============================================================================
c [1mFound solution: -6647[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       690 | 5156269 15087992 | 1718756     662    26235    39.6 |  0.003 % |
c ==============================================================================
c [1mFound solution: -6679[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       701 | 5156277 15088010 | 1718759     673    26828    39.9 |  0.003 % |
c ==============================================================================
c [1mFound solution: -6714[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       708 | 5156285 15088029 | 1718761     680    27401    40.3 |  0.003 % |
c ==============================================================================
c [1mFound solution: -6740[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       715 | 5156293 15088047 | 1718764     687    28618    41.7 |  0.003 % |
c ==============================================================================
c [1mFound solution: -6747[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       724 | 5156299 15088060 | 1718766     696    29223    42.0 |  0.003 % |
c |       825 | 5156299 15088060 | 1890642     797    32942    41.3 |  0.003 % |
c ==============================================================================
c [1mFound solution: -6985[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       902 | 5156317 15088105 | 1718772     874    37385    42.8 |  0.003 % |
c |      1002 | 5156317 15088105 | 1890649     974    41750    42.9 |  0.003 % |
c |      1152 | 5156317 15088105 | 2079714    1124    45684    40.6 |  0.003 % |
c ==============================================================================
c [1mFound solution: -6991[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1189 | 5156325 15088126 | 1718775    1161    47180    40.6 |  0.003 % |
c ==============================================================================
c [1mFound solution: -7051[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1214 | 5156331 15088141 | 1718777    1186    47932    40.4 |  0.003 % |
c ==============================================================================
c [1mFound solution: -7079[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1216 | 5156337 15088155 | 1718779    1188    48214    40.6 |  0.003 % |
c |      1317 | 5156337 15088155 | 1890656    1289    52973    41.1 |  0.003 % |
c |      1468 | 5156337 15088155 | 2079722    1440    57393    39.9 |  0.003 % |
c |      1694 | 5156337 15088155 | 2287694    1666    64669    38.8 |  0.003 % |
c ==============================================================================
c [1mFound solution: -7111[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1908 | 5156343 15088169 | 1718781    1880    75091    39.9 |  0.003 % |
c ==============================================================================
c [1mFound solution: -7117[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1910 | 5156349 15088183 | 1718783    1882    75110    39.9 |  0.003 % |
c ==============================================================================
c [1mFound solution: -7144[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1913 | 5156358 15088204 | 1718786    1885    75804    40.2 |  0.003 % |
c ==============================================================================
c [1mFound solution: -7192[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1958 | 5156364 15088218 | 1718788    1930    79517    41.2 |  0.003 % |
c |      2059 | 5156364 15088218 | 1890666    2031    83368    41.0 |  0.003 % |
c ==============================================================================
c [1mFound solution: -7208[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2181 | 5156373 15088239 | 1718791    2153    87609    40.7 |  0.003 % |
c |      2282 | 5156373 15088239 | 1890670    2254    92030    40.8 |  0.003 % |
c |      2433 | 5156373 15088239 | 2079737    2405    96377    40.1 |  0.003 % |
c |      2658 | 5156373 15088239 | 2287710    2630   102788    39.1 |  0.003 % |
c ==============================================================================
c [1mFound solution: -7275[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2845 | 5156377 15088248 | 1718792    2817   107257    38.1 |  0.003 % |
c ==============================================================================
c [1mFound solution: -7296[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2853 | 5156396 15088297 | 1718798    2825   108280    38.3 |  0.003 % |
c ==============================================================================
c [1mFound solution: -7330[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2904 | 5156403 15088317 | 1718801    2876   110072    38.3 |  0.003 % |
c ==============================================================================
c [1mFound solution: -7337[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2950 | 5156409 15088331 | 1718803    2922   113673    38.9 |  0.003 % |
c |      3050 | 5156409 15088331 | 1890683    3022   117795    39.0 |  0.004 % |
c |      3201 | 5156409 15088331 | 2079751    3173   121718    38.4 |  0.004 % |
c ==============================================================================
c [1mFound solution: -7338[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3324 | 5156417 15088349 | 1718805    3296   129954    39.4 |  0.004 % |
c ==============================================================================
c [1mFound solution: -7351[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3387 | 5156424 15088366 | 1718808    3359   133995    39.9 |  0.004 % |
c |      3488 | 5156424 15088366 | 1890688    3460   141236    40.8 |  0.004 % |
c |      3638 | 5156424 15088366 | 2079757    3610   150591    41.7 |  0.004 % |
c |      3865 | 5156424 15088366 | 2287733    3837   159452    41.6 |  0.004 % |
c ==============================================================================
c [1mFound solution: -7354[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3947 | 5156427 15088373 | 1718809    3919   164302    41.9 |  0.004 % |
c |      4049 | 5156427 15088373 | 1890689    4021   169309    42.1 |  0.004 % |
c ==============================================================================
c [1mFound solution: -7358[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4050 | 5156433 15088387 | 1718811    4022   169353    42.1 |  0.004 % |
c ==============================================================================
c [1mFound solution: -7373[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4136 | 5156442 15088408 | 1718814    4108   174747    42.5 |  0.004 % |
c |      4237 | 5156442 15088408 | 1890695    4209   180949    43.0 |  0.004 % |
c |      4387 | 5156442 15088408 | 2079764    4359   186995    42.9 |  0.004 % |
c |      4612 | 5156442 15088408 | 2287741    4584   205086    44.7 |  0.004 % |
c |      4950 | 5156442 15088408 | 2516515    4922   219417    44.6 |  0.004 % |
c ==============================================================================
c [1mFound solution: -7447[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5093 | 5156450 15088426 | 1718816    5065   228648    45.1 |  0.004 % |
c |      5193 | 5156450 15088426 | 1890697    5165   232936    45.1 |  0.004 % |
c |      5343 | 5156450 15088426 | 2079767    5315   240786    45.3 |  0.004 % |
c |      5568 | 5156450 15088426 | 2287744    5540   251666    45.4 |  0.004 % |
c |      5905 | 5156450 15088426 | 2516518    5877   270237    46.0 |  0.004 % |
#### 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.89 0.93 0.90 2/54 1366
Raw data (stat): 1366 (runsolver) R 1365 11931 11930 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 549846078 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 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.0003 s]
Raw data (loadavg): 0.91 0.94 0.90 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 31755 0 0 0 931 67 0 0 25 0 1 0 549846078 85336064 19164 4294967295 134512640 134672761 3221224528 3221221720 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20834 19164 603 41 0 20793 0
vsize: 83336
[startup+20.001 s]
Raw data (loadavg): 0.92 0.94 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 84112 0 0 0 1811 187 0 0 25 0 1 0 549846078 323252224 70451 4294967295 134512640 134672761 3221224528 3221217264 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 78919 70453 603 41 0 78878 0
vsize: 315676
[startup+30.0014 s]
Raw data (loadavg): 0.93 0.94 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 143268 0 0 0 2668 331 0 0 25 0 1 0 549846078 599166976 129607 4294967295 134512640 134672761 3221224528 3221216496 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 146281 129608 603 41 0 146240 0
vsize: 585124
[startup+40.0017 s]
Raw data (loadavg): 0.94 0.94 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 168262 0 0 0 3610 389 0 0 25 0 1 0 549846078 681082880 154482 4294967295 134512640 134672761 3221224528 3221223828 134556685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 166280 154482 603 41 0 166239 0
vsize: 665120
[startup+50.0027 s]
Raw data (loadavg): 0.95 0.94 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 169686 0 0 0 4606 392 0 0 25 0 1 0 549846078 686895104 155906 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 167699 155906 603 41 0 167658 0
vsize: 670796
[startup+60.0018 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 169777 0 0 0 5606 393 0 0 25 0 1 0 549846078 687300608 155997 4294967295 134512640 134672761 3221224528 3221223700 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 167798 155997 603 41 0 167757 0
vsize: 671192
[startup+70.0029 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 170152 0 0 0 6605 394 0 0 25 0 1 0 549846078 695574528 156316 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 169818 156316 603 41 0 169777 0
vsize: 679272
[startup+80.004 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 170787 0 0 0 7604 395 0 0 25 0 1 0 549846078 697204736 156894 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 170216 156894 603 41 0 170175 0
vsize: 680864
[startup+90.0043 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171041 0 0 0 8602 396 0 0 25 0 1 0 549846078 698286080 157148 4294967295 134512640 134672761 3221224528 3221223696 134560806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 170480 157148 603 41 0 170439 0
vsize: 681920
[startup+100.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171066 0 0 0 9602 396 0 0 25 0 1 0 549846078 698286080 157173 4294967295 134512640 134672761 3221224528 3221223828 134556671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 170480 157173 603 41 0 170439 0
vsize: 681920
[startup+110.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171228 0 0 0 10601 397 0 0 25 0 1 0 549846078 699129856 157335 4294967295 134512640 134672761 3221224528 3221223680 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 170686 157335 603 41 0 170645 0
vsize: 682744
[startup+120.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171366 0 0 0 11601 397 0 0 25 0 1 0 549846078 699670528 157473 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 170818 157473 603 41 0 170777 0
vsize: 683272
[startup+130.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171435 0 0 0 12600 398 0 0 25 0 1 0 549846078 699940864 157542 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 170884 157542 603 41 0 170843 0
vsize: 683536
[startup+140.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171447 0 0 0 13601 398 0 0 25 0 1 0 549846078 699940864 157554 4294967295 134512640 134672761 3221224528 3221223792 134562218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 170884 157554 603 41 0 170843 0
vsize: 683536
[startup+150.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171474 0 0 0 14601 398 0 0 25 0 1 0 549846078 700076032 157581 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 170917 157581 603 41 0 170876 0
vsize: 683668
[startup+160.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171484 0 0 0 15601 398 0 0 25 0 1 0 549846078 700076032 157591 4294967295 134512640 134672761 3221224528 3221223664 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 170917 157591 603 41 0 170876 0
vsize: 683668
[startup+170.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171488 0 0 0 16601 398 0 0 25 0 1 0 549846078 700076032 157595 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 170917 157595 603 41 0 170876 0
vsize: 683668
[startup+180.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171489 0 0 0 17601 398 0 0 25 0 1 0 549846078 700194816 157596 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 170946 157596 603 41 0 170905 0
vsize: 683784
[startup+190.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171493 0 0 0 18601 398 0 0 25 0 1 0 549846078 700194816 157600 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 170946 157600 603 41 0 170905 0
vsize: 683784
[startup+200.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171500 0 0 0 19601 398 0 0 25 0 1 0 549846078 700194816 157607 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 170946 157607 603 41 0 170905 0
vsize: 683784
[startup+210.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171503 0 0 0 20601 399 0 0 25 0 1 0 549846078 700194816 157610 4294967295 134512640 134672761 3221224528 3221223712 134557999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 170946 157610 603 41 0 170905 0
vsize: 683784
[startup+220.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171505 0 0 0 21601 399 0 0 25 0 1 0 549846078 700194816 157612 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 170946 157612 603 41 0 170905 0
vsize: 683784
[startup+230.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171506 0 0 0 22601 399 0 0 25 0 1 0 549846078 700194816 157613 4294967295 134512640 134672761 3221224528 3221223712 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 170946 157613 603 41 0 170905 0
vsize: 683784
[startup+240.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171512 0 0 0 23601 399 0 0 25 0 1 0 549846078 700194816 157619 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 170946 157619 603 41 0 170905 0
vsize: 683784
[startup+250.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171517 0 0 0 24600 399 0 0 25 0 1 0 549846078 700194816 157624 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 170946 157624 603 41 0 170905 0
vsize: 683784
[startup+260.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171520 0 0 0 25601 399 0 0 25 0 1 0 549846078 700321792 157627 4294967295 134512640 134672761 3221224528 3221223696 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 170977 157627 603 41 0 170936 0
vsize: 683908
[startup+270.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171522 0 0 0 26601 399 0 0 25 0 1 0 549846078 700321792 157629 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 170977 157629 603 41 0 170936 0
vsize: 683908
[startup+280.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171527 0 0 0 27601 399 0 0 25 0 1 0 549846078 700321792 157634 4294967295 134512640 134672761 3221224528 3221223828 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 170977 157634 603 41 0 170936 0
vsize: 683908
[startup+290.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171528 0 0 0 28601 399 0 0 25 0 1 0 549846078 700321792 157635 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 170977 157635 603 41 0 170936 0
vsize: 683908
[startup+300.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171530 0 0 0 29601 399 0 0 25 0 1 0 549846078 700321792 157637 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 170977 157637 603 41 0 170936 0
vsize: 683908
[startup+310.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171536 0 0 0 30601 399 0 0 25 0 1 0 549846078 700321792 157643 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 170977 157643 603 41 0 170936 0
vsize: 683908
[startup+320.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171541 0 0 0 31601 399 0 0 25 0 1 0 549846078 700321792 157648 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 170977 157648 603 41 0 170936 0
vsize: 683908
[startup+330.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171552 0 0 0 32602 399 0 0 25 0 1 0 549846078 700456960 157659 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 171010 157659 603 41 0 170969 0
vsize: 684040
[startup+340.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171557 0 0 0 33602 399 0 0 25 0 1 0 549846078 700456960 157664 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 171010 157664 603 41 0 170969 0
vsize: 684040
[startup+350.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171565 0 0 0 34602 399 0 0 25 0 1 0 549846078 700456960 157672 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 171010 157672 603 41 0 170969 0
vsize: 684040
[startup+360.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171568 0 0 0 35602 399 0 0 25 0 1 0 549846078 700456960 157675 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 171010 157675 603 41 0 170969 0
vsize: 684040
[startup+370.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171570 0 0 0 36602 399 0 0 25 0 1 0 549846078 700456960 157677 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 171010 157677 603 41 0 170969 0
vsize: 684040
[startup+380.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171573 0 0 0 37602 400 0 0 25 0 1 0 549846078 700456960 157680 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 171010 157680 603 41 0 170969 0
vsize: 684040
[startup+390.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171577 0 0 0 38603 400 0 0 25 0 1 0 549846078 700456960 157684 4294967295 134512640 134672761 3221224528 3221223712 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 171010 157684 603 41 0 170969 0
vsize: 684040
[startup+400.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171580 0 0 0 39603 400 0 0 25 0 1 0 549846078 700456960 157687 4294967295 134512640 134672761 3221224528 3221223728 134557828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 171010 157687 603 41 0 170969 0
vsize: 684040
[startup+410.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171582 0 0 0 40603 400 0 0 25 0 1 0 549846078 700456960 157689 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 171010 157689 603 41 0 170969 0
vsize: 684040
[startup+420.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171587 0 0 0 41603 400 0 0 25 0 1 0 549846078 700592128 157694 4294967295 134512640 134672761 3221224528 3221223712 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 171043 157694 603 41 0 171002 0
vsize: 684172
[startup+430.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171593 0 0 0 42603 400 0 0 25 0 1 0 549846078 700592128 157700 4294967295 134512640 134672761 3221224528 3221223712 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 171043 157700 603 41 0 171002 0
vsize: 684172
[startup+440.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171596 0 0 0 43604 400 0 0 25 0 1 0 549846078 700592128 157703 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 171043 157703 603 41 0 171002 0
vsize: 684172
[startup+450.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171620 0 0 0 44604 400 0 0 25 0 1 0 549846078 700592128 157727 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 171043 157727 603 41 0 171002 0
vsize: 684172
[startup+460.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171623 0 0 0 45604 400 0 0 25 0 1 0 549846078 700592128 157730 4294967295 134512640 134672761 3221224528 3221223696 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 171043 157730 603 41 0 171002 0
vsize: 684172
[startup+470.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171628 0 0 0 46604 400 0 0 25 0 1 0 549846078 700592128 157735 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 171043 157735 603 41 0 171002 0
vsize: 684172
[startup+480.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171632 0 0 0 47604 400 0 0 25 0 1 0 549846078 700592128 157739 4294967295 134512640 134672761 3221224528 3221223860 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 171043 157739 603 41 0 171002 0
vsize: 684172
[startup+490.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171633 0 0 0 48605 400 0 0 25 0 1 0 549846078 700592128 157740 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 171043 157740 603 41 0 171002 0
vsize: 684172
[startup+500.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171634 0 0 0 49605 400 0 0 25 0 1 0 549846078 700715008 157741 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 171073 157741 603 41 0 171032 0
vsize: 684292
[startup+510.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171638 0 0 0 50605 400 0 0 25 0 1 0 549846078 700715008 157745 4294967295 134512640 134672761 3221224528 3221223828 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 171073 157745 603 41 0 171032 0
vsize: 684292
[startup+520.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171639 0 0 0 51605 400 0 0 25 0 1 0 549846078 700715008 157746 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 171073 157746 603 41 0 171032 0
vsize: 684292
[startup+530.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171644 0 0 0 52605 400 0 0 25 0 1 0 549846078 700715008 157751 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 171073 157751 603 41 0 171032 0
vsize: 684292
[startup+540.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171649 0 0 0 53605 400 0 0 25 0 1 0 549846078 700715008 157756 4294967295 134512640 134672761 3221224528 3221223664 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 171073 157756 603 41 0 171032 0
vsize: 684292
[startup+550.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171654 0 0 0 54606 400 0 0 25 0 1 0 549846078 700715008 157761 4294967295 134512640 134672761 3221224528 3221223696 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 171073 157761 603 41 0 171032 0
vsize: 684292
[startup+560.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171658 0 0 0 55606 400 0 0 25 0 1 0 549846078 700715008 157765 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 171073 157765 603 41 0 171032 0
vsize: 684292
[startup+570.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171661 0 0 0 56606 400 0 0 25 0 1 0 549846078 700715008 157768 4294967295 134512640 134672761 3221224528 3221223728 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 171073 157768 603 41 0 171032 0
vsize: 684292
[startup+580.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171664 0 0 0 57606 400 0 0 25 0 1 0 549846078 700846080 157771 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 171105 157771 603 41 0 171064 0
vsize: 684420
[startup+590.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171671 0 0 0 58606 400 0 0 25 0 1 0 549846078 700846080 157778 4294967295 134512640 134672761 3221224528 3221223728 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 171105 157778 603 41 0 171064 0
vsize: 684420
[startup+600.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171680 0 0 0 59607 400 0 0 25 0 1 0 549846078 700846080 157787 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 171105 157787 603 41 0 171064 0
vsize: 684420
[startup+610.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171683 0 0 0 60607 400 0 0 25 0 1 0 549846078 700846080 157790 4294967295 134512640 134672761 3221224528 3221223728 134557828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 171105 157790 603 41 0 171064 0
vsize: 684420
[startup+620.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171685 0 0 0 61607 400 0 0 25 0 1 0 549846078 700846080 157792 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 171105 157792 603 41 0 171064 0
vsize: 684420
[startup+630.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171689 0 0 0 62607 400 0 0 25 0 1 0 549846078 700846080 157796 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 171105 157796 603 41 0 171064 0
vsize: 684420
[startup+640.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171692 0 0 0 63607 400 0 0 25 0 1 0 549846078 700846080 157799 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 171105 157799 603 41 0 171064 0
vsize: 684420
[startup+650.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171695 0 0 0 64607 400 0 0 25 0 1 0 549846078 700846080 157802 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 171105 157802 603 41 0 171064 0
vsize: 684420
[startup+660.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171698 0 0 0 65608 400 0 0 25 0 1 0 549846078 700977152 157805 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 171137 157805 603 41 0 171096 0
vsize: 684548
[startup+670.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171700 0 0 0 66608 400 0 0 25 0 1 0 549846078 700977152 157807 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 171137 157807 603 41 0 171096 0
vsize: 684548
[startup+680.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171703 0 0 0 67608 400 0 0 25 0 1 0 549846078 700977152 157810 4294967295 134512640 134672761 3221224528 3221223696 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 171137 157810 603 41 0 171096 0
vsize: 684548
[startup+690.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171707 0 0 0 68608 400 0 0 25 0 1 0 549846078 700977152 157814 4294967295 134512640 134672761 3221224528 3221223828 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 171137 157814 603 41 0 171096 0
vsize: 684548
[startup+700.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171707 0 0 0 69608 400 0 0 25 0 1 0 549846078 700977152 157814 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 171137 157814 603 41 0 171096 0
vsize: 684548
[startup+710.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171709 0 0 0 70609 400 0 0 25 0 1 0 549846078 700977152 157816 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 171137 157816 603 41 0 171096 0
vsize: 684548
[startup+720.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171712 0 0 0 71609 400 0 0 25 0 1 0 549846078 700977152 157819 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 171137 157819 603 41 0 171096 0
vsize: 684548
[startup+730.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171714 0 0 0 72609 400 0 0 25 0 1 0 549846078 700977152 157821 4294967295 134512640 134672761 3221224528 3221223696 134561372 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 171137 157821 603 41 0 171096 0
vsize: 684548
[startup+740.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171719 0 0 0 73609 400 0 0 25 0 1 0 549846078 700977152 157826 4294967295 134512640 134672761 3221224528 3221223728 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 171137 157826 603 41 0 171096 0
vsize: 684548
[startup+750.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171723 0 0 0 74609 400 0 0 25 0 1 0 549846078 700977152 157830 4294967295 134512640 134672761 3221224528 3221223652 134566071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 171137 157830 603 41 0 171096 0
vsize: 684548
[startup+760.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171726 0 0 0 75610 400 0 0 25 0 1 0 549846078 700977152 157833 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 171137 157833 603 41 0 171096 0
vsize: 684548
[startup+770.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171730 0 0 0 76610 400 0 0 25 0 1 0 549846078 701108224 157837 4294967295 134512640 134672761 3221224528 3221223828 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 171169 157837 603 41 0 171128 0
vsize: 684676
[startup+780.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171733 0 0 0 77610 400 0 0 25 0 1 0 549846078 701108224 157840 4294967295 134512640 134672761 3221224528 3221223728 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 171169 157840 603 41 0 171128 0
vsize: 684676
[startup+790.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171738 0 0 0 78610 400 0 0 25 0 1 0 549846078 701108224 157845 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 171169 157845 603 41 0 171128 0
vsize: 684676
[startup+800.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171744 0 0 0 79610 400 0 0 25 0 1 0 549846078 701108224 157851 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 171169 157851 603 41 0 171128 0
vsize: 684676
[startup+810.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171747 0 0 0 80610 400 0 0 25 0 1 0 549846078 701108224 157854 4294967295 134512640 134672761 3221224528 3221223696 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 171169 157854 603 41 0 171128 0
vsize: 684676
[startup+820.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171750 0 0 0 81610 400 0 0 25 0 1 0 549846078 701108224 157857 4294967295 134512640 134672761 3221224528 3221223696 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 171169 157857 603 41 0 171128 0
vsize: 684676
[startup+830.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171753 0 0 0 82611 400 0 0 25 0 1 0 549846078 701108224 157860 4294967295 134512640 134672761 3221224528 3221223664 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 171169 157860 603 41 0 171128 0
vsize: 684676
[startup+840.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171756 0 0 0 83611 400 0 0 25 0 1 0 549846078 701108224 157863 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 171169 157863 603 41 0 171128 0
vsize: 684676
[startup+850.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171757 0 0 0 84611 400 0 0 25 0 1 0 549846078 701108224 157864 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 171169 157864 603 41 0 171128 0
vsize: 684676
[startup+860.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171762 0 0 0 85611 400 0 0 25 0 1 0 549846078 701243392 157869 4294967295 134512640 134672761 3221224528 3221223728 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 171202 157869 603 41 0 171161 0
vsize: 684808
[startup+870.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171766 0 0 0 86611 400 0 0 25 0 1 0 549846078 701243392 157873 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 171202 157873 603 41 0 171161 0
vsize: 684808
[startup+880.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171768 0 0 0 87611 400 0 0 25 0 1 0 549846078 701243392 157875 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 171202 157875 603 41 0 171161 0
vsize: 684808
[startup+890.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171770 0 0 0 88612 400 0 0 25 0 1 0 549846078 701243392 157877 4294967295 134512640 134672761 3221224528 3221223696 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 171202 157877 603 41 0 171161 0
vsize: 684808
[startup+900.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171776 0 0 0 89612 400 0 0 25 0 1 0 549846078 701243392 157883 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 171202 157883 603 41 0 171161 0
vsize: 684808
[startup+910.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171778 0 0 0 90612 400 0 0 25 0 1 0 549846078 701243392 157885 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 171202 157885 603 41 0 171161 0
vsize: 684808
[startup+920.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171785 0 0 0 91612 400 0 0 25 0 1 0 549846078 701243392 157892 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 171202 157892 603 41 0 171161 0
vsize: 684808
[startup+930.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171789 0 0 0 92612 400 0 0 25 0 1 0 549846078 701243392 157896 4294967295 134512640 134672761 3221224528 3221223664 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 171202 157896 603 41 0 171161 0
vsize: 684808
[startup+940.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171795 0 0 0 93612 400 0 0 25 0 1 0 549846078 701378560 157902 4294967295 134512640 134672761 3221224528 3221223728 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 171235 157902 603 41 0 171194 0
vsize: 684940
[startup+950.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171801 0 0 0 94613 400 0 0 25 0 1 0 549846078 701378560 157908 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 171235 157908 603 41 0 171194 0
vsize: 684940
[startup+960.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171809 0 0 0 95613 400 0 0 25 0 1 0 549846078 701378560 157916 4294967295 134512640 134672761 3221224528 3221223728 134557822 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 171235 157916 603 41 0 171194 0
vsize: 684940
[startup+970.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171814 0 0 0 96612 400 0 0 25 0 1 0 549846078 701378560 157921 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 171235 157921 603 41 0 171194 0
vsize: 684940
[startup+980.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171818 0 0 0 97613 400 0 0 25 0 1 0 549846078 701378560 157925 4294967295 134512640 134672761 3221224528 3221223632 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 171235 157925 603 41 0 171194 0
vsize: 684940
[startup+990.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171821 0 0 0 98613 400 0 0 25 0 1 0 549846078 701378560 157928 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 171235 157928 603 41 0 171194 0
vsize: 684940
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171824 0 0 0 99613 400 0 0 25 0 1 0 549846078 701509632 157931 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 171267 157931 603 41 0 171226 0
vsize: 685068
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171827 0 0 0 100613 400 0 0 25 0 1 0 549846078 701509632 157934 4294967295 134512640 134672761 3221224528 3221223696 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 171267 157934 603 41 0 171226 0
vsize: 685068
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1366
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171829 0 0 0 101613 400 0 0 25 0 1 0 549846078 701509632 157936 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 171267 157936 603 41 0 171226 0
vsize: 685068
[startup+1030.03 s]
Raw data (loadavg): 1.15 1.00 0.92 2/54 1419
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171836 0 0 0 102612 402 0 0 25 0 1 0 549846078 701509632 157943 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171267 157943 603 41 0 171226 0
vsize: 685068
[startup+1040.03 s]
Raw data (loadavg): 1.12 1.00 0.92 2/54 1419
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171841 0 0 0 103612 402 0 0 25 0 1 0 549846078 701509632 157948 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171267 157948 603 41 0 171226 0
vsize: 685068
[startup+1050.03 s]
Raw data (loadavg): 1.10 1.00 0.92 2/54 1419
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171844 0 0 0 104612 402 0 0 25 0 1 0 549846078 701509632 157951 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171267 157951 603 41 0 171226 0
vsize: 685068
[startup+1060.03 s]
Raw data (loadavg): 1.09 1.00 0.92 2/54 1419
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171846 0 0 0 105612 402 0 0 25 0 1 0 549846078 701509632 157953 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171267 157953 603 41 0 171226 0
vsize: 685068
[startup+1070.03 s]
Raw data (loadavg): 1.07 1.00 0.92 2/54 1419
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171851 0 0 0 106612 402 0 0 25 0 1 0 549846078 701509632 157958 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171267 157958 603 41 0 171226 0
vsize: 685068
[startup+1080.03 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 1419
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171857 0 0 0 107612 402 0 0 25 0 1 0 549846078 701640704 157964 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171299 157964 603 41 0 171258 0
vsize: 685196
[startup+1090.03 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 1419
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171863 0 0 0 108613 402 0 0 25 0 1 0 549846078 701640704 157970 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171299 157970 603 41 0 171258 0
vsize: 685196
[startup+1100.04 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 1419
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171866 0 0 0 109613 402 0 0 25 0 1 0 549846078 701640704 157973 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171299 157973 603 41 0 171258 0
vsize: 685196
[startup+1110.04 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 1421
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171870 0 0 0 110613 402 0 0 25 0 1 0 549846078 701640704 157977 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171299 157977 603 41 0 171258 0
vsize: 685196
[startup+1120.04 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 1421
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171876 0 0 0 111613 402 0 0 25 0 1 0 549846078 701640704 157983 4294967295 134512640 134672761 3221224528 3221223728 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171299 157983 603 41 0 171258 0
vsize: 685196
[startup+1130.04 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 1421
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171888 0 0 0 112613 402 0 0 25 0 1 0 549846078 701640704 157995 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171299 157995 603 41 0 171258 0
vsize: 685196
[startup+1140.04 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 1421
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171894 0 0 0 113613 403 0 0 25 0 1 0 549846078 701640704 158001 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171299 158001 603 41 0 171258 0
vsize: 685196
[startup+1150.04 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 1421
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171900 0 0 0 114613 403 0 0 25 0 1 0 549846078 701771776 158007 4294967295 134512640 134672761 3221224528 3221223676 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171331 158007 603 41 0 171290 0
vsize: 685324
[startup+1160.04 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 1421
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171910 0 0 0 115613 403 0 0 25 0 1 0 549846078 701771776 158017 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171331 158017 603 41 0 171290 0
vsize: 685324
[startup+1170.04 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 1421
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171914 0 0 0 116613 403 0 0 25 0 1 0 549846078 701771776 158021 4294967295 134512640 134672761 3221224528 3221223680 134561040 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171331 158021 603 41 0 171290 0
vsize: 685324
[startup+1180.04 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 1421
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171923 0 0 0 117613 403 0 0 25 0 1 0 549846078 701771776 158030 4294967295 134512640 134672761 3221224528 3221223696 134560822 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171331 158030 603 41 0 171290 0
vsize: 685324
[startup+1190.04 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 1421
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171931 0 0 0 118614 403 0 0 25 0 1 0 549846078 701771776 158038 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171331 158038 603 41 0 171290 0
vsize: 685324
[startup+1200.04 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 1421
Raw data (stat): 1366 (minisat+) R 1365 11931 11930 0 -1 0 171938 0 0 0 119613 403 0 0 25 0 1 0 549846078 701902848 158045 4294967295 134512640 134672761 3221224528 3221223696 134560888 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171363 158045 603 41 0 171322 0
vsize: 685452
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.35 s]
Raw data (loadavg): 1.01 1.00 0.92 1/54 1421
Raw data (stat): 1366 (minisat+) Z 1365 11931 11930 0 -1 12 171941 0 0 0 119613 435 0 0 25 0 1 0 549846078 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.35
CPU time (s): 1200.49
CPU user time (s): 1196.14
CPU system time (s): 4.35034
CPU usage (%): 100.011
Max. virtual memory (Kb): 685452
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####