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/submitted/een/normalized-lseu.opb
MD5SUM	a578bf261896413ca78de4dc6db2447f
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	1120
Optimality of the best value was proved	NO
Number of terms in the objective function	85
Biggest coefficient in the objective function	517
Number of bits for the biggest coefficient in the objective function	10
Sum of the numbers in the objective function	15494
Number of bits of the sum of numbers in the objective function	14
Biggest number in a constraint	1656
Number of bits of the biggest number in a constraint	11
Biggest sum of numbers in a constraint	15494
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.02184
Number of variables	89
Total number of constraints	28
Number of constraints which are clauses	2
Number of constraints which are cardinality constraints (but not clauses)	15
Number of constraints which are nor clauses,nor cardinality constraints	11
Minimum length of a constraint	2
Maximum length of a constraint	47
Trace number 6970

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc18 THE 2005-04-14 20:45:37 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=5030 boxname=wulflinc18 idbench=387 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  a578bf261896413ca78de4dc6db2447f  /oldhome/oroussel/tmp/wulflinc18/normalized-lseu.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc18/normalized-lseu.opb /oldhome/oroussel/tmp/wulflinc18/normalized-lseu.opb
IDLAUNCH: 5030
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.177
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.177
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        838560 kB
Buffers:         35724 kB
Cached:         124368 kB
SwapCached:        320 kB
Active:          60240 kB
Inactive:       102972 kB
HighTotal:      131008 kB
HighFree:         2688 kB
LowTotal:       903652 kB
LowFree:        835872 kB
SwapTotal:     2097892 kB
SwapFree:      2097572 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6936 kB
Slab:            27220 kB
Committed_AS:    63712 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 20:55:46 (client local time) WITH STATUS 30 IN 608.67 SECONDS
stats: 5030 0 608.67 30
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 28 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #
c   -- Clauses(.)/Splits(s): .....s
c ---[  26]---> BDD-cost:    3
c ---[  25]---> BDD-cost:    3
c ---[  24]---> BDD-cost:    3
c ---[  23]---> BDD-cost:    3
c ---[  22]---> BDD-cost:    3
c ---[  21]---> BDD-cost:    5
c ---[  20]---> BDD-cost:    5
c ---[  19]---> BDD-cost:    5
c ---[  17]---> BDD-cost:    5
c ---[  16]---> BDD-cost:    7
c ---[  15]---> BDD-cost:    7
c ---[  14]---> BDD-cost:    7
c ---[  13]---> BDD-cost:    7
c ---[  12]---> BDD-cost:    7
c ---[   9]---> BDD-cost:   11
c ---[   8]---> BDD-cost:   16
c ---[   7]---> BDD-cost:   28
c ---[   6]---> BDD-cost:  202
c ---[   4]---> BDD-cost:  469
c ---[   3]---> BDD-cost: 1803
c ---[   1]---> BDD-cost: 5998
c ---[   0]---> BDD-cost:   22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   23842    70296 |    7947       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 3310[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:12496     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        12 |   53328   139237 |   17776      12       97     8.1 |  0.000 % |
c |       112 |   53312   139205 |   19553     111     4698    42.3 |  0.163 % |
c |       262 |   53204   138963 |   21508     257     5822    22.7 |  0.309 % |
c ==============================================================================
c [1mFound solution: 3298[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       337 |   52611   137720 |   17537     293     5946    20.3 |  0.309 % |
c ==============================================================================
c [1mFound solution: 3255[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       340 |   52790   138131 |   17596     296     5967    20.2 |  0.309 % |
c |       440 |   51339   134810 |   19355     371     6882    18.5 |  3.858 % |
c ==============================================================================
c [1mFound solution: 2963[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       505 |   50435   132753 |   16811     380     6839    18.0 |  3.858 % |
c |       607 |   49708   131081 |   18492     470     8443    18.0 |  6.875 % |
c ==============================================================================
c [1mFound solution: 2922[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       687 |   49635   130940 |   16545     545    12350    22.7 |  6.875 % |
c |       788 |   49635   130940 |   18199     646    14765    22.9 |  7.157 % |
c |       939 |   48823   129062 |   20019     778    16254    20.9 |  8.581 % |
c |      1164 |   48001   127169 |   22021     956    20857    21.8 |  9.777 % |
c |      1502 |   47748   126585 |   24223    1277    27208    21.3 | 10.158 % |
c |      2009 |   47681   126427 |   26645    1782    42929    24.1 | 10.270 % |
c ==============================================================================
c [1mFound solution: 2902[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2245 |   47793   126719 |   15931    2018    52194    25.9 | 10.270 % |
c |      2345 |   47793   126719 |   17524    2118    57251    27.0 | 10.258 % |
c ==============================================================================
c [1mFound solution: 2429[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2373 |   47901   126996 |   15967    2146    58216    27.1 | 10.258 % |
c |      2473 |   47901   126996 |   17563    2246    61107    27.2 | 10.249 % |
c ==============================================================================
c [1mFound solution: 2160[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2507 |   47922   127061 |   15974    2280    63410    27.8 | 10.249 % |
c ==============================================================================
c [1mFound solution: 1880[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2516 |   47943   127129 |   15981    2289    63648    27.8 | 10.249 % |
c ==============================================================================
c [1mFound solution: 1828[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2612 |   47951   127150 |   15983    2385    68018    28.5 | 10.249 % |
c ==============================================================================
c [1mFound solution: 1804[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2650 |   47958   127166 |   15986    2423    70008    28.9 | 10.249 % |
c |      2750 |   47958   127166 |   17584    2523    73306    29.1 | 10.250 % |
c |      2902 |   47958   127166 |   19343    2675    80079    29.9 | 10.250 % |
c |      3127 |   47901   127036 |   21277    2899    91133    31.4 | 10.336 % |
c |      3465 |   47901   127036 |   23405    3237   107745    33.3 | 10.336 % |
c ==============================================================================
c [1mFound solution: 1802[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3926 |   47906   127048 |   15968    3698   135475    36.6 | 10.336 % |
c |      4026 |   47906   127048 |   17564    3798   141406    37.2 | 10.339 % |
c |      4176 |   47906   127048 |   19321    3948   149355    37.8 | 10.339 % |
c |      4402 |   47906   127048 |   21253    4174   163065    39.1 | 10.339 % |
c ==============================================================================
c [1mFound solution: 1787[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4623 |   48005   127304 |   16001    4395   177764    40.4 | 10.339 % |
c |      4724 |   48005   127304 |   17601    4496   180004    40.0 | 10.329 % |
c |      4874 |   48005   127304 |   19361    4646   183991    39.6 | 10.329 % |
c |      5099 |   48005   127304 |   21297    4871   190244    39.1 | 10.329 % |
c |      5436 |   48005   127304 |   23427    5208   198741    38.2 | 10.329 % |
c |      5945 |   48005   127304 |   25769    5717   214518    37.5 | 10.329 % |
c |      6708 |   48005   127304 |   28346    6480   238731    36.8 | 10.329 % |
c |      7852 |   48005   127304 |   31181    7624   266707    35.0 | 10.329 % |
c |      9565 |   48005   127304 |   34299    9337   311384    33.3 | 10.329 % |
c |     12128 |   47946   127169 |   37729   11898   386342    32.5 | 10.414 % |
c ==============================================================================
c [1mFound solution: 1740[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14665 |   47865   127003 |   15955    5802   209399    36.1 | 10.414 % |
c |     14766 |   47865   127003 |   17550    5903   214200    36.3 | 10.552 % |
c |     14916 |   47865   127003 |   19305    6053   220634    36.5 | 10.552 % |
c |     15142 |   47842   126948 |   21236    6276   229395    36.6 | 10.602 % |
c |     15479 |   47842   126948 |   23359    6613   241806    36.6 | 10.602 % |
c ==============================================================================
c [1mFound solution: 1711[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     15912 |   47850   126981 |   15950    7046   262257    37.2 | 10.602 % |
c |     16012 |   47850   126981 |   17545    7146   267359    37.4 | 10.604 % |
c |     16162 |   47850   126981 |   19299    7296   275535    37.8 | 10.604 % |
c |     16388 |   47850   126981 |   21229    7522   286341    38.1 | 10.604 % |
c |     16725 |   47850   126981 |   23352    7859   300573    38.2 | 10.604 % |
c |     17233 |   47850   126981 |   25687    8367   320546    38.3 | 10.604 % |
c |     17993 |   47557   126299 |   28256    9121   351146    38.5 | 11.056 % |
c |     19133 |   47453   126063 |   31082   10257   433012    42.2 | 11.196 % |
c ==============================================================================
c [1mFound solution: 1607[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19500 |   47528   126248 |   15842   10624   451563    42.5 | 11.196 % |
c |     19600 |   47528   126248 |   17426   10724   454574    42.4 | 11.200 % |
c |     19750 |   47528   126248 |   19168   10874   459940    42.3 | 11.200 % |
c ==============================================================================
c [1mFound solution: 1588[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19830 |   47535   126268 |   15845   10954   462149    42.2 | 11.200 % |
c |     19930 |   47535   126268 |   17429   11054   465515    42.1 | 11.202 % |
c ==============================================================================
c [1mFound solution: 1587[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20008 |   47539   126279 |   15846   11132   468364    42.1 | 11.202 % |
c |     20108 |   47539   126279 |   17430   11232   473653    42.2 | 11.206 % |
c ==============================================================================
c [1mFound solution: 1563[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20256 |   47543   126290 |   15847   11380   481343    42.3 | 11.206 % |
c |     20356 |   47543   126290 |   17431   11480   485481    42.3 | 11.209 % |
c |     20508 |   47543   126290 |   19174   11632   489972    42.1 | 11.209 % |
c |     20733 |   47543   126290 |   21092   11857   495826    41.8 | 11.209 % |
c |     21070 |   47543   126290 |   23201   12194   507365    41.6 | 11.209 % |
c |     21577 |   47543   126290 |   25521   12701   521923    41.1 | 11.209 % |
c |     22336 |   47543   126290 |   28073   13460   548597    40.8 | 11.209 % |
c |     23476 |   47539   126281 |   30881   14599   593826    40.7 | 11.214 % |
c ==============================================================================
c [1mFound solution: 1526[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     23805 |   47449   126085 |   15816   14926   608071    40.7 | 11.214 % |
c ==============================================================================
c [1mFound solution: 1503[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     23882 |   47454   126097 |   15818   15003   611506    40.8 | 11.214 % |
c ==============================================================================
c [1mFound solution: 1492[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     23948 |   47459   126108 |   15819   15069   614061    40.7 | 11.214 % |
c ==============================================================================
c [1mFound solution: 1489[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     23953 |   47466   126124 |   15822   15074   614181    40.7 | 11.214 % |
c |     24054 |   47466   126124 |   17404   15175   617698    40.7 | 11.366 % |
c ==============================================================================
c [1mFound solution: 1474[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     24152 |   47473   126140 |   15824   15273   621487    40.7 | 11.366 % |
c |     24252 |   47473   126140 |   17406   15373   625677    40.7 | 11.368 % |
c |     24402 |   47473   126140 |   19147   15523   631688    40.7 | 11.368 % |
c |     24627 |   47473   126140 |   21061   15748   640702    40.7 | 11.368 % |
c |     24966 |   47473   126140 |   23167   16087   652835    40.6 | 11.368 % |
c |     25474 |   47137   125365 |   25484   16588   670699    40.4 | 11.893 % |
c |     26234 |   46646   124227 |   28033   17342   701952    40.5 | 12.678 % |
c ==============================================================================
c [1mFound solution: 1430[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26853 |   46556   124018 |   15518   17954   724254    40.3 | 12.678 % |
c |     26954 |   46556   124018 |   17069   18055   726900    40.3 | 12.849 % |
c |     27104 |   46556   124018 |   18776   18205   734802    40.4 | 12.849 % |
c |     27331 |   46556   124018 |   20654   18432   745297    40.4 | 12.849 % |
c |     27669 |   46191   123170 |   22719   18757   751877    40.1 | 13.434 % |
c |     28176 |   45405   121352 |   24991   19136   763912    39.9 | 14.688 % |
c |     28935 |   45405   121352 |   27491   19895   794574    39.9 | 14.688 % |
c |     30074 |   45359   121246 |   30240   21032   835481    39.7 | 14.758 % |
c ==============================================================================
c [1mFound solution: 1330[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     30646 |   45366   121262 |   15122   21604   860437    39.8 | 14.758 % |
c |     30748 |   45366   121262 |   16634   10904   351647    32.2 | 14.760 % |
c |     30898 |   45366   121262 |   18297   11054   356563    32.3 | 14.760 % |
c |     31123 |   45366   121262 |   20127   11279   366016    32.5 | 14.760 % |
c ==============================================================================
c [1mFound solution: 1325[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     31161 |   45371   121274 |   15123   11317   367798    32.5 | 14.760 % |
c |     31262 |   45371   121274 |   16635   11418   371578    32.5 | 14.763 % |
c |     31413 |   45371   121274 |   18298   11569   375783    32.5 | 14.763 % |
c |     31639 |   45371   121274 |   20128   11795   382255    32.4 | 14.763 % |
c |     31976 |   45371   121274 |   22141   12132   389944    32.1 | 14.763 % |
c |     32486 |   45371   121274 |   24355   12642   404067    32.0 | 14.763 % |
c |     33247 |   45371   121274 |   26791   13403   439779    32.8 | 14.763 % |
c |     34387 |   45357   121240 |   29470   14538   486647    33.5 | 14.778 % |
c ==============================================================================
c [1mFound solution: 1319[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     36052 |   45348   121219 |   15116   16202   557783    34.4 | 14.778 % |
c |     36153 |   45348   121219 |   16627   16303   561701    34.5 | 14.801 % |
c |     36303 |   45348   121219 |   18290   16453   568068    34.5 | 14.801 % |
c ==============================================================================
c [1mFound solution: 1309[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     36322 |   45417   121384 |   15139   16472   568834    34.5 | 14.801 % |
c |     36424 |   45417   121384 |   16652   16574   572089    34.5 | 14.799 % |
c |     36575 |   45417   121384 |   18318   16725   578103    34.6 | 14.799 % |
c |     36801 |   45417   121384 |   20150   16951   588872    34.7 | 14.799 % |
c ==============================================================================
c [1mFound solution: 1302[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     37044 |   45421   121393 |   15140   17194   600354    34.9 | 14.799 % |
c |     37145 |   45421   121393 |   16654   17295   605273    35.0 | 14.802 % |
c ==============================================================================
c [1mFound solution: 1292[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     37229 |   45435   121428 |   15145   17379   608747    35.0 | 14.802 % |
c |     37331 |   45435   121428 |   16659   17481   613311    35.1 | 14.801 % |
c ==============================================================================
c [1mFound solution: 1230[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     37339 |   45442   121448 |   15147   17489   613587    35.1 | 14.801 % |
c |     37439 |   45442   121448 |   16661   17589   617654    35.1 | 14.802 % |
c |     37590 |   45442   121448 |   18327   17740   623640    35.2 | 14.802 % |
c |     37815 |   45442   121448 |   20160   17965   632939    35.2 | 14.802 % |
c ==============================================================================
c [1mFound solution: 1221[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     37978 |   45445   121455 |   15148   18128   640411    35.3 | 14.802 % |
c |     38079 |   45445   121455 |   16662    9165   293847    32.1 | 14.806 % |
c |     38229 |   45445   121455 |   18329    9315   298243    32.0 | 14.806 % |
c |     38454 |   45445   121455 |   20161    9540   305599    32.0 | 14.806 % |
c ==============================================================================
c [1mFound solution: 1215[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     38476 |   45450   121467 |   15150    9562   306372    32.0 | 14.806 % |
c ==============================================================================
c [1mFound solution: 1153[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     38567 |   45455   121478 |   15151    9653   309883    32.1 | 14.806 % |
c ==============================================================================
c [1mFound solution: 1136[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     38568 |   45461   121493 |   15153    9654   309904    32.1 | 14.806 % |
c |     38668 |   45461   121493 |   16668    9754   312924    32.1 | 14.813 % |
c |     38822 |   45461   121493 |   18335    9908   316872    32.0 | 14.813 % |
c |     39047 |   45461   121493 |   20168   10133   323707    31.9 | 14.813 % |
c |     39384 |   45461   121493 |   22185   10470   333289    31.8 | 14.813 % |
c |     39890 |   45457   121484 |   24404   10975   348814    31.8 | 14.818 % |
c |     40649 |   45457   121484 |   26844   11734   371697    31.7 | 14.818 % |
c |     41788 |   45437   121437 |   29528   12871   401192    31.2 | 14.833 % |
c |     43496 |   45437   121437 |   32481   14579   453702    31.1 | 14.833 % |
c ==============================================================================
c [1mFound solution: 1128[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     45439 |   45441   121447 |   15147   16522   527626    31.9 | 14.833 % |
c |     45539 |   45379   121301 |   16661   16621   529249    31.8 | 14.935 % |
c |     45696 |   45379   121301 |   18327   16778   531296    31.7 | 14.935 % |
c |     45921 |   45379   121301 |   20160   17003   539062    31.7 | 14.935 % |
c |     46260 |   45379   121301 |   22176   17342   549123    31.7 | 14.935 % |
c |     46767 |   45379   121301 |   24394   17849   564499    31.6 | 14.935 % |
c |     47528 |   45379   121301 |   26833   18610   583212    31.3 | 14.935 % |
c |     48667 |   45379   121301 |   29517   19749   615658    31.2 | 14.935 % |
c |     50375 |   45379   121301 |   32468   21457   685002    31.9 | 14.935 % |
c |     52940 |   45379   121301 |   35715   24022   786924    32.8 | 14.935 % |
c |     56784 |   45379   121301 |   39287   27866   923230    33.1 | 14.935 % |
c ==============================================================================
c [1mFound solution: 1120[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     57940 |   45382   121308 |   15127   29022   962363    33.2 | 14.935 % |
c |     58042 |   45382   121308 |   16639   14613   441762    30.2 | 14.939 % |
c |     58192 |   45382   121308 |   18303   14763   446956    30.3 | 14.939 % |
c |     58418 |   45382   121308 |   20134   14989   454161    30.3 | 14.939 % |
c |     58762 |   45382   121308 |   22147   15333   464669    30.3 | 14.939 % |
c |     59268 |   45382   121308 |   24362   15839   479806    30.3 | 14.939 % |
c |     60028 |   45382   121308 |   26798   16599   501294    30.2 | 14.939 % |
c |     61169 |   45382   121308 |   29478   17740   541348    30.5 | 14.939 % |
c |     62879 |   45382   121308 |   32426   19450   605293    31.1 | 14.939 % |
c |     65441 |   45382   121308 |   35668   22012   702077    31.9 | 14.939 % |
c |     69287 |   45382   121308 |   39235   25858   821529    31.8 | 14.939 % |
c |     75057 |   45382   121308 |   43159   31628  1051655    33.3 | 14.939 % |
c |     83706 |   45382   121308 |   47475   40277  1345729    33.4 | 14.939 % |
c |     96680 |   45334   121197 |   52222   19901   543345    27.3 | 15.008 % |
c ==============================================================================
c [1mOptimal solution: 1120[0m
s OPTIMUM FOUND
v x0 x1 -x2 -x3 -x4 -x5 -x6 -x7 -x8 x9 -x10 -x11 -x12 -x13 -x14 -x15 -x16 -x17 -x18 -x19 -x20 -x21 x22 -x23 -x24 -x25 -x26 -x27 -x28 x29 -x30 -x31 -x32 -x33 x34 -x35 -x36 -x37 -x38 x39 -x40 -x41 -x42 -x43 -x44 -x45 x46 -x47 x48 -x49 -x50 -x51 -x52 -x53 -x54 -x55 -x56 -x57 -x58 x59 -x60 x61 -x62 -x63 -x64 -x65 -x66 -x67 -x68 -x69 -x70 -x71 -x72 -x73 -x74 -x75 -x76 -x77 -x78 -x79 -x80 x81 -x82 -x83 -x84 -x85 x86 -x87 -x88
c _______________________________________________________________________________
c 
c restarts              : 156
c conflicts             : 113246         (186 /sec)
c decisions             : 216557         (356 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 608.497 s
c _______________________________________________________________________________
#### 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.84 0.94 0.68 2/55 2381
Raw data (stat): 2381 (runsolver) R 2380 20024 20023 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 487568598 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0006 s]
Raw data (loadavg): 0.87 0.94 0.69 2/55 2381
Raw data (stat): 2381 (minisat+) R 2380 20024 20023 0 -1 0 2130 0 0 0 994 4 0 0 25 0 1 0 487568598 10948608 2042 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2673 2042 603 41 0 2632 0
vsize: 10692
[startup+20.0009 s]
Raw data (loadavg): 0.89 0.94 0.69 2/55 2381
Raw data (stat): 2381 (minisat+) R 2380 20024 20023 0 -1 0 2269 0 0 0 1992 5 0 0 25 0 1 0 487568598 11620352 2181 4294967295 134512640 134672761 3221224560 3221223728 134560813 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2837 2181 603 41 0 2796 0
vsize: 11348
[startup+30.0014 s]
Raw data (loadavg): 0.90 0.94 0.69 2/55 2381
Raw data (stat): 2381 (minisat+) R 2380 20024 20023 0 -1 0 2367 0 0 0 2991 6 0 0 25 0 1 0 487568598 12029952 2279 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2937 2279 603 41 0 2896 0
vsize: 11748
[startup+40.002 s]
Raw data (loadavg): 0.92 0.94 0.69 2/55 2381
Raw data (stat): 2381 (minisat+) R 2380 20024 20023 0 -1 0 2474 0 0 0 3990 6 0 0 25 0 1 0 487568598 12480512 2386 4294967295 134512640 134672761 3221224560 3221223744 134558687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3047 2386 603 41 0 3006 0
vsize: 12188
[startup+50.0027 s]
Raw data (loadavg): 0.93 0.94 0.70 2/55 2381
Raw data (stat): 2381 (minisat+) R 2380 20024 20023 0 -1 0 2567 0 0 0 4990 6 0 0 25 0 1 0 487568598 12877824 2479 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3144 2479 603 41 0 3103 0
vsize: 12576
[startup+60.0029 s]
Raw data (loadavg): 0.94 0.94 0.70 2/55 2381
Raw data (stat): 2381 (minisat+) R 2380 20024 20023 0 -1 0 2645 0 0 0 5990 6 0 0 25 0 1 0 487568598 13152256 2557 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3211 2557 603 41 0 3170 0
vsize: 12844
[startup+70.0038 s]
Raw data (loadavg): 0.95 0.95 0.70 2/55 2383
Raw data (stat): 2381 (minisat+) R 2380 20024 20023 0 -1 0 2645 0 0 0 6990 7 0 0 25 0 1 0 487568598 13152256 2557 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3211 2557 603 41 0 3170 0
vsize: 12844
[startup+80.0044 s]
Raw data (loadavg): 0.96 0.95 0.71 2/55 2383
Raw data (stat): 2381 (minisat+) R 2380 20024 20023 0 -1 0 2647 0 0 0 7990 7 0 0 25 0 1 0 487568598 13152256 2559 4294967295 134512640 134672761 3221224560 3221223664 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3211 2559 603 41 0 3170 0
vsize: 12844
[startup+90.0057 s]
Raw data (loadavg): 0.96 0.95 0.71 2/55 2383
Raw data (stat): 2381 (minisat+) R 2380 20024 20023 0 -1 0 2742 0 0 0 8990 7 0 0 25 0 1 0 487568598 13545472 2654 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3307 2654 603 41 0 3266 0
vsize: 13228
[startup+100.006 s]
Raw data (loadavg): 0.97 0.95 0.71 2/55 2383
Raw data (stat): 2381 (minisat+) R 2380 20024 20023 0 -1 0 2842 0 0 0 9990 8 0 0 25 0 1 0 487568598 13942784 2754 4294967295 134512640 134672761 3221224560 3221223696 134560577 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3404 2754 603 41 0 3363 0
vsize: 13616
[startup+110.005 s]
Raw data (loadavg): 0.97 0.95 0.71 2/55 2383
Raw data (stat): 2381 (minisat+) R 2380 20024 20023 0 -1 0 2936 0 0 0 10990 8 0 0 25 0 1 0 487568598 14327808 2848 4294967295 134512640 134672761 3221224560 3221223696 134560706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3498 2848 603 41 0 3457 0
vsize: 13992
[startup+120.005 s]
Raw data (loadavg): 0.98 0.95 0.72 2/55 2383
Raw data (stat): 2381 (minisat+) R 2380 20024 20023 0 -1 0 3032 0 0 0 11990 8 0 0 25 0 1 0 487568598 14729216 2944 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3596 2944 603 41 0 3555 0
vsize: 14384
[startup+130.005 s]
Raw data (loadavg): 0.98 0.95 0.72 2/55 2383
Raw data (stat): 2381 (minisat+) R 2380 20024 20023 0 -1 0 3106 0 0 0 12989 8 0 0 25 0 1 0 487568598 15126528 3018 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3693 3018 603 41 0 3652 0
vsize: 14772
[startup+140.006 s]
Raw data (loadavg): 0.98 0.95 0.72 2/55 2383
Raw data (stat): 2381 (minisat+) R 2380 20024 20023 0 -1 0 3182 0 0 0 13989 9 0 0 25 0 1 0 487568598 15392768 3094 4294967295 134512640 134672761 3221224560 3221223760 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3758 3094 603 41 0 3717 0
vsize: 15032
[startup+150.006 s]
Raw data (loadavg): 0.98 0.95 0.73 2/55 2383
Raw data (stat): 2381 (minisat+) R 2380 20024 20023 0 -1 0 3203 0 0 0 14989 9 0 0 25 0 1 0 487568598 15527936 3115 4294967295 134512640 134672761 3221224560 3221223744 134558656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3791 3115 603 41 0 3750 0
vsize: 15164
[startup+160.006 s]
Raw data (loadavg): 0.99 0.95 0.73 2/55 2383
Raw data (stat): 2381 (minisat+) R 2380 20024 20023 0 -1 0 3203 0 0 0 15990 9 0 0 25 0 1 0 487568598 15527936 3115 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3791 3115 603 41 0 3750 0
vsize: 15164
[startup+170.007 s]
Raw data (loadavg): 0.99 0.96 0.73 2/55 2383
Raw data (stat): 2381 (minisat+) R 2380 20024 20023 0 -1 0 3207 0 0 0 16990 9 0 0 25 0 1 0 487568598 15527936 3119 4294967295 134512640 134672761 3221224560 3221223760 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3791 3119 603 41 0 3750 0
vsize: 15164
[startup+180.007 s]
Raw data (loadavg): 0.99 0.96 0.73 2/55 2383
Raw data (stat): 2381 (minisat+) R 2380 20024 20023 0 -1 0 3215 0 0 0 17990 9 0 0 25 0 1 0 487568598 15527936 3127 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3791 3127 603 41 0 3750 0
vsize: 15164
[startup+190.008 s]
Raw data (loadavg): 0.99 0.96 0.73 2/55 2383
Raw data (stat): 2381 (minisat+) R 2380 20024 20023 0 -1 0 3231 0 0 0 18990 9 0 0 25 0 1 0 487568598 15663104 3143 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3824 3143 603 41 0 3783 0
vsize: 15296
[startup+200.009 s]
Raw data (loadavg): 0.99 0.96 0.74 2/55 2383
Raw data (stat): 2381 (minisat+) R 2380 20024 20023 0 -1 0 3250 0 0 0 19990 9 0 0 25 0 1 0 487568598 15663104 3162 4294967295 134512640 134672761 3221224560 3221223696 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3824 3162 603 41 0 3783 0
vsize: 15296
[startup+210.009 s]
Raw data (loadavg): 0.99 0.96 0.74 2/55 2383
Raw data (stat): 2381 (minisat+) R 2380 20024 20023 0 -1 0 3250 0 0 0 20990 9 0 0 25 0 1 0 487568598 15663104 3162 4294967295 134512640 134672761 3221224560 3221223696 134560604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3824 3162 603 41 0 3783 0
vsize: 15296
[startup+220.01 s]
Raw data (loadavg): 0.99 0.96 0.74 2/55 2383
Raw data (stat): 2381 (minisat+) R 2380 20024 20023 0 -1 0 3304 0 0 0 21990 9 0 0 25 0 1 0 487568598 15958016 3216 4294967295 134512640 134672761 3221224560 3221223728 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3896 3216 603 41 0 3855 0
vsize: 15584
[startup+230.01 s]
Raw data (loadavg): 0.99 0.96 0.74 2/55 2383
Raw data (stat): 2381 (minisat+) R 2380 20024 20023 0 -1 0 3324 0 0 0 22990 10 0 0 25 0 1 0 487568598 15958016 3236 4294967295 134512640 134672761 3221224560 3221223728 134560964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3896 3236 603 41 0 3855 0
vsize: 15584
[startup+240.012 s]
Raw data (loadavg): 0.99 0.96 0.74 2/55 2383
Raw data (stat): 2381 (minisat+) R 2380 20024 20023 0 -1 0 3334 0 0 0 23991 10 0 0 25 0 1 0 487568598 15958016 3246 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3896 3246 603 41 0 3855 0
vsize: 15584
[startup+250.012 s]
Raw data (loadavg): 0.99 0.96 0.75 2/55 2383
Raw data (stat): 2381 (minisat+) R 2380 20024 20023 0 -1 0 3337 0 0 0 24991 10 0 0 25 0 1 0 487568598 15958016 3249 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3896 3249 603 41 0 3855 0
vsize: 15584
[startup+260.012 s]
Raw data (loadavg): 0.99 0.96 0.75 2/55 2383
Raw data (stat): 2381 (minisat+) R 2380 20024 20023 0 -1 0 3375 0 0 0 25991 10 0 0 25 0 1 0 487568598 16252928 3287 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3968 3287 603 41 0 3927 0
vsize: 15872
[startup+270.013 s]
Raw data (loadavg): 0.99 0.97 0.75 2/55 2383
Raw data (stat): 2381 (minisat+) R 2380 20024 20023 0 -1 0 3458 0 0 0 26991 10 0 0 25 0 1 0 487568598 16519168 3370 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4033 3370 603 41 0 3992 0
vsize: 16132
[startup+280.013 s]
Raw data (loadavg): 0.99 0.97 0.75 2/55 2383
Raw data (stat): 2381 (minisat+) R 2380 20024 20023 0 -1 0 3514 0 0 0 27991 10 0 0 25 0 1 0 487568598 16797696 3426 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4101 3426 603 41 0 4060 0
vsize: 16404
[startup+290.014 s]
Raw data (loadavg): 0.99 0.97 0.75 2/55 2383
Raw data (stat): 2381 (minisat+) R 2380 20024 20023 0 -1 0 3516 0 0 0 28991 10 0 0 25 0 1 0 487568598 16797696 3428 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4101 3428 603 41 0 4060 0
vsize: 16404
[startup+300.014 s]
Raw data (loadavg): 0.99 0.97 0.76 2/55 2383
Raw data (stat): 2381 (minisat+) R 2380 20024 20023 0 -1 0 3527 0 0 0 29991 10 0 0 25 0 1 0 487568598 16797696 3439 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4101 3439 603 41 0 4060 0
vsize: 16404
[startup+310.014 s]
Raw data (loadavg): 0.99 0.97 0.76 2/55 2383
Raw data (stat): 2381 (minisat+) R 2380 20024 20023 0 -1 0 3538 0 0 0 30991 10 0 0 25 0 1 0 487568598 16986112 3450 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4147 3450 603 41 0 4106 0
vsize: 16588
[startup+320.015 s]
Raw data (loadavg): 0.99 0.97 0.76 2/55 2383
Raw data (stat): 2381 (minisat+) R 2380 20024 20023 0 -1 0 3549 0 0 0 31991 10 0 0 25 0 1 0 487568598 16986112 3461 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4147 3461 603 41 0 4106 0
vsize: 16588
[startup+330.015 s]
Raw data (loadavg): 0.99 0.97 0.76 2/55 2383
Raw data (stat): 2381 (minisat+) R 2380 20024 20023 0 -1 0 3571 0 0 0 32992 10 0 0 25 0 1 0 487568598 17182720 3483 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4195 3483 603 41 0 4154 0
vsize: 16780
[startup+340.015 s]
Raw data (loadavg): 0.99 0.97 0.76 2/55 2383
Raw data (stat): 2381 (minisat+) R 2380 20024 20023 0 -1 0 3584 0 0 0 33992 10 0 0 25 0 1 0 487568598 17182720 3496 4294967295 134512640 134672761 3221224560 3221223724 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4195 3496 603 41 0 4154 0
vsize: 16780
[startup+350.016 s]
Raw data (loadavg): 0.99 0.97 0.77 2/55 2383
Raw data (stat): 2381 (minisat+) R 2380 20024 20023 0 -1 0 3584 0 0 0 34992 10 0 0 25 0 1 0 487568598 17182720 3496 4294967295 134512640 134672761 3221224560 3221223664 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4195 3496 603 41 0 4154 0
vsize: 16780
[startup+360.017 s]
Raw data (loadavg): 0.99 0.97 0.77 2/55 2383
Raw data (stat): 2381 (minisat+) R 2380 20024 20023 0 -1 0 3584 0 0 0 35992 10 0 0 25 0 1 0 487568598 17182720 3496 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4195 3496 603 41 0 4154 0
vsize: 16780
[startup+370.017 s]
Raw data (loadavg): 0.99 0.97 0.77 2/55 2385
Raw data (stat): 2381 (minisat+) R 2380 20024 20023 0 -1 0 3638 0 0 0 36992 11 0 0 25 0 1 0 487568598 17444864 3550 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4259 3550 603 41 0 4218 0
vsize: 17036
[startup+380.017 s]
Raw data (loadavg): 0.99 0.97 0.77 2/55 2385
Raw data (stat): 2381 (minisat+) R 2380 20024 20023 0 -1 0 3718 0 0 0 37992 11 0 0 25 0 1 0 487568598 17711104 3630 4294967295 134512640 134672761 3221224560 3221223664 134560237 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4324 3630 603 41 0 4283 0
vsize: 17296
[startup+390.019 s]
Raw data (loadavg): 0.99 0.97 0.77 2/55 2385
Raw data (stat): 2381 (minisat+) R 2380 20024 20023 0 -1 0 3797 0 0 0 38992 11 0 0 25 0 1 0 487568598 18108416 3709 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4421 3709 603 41 0 4380 0
vsize: 17684
[startup+400.019 s]
Raw data (loadavg): 0.99 0.97 0.78 2/55 2385
Raw data (stat): 2381 (minisat+) R 2380 20024 20023 0 -1 0 3876 0 0 0 39992 12 0 0 25 0 1 0 487568598 18378752 3788 4294967295 134512640 134672761 3221224560 3221223728 134560833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4487 3788 603 41 0 4446 0
vsize: 17948
[startup+410.019 s]
Raw data (loadavg): 0.99 0.97 0.78 2/55 2385
Raw data (stat): 2381 (minisat+) R 2380 20024 20023 0 -1 0 3949 0 0 0 40992 12 0 0 25 0 1 0 487568598 18640896 3861 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4551 3861 603 41 0 4510 0
vsize: 18204
[startup+420.02 s]
Raw data (loadavg): 0.99 0.97 0.78 2/55 2385
Raw data (stat): 2381 (minisat+) R 2380 20024 20023 0 -1 0 4005 0 0 0 41991 12 0 0 25 0 1 0 487568598 18911232 3917 4294967295 134512640 134672761 3221224560 3221223696 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4617 3917 603 41 0 4576 0
vsize: 18468
[startup+430.02 s]
Raw data (loadavg): 0.99 0.97 0.78 2/55 2385
Raw data (stat): 2381 (minisat+) R 2380 20024 20023 0 -1 0 4079 0 0 0 42991 12 0 0 25 0 1 0 487568598 19402752 3991 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4737 3991 603 41 0 4696 0
vsize: 18948
[startup+440.021 s]
Raw data (loadavg): 0.99 0.97 0.78 2/55 2385
Raw data (stat): 2381 (minisat+) R 2380 20024 20023 0 -1 0 4139 0 0 0 43991 13 0 0 25 0 1 0 487568598 19533824 4051 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4769 4051 603 41 0 4728 0
vsize: 19076
[startup+450.022 s]
Raw data (loadavg): 0.99 0.97 0.79 2/55 2385
Raw data (stat): 2381 (minisat+) R 2380 20024 20023 0 -1 0 4202 0 0 0 44991 13 0 0 25 0 1 0 487568598 19828736 4114 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4841 4114 603 41 0 4800 0
vsize: 19364
[startup+460.021 s]
Raw data (loadavg): 0.99 0.97 0.79 2/55 2385
Raw data (stat): 2381 (minisat+) R 2380 20024 20023 0 -1 0 4269 0 0 0 45991 13 0 0 25 0 1 0 487568598 20127744 4181 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4914 4181 603 41 0 4873 0
vsize: 19656
[startup+470.021 s]
Raw data (loadavg): 0.99 0.97 0.79 2/55 2385
Raw data (stat): 2381 (minisat+) R 2380 20024 20023 0 -1 0 4328 0 0 0 46991 13 0 0 25 0 1 0 487568598 20393984 4240 4294967295 134512640 134672761 3221224560 3221223728 134561391 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4979 4240 603 41 0 4938 0
vsize: 19916
[startup+480.022 s]
Raw data (loadavg): 0.99 0.97 0.79 2/55 2385
Raw data (stat): 2381 (minisat+) R 2380 20024 20023 0 -1 0 4383 0 0 0 47991 13 0 0 25 0 1 0 487568598 20660224 4295 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5044 4295 603 41 0 5003 0
vsize: 20176
[startup+490.022 s]
Raw data (loadavg): 0.99 0.97 0.79 2/55 2385
Raw data (stat): 2381 (minisat+) R 2380 20024 20023 0 -1 0 4447 0 0 0 48991 14 0 0 25 0 1 0 487568598 20926464 4359 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5109 4359 603 41 0 5068 0
vsize: 20436
[startup+500.022 s]
Raw data (loadavg): 0.99 0.97 0.80 2/55 2385
Raw data (stat): 2381 (minisat+) R 2380 20024 20023 0 -1 0 4518 0 0 0 49991 14 0 0 25 0 1 0 487568598 21192704 4430 4294967295 134512640 134672761 3221224560 3221223664 134560198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5174 4430 603 41 0 5133 0
vsize: 20696
[startup+510.023 s]
Raw data (loadavg): 0.99 0.97 0.80 2/55 2385
Raw data (stat): 2381 (minisat+) R 2380 20024 20023 0 -1 0 4532 0 0 0 50991 14 0 0 25 0 1 0 487568598 21323776 4444 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5206 4444 603 41 0 5165 0
vsize: 20824
[startup+520.023 s]
Raw data (loadavg): 0.99 0.97 0.80 2/55 2385
Raw data (stat): 2381 (minisat+) R 2380 20024 20023 0 -1 0 4532 0 0 0 51991 14 0 0 25 0 1 0 487568598 21323776 4444 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5206 4444 603 41 0 5165 0
vsize: 20824
[startup+530.023 s]
Raw data (loadavg): 0.99 0.97 0.80 2/55 2385
Raw data (stat): 2381 (minisat+) R 2380 20024 20023 0 -1 0 4532 0 0 0 52992 14 0 0 25 0 1 0 487568598 21323776 4444 4294967295 134512640 134672761 3221224560 3221223728 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5206 4444 603 41 0 5165 0
vsize: 20824
[startup+540.024 s]
Raw data (loadavg): 0.99 0.97 0.80 2/55 2385
Raw data (stat): 2381 (minisat+) R 2380 20024 20023 0 -1 0 4532 0 0 0 53992 14 0 0 25 0 1 0 487568598 21323776 4444 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5206 4444 603 41 0 5165 0
vsize: 20824
[startup+550.025 s]
Raw data (loadavg): 0.99 0.97 0.81 2/55 2385
Raw data (stat): 2381 (minisat+) R 2380 20024 20023 0 -1 0 4532 0 0 0 54992 14 0 0 25 0 1 0 487568598 21323776 4444 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5206 4444 603 41 0 5165 0
vsize: 20824
[startup+560.025 s]
Raw data (loadavg): 0.99 0.97 0.81 2/55 2385
Raw data (stat): 2381 (minisat+) R 2380 20024 20023 0 -1 0 4532 0 0 0 55992 14 0 0 25 0 1 0 487568598 21323776 4444 4294967295 134512640 134672761 3221224560 3221223760 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5206 4444 603 41 0 5165 0
vsize: 20824
[startup+570.025 s]
Raw data (loadavg): 0.99 0.97 0.81 2/55 2385
Raw data (stat): 2381 (minisat+) R 2380 20024 20023 0 -1 0 4532 0 0 0 56992 14 0 0 25 0 1 0 487568598 21323776 4444 4294967295 134512640 134672761 3221224560 3221223760 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5206 4444 603 41 0 5165 0
vsize: 20824
[startup+580.025 s]
Raw data (loadavg): 0.99 0.97 0.81 2/55 2385
Raw data (stat): 2381 (minisat+) R 2380 20024 20023 0 -1 0 4532 0 0 0 57993 14 0 0 25 0 1 0 487568598 21323776 4444 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5206 4444 603 41 0 5165 0
vsize: 20824
[startup+590.025 s]
Raw data (loadavg): 0.99 0.97 0.81 2/55 2385
Raw data (stat): 2381 (minisat+) R 2380 20024 20023 0 -1 0 4532 0 0 0 58993 14 0 0 25 0 1 0 487568598 21323776 4444 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5206 4444 603 41 0 5165 0
vsize: 20824
[startup+600.026 s]
Raw data (loadavg): 0.99 0.97 0.81 2/55 2385
Raw data (stat): 2381 (minisat+) R 2380 20024 20023 0 -1 0 4535 0 0 0 59993 14 0 0 25 0 1 0 487568598 21323776 4447 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5206 4447 603 41 0 5165 0
vsize: 20824
[startup+608.615 s]
Raw data (loadavg): 0.99 0.97 0.82 1/54 2385
Raw data (stat): 2381 (minisat+) R 2380 20024 20023 0 -1 0 4535 0 0 0 59993 14 0 0 25 0 1 0 487568598 21323776 4447 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5206 4447 603 41 0 5165 0
vsize: 0

Child status: 30
Real time (s): 608.614
CPU time (s): 608.67
CPU user time (s): 608.514
CPU system time (s): 0.155976
CPU usage (%): 100.009
Max. virtual memory (Kb): 20824
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	1120
#### END VERIFIER DATA ####