PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-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.01884
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 15541

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.080
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:        586340 kB
Buffers:          8068 kB
Cached:         412216 kB
SwapCached:        432 kB
Active:          32796 kB
Inactive:       389640 kB
HighTotal:      131008 kB
HighFree:          420 kB
LowTotal:       903652 kB
LowFree:        585920 kB
SwapTotal:     2097892 kB
SwapFree:      2096708 kB
Dirty:              48 kB
Writeback:           0 kB
Mapped:           5932 kB
Slab:            20136 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 05:18:08 (client local time) WITH STATUS 10 IN 1200.45 SECONDS
stats: 17263 7 1200.45 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.75 0.91 0.89 2/54 25116
Raw data (stat): 25116 (runsolver) R 25115 28546 28545 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 542375213 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0001 s]
Raw data (loadavg): 0.79 0.91 0.89 2/54 25116
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 31061 0 0 0 935 64 0 0 25 0 1 0 542375213 83750912 18595 4294967295 134512640 134672761 3221224544 3221220512 134594520 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20447 18603 603 41 0 20406 0
vsize: 81788
[startup+20.001 s]
Raw data (loadavg): 0.82 0.91 0.89 2/54 25116
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 82211 0 0 0 1819 180 0 0 25 0 1 0 542375213 317431808 68550 4294967295 134512640 134672761 3221224544 3221213440 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77498 68551 603 41 0 77457 0
vsize: 309992
[startup+30.0017 s]
Raw data (loadavg): 0.85 0.92 0.89 2/54 25116
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 140862 0 0 0 2675 324 0 0 25 0 1 0 542375213 591818752 127201 4294967295 134512640 134672761 3221224544 3221210852 1075346926 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 144487 127202 603 41 0 144446 0
vsize: 577948
[startup+40.0012 s]
Raw data (loadavg): 0.87 0.92 0.89 2/54 25116
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 168013 0 0 0 3614 385 0 0 25 0 1 0 542375213 680468480 154295 4294967295 134512640 134672761 3221224544 3221223696 134565036 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 166130 154295 603 41 0 166089 0
vsize: 664520
[startup+50.0022 s]
Raw data (loadavg): 0.89 0.92 0.90 2/54 25116
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 169613 0 0 0 4609 389 0 0 25 0 1 0 542375213 686624768 155833 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 167633 155833 603 41 0 167592 0
vsize: 670532
[startup+60.0018 s]
Raw data (loadavg): 0.91 0.92 0.90 2/54 25116
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 169777 0 0 0 5609 389 0 0 25 0 1 0 542375213 687300608 155997 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 167798 155997 603 41 0 167757 0
vsize: 671192
[startup+70.0022 s]
Raw data (loadavg): 0.92 0.92 0.90 2/54 25116
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 170143 0 0 0 6608 390 0 0 25 0 1 0 542375213 695574528 156307 4294967295 134512640 134672761 3221224544 3221223712 134564636 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 169818 156307 603 41 0 169777 0
vsize: 679272
[startup+80.0031 s]
Raw data (loadavg): 0.93 0.93 0.90 2/54 25116
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 170443 0 0 0 7608 391 0 0 25 0 1 0 542375213 696250368 156550 4294967295 134512640 134672761 3221224544 3221223696 134565039 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 169983 156550 603 41 0 169942 0
vsize: 679932
[startup+90.0029 s]
Raw data (loadavg): 0.94 0.93 0.90 2/54 25116
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 170941 0 0 0 8606 392 0 0 25 0 1 0 542375213 697880576 157048 4294967295 134512640 134672761 3221224544 3221223844 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 170381 157048 603 41 0 170340 0
vsize: 681524
[startup+100.003 s]
Raw data (loadavg): 0.95 0.93 0.90 2/54 25116
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171061 0 0 0 9606 392 0 0 25 0 1 0 542375213 698286080 157168 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 170480 157168 603 41 0 170439 0
vsize: 681920
[startup+110.003 s]
Raw data (loadavg): 0.96 0.93 0.90 2/54 25116
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171223 0 0 0 10605 393 0 0 25 0 1 0 542375213 699129856 157330 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 170686 157330 603 41 0 170645 0
vsize: 682744
[startup+120.004 s]
Raw data (loadavg): 0.96 0.93 0.90 2/55 25117
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171331 0 0 0 11605 393 0 0 25 0 1 0 542375213 699535360 157438 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 170785 157438 603 41 0 170744 0
vsize: 683140
[startup+130.004 s]
Raw data (loadavg): 1.12 0.97 0.91 3/57 25165
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171422 0 0 0 12604 394 0 0 25 0 1 0 542375213 699805696 157529 4294967295 134512640 134672761 3221224544 3221223808 134562495 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 170851 157529 603 41 0 170810 0
vsize: 683404
[startup+140.004 s]
Raw data (loadavg): 1.10 0.97 0.91 2/54 25169
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171443 0 0 0 13598 394 0 0 25 0 1 0 542375213 699940864 157550 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 170884 157550 603 41 0 170843 0
vsize: 683536
[startup+150.005 s]
Raw data (loadavg): 1.09 0.97 0.91 2/54 25169
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171450 0 0 0 14598 394 0 0 25 0 1 0 542375213 699940864 157557 4294967295 134512640 134672761 3221224544 3221223844 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 170884 157557 603 41 0 170843 0
vsize: 683536
[startup+160.005 s]
Raw data (loadavg): 1.07 0.97 0.91 2/54 25169
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171479 0 0 0 15598 395 0 0 25 0 1 0 542375213 700076032 157586 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 170917 157586 603 41 0 170876 0
vsize: 683668
[startup+170.005 s]
Raw data (loadavg): 1.06 0.97 0.91 2/54 25169
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171485 0 0 0 16598 395 0 0 25 0 1 0 542375213 700076032 157592 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 170917 157592 603 41 0 170876 0
vsize: 683668
[startup+180.005 s]
Raw data (loadavg): 1.05 0.97 0.91 2/54 25169
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171488 0 0 0 17598 395 0 0 25 0 1 0 542375213 700076032 157595 4294967295 134512640 134672761 3221224544 3221223712 134564705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 170917 157595 603 41 0 170876 0
vsize: 683668
[startup+190.005 s]
Raw data (loadavg): 1.04 0.97 0.91 2/54 25169
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171489 0 0 0 18598 395 0 0 25 0 1 0 542375213 700194816 157596 4294967295 134512640 134672761 3221224544 3221223720 134553585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 170946 157596 603 41 0 170905 0
vsize: 683784
[startup+200.005 s]
Raw data (loadavg): 1.04 0.97 0.91 2/54 25169
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171495 0 0 0 19599 395 0 0 25 0 1 0 542375213 700194816 157602 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 170946 157602 603 41 0 170905 0
vsize: 683784
[startup+210.005 s]
Raw data (loadavg): 1.03 0.97 0.91 2/54 25171
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171500 0 0 0 20599 395 0 0 25 0 1 0 542375213 700194816 157607 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 170946 157607 603 41 0 170905 0
vsize: 683784
[startup+220.009 s]
Raw data (loadavg): 1.02 0.97 0.91 2/54 25171
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171505 0 0 0 21599 395 0 0 25 0 1 0 542375213 700194816 157612 4294967295 134512640 134672761 3221224544 3221223844 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 170946 157612 603 41 0 170905 0
vsize: 683784
[startup+230.009 s]
Raw data (loadavg): 1.02 0.97 0.91 2/54 25171
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171505 0 0 0 22599 395 0 0 25 0 1 0 542375213 700194816 157612 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 170946 157612 603 41 0 170905 0
vsize: 683784
[startup+240.009 s]
Raw data (loadavg): 1.02 0.97 0.91 2/54 25171
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171506 0 0 0 23599 395 0 0 25 0 1 0 542375213 700194816 157613 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 170946 157613 603 41 0 170905 0
vsize: 683784
[startup+250.009 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 25171
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171512 0 0 0 24599 395 0 0 25 0 1 0 542375213 700194816 157619 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 170946 157619 603 41 0 170905 0
vsize: 683784
[startup+260.009 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 25171
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171517 0 0 0 25600 395 0 0 25 0 1 0 542375213 700194816 157624 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 170946 157624 603 41 0 170905 0
vsize: 683784
[startup+270.01 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 25171
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171520 0 0 0 26600 395 0 0 25 0 1 0 542375213 700321792 157627 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 170977 157627 603 41 0 170936 0
vsize: 683908
[startup+280.01 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 25171
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171522 0 0 0 27600 395 0 0 25 0 1 0 542375213 700321792 157629 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 170977 157629 603 41 0 170936 0
vsize: 683908
[startup+290.01 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 25171
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171524 0 0 0 28600 395 0 0 25 0 1 0 542375213 700321792 157631 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 170977 157631 603 41 0 170936 0
vsize: 683908
[startup+300.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25171
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171528 0 0 0 29600 395 0 0 25 0 1 0 542375213 700321792 157635 4294967295 134512640 134672761 3221224544 3221223844 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 170977 157635 603 41 0 170936 0
vsize: 683908
[startup+310.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25171
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171530 0 0 0 30600 395 0 0 25 0 1 0 542375213 700321792 157637 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 170977 157637 603 41 0 170936 0
vsize: 683908
[startup+320.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25171
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171533 0 0 0 31600 395 0 0 25 0 1 0 542375213 700321792 157640 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 170977 157640 603 41 0 170936 0
vsize: 683908
[startup+330.011 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25171
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171539 0 0 0 32600 395 0 0 25 0 1 0 542375213 700321792 157646 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 170977 157646 603 41 0 170936 0
vsize: 683908
[startup+340.011 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25171
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171545 0 0 0 33600 396 0 0 25 0 1 0 542375213 700321792 157652 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 170977 157652 603 41 0 170936 0
vsize: 683908
[startup+350.012 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25171
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171556 0 0 0 34600 396 0 0 25 0 1 0 542375213 700456960 157663 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171010 157663 603 41 0 170969 0
vsize: 684040
[startup+360.011 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25171
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171560 0 0 0 35600 396 0 0 25 0 1 0 542375213 700456960 157667 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171010 157667 603 41 0 170969 0
vsize: 684040
[startup+370.012 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25171
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171566 0 0 0 36601 396 0 0 25 0 1 0 542375213 700456960 157673 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171010 157673 603 41 0 170969 0
vsize: 684040
[startup+380.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25171
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171568 0 0 0 37601 396 0 0 25 0 1 0 542375213 700456960 157675 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171010 157675 603 41 0 170969 0
vsize: 684040
[startup+390.012 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25171
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171570 0 0 0 38601 396 0 0 25 0 1 0 542375213 700456960 157677 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171010 157677 603 41 0 170969 0
vsize: 684040
[startup+400.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25171
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171576 0 0 0 39601 396 0 0 25 0 1 0 542375213 700456960 157683 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171010 157683 603 41 0 170969 0
vsize: 684040
[startup+410.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25171
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171578 0 0 0 40601 396 0 0 25 0 1 0 542375213 700456960 157685 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171010 157685 603 41 0 170969 0
vsize: 684040
[startup+420.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25171
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171580 0 0 0 41601 396 0 0 25 0 1 0 542375213 700456960 157687 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171010 157687 603 41 0 170969 0
vsize: 684040
[startup+430.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25171
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171583 0 0 0 42602 396 0 0 25 0 1 0 542375213 700456960 157690 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171010 157690 603 41 0 170969 0
vsize: 684040
[startup+440.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25171
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171588 0 0 0 43602 397 0 0 25 0 1 0 542375213 700592128 157695 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171043 157695 603 41 0 171002 0
vsize: 684172
[startup+450.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25171
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171594 0 0 0 44602 397 0 0 25 0 1 0 542375213 700592128 157701 4294967295 134512640 134672761 3221224544 3221223744 134557887 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171043 157701 603 41 0 171002 0
vsize: 684172
[startup+460.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25171
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171596 0 0 0 45602 397 0 0 25 0 1 0 542375213 700592128 157703 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171043 157703 603 41 0 171002 0
vsize: 684172
[startup+470.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25171
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171620 0 0 0 46602 397 0 0 25 0 1 0 542375213 700592128 157727 4294967295 134512640 134672761 3221224544 3221223744 134557913 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171043 157727 603 41 0 171002 0
vsize: 684172
[startup+480.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25171
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171623 0 0 0 47602 397 0 0 25 0 1 0 542375213 700592128 157730 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171043 157730 603 41 0 171002 0
vsize: 684172
[startup+490.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25173
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171627 0 0 0 48602 397 0 0 25 0 1 0 542375213 700592128 157734 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171043 157734 603 41 0 171002 0
vsize: 684172
[startup+500.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25173
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171629 0 0 0 49603 397 0 0 25 0 1 0 542375213 700592128 157736 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171043 157736 603 41 0 171002 0
vsize: 684172
[startup+510.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25173
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171633 0 0 0 50603 397 0 0 25 0 1 0 542375213 700592128 157740 4294967295 134512640 134672761 3221224544 3221223844 134556627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171043 157740 603 41 0 171002 0
vsize: 684172
[startup+520.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25173
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171634 0 0 0 51603 397 0 0 25 0 1 0 542375213 700715008 157741 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171073 157741 603 41 0 171032 0
vsize: 684292
[startup+530.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25173
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171636 0 0 0 52603 397 0 0 25 0 1 0 542375213 700715008 157743 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171073 157743 603 41 0 171032 0
vsize: 684292
[startup+540.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25173
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171638 0 0 0 53603 397 0 0 25 0 1 0 542375213 700715008 157745 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171073 157745 603 41 0 171032 0
vsize: 684292
[startup+550.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25173
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171644 0 0 0 54603 397 0 0 25 0 1 0 542375213 700715008 157751 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171073 157751 603 41 0 171032 0
vsize: 684292
[startup+560.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25173
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171645 0 0 0 55603 397 0 0 25 0 1 0 542375213 700715008 157752 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171073 157752 603 41 0 171032 0
vsize: 684292
[startup+570.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25173
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171649 0 0 0 56603 397 0 0 25 0 1 0 542375213 700715008 157756 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171073 157756 603 41 0 171032 0
vsize: 684292
[startup+580.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25173
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171656 0 0 0 57604 397 0 0 25 0 1 0 542375213 700715008 157763 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171073 157763 603 41 0 171032 0
vsize: 684292
[startup+590.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25173
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171659 0 0 0 58604 397 0 0 25 0 1 0 542375213 700715008 157766 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171073 157766 603 41 0 171032 0
vsize: 684292
[startup+600.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25173
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171663 0 0 0 59604 397 0 0 25 0 1 0 542375213 700715008 157770 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171073 157770 603 41 0 171032 0
vsize: 684292
[startup+610.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25173
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171664 0 0 0 60604 397 0 0 25 0 1 0 542375213 700846080 157771 4294967295 134512640 134672761 3221224544 3221223680 134560557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171105 157771 603 41 0 171064 0
vsize: 684420
[startup+620.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25173
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171673 0 0 0 61604 397 0 0 25 0 1 0 542375213 700846080 157780 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171105 157780 603 41 0 171064 0
vsize: 684420
[startup+630.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25173
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171681 0 0 0 62604 397 0 0 25 0 1 0 542375213 700846080 157788 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171105 157788 603 41 0 171064 0
vsize: 684420
[startup+640.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25173
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171683 0 0 0 63604 397 0 0 25 0 1 0 542375213 700846080 157790 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171105 157790 603 41 0 171064 0
vsize: 684420
[startup+650.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25173
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171686 0 0 0 64604 397 0 0 25 0 1 0 542375213 700846080 157793 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171105 157793 603 41 0 171064 0
vsize: 684420
[startup+660.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25173
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171690 0 0 0 65605 397 0 0 25 0 1 0 542375213 700846080 157797 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171105 157797 603 41 0 171064 0
vsize: 684420
[startup+670.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25173
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171692 0 0 0 66605 398 0 0 25 0 1 0 542375213 700846080 157799 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171105 157799 603 41 0 171064 0
vsize: 684420
[startup+680.018 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25173
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171695 0 0 0 67605 398 0 0 25 0 1 0 542375213 700846080 157802 4294967295 134512640 134672761 3221224544 3221223712 134564502 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171105 157802 603 41 0 171064 0
vsize: 684420
[startup+690.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25173
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171698 0 0 0 68605 398 0 0 25 0 1 0 542375213 700977152 157805 4294967295 134512640 134672761 3221224544 3221223712 134564738 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171137 157805 603 41 0 171096 0
vsize: 684548
[startup+700.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25173
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171700 0 0 0 69605 398 0 0 25 0 1 0 542375213 700977152 157807 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171137 157807 603 41 0 171096 0
vsize: 684548
[startup+710.018 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25173
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171703 0 0 0 70605 398 0 0 25 0 1 0 542375213 700977152 157810 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171137 157810 603 41 0 171096 0
vsize: 684548
[startup+720.018 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25173
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171704 0 0 0 71606 398 0 0 25 0 1 0 542375213 700977152 157811 4294967295 134512640 134672761 3221224544 3221223724 134565156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171137 157811 603 41 0 171096 0
vsize: 684548
[startup+730.018 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25173
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171707 0 0 0 72606 398 0 0 25 0 1 0 542375213 700977152 157814 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171137 157814 603 41 0 171096 0
vsize: 684548
[startup+740.018 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25173
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171709 0 0 0 73606 398 0 0 25 0 1 0 542375213 700977152 157816 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171137 157816 603 41 0 171096 0
vsize: 684548
[startup+750.018 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25173
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171711 0 0 0 74606 398 0 0 25 0 1 0 542375213 700977152 157818 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171137 157818 603 41 0 171096 0
vsize: 684548
[startup+760.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25173
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171713 0 0 0 75606 398 0 0 25 0 1 0 542375213 700977152 157820 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171137 157820 603 41 0 171096 0
vsize: 684548
[startup+770.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25173
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171717 0 0 0 76606 398 0 0 25 0 1 0 542375213 700977152 157824 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171137 157824 603 41 0 171096 0
vsize: 684548
[startup+780.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25173
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171721 0 0 0 77607 398 0 0 25 0 1 0 542375213 700977152 157828 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171137 157828 603 41 0 171096 0
vsize: 684548
[startup+790.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25173
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171725 0 0 0 78607 398 0 0 25 0 1 0 542375213 700977152 157832 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171137 157832 603 41 0 171096 0
vsize: 684548
[startup+800.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25173
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171728 0 0 0 79607 398 0 0 25 0 1 0 542375213 701108224 157835 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171169 157835 603 41 0 171128 0
vsize: 684676
[startup+810.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25173
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171730 0 0 0 80607 398 0 0 25 0 1 0 542375213 701108224 157837 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171169 157837 603 41 0 171128 0
vsize: 684676
[startup+820.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25173
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171735 0 0 0 81607 398 0 0 25 0 1 0 542375213 701108224 157842 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171169 157842 603 41 0 171128 0
vsize: 684676
[startup+830.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25173
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171741 0 0 0 82607 398 0 0 25 0 1 0 542375213 701108224 157848 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171169 157848 603 41 0 171128 0
vsize: 684676
[startup+840.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25173
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171745 0 0 0 83607 398 0 0 25 0 1 0 542375213 701108224 157852 4294967295 134512640 134672761 3221224544 3221223728 134559041 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171169 157852 603 41 0 171128 0
vsize: 684676
[startup+850.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25173
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171748 0 0 0 84608 398 0 0 25 0 1 0 542375213 701108224 157855 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171169 157855 603 41 0 171128 0
vsize: 684676
[startup+860.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25173
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171751 0 0 0 85608 398 0 0 25 0 1 0 542375213 701108224 157858 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171169 157858 603 41 0 171128 0
vsize: 684676
[startup+870.021 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25173
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171755 0 0 0 86608 398 0 0 25 0 1 0 542375213 701108224 157862 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171169 157862 603 41 0 171128 0
vsize: 684676
[startup+880.022 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25173
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171756 0 0 0 87608 398 0 0 25 0 1 0 542375213 701108224 157863 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171169 157863 603 41 0 171128 0
vsize: 684676
[startup+890.022 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25173
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171757 0 0 0 88609 398 0 0 25 0 1 0 542375213 701108224 157864 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171169 157864 603 41 0 171128 0
vsize: 684676
[startup+900.023 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25173
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171762 0 0 0 89609 398 0 0 25 0 1 0 542375213 701243392 157869 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171202 157869 603 41 0 171161 0
vsize: 684808
[startup+910.023 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25173
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171766 0 0 0 90609 398 0 0 25 0 1 0 542375213 701243392 157873 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171202 157873 603 41 0 171161 0
vsize: 684808
[startup+920.024 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25173
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171767 0 0 0 91609 398 0 0 25 0 1 0 542375213 701243392 157874 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171202 157874 603 41 0 171161 0
vsize: 684808
[startup+930.024 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25173
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171770 0 0 0 92609 398 0 0 25 0 1 0 542375213 701243392 157877 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171202 157877 603 41 0 171161 0
vsize: 684808
[startup+940.024 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25173
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171776 0 0 0 93609 399 0 0 25 0 1 0 542375213 701243392 157883 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171202 157883 603 41 0 171161 0
vsize: 684808
[startup+950.025 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25173
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171777 0 0 0 94609 399 0 0 25 0 1 0 542375213 701243392 157884 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171202 157884 603 41 0 171161 0
vsize: 684808
[startup+960.025 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25173
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171781 0 0 0 95609 399 0 0 25 0 1 0 542375213 701243392 157888 4294967295 134512640 134672761 3221224544 3221223712 134560968 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171202 157888 603 41 0 171161 0
vsize: 684808
[startup+970.026 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25173
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171788 0 0 0 96609 399 0 0 25 0 1 0 542375213 701243392 157895 4294967295 134512640 134672761 3221224544 3221223680 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171202 157895 603 41 0 171161 0
vsize: 684808
[startup+980.026 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25173
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171793 0 0 0 97609 399 0 0 25 0 1 0 542375213 701378560 157900 4294967295 134512640 134672761 3221224544 3221223712 134560828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171235 157900 603 41 0 171194 0
vsize: 684940
[startup+990.025 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25173
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171798 0 0 0 98609 399 0 0 25 0 1 0 542375213 701378560 157905 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171235 157905 603 41 0 171194 0
vsize: 684940
[startup+1000.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25173
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171805 0 0 0 99609 399 0 0 25 0 1 0 542375213 701378560 157912 4294967295 134512640 134672761 3221224544 3221223712 134560864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171235 157912 603 41 0 171194 0
vsize: 684940
[startup+1010.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25173
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171812 0 0 0 100609 399 0 0 25 0 1 0 542375213 701378560 157919 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171235 157919 603 41 0 171194 0
vsize: 684940
[startup+1020.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25173
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171815 0 0 0 101609 399 0 0 25 0 1 0 542375213 701378560 157922 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171235 157922 603 41 0 171194 0
vsize: 684940
[startup+1030.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25173
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171819 0 0 0 102610 399 0 0 25 0 1 0 542375213 701378560 157926 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171235 157926 603 41 0 171194 0
vsize: 684940
[startup+1040.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25173
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171822 0 0 0 103610 400 0 0 25 0 1 0 542375213 701378560 157929 4294967295 134512640 134672761 3221224544 3221223712 134561378 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171235 157929 603 41 0 171194 0
vsize: 684940
[startup+1050.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25173
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171825 0 0 0 104610 400 0 0 25 0 1 0 542375213 701509632 157932 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171267 157932 603 41 0 171226 0
vsize: 685068
[startup+1060.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25173
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171827 0 0 0 105610 400 0 0 25 0 1 0 542375213 701509632 157934 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171267 157934 603 41 0 171226 0
vsize: 685068
[startup+1070.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25173
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171831 0 0 0 106610 400 0 0 25 0 1 0 542375213 701509632 157938 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171267 157938 603 41 0 171226 0
vsize: 685068
[startup+1080.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25173
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171838 0 0 0 107610 400 0 0 25 0 1 0 542375213 701509632 157945 4294967295 134512640 134672761 3221224544 3221223744 134557828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171267 157945 603 41 0 171226 0
vsize: 685068
[startup+1090.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25173
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171841 0 0 0 108610 400 0 0 25 0 1 0 542375213 701509632 157948 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171267 157948 603 41 0 171226 0
vsize: 685068
[startup+1100.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25173
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171844 0 0 0 109611 400 0 0 25 0 1 0 542375213 701509632 157951 4294967295 134512640 134672761 3221224544 3221223712 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+1110.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25173
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171846 0 0 0 110611 400 0 0 25 0 1 0 542375213 701509632 157953 4294967295 134512640 134672761 3221224544 3221223712 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+1120.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25173
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171851 0 0 0 111611 400 0 0 25 0 1 0 542375213 701509632 157958 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171267 157958 603 41 0 171226 0
vsize: 685068
[startup+1130.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25173
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171855 0 0 0 112611 400 0 0 25 0 1 0 542375213 701509632 157962 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171267 157962 603 41 0 171226 0
vsize: 685068
[startup+1140.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25173
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171860 0 0 0 113611 400 0 0 25 0 1 0 542375213 701640704 157967 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171299 157967 603 41 0 171258 0
vsize: 685196
[startup+1150.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25173
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171865 0 0 0 114612 400 0 0 25 0 1 0 542375213 701640704 157972 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171299 157972 603 41 0 171258 0
vsize: 685196
[startup+1160.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25173
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171869 0 0 0 115612 400 0 0 25 0 1 0 542375213 701640704 157976 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171299 157976 603 41 0 171258 0
vsize: 685196
[startup+1170.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25173
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171874 0 0 0 116612 400 0 0 25 0 1 0 542375213 701640704 157981 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171299 157981 603 41 0 171258 0
vsize: 685196
[startup+1180.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25173
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171886 0 0 0 117612 400 0 0 25 0 1 0 542375213 701640704 157993 4294967295 134512640 134672761 3221224544 3221223708 134561028 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171299 157993 603 41 0 171258 0
vsize: 685196
[startup+1190.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25173
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171890 0 0 0 118612 400 0 0 25 0 1 0 542375213 701640704 157997 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171299 157997 603 41 0 171258 0
vsize: 685196
[startup+1200.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 25173
Raw data (stat): 25116 (minisat+) R 25115 28546 28545 0 -1 0 171895 0 0 0 119612 400 0 0 25 0 1 0 542375213 701640704 158002 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 171299 158002 603 41 0 171258 0
vsize: 685196
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.35 s]
Raw data (loadavg): 1.00 0.97 0.91 1/54 25173
Raw data (stat): 25116 (minisat+) Z 25115 28546 28545 0 -1 12 171898 0 0 0 119612 432 0 0 25 0 1 0 542375213 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.45
CPU user time (s): 1196.13
CPU system time (s): 4.32534
CPU usage (%): 100.009
Max. virtual memory (Kb): 685196
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####