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/plato.asu.edu/pub/milp/normalized-mps-v2-13-7-neos5.opb
MD5SUM	4f5f6e30a602f3968daa9ca41c7da043
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	2058
Optimality of the best value was proved	NO
Number of terms in the objective function	133
Biggest coefficient in the objective function	128
Number of bits for the biggest coefficient in the objective function	8
Sum of the numbers in the objective function	9334
Number of bits of the sum of numbers in the objective function	14
Biggest number in a constraint	1024
Number of bits of the biggest number in a constraint	11
Biggest sum of numbers in a constraint	9334
Number of bits of the biggest sum of numbers	14
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.05284
Number of variables	133
Total number of constraints	126
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	56
Number of constraints which are nor clauses,nor cardinality constraints	70
Minimum length of a constraint	1
Maximum length of a constraint	81
Trace number 14077

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc31 THE 2005-04-20 22:50:11 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=19713 boxname=wulflinc31 idbench=1517 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  4f5f6e30a602f3968daa9ca41c7da043  /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-13-7-neos5.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-13-7-neos5.opb
IDLAUNCH: 19713
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.153
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.153
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:        506976 kB
Buffers:         32092 kB
Cached:         458960 kB
SwapCached:        588 kB
Active:          68172 kB
Inactive:       424972 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        506724 kB
SwapTotal:     2097892 kB
SwapFree:      2096468 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           5100 kB
Slab:            28904 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-20 23:10:13 (client local time) WITH STATUS 10 IN 1200.35 SECONDS
stats: 19713 7 1200.35 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 73 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[  72]---> BDD-cost:    7
c ---[  71]---> BDD-cost:    7
c ---[  70]---> BDD-cost:    7
c ---[  69]---> BDD-cost:    7
c ---[  68]---> BDD-cost:    7
c ---[  67]---> BDD-cost:    7
c ---[  66]---> BDD-cost:    7
c ---[  65]---> BDD-cost:    7
c ---[  64]---> BDD-cost:    7
c ---[  63]---> BDD-cost:    7
c ---[  62]---> Sorter-cost:  382     Base:
c ---[  61]---> Sorter-cost:  717     Base: 2 2 2 2 2 2 2
c ---[  60]---> Sorter-cost:  417     Base: 2 2 2 2 2 2 2
c ---[  59]---> Sorter-cost: 1147     Base: 2 2 2 2 2 2 2
c ---[  58]---> Sorter-cost:  868     Base: 2 2 2 2 2 2 2
c ---[  57]---> Sorter-cost:  429     Base: 2 2 2 2 2 2 2
c ---[  56]---> Sorter-cost:  989     Base: 2 2 2 2 2 2 2
c ---[  55]---> Sorter-cost:  866     Base: 2 2 2 2 2 2 2
c ---[  54]---> Sorter-cost:  898     Base: 2 2 2 2 2 2 2
c ---[  53]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2
c ---[  52]---> Sorter-cost: 1011     Base: 2 2 2 2 2 2 2
c ---[  51]---> Sorter-cost:  216     Base:
c ---[  50]---> Sorter-cost:  856     Base: 2 2 2 2 2 2 2
c ---[  49]---> Sorter-cost: 1043     Base: 2 2 2 2 2 2 2
c ---[  48]---> Sorter-cost:  488     Base: 2 2 2 2 2 2 2
c ---[  47]---> Sorter-cost:  329     Base: 2 2 2 2 2 2 2
c ---[  46]---> Sorter-cost:  373     Base: 2 2 2 2 2 2 2
c ---[  45]---> Sorter-cost:  405     Base: 2 2 2 2 2 2 2
c ---[  44]---> Sorter-cost:  343     Base: 2 2 2 2 2 2 2
c ---[  43]---> Sorter-cost:  365     Base: 2 2 2 2 2 2 2
c ---[  42]---> Sorter-cost:  397     Base: 2 2 2 2 2 2 2
c ---[  41]---> Sorter-cost:  379     Base: 2 2 2 2 2 2 2
c ---[  40]---> Sorter-cost:  351     Base: 2 2 2 2 2 2 2
c ---[  39]---> Sorter-cost:  399     Base: 2 2 2 2 2 2 2
c ---[  38]---> Sorter-cost:  955     Base: 2 2 2 2 2 2 2
c ---[  37]---> Sorter-cost:  345     Base: 2 2 2 2 2 2 2
c ---[  36]---> Sorter-cost:  365     Base: 2 2 2 2 2 2 2
c ---[  35]---> Sorter-cost:  397     Base: 2 2 2 2 2 2 2
c ---[  34]---> Sorter-cost:  379     Base: 2 2 2 2 2 2 2
c ---[  33]---> Sorter-cost:  399     Base: 2 2 2 2 2 2 2
c ---[  32]---> Sorter-cost:  969     Base: 2 2 2 2 2 2 2
c ---[  31]---> Sorter-cost:  405     Base: 2 2 2 2 2 2 2
c ---[  30]---> Sorter-cost:  417     Base: 2 2 2 2 2 2 2
c ---[  29]---> Sorter-cost:  311     Base: 2 2 2 2 2 2 2
c ---[  28]---> Sorter-cost:  828     Base: 2 2 2 2 2 2 2
c ---[  27]---> Sorter-cost: 1013     Base: 2 2 2 2 2 2 2
c ---[  26]---> Sorter-cost:  337     Base: 2 2 2 2 2 2 2
c ---[  25]---> Sorter-cost:  329     Base: 2 2 2 2 2 2 2
c ---[  24]---> Sorter-cost:  319     Base: 2 2 2 2 2 2 2
c ---[  23]---> Sorter-cost:  365     Base: 2 2 2 2 2 2 2
c ---[  22]---> Sorter-cost:  397     Base: 2 2 2 2 2 2 2
c ---[  21]---> Sorter-cost:  329     Base: 2 2 2 2 2 2 2
c ---[  20]---> Sorter-cost:  319     Base: 2 2 2 2 2 2 2
c ---[  19]---> Sorter-cost:  365     Base: 2 2 2 2 2 2 2
c ---[  18]---> Sorter-cost:  319     Base: 2 2 2 2 2 2 2
c ---[  17]---> Sorter-cost:  397     Base: 2 2 2 2 2 2 2
c ---[  16]---> Sorter-cost:  329     Base: 2 2 2 2 2 2 2
c ---[  15]---> Sorter-cost:  355     Base: 2 2 2 2 2 2 2
c ---[  14]---> Sorter-cost:  387     Base: 2 2 2 2 2 2 2
c ---[  13]---> Sorter-cost:  389     Base: 2 2 2 2 2 2 2
c ---[  12]---> Sorter-cost:  409     Base: 2 2 2 2 2 2 2
c ---[  11]---> Sorter-cost:  810     Base: 2 2 2 2 2 2 2
c ---[  10]---> Sorter-cost:  329     Base: 2 2 2 2 2 2 2
c ---[   9]---> Sorter-cost:  329     Base: 2 2 2 2 2 2 2
c ---[   8]---> Sorter-cost:  319     Base: 2 2 2 2 2 2 2
c ---[   7]---> Sorter-cost:  319     Base: 2 2 2 2 2 2 2
c ---[   6]---> Sorter-cost:  329     Base: 2 2 2 2 2 2 2
c ---[   5]---> Sorter-cost:  355     Base: 2 2 2 2 2 2 2
c ---[   4]---> Sorter-cost:  387     Base: 2 2 2 2 2 2 2
c ---[   3]---> Sorter-cost:  319     Base: 2 2 2 2 2 2 2
c ---[   2]---> Sorter-cost:  130     Base:
c ---[   1]---> Sorter-cost:  301     Base: 2 2 2 2 2 2 2
c ---[   0]---> Sorter-cost:  301     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   25058    60127 |    8352       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 7865[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 2067     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         2 |   29745    71113 |    9915       2       22    11.0 |  0.000 % |
c ==============================================================================
c [1mFound solution: 4982[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        57 |   29959    71656 |    9986      57      225     3.9 |  0.000 % |
c ==============================================================================
c [1mFound solution: 4278[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       104 |   30029    71844 |   10009     104      412     4.0 |  0.000 % |
c ==============================================================================
c [1mFound solution: 3709[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       122 |   30077    71967 |   10025     122      476     3.9 |  0.000 % |
c ==============================================================================
c [1mFound solution: 3587[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       129 |   30088    71998 |   10029     129      559     4.3 |  0.000 % |
c ==============================================================================
c [1mFound solution: 2685[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       213 |   30158    72168 |   10052     213     1235     5.8 |  0.000 % |
c ==============================================================================
c [1mFound solution: 2654[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       235 |   30170    72207 |   10056     235     1355     5.8 |  0.000 % |
c ==============================================================================
c [1mFound solution: 2646[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       244 |   30177    72225 |   10059     244     1386     5.7 |  0.000 % |
c ==============================================================================
c [1mFound solution: 2645[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       244 |   30184    72243 |   10061     244     1386     5.7 |  0.000 % |
c ==============================================================================
c [1mFound solution: 2642[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       244 |   30194    72272 |   10064     244     1386     5.7 |  0.000 % |
c ==============================================================================
c [1mFound solution: 2641[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       244 |   30203    72294 |   10067     244     1386     5.7 |  0.000 % |
c ==============================================================================
c [1mFound solution: 2581[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       244 |   30207    72303 |   10069     244     1386     5.7 |  0.000 % |
c ==============================================================================
c [1mFound solution: 2578[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       244 |   30211    72312 |   10070     244     1386     5.7 |  0.000 % |
c ==============================================================================
c [1mFound solution: 2577[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       244 |   30215    72321 |   10071     244     1386     5.7 |  0.000 % |
c ==============================================================================
c [1mFound solution: 2575[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       257 |   30221    72335 |   10073     257     1482     5.8 |  0.000 % |
c ==============================================================================
c [1mFound solution: 2562[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       283 |   30228    72351 |   10076     283     1645     5.8 |  0.000 % |
c |       383 |   30228    72351 |   11083     383     2370     6.2 |  0.519 % |
c |       533 |   30222    72339 |   12191     532     3734     7.0 |  0.535 % |
c ==============================================================================
c [1mFound solution: 2433[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       539 |   30243    72391 |   10081     538     3828     7.1 |  0.535 % |
c ==============================================================================
c [1mFound solution: 2432[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       568 |   30255    72425 |   10085     567     4202     7.4 |  0.535 % |
c ==============================================================================
c [1mFound solution: 2304[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       599 |   30265    72449 |   10088     598     4520     7.6 |  0.535 % |
c |       701 |   30265    72449 |   11096     700     5583     8.0 |  0.551 % |
c |       853 |   30265    72449 |   12206     852     8308     9.8 |  0.551 % |
c |      1079 |   30265    72449 |   13427    1078    11040    10.2 |  0.551 % |
c |      1416 |   30265    72449 |   14769    1415    16310    11.5 |  0.551 % |
c ==============================================================================
c [1mFound solution: 2303[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1905 |   30271    72462 |   10090    1904    21674    11.4 |  0.551 % |
c |      2009 |   30269    72458 |   11099    2005    22744    11.3 |  0.562 % |
c |      2160 |   30269    72458 |   12208    2156    25543    11.8 |  0.562 % |
c |      2385 |   30259    72437 |   13429    2358    28130    11.9 |  0.594 % |
c |      2724 |   30258    72434 |   14772    2672    35247    13.2 |  0.599 % |
c ==============================================================================
c [1mFound solution: 2302[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2936 |   30263    72445 |   10087    2884    40313    14.0 |  0.599 % |
c |      3038 |   30263    72445 |   11095    2986    41318    13.8 |  0.605 % |
c |      3188 |   30263    72445 |   12205    3136    43360    13.8 |  0.605 % |
c |      3414 |   30263    72445 |   13425    3362    47053    14.0 |  0.605 % |
c ==============================================================================
c [1mFound solution: 2280[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3647 |   30287    72507 |   10095    3595    50008    13.9 |  0.605 % |
c |      3747 |   30287    72507 |   11104    3695    52982    14.3 |  0.615 % |
c |      3897 |   30287    72507 |   12214    3845    55042    14.3 |  0.615 % |
c ==============================================================================
c [1mFound solution: 2278[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4089 |   30295    72532 |   10098    4037    60000    14.9 |  0.615 % |
c |      4189 |   30293    72528 |   11107    4136    61270    14.8 |  0.626 % |
c |      4340 |   30293    72528 |   12218    4287    62565    14.6 |  0.626 % |
c |      4565 |   30293    72528 |   13440    4512    68337    15.1 |  0.626 % |
c |      4905 |   30293    72528 |   14784    4852    84491    17.4 |  0.626 % |
c |      5411 |   30293    72528 |   16262    5358    96213    18.0 |  0.626 % |
c |      6170 |   30287    72514 |   17889    6098   112050    18.4 |  0.647 % |
c ==============================================================================
c [1mFound solution: 2228[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6491 |   30294    72533 |   10098    6419   118900    18.5 |  0.647 % |
c |      6591 |   30294    72533 |   11107    6519   121991    18.7 |  0.652 % |
c |      6742 |   30294    72533 |   12218    6670   123908    18.6 |  0.652 % |
c |      6967 |   30294    72533 |   13440    6895   128894    18.7 |  0.652 % |
c |      7304 |   30294    72533 |   14784    7232   135222    18.7 |  0.652 % |
c |      7810 |   30294    72533 |   16262    7738   154229    19.9 |  0.652 % |
c ==============================================================================
c [1mFound solution: 2163[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7969 |   30301    72554 |   10100    7897   156108    19.8 |  0.652 % |
c |      8069 |   30301    72554 |   11110    7997   158680    19.8 |  0.658 % |
c |      8219 |   30301    72554 |   12221    8147   164256    20.2 |  0.658 % |
c |      8444 |   30301    72554 |   13443    8372   168166    20.1 |  0.658 % |
c ==============================================================================
c [1mFound solution: 2049[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8508 |   30308    72569 |   10102    8436   171099    20.3 |  0.658 % |
c |      8608 |   30308    72569 |   11112    8536   173093    20.3 |  0.663 % |
c |      8760 |   30308    72569 |   12223    8688   176166    20.3 |  0.663 % |
c |      8985 |   30308    72569 |   13445    8913   183116    20.5 |  0.663 % |
c |      9322 |   30308    72569 |   14790    9250   209552    22.7 |  0.663 % |
c ==============================================================================
c [1mFound solution: 2048[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9770 |   30304    72561 |   10101    9696   232110    23.9 |  0.663 % |
c |      9871 |   30304    72561 |   11111    9797   233194    23.8 |  0.690 % |
c |     10021 |   30304    72561 |   12222    9947   238904    24.0 |  0.690 % |
c |     10246 |   30304    72561 |   13444   10172   243667    24.0 |  0.690 % |
c |     10584 |   30304    72561 |   14788   10510   257383    24.5 |  0.690 % |
c |     11090 |   30304    72561 |   16267   11016   272958    24.8 |  0.690 % |
c |     11849 |   30304    72561 |   17894   11775   305277    25.9 |  0.690 % |
c |     12988 |   30304    72561 |   19683   12914   325888    25.2 |  0.690 % |
c |     14697 |   30304    72561 |   21652   14623   466104    31.9 |  0.690 % |
c |     17260 |   30289    72526 |   23817   17110   529488    30.9 |  0.717 % |
c ==============================================================================
c [1mFound solution: 2042[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20917 |   30278    72502 |   10092   20754   676782    32.6 |  0.717 % |
c |     21017 |   30278    72502 |   11101    5289   123412    23.3 |  0.781 % |
c |     21167 |   30278    72502 |   12211    5439   126170    23.2 |  0.781 % |
c |     21393 |   30278    72502 |   13432    5665   129534    22.9 |  0.781 % |
c |     21730 |   30278    72502 |   14775    6002   155817    26.0 |  0.781 % |
c |     22236 |   30278    72502 |   16253    6508   178176    27.4 |  0.781 % |
c |     22995 |   30278    72502 |   17878    7267   199606    27.5 |  0.781 % |
c |     24137 |   30276    72498 |   19666    8408   238458    28.4 |  0.787 % |
c |     25845 |   30276    72498 |   21633   10116   276591    27.3 |  0.787 % |
c |     28408 |   30276    72498 |   23796   12679   426829    33.7 |  0.787 % |
c |     32252 |   30276    72498 |   26176   16523   540088    32.7 |  0.787 % |
c ==============================================================================
c [1mFound solution: 2040[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     37912 |   30282    72511 |   10094   22183   733704    33.1 |  0.787 % |
c |     38015 |   30282    72511 |   11103    5650   122697    21.7 |  0.792 % |
c |     38165 |   30282    72511 |   12213    5800   128333    22.1 |  0.792 % |
c |     38390 |   30282    72511 |   13435    6025   138366    23.0 |  0.792 % |
c |     38727 |   30282    72511 |   14778    6362   150039    23.6 |  0.792 % |
c |     39234 |   30282    72511 |   16256    6869   168341    24.5 |  0.792 % |
c |     39995 |   30282    72511 |   17882    7630   190345    24.9 |  0.792 % |
c |     41137 |   30282    72511 |   19670    8772   221960    25.3 |  0.792 % |
c |     42846 |   30282    72511 |   21637   10481   293277    28.0 |  0.792 % |
c |     45409 |   30282    72511 |   23801   13044   470017    36.0 |  0.792 % |
c |     49257 |   30282    72511 |   26181   16892   662441    39.2 |  0.792 % |
c ==============================================================================
c [1mFound solution: 2038[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     50921 |   30293    72537 |   10097   18556   729401    39.3 |  0.792 % |
c |     51021 |   30293    72537 |   11106    9378   293455    31.3 |  0.813 % |
c |     51171 |   30293    72537 |   12217    9528   298447    31.3 |  0.813 % |
c |     51396 |   30293    72537 |   13439    9753   303506    31.1 |  0.813 % |
c |     51733 |   30293    72537 |   14783   10090   316145    31.3 |  0.813 % |
c |     52240 |   30293    72537 |   16261   10597   338448    31.9 |  0.813 % |
c |     52999 |   30293    72537 |   17887   11356   372821    32.8 |  0.813 % |
c |     54138 |   30293    72537 |   19676   12495   422072    33.8 |  0.813 % |
c |     55846 |   30293    72537 |   21643   14203   509563    35.9 |  0.813 % |
c |     58408 |   30293    72537 |   23808   16765   655374    39.1 |  0.813 % |
c |     62254 |   30293    72537 |   26189   20611   938462    45.5 |  0.813 % |
c |     68021 |   30293    72537 |   28807   26378  1255036    47.6 |  0.813 % |
c |     76670 |   30293    72537 |   31688   35027  2091568    59.7 |  0.813 % |
c |     89644 |   30293    72537 |   34857   29230  2035256    69.6 |  0.813 % |
c |    109106 |   30293    72537 |   38343   24662  1710977    69.4 |  0.813 % |
c |    138298 |   30289    72528 |   42177   31620  2254632    71.3 |  0.819 % |
c |    182089 |   30289    72528 |   46395   42844  4397296   102.6 |  0.819 % |
c ==============================================================================
c [1mFound solution: 2037[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    208814 |   30294    72543 |   10098   40026  3122766    78.0 |  0.819 % |
c |    208914 |   30294    72543 |   11107    9107   453328    49.8 |  0.824 % |
c |    209066 |   30294    72543 |   12218    9259   460063    49.7 |  0.824 % |
c |    209291 |   30294    72543 |   13440    9484   473442    49.9 |  0.824 % |
c |    209628 |   30294    72543 |   14784    9821   497096    50.6 |  0.824 % |
c |    210134 |   30294    72543 |   16262   10327   513875    49.8 |  0.824 % |
c |    210893 |   30294    72543 |   17889   11086   558188    50.4 |  0.824 % |
c |    212033 |   30294    72543 |   19678   12226   646452    52.9 |  0.824 % |
c |    213742 |   30294    72543 |   21645   13935   758196    54.4 |  0.824 % |
c |    216305 |   30294    72543 |   23810   16498   885107    53.6 |  0.824 % |
c ==============================================================================
c [1mFound solution: 2036[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    217979 |   30298    72553 |   10099   18172   958657    52.8 |  0.824 % |
c |    218079 |   30298    72553 |   11108    9186   260984    28.4 |  0.829 % |
c |    218231 |   30298    72553 |   12219    9338   264238    28.3 |  0.829 % |
c |    218460 |   30298    72553 |   13441    9567   270453    28.3 |  0.829 % |
c |    218797 |   30298    72553 |   14785    9904   281067    28.4 |  0.829 % |
c |    219305 |   30298    72553 |   16264   10412   301155    28.9 |  0.829 % |
c |    220065 |   30298    72553 |   17890   11172   328923    29.4 |  0.829 % |
c |    221206 |   30298    72553 |   19680   12313   374119    30.4 |  0.829 % |
c |    222915 |   30298    72553 |   21648   14022   413782    29.5 |  0.829 % |
c ==============================================================================
c [1mFound solution: 2035[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    225286 |   30301    72560 |   10100   16393   497229    30.3 |  0.829 % |
c |    225386 |   30301    72560 |   11110    8297   146061    17.6 |  0.834 % |
c |    225538 |   30301    72560 |   12221    8449   150054    17.8 |  0.834 % |
c |    225763 |   30301    72560 |   13443    8674   154553    17.8 |  0.834 % |
c |    226100 |   30301    72560 |   14787    9011   161769    18.0 |  0.834 % |
c |    226606 |   30301    72560 |   16266    9517   181575    19.1 |  0.834 % |
c |    227366 |   30301    72560 |   17892   10277   216146    21.0 |  0.834 % |
c |    228506 |   30301    72560 |   19682   11417   261748    22.9 |  0.834 % |
c |    230214 |   30301    72560 |   21650   13125   312840    23.8 |  0.834 % |
c ==============================================================================
c [1mFound solution: 2034[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    232171 |   30305    72571 |   10101   15082   399414    26.5 |  0.834 % |
c |    232271 |   30305    72571 |   11111    7641   150076    19.6 |  0.840 % |
c |    232421 |   30298    72556 |   12222    7754   152557    19.7 |  0.861 % |
c |    232646 |   30298    72556 |   13444    7979   171379    21.5 |  0.861 % |
c |    232985 |   30298    72556 |   14788    8318   184740    22.2 |  0.861 % |
c |    233492 |   30298    72556 |   16267    8825   211213    23.9 |  0.861 % |
c |    234251 |   30298    72556 |   17894    9584   244037    25.5 |  0.861 % |
c |    235390 |   30298    72556 |   19683   10723   305332    28.5 |  0.861 % |
c |    237099 |   30298    72556 |   21652   12432   363109    29.2 |  0.861 % |
c |    239661 |   30298    72556 |   23817   14994   486752    32.5 |  0.861 % |
c |    243505 |   30298    72556 |   26199   18838   856949    45.5 |  0.861 % |
c ==============================================================================
c [1mFound solution: 2018[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    246171 |   30304    72571 |   10101   21504   948392    44.1 |  0.861 % |
c |    246272 |   30304    72571 |   11111    5477    65194    11.9 |  0.866 % |
c |    246423 |   30304    72571 |   12222    5628    67034    11.9 |  0.866 % |
c |    246648 |   30304    72571 |   13444    5853    76394    13.1 |  0.866 % |
c |    246985 |   30304    72571 |   14788    6190    92176    14.9 |  0.866 % |
c |    247491 |   30304    72571 |   16267    6696   128503    19.2 |  0.866 % |
c |    248250 |   30304    72571 |   17894    7455   161534    21.7 |  0.866 % |
c |    249389 |   30304    72571 |   19683    8594   239195    27.8 |  0.866 % |
c |    251097 |   30304    72571 |   21652   10302   363537    35.3 |  0.866 % |
c |    253660 |   30304    72571 |   23817   12865   469870    36.5 |  0.866 % |
c |    257506 |   30304    72571 |   26199   16711   628632    37.6 |  0.866 % |
c |    263273 |   30304    72571 |   28819   22478  1114326    49.6 |  0.866 % |
c |    271922 |   30304    72571 |   31701   31127  1854890    59.6 |  0.866 % |
c ==============================================================================
c [1mFound solution: 2017[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    272492 |   30310    72586 |   10103   31697  1879788    59.3 |  0.866 % |
c |    272593 |   30310    72586 |   11113    8026   239606    29.9 |  0.871 % |
c |    272743 |   30310    72586 |   12224    8176   244624    29.9 |  0.872 % |
c |    272968 |   30310    72586 |   13447    8401   248454    29.6 |  0.871 % |
c |    273305 |   30310    72586 |   14791    8738   257058    29.4 |  0.871 % |
c |    273811 |   30114    72175 |   16270    9201   282448    30.7 |  1.366 % |
c |    274571 |   30114    72175 |   17898    9961   344514    34.6 |  1.366 % |
c |    275710 |   30114    72175 |   19687   11100   419701    37.8 |  1.366 % |
c |    277419 |   30114    72175 |   21656   12809   518184    40.5 |  1.366 % |
c |    279987 |   30114    72175 |   23822   15377   725371    47.2 |  1.366 % |
c |    283832 |   30114    72175 |   26204   19222  1130563    58.8 |  1.366 % |
c |    289601 |   30114    72175 |   28825   24991  1796894    71.9 |  1.366 % |
c |    298250 |   30114    72175 |   31707   33640  2795713    83.1 |  1.366 % |
c ==============================================================================
c [1mFound solution: 2016[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    306549 |   30112    72174 |   10037   25118  1840003    73.3 |  1.366 % |
c |    306650 |   30112    72174 |   11040    6381    90787    14.2 |  1.393 % |
c |    306800 |   30112    72174 |   12144    6531    94048    14.4 |  1.393 % |
c |    307026 |   30112    72174 |   13359    6757   102663    15.2 |  1.393 % |
c |    307363 |   30112    72174 |   14695    7094   120332    17.0 |  1.393 % |
c |    307869 |   30112    72174 |   16164    7600   143661    18.9 |  1.393 % |
c |    308630 |   30112    72174 |   17781    8361   165407    19.8 |  1.393 % |
c |    309769 |   30091    72125 |   19559    9486   225158    23.7 |  1.431 % |
c |    311478 |   30091    72125 |   21515   11195   273080    24.4 |  1.431 % |
c |    314040 |   30091    72125 |   23666   13757   442865    32.2 |  1.431 % |
c |    317884 |   30091    72125 |   26033   17601   650760    37.0 |  1.431 % |
c |    323650 |   30080    72102 |   28636   23363   995344    42.6 |  1.452 % |
c |    332299 |   30058    72055 |   31500   15252   514538    33.7 |  1.500 % |
c |    345274 |   30058    72055 |   34650   28227  1015690    36.0 |  1.501 % |
c ==============================================================================
c [1mFound solution: 1987[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    348188 |   30065    72071 |   10021   31141  1135656    36.5 |  1.501 % |
c |    348288 |   30065    72071 |   11023    7886   130211    16.5 |  1.506 % |
c |    348440 |   30065    72071 |   12125    8038   133603    16.6 |  1.506 % |
c |    348665 |   30065    72071 |   13337    8263   138357    16.7 |  1.506 % |
c |    349002 |   30065    72071 |   14671    8600   165696    19.3 |  1.506 % |
c |    349508 |   30060    72060 |   16138    9091   192789    21.2 |  1.522 % |
c |    350267 |   30060    72060 |   17752    9850   229398    23.3 |  1.522 % |
c |    351406 |   30060    72060 |   19528   10989   320079    29.1 |  1.522 % |
c |    353114 |   30060    72060 |   21480   12697   397146    31.3 |  1.522 % |
c ==============================================================================
c [1mFound solution: 1986[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    354243 |   30066    72074 |   10022   13826   467725    33.8 |  1.522 % |
c |    354343 |   30066    72074 |   11024    7013   154795    22.1 |  1.527 % |
c |    354493 |   30066    72074 |   12126    7163   158225    22.1 |  1.527 % |
c |    354720 |   30066    72074 |   13339    7390   167735    22.7 |  1.527 % |
c |    355057 |   30066    72074 |   14673    7727   174615    22.6 |  1.527 % |
c |    355563 |   30066    72074 |   16140    8233   189784    23.1 |  1.527 % |
c |    356322 |   30066    72074 |   17754    8992   221782    24.7 |  1.527 % |
c |    357461 |   30066    72074 |   19530   10131   287813    28.4 |  1.527 % |
c |    359169 |   30063    72067 |   21483   11804   379485    32.1 |  1.537 % |
c |    361731 |   30063    72067 |   23631   14366   515415    35.9 |  1.538 % |
c |    365576 |   30063    72067 |   25994   18211   857635    47.1 |  1.538 % |
c |    371342 |   30063    72067 |   28593   23977  1254320    52.3 |  1.538 % |
c ==============================================================================
c [1mFound solution: 1985[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    379796 |   30069    72081 |   10023   32431  1921379    59.2 |  1.538 % |
c |    379896 |   30069    72081 |   11025    8208   230839    28.1 |  1.543 % |
c |    380046 |   30052    72046 |   12127    8349   238475    28.6 |  1.591 % |
c |    380271 |   30052    72046 |   13340    8574   242818    28.3 |  1.591 % |
c |    380608 |   30052    72046 |   14674    8911   253941    28.5 |  1.591 % |
c |    381114 |   30052    72046 |   16142    9417   272863    29.0 |  1.591 % |
c |    381873 |   30052    72046 |   17756   10176   294633    29.0 |  1.591 % |
c |    383013 |   30052    72046 |   19531   11316   425644    37.6 |  1.591 % |
c |    384721 |   30052    72046 |   21485   13024   514701    39.5 |  1.591 % |
c |    387284 |   30039    72019 |   23633   15576   811143    52.1 |  1.629 % |
c |    391130 |   30039    72019 |   25997   19422   993229    51.1 |  1.629 % |
c |    396897 |   30039    72019 |   28596   25189  1197276    47.5 |  1.629 % |
c |    405546 |   30039    72019 |   31456   33838  2349966    69.4 |  1.629 % |
c ==============================================================================
c [1mFound solution: 1984[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    412452 |   30045    72033 |   10015   23825  1563799    65.6 |  1.629 % |
c |    412553 |   30045    72033 |   11016    6058    63936    10.6 |  1.634 % |
c |    412706 |   30045    72033 |   12118    6211    66641    10.7 |  1.634 % |
c |    412931 |   30045    72033 |   13329    6436    73707    11.5 |  1.634 % |
c |    413268 |   30045    72033 |   14662    6772    82297    12.2 |  1.650 % |
c |    413774 |   30040    72022 |   16129    7277    90265    12.4 |  1.650 % |
c |    414535 |   30040    72022 |   17742    8038   122557    15.2 |  1.650 % |
c |    415674 |   30040    72022 |   19516    9177   145477    15.9 |  1.650 % |
c |    417383 |   30040    72022 |   21468   10886   341590    31.4 |  1.650 % |
c |    419946 |   30040    72022 |   23614   13449   485434    36.1 |  1.650 % |
c |    423792 |   30040    72022 |   25976   17295   651050    37.6 |  1.650 % |
c |    429558 |   30040    72022 |   28573   23061   852779    37.0 |  1.650 % |
c |    438208 |   30016    71967 |   31431   31704  1553912    49.0 |  1.687 % |
c |    451183 |   30002    71936 |   34574   28660  2011024    70.2 |  1.730 % |
c ==============================================================================
c [1mFound solution: 1963[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    465057 |   30009    71953 |   10003   24428  1513836    62.0 |  1.730 % |
c |    465157 |   30006    71946 |   11003    6206   165676    26.7 |  1.746 % |
c |    465307 |   30006    71946 |   12103    6356   171394    27.0 |  1.746 % |
c |    465536 |   29882    71673 |   13313    6550   174477    26.6 |  2.095 % |
c |    465874 |   29877    71661 |   14645    6674   179880    27.0 |  2.111 % |
c |    466380 |   29877    71661 |   16109    7180   197269    27.5 |  2.111 % |
c |    467142 |   29877    71661 |   17720    7942   239540    30.2 |  2.111 % |
c |    468282 |   29877    71661 |   19493    9082   291813    32.1 |  2.111 % |
c |    469990 |   29877    71661 |   21442   10790   344114    31.9 |  2.111 % |
c |    472553 |   29877    71661 |   23586   13353   432431    32.4 |  2.111 % |
c |    476397 |   29877    71661 |   25945   17197   576325    33.5 |  2.111 % |
c |    482163 |   29877    71661 |   28539   22963  1062955    46.3 |  2.111 % |
c |    490812 |   29873    71653 |   31393   31610  1482964    46.9 |  2.122 % |
c |    503787 |   29873    71653 |   34533   22465  1213509    54.0 |  2.122 % |
c |    523249 |   29873    71653 |   37986   21048  1041990    49.5 |  2.122 % |
c |    552441 |   29865    71635 |   41785   23381  2648690   113.3 |  2.149 % |
c |    596230 |   29865    71635 |   45963   36314  3603614    99.2 |  2.149 % |
#### 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.86 0.95 0.91 2/54 15495
Raw data (stat): 15495 (runsolver) R 15494 23176 23175 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 540156856 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 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.0008 s]
Raw data (loadavg): 0.88 0.95 0.91 2/54 15495
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 2146 0 0 0 994 4 0 0 25 0 1 0 540156856 11161600 2068 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2725 2068 603 41 0 2684 0
vsize: 10900
[startup+20.0068 s]
Raw data (loadavg): 0.90 0.96 0.91 2/54 15495
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 2554 0 0 0 1994 6 0 0 25 0 1 0 540156856 12894208 2476 4294967295 134512640 134672761 3221224624 3221223792 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3148 2476 603 41 0 3107 0
vsize: 12592
[startup+30.114 s]
Raw data (loadavg): 0.92 0.96 0.91 2/54 15495
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 2809 0 0 0 3003 7 0 0 25 0 1 0 540156856 13979648 2731 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3413 2731 603 41 0 3372 0
vsize: 13652
[startup+40.1146 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 15495
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 2809 0 0 0 4003 7 0 0 25 0 1 0 540156856 13979648 2731 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3413 2731 603 41 0 3372 0
vsize: 13652
[startup+50.1161 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 15495
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 2926 0 0 0 5002 8 0 0 25 0 1 0 540156856 14372864 2848 4294967295 134512640 134672761 3221224624 3221223748 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3509 2848 603 41 0 3468 0
vsize: 14036
[startup+60.1165 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 15495
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 2926 0 0 0 6002 8 0 0 25 0 1 0 540156856 14372864 2848 4294967295 134512640 134672761 3221224624 3221223792 134560806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3509 2848 603 41 0 3468 0
vsize: 14036
[startup+70.1178 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 15495
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 2945 0 0 0 7002 8 0 0 25 0 1 0 540156856 14508032 2867 4294967295 134512640 134672761 3221224624 3221223728 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3542 2867 603 41 0 3501 0
vsize: 14168
[startup+80.1188 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 15495
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 3340 0 0 0 8000 10 0 0 25 0 1 0 540156856 16105472 3262 4294967295 134512640 134672761 3221224624 3221223808 134558890 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3932 3262 603 41 0 3891 0
vsize: 15728
[startup+90.1193 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 15495
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 3876 0 0 0 8999 11 0 0 25 0 1 0 540156856 18243584 3798 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4454 3798 603 41 0 4413 0
vsize: 17816
[startup+100.12 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 15495
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 4442 0 0 0 9997 13 0 0 25 0 1 0 540156856 20647936 4364 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5041 4364 603 41 0 5000 0
vsize: 20164
[startup+110.122 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 15495
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 4442 0 0 0 10997 14 0 0 25 0 1 0 540156856 20647936 4364 4294967295 134512640 134672761 3221224624 3221223728 134560287 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5041 4364 603 41 0 5000 0
vsize: 20164
[startup+120.122 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 15495
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 4442 0 0 0 11997 14 0 0 25 0 1 0 540156856 20647936 4364 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5041 4364 603 41 0 5000 0
vsize: 20164
[startup+130.123 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 15495
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 4816 0 0 0 12996 15 0 0 25 0 1 0 540156856 22249472 4738 4294967295 134512640 134672761 3221224624 3221223692 1075346557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5432 4738 603 41 0 5391 0
vsize: 21728
[startup+140.124 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 15495
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 5382 0 0 0 13994 17 0 0 25 0 1 0 540156856 24518656 5304 4294967295 134512640 134672761 3221224624 3221223792 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5986 5304 603 41 0 5945 0
vsize: 23944
[startup+150.125 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15495
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 5617 0 0 0 14993 18 0 0 25 0 1 0 540156856 25456640 5539 4294967295 134512640 134672761 3221224624 3221223728 134560031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6215 5539 603 41 0 6174 0
vsize: 24860
[startup+160.125 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15495
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 5618 0 0 0 15994 18 0 0 25 0 1 0 540156856 25456640 5540 4294967295 134512640 134672761 3221224624 3221223792 134560948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6215 5540 603 41 0 6174 0
vsize: 24860
[startup+170.126 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15495
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 5618 0 0 0 16993 18 0 0 25 0 1 0 540156856 25456640 5540 4294967295 134512640 134672761 3221224624 3221223728 134560019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6215 5540 603 41 0 6174 0
vsize: 24860
[startup+180.127 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15495
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 5619 0 0 0 17993 19 0 0 25 0 1 0 540156856 25456640 5541 4294967295 134512640 134672761 3221224624 3221223792 134560825 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6215 5541 603 41 0 6174 0
vsize: 24860
[startup+190.128 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15495
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 5674 0 0 0 18993 19 0 0 25 0 1 0 540156856 25722880 5596 4294967295 134512640 134672761 3221224624 3221223760 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6280 5596 603 41 0 6239 0
vsize: 25120
[startup+200.129 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15495
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 5693 0 0 0 19993 19 0 0 25 0 1 0 540156856 25858048 5615 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6313 5615 603 41 0 6272 0
vsize: 25252
[startup+210.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15495
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 5693 0 0 0 20992 20 0 0 25 0 1 0 540156856 25858048 5615 4294967295 134512640 134672761 3221224624 3221223728 134560393 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6313 5615 603 41 0 6272 0
vsize: 25252
[startup+220.131 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15495
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 5693 0 0 0 21992 20 0 0 25 0 1 0 540156856 25858048 5615 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6313 5615 603 41 0 6272 0
vsize: 25252
[startup+230.131 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15495
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 5693 0 0 0 22992 20 0 0 25 0 1 0 540156856 25858048 5615 4294967295 134512640 134672761 3221224624 3221223808 134559594 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6313 5615 603 41 0 6272 0
vsize: 25252
[startup+240.132 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15495
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 6055 0 0 0 23991 21 0 0 25 0 1 0 540156856 27336704 5977 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6674 5977 603 41 0 6633 0
vsize: 26696
[startup+250.133 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15495
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 6404 0 0 0 24990 22 0 0 25 0 1 0 540156856 28688384 6326 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7004 6326 603 41 0 6963 0
vsize: 28016
[startup+260.134 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15495
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 6847 0 0 0 25988 25 0 0 25 0 1 0 540156856 30547968 6769 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7458 6769 603 41 0 7417 0
vsize: 29832
[startup+270.139 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15495
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 7024 0 0 0 26988 25 0 0 25 0 1 0 540156856 31203328 6946 4294967295 134512640 134672761 3221224624 3221223792 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7618 6946 603 41 0 7577 0
vsize: 30472
[startup+280.139 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15495
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 7024 0 0 0 27988 26 0 0 25 0 1 0 540156856 31203328 6946 4294967295 134512640 134672761 3221224624 3221223808 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7618 6946 603 41 0 7577 0
vsize: 30472
[startup+290.139 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15495
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 7024 0 0 0 28987 26 0 0 25 0 1 0 540156856 31203328 6946 4294967295 134512640 134672761 3221224624 3221223808 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7618 6946 603 41 0 7577 0
vsize: 30472
[startup+300.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15495
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 7029 0 0 0 29987 26 0 0 25 0 1 0 540156856 31338496 6951 4294967295 134512640 134672761 3221224624 3221223792 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7651 6951 603 41 0 7610 0
vsize: 30604
[startup+310.145 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15495
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 7029 0 0 0 30987 27 0 0 25 0 1 0 540156856 31338496 6951 4294967295 134512640 134672761 3221224624 3221223792 134560994 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7651 6951 603 41 0 7610 0
vsize: 30604
[startup+320.155 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15495
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 7029 0 0 0 31987 28 0 0 25 0 1 0 540156856 31338496 6951 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7651 6951 603 41 0 7610 0
vsize: 30604
[startup+330.172 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15495
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 7029 0 0 0 32988 28 0 0 25 0 1 0 540156856 31338496 6951 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7651 6951 603 41 0 7610 0
vsize: 30604
[startup+340.172 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15495
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 7077 0 0 0 33988 28 0 0 25 0 1 0 540156856 31469568 6999 4294967295 134512640 134672761 3221224624 3221223792 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7683 6999 603 41 0 7642 0
vsize: 30732
[startup+350.18 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15495
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 7428 0 0 0 34987 30 0 0 25 0 1 0 540156856 32931840 7350 4294967295 134512640 134672761 3221224624 3221223792 134560917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8040 7350 603 41 0 7999 0
vsize: 32160
[startup+360.181 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15495
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 7717 0 0 0 35986 31 0 0 25 0 1 0 540156856 34131968 7639 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8333 7639 603 41 0 8292 0
vsize: 33332
[startup+370.181 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15495
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 7717 0 0 0 36986 32 0 0 25 0 1 0 540156856 34131968 7639 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8333 7639 603 41 0 8292 0
vsize: 33332
[startup+380.181 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15495
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 7717 0 0 0 37986 32 0 0 25 0 1 0 540156856 34131968 7639 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8333 7639 603 41 0 8292 0
vsize: 33332
[startup+390.187 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15495
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 7717 0 0 0 38986 32 0 0 25 0 1 0 540156856 34131968 7639 4294967295 134512640 134672761 3221224624 3221223808 134558360 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8333 7639 603 41 0 8292 0
vsize: 33332
[startup+400.187 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15495
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 7717 0 0 0 39986 32 0 0 25 0 1 0 540156856 34131968 7639 4294967295 134512640 134672761 3221224624 3221223824 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8333 7639 603 41 0 8292 0
vsize: 33332
[startup+410.188 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15495
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 7717 0 0 0 40986 32 0 0 25 0 1 0 540156856 34131968 7639 4294967295 134512640 134672761 3221224624 3221223776 134561249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8333 7639 603 41 0 8292 0
vsize: 33332
[startup+420.189 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15495
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 7717 0 0 0 41986 32 0 0 25 0 1 0 540156856 34131968 7639 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8333 7639 603 41 0 8292 0
vsize: 33332
[startup+430.189 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15495
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 7749 0 0 0 42986 33 0 0 25 0 1 0 540156856 34394112 7671 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8397 7671 603 41 0 8356 0
vsize: 33588
[startup+440.19 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15495
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 7749 0 0 0 43987 33 0 0 25 0 1 0 540156856 34394112 7671 4294967295 134512640 134672761 3221224624 3221223760 134560596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8397 7671 603 41 0 8356 0
vsize: 33588
[startup+450.19 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15495
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 7749 0 0 0 44987 33 0 0 25 0 1 0 540156856 34394112 7671 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8397 7671 603 41 0 8356 0
vsize: 33588
[startup+460.191 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15495
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 7749 0 0 0 45987 33 0 0 25 0 1 0 540156856 34656256 7671 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8461 7671 603 41 0 8420 0
vsize: 33844
[startup+470.192 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15495
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 7749 0 0 0 46987 33 0 0 25 0 1 0 540156856 34656256 7671 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8461 7671 603 41 0 8420 0
vsize: 33844
[startup+480.191 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15495
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 7749 0 0 0 47987 33 0 0 25 0 1 0 540156856 34656256 7671 4294967295 134512640 134672761 3221224624 3221223808 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8461 7671 603 41 0 8420 0
vsize: 33844
[startup+490.195 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15495
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 7749 0 0 0 48988 33 0 0 25 0 1 0 540156856 34656256 7671 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8461 7671 603 41 0 8420 0
vsize: 33844
[startup+500.195 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15495
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 7749 0 0 0 49987 33 0 0 25 0 1 0 540156856 34656256 7671 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8461 7671 603 41 0 8420 0
vsize: 33844
[startup+510.196 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15495
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 7749 0 0 0 50987 33 0 0 25 0 1 0 540156856 34656256 7671 4294967295 134512640 134672761 3221224624 3221223792 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8461 7671 603 41 0 8420 0
vsize: 33844
[startup+520.199 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15495
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 7750 0 0 0 51988 33 0 0 25 0 1 0 540156856 34656256 7672 4294967295 134512640 134672761 3221224624 3221223808 134559031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8461 7672 603 41 0 8420 0
vsize: 33844
[startup+530.203 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15495
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 7750 0 0 0 52988 33 0 0 25 0 1 0 540156856 34656256 7672 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8461 7672 603 41 0 8420 0
vsize: 33844
[startup+540.204 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15495
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 7750 0 0 0 53988 33 0 0 25 0 1 0 540156856 34656256 7672 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8461 7672 603 41 0 8420 0
vsize: 33844
[startup+550.203 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15495
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 7752 0 0 0 54988 33 0 0 25 0 1 0 540156856 34656256 7674 4294967295 134512640 134672761 3221224624 3221223792 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8461 7674 603 41 0 8420 0
vsize: 33844
[startup+560.205 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15495
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 7752 0 0 0 55988 33 0 0 25 0 1 0 540156856 34656256 7674 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8461 7674 603 41 0 8420 0
vsize: 33844
[startup+570.205 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15495
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 7752 0 0 0 56989 33 0 0 25 0 1 0 540156856 34656256 7674 4294967295 134512640 134672761 3221224624 3221223824 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8461 7674 603 41 0 8420 0
vsize: 33844
[startup+580.204 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15495
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 7752 0 0 0 57989 33 0 0 25 0 1 0 540156856 34656256 7674 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8461 7674 603 41 0 8420 0
vsize: 33844
[startup+590.204 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15495
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 7752 0 0 0 58989 33 0 0 25 0 1 0 540156856 34656256 7674 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8461 7674 603 41 0 8420 0
vsize: 33844
[startup+600.205 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 15548
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 7752 0 0 0 59988 34 0 0 25 0 1 0 540156856 34656256 7674 4294967295 134512640 134672761 3221224624 3221223760 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8461 7674 603 41 0 8420 0
vsize: 33844
[startup+610.206 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 15548
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 7752 0 0 0 60988 34 0 0 25 0 1 0 540156856 34656256 7674 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8461 7674 603 41 0 8420 0
vsize: 33844
[startup+620.206 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 15548
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 7752 0 0 0 61988 34 0 0 25 0 1 0 540156856 34656256 7674 4294967295 134512640 134672761 3221224624 3221223792 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8461 7674 603 41 0 8420 0
vsize: 33844
[startup+630.206 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 15548
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 7752 0 0 0 62988 34 0 0 25 0 1 0 540156856 34656256 7674 4294967295 134512640 134672761 3221224624 3221223808 134559540 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8461 7674 603 41 0 8420 0
vsize: 33844
[startup+640.207 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 15548
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 7752 0 0 0 63988 34 0 0 25 0 1 0 540156856 34656256 7674 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8461 7674 603 41 0 8420 0
vsize: 33844
[startup+650.207 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 15548
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 7752 0 0 0 64988 34 0 0 25 0 1 0 540156856 34656256 7674 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8461 7674 603 41 0 8420 0
vsize: 33844
[startup+660.208 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 15550
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 7754 0 0 0 65988 34 0 0 25 0 1 0 540156856 34656256 7676 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8461 7676 603 41 0 8420 0
vsize: 33844
[startup+670.209 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 15550
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 7754 0 0 0 66988 34 0 0 25 0 1 0 540156856 34656256 7676 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8461 7676 603 41 0 8420 0
vsize: 33844
[startup+680.209 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 15550
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 7754 0 0 0 67988 35 0 0 25 0 1 0 540156856 34656256 7676 4294967295 134512640 134672761 3221224624 3221223792 134560979 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8461 7676 603 41 0 8420 0
vsize: 33844
[startup+690.21 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 15550
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 7754 0 0 0 68989 35 0 0 25 0 1 0 540156856 34656256 7676 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8461 7676 603 41 0 8420 0
vsize: 33844
[startup+700.211 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 15550
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 7754 0 0 0 69989 35 0 0 25 0 1 0 540156856 34656256 7676 4294967295 134512640 134672761 3221224624 3221223728 134560381 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8461 7676 603 41 0 8420 0
vsize: 33844
[startup+710.212 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 15550
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 7754 0 0 0 70989 35 0 0 25 0 1 0 540156856 34656256 7676 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8461 7676 603 41 0 8420 0
vsize: 33844
[startup+720.211 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 15550
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 7754 0 0 0 71989 35 0 0 25 0 1 0 540156856 34656256 7676 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8461 7676 603 41 0 8420 0
vsize: 33844
[startup+730.212 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15550
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 7754 0 0 0 72989 35 0 0 25 0 1 0 540156856 34656256 7676 4294967295 134512640 134672761 3221224624 3221223792 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8461 7676 603 41 0 8420 0
vsize: 33844
[startup+740.213 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15550
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 7754 0 0 0 73989 35 0 0 25 0 1 0 540156856 34656256 7676 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8461 7676 603 41 0 8420 0
vsize: 33844
[startup+750.213 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15550
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 7754 0 0 0 74989 35 0 0 25 0 1 0 540156856 34656256 7676 4294967295 134512640 134672761 3221224624 3221223728 134560291 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8461 7676 603 41 0 8420 0
vsize: 33844
[startup+760.213 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15550
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 7754 0 0 0 75990 35 0 0 25 0 1 0 540156856 34656256 7676 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8461 7676 603 41 0 8420 0
vsize: 33844
[startup+770.214 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15550
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 7754 0 0 0 76990 35 0 0 25 0 1 0 540156856 34656256 7676 4294967295 134512640 134672761 3221224624 3221223808 134559498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8461 7676 603 41 0 8420 0
vsize: 33844
[startup+780.214 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15550
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 7754 0 0 0 77990 35 0 0 25 0 1 0 540156856 34656256 7676 4294967295 134512640 134672761 3221224624 3221223728 134560410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8461 7676 603 41 0 8420 0
vsize: 33844
[startup+790.214 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15550
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 7754 0 0 0 78990 35 0 0 25 0 1 0 540156856 34656256 7676 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8461 7676 603 41 0 8420 0
vsize: 33844
[startup+800.214 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15550
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 7754 0 0 0 79990 35 0 0 25 0 1 0 540156856 34656256 7676 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8461 7676 603 41 0 8420 0
vsize: 33844
[startup+810.215 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15550
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 7754 0 0 0 80990 35 0 0 25 0 1 0 540156856 34656256 7676 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8461 7676 603 41 0 8420 0
vsize: 33844
[startup+820.216 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15550
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 7754 0 0 0 81990 35 0 0 25 0 1 0 540156856 34656256 7676 4294967295 134512640 134672761 3221224624 3221223808 134559176 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8461 7676 603 41 0 8420 0
vsize: 33844
[startup+830.216 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15550
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 7754 0 0 0 82990 35 0 0 25 0 1 0 540156856 34656256 7676 4294967295 134512640 134672761 3221224624 3221223748 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8461 7676 603 41 0 8420 0
vsize: 33844
[startup+840.217 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15550
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 7754 0 0 0 83990 36 0 0 25 0 1 0 540156856 34656256 7676 4294967295 134512640 134672761 3221224624 3221223728 134560224 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8461 7676 603 41 0 8420 0
vsize: 33844
[startup+850.217 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15550
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 7754 0 0 0 84990 36 0 0 25 0 1 0 540156856 34656256 7676 4294967295 134512640 134672761 3221224624 3221223760 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8461 7676 603 41 0 8420 0
vsize: 33844
[startup+860.218 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15550
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 7754 0 0 0 85991 36 0 0 25 0 1 0 540156856 34656256 7676 4294967295 134512640 134672761 3221224624 3221223824 134557885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8461 7676 603 41 0 8420 0
vsize: 33844
[startup+870.218 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15550
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 7754 0 0 0 86991 36 0 0 25 0 1 0 540156856 34656256 7676 4294967295 134512640 134672761 3221224624 3221223728 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8461 7676 603 41 0 8420 0
vsize: 33844
[startup+880.218 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15550
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 7754 0 0 0 87991 36 0 0 25 0 1 0 540156856 34656256 7676 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8461 7676 603 41 0 8420 0
vsize: 33844
[startup+890.219 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15550
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 7754 0 0 0 88991 36 0 0 25 0 1 0 540156856 34656256 7676 4294967295 134512640 134672761 3221224624 3221223788 134560077 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8461 7676 603 41 0 8420 0
vsize: 33844
[startup+900.218 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15550
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 7754 0 0 0 89991 36 0 0 25 0 1 0 540156856 34656256 7676 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8461 7676 603 41 0 8420 0
vsize: 33844
[startup+910.22 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15550
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 7754 0 0 0 90992 36 0 0 25 0 1 0 540156856 34656256 7676 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8461 7676 603 41 0 8420 0
vsize: 33844
[startup+920.22 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15552
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 7754 0 0 0 91992 36 0 0 25 0 1 0 540156856 34656256 7676 4294967295 134512640 134672761 3221224624 3221223792 134561115 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8461 7676 603 41 0 8420 0
vsize: 33844
[startup+930.22 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15552
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 7754 0 0 0 92992 36 0 0 25 0 1 0 540156856 34656256 7676 4294967295 134512640 134672761 3221224624 3221223808 134559622 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8461 7676 603 41 0 8420 0
vsize: 33844
[startup+940.221 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15552
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 7754 0 0 0 93992 36 0 0 25 0 1 0 540156856 34656256 7676 4294967295 134512640 134672761 3221224624 3221223728 134560326 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8461 7676 603 41 0 8420 0
vsize: 33844
[startup+950.222 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15552
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 7754 0 0 0 94992 36 0 0 25 0 1 0 540156856 34656256 7676 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8461 7676 603 41 0 8420 0
vsize: 33844
[startup+960.223 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15552
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 7754 0 0 0 95993 36 0 0 25 0 1 0 540156856 34656256 7676 4294967295 134512640 134672761 3221224624 3221223728 134560410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8461 7676 603 41 0 8420 0
vsize: 33844
[startup+970.223 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15552
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 8047 0 0 0 96992 37 0 0 25 0 1 0 540156856 35852288 7969 4294967295 134512640 134672761 3221224624 3221223728 134560510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8753 7969 603 41 0 8712 0
vsize: 35012
[startup+980.223 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15552
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 8462 0 0 0 97990 39 0 0 25 0 1 0 540156856 37580800 8384 4294967295 134512640 134672761 3221224624 3221223728 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9175 8384 603 41 0 9134 0
vsize: 36700
[startup+990.224 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15552
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 8938 0 0 0 98989 40 0 0 25 0 1 0 540156856 39473152 8860 4294967295 134512640 134672761 3221224624 3221223808 134559345 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9637 8860 603 41 0 9596 0
vsize: 38548
[startup+1000.22 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15552
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 9368 0 0 0 99987 42 0 0 25 0 1 0 540156856 41345024 9290 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10094 9290 603 41 0 10053 0
vsize: 40376
[startup+1010.22 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15552
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 9780 0 0 0 100987 43 0 0 25 0 1 0 540156856 42958848 9702 4294967295 134512640 134672761 3221224624 3221223792 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10488 9702 603 41 0 10447 0
vsize: 41952
[startup+1020.23 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15552
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 10133 0 0 0 101986 44 0 0 25 0 1 0 540156856 44412928 10055 4294967295 134512640 134672761 3221224624 3221223728 134559927 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10843 10055 603 41 0 10802 0
vsize: 43372
[startup+1030.23 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15552
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 10133 0 0 0 102986 44 0 0 25 0 1 0 540156856 44412928 10055 4294967295 134512640 134672761 3221224624 3221223728 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10843 10055 603 41 0 10802 0
vsize: 43372
[startup+1040.23 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15552
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 10133 0 0 0 103986 44 0 0 25 0 1 0 540156856 44412928 10055 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10843 10055 603 41 0 10802 0
vsize: 43372
[startup+1050.23 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15552
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 10133 0 0 0 104986 44 0 0 25 0 1 0 540156856 44412928 10055 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10843 10055 603 41 0 10802 0
vsize: 43372
[startup+1060.23 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15552
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 10133 0 0 0 105986 45 0 0 25 0 1 0 540156856 44412928 10055 4294967295 134512640 134672761 3221224624 3221223728 134560034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10843 10055 603 41 0 10802 0
vsize: 43372
[startup+1070.23 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15552
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 10133 0 0 0 106985 45 0 0 25 0 1 0 540156856 44412928 10055 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10843 10055 603 41 0 10802 0
vsize: 43372
[startup+1080.23 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15552
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 10133 0 0 0 107985 45 0 0 25 0 1 0 540156856 44412928 10055 4294967295 134512640 134672761 3221224624 3221223776 134559753 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10843 10055 603 41 0 10802 0
vsize: 43372
[startup+1090.23 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15552
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 10133 0 0 0 108986 45 0 0 25 0 1 0 540156856 44412928 10055 4294967295 134512640 134672761 3221224624 3221223760 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10843 10055 603 41 0 10802 0
vsize: 43372
[startup+1100.23 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15552
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 10138 0 0 0 109986 45 0 0 25 0 1 0 540156856 44412928 10060 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10843 10060 603 41 0 10802 0
vsize: 43372
[startup+1110.23 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15552
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 10138 0 0 0 110986 45 0 0 25 0 1 0 540156856 44412928 10060 4294967295 134512640 134672761 3221224624 3221223788 134565024 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10843 10060 603 41 0 10802 0
vsize: 43372
[startup+1120.23 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15552
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 10138 0 0 0 111986 45 0 0 25 0 1 0 540156856 44412928 10060 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10843 10060 603 41 0 10802 0
vsize: 43372
[startup+1130.23 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15552
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 10138 0 0 0 112986 45 0 0 25 0 1 0 540156856 44412928 10060 4294967295 134512640 134672761 3221224624 3221223728 134560376 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10843 10060 603 41 0 10802 0
vsize: 43372
[startup+1140.23 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15552
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 10138 0 0 0 113986 45 0 0 25 0 1 0 540156856 44412928 10060 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10843 10060 603 41 0 10802 0
vsize: 43372
[startup+1150.23 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15552
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 10138 0 0 0 114987 45 0 0 25 0 1 0 540156856 44412928 10060 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10843 10060 603 41 0 10802 0
vsize: 43372
[startup+1160.23 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15552
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 10138 0 0 0 115987 45 0 0 25 0 1 0 540156856 44412928 10060 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10843 10060 603 41 0 10802 0
vsize: 43372
[startup+1170.23 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15552
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 10138 0 0 0 116987 45 0 0 25 0 1 0 540156856 44412928 10060 4294967295 134512640 134672761 3221224624 3221223728 134560158 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10843 10060 603 41 0 10802 0
vsize: 43372
[startup+1180.23 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15552
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 10138 0 0 0 117987 45 0 0 25 0 1 0 540156856 44412928 10060 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10843 10060 603 41 0 10802 0
vsize: 43372
[startup+1190.23 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15552
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 10138 0 0 0 118987 45 0 0 25 0 1 0 540156856 44412928 10060 4294967295 134512640 134672761 3221224624 3221223760 134560657 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10843 10060 603 41 0 10802 0
vsize: 43372
[startup+1200.23 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 15552
Raw data (stat): 15495 (minisat+) R 15494 23176 23175 0 -1 0 10138 0 0 0 119987 45 0 0 25 0 1 0 540156856 44412928 10060 4294967295 134512640 134672761 3221224624 3221223764 134560556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10843 10060 603 41 0 10802 0
vsize: 43372
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.25 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 15552
Raw data (stat): 15495 (minisat+) Z 15494 23176 23175 0 -1 12 10141 0 0 0 119987 47 0 0 25 0 1 0 540156856 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.25
CPU time (s): 1200.35
CPU user time (s): 1199.88
CPU system time (s): 0.473927
CPU usage (%): 100.008
Max. virtual memory (Kb): 43372
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####