PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-lseu.opb
MD5SUM	99657262afbbfce7034a3ec6b29d9b3b
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.02884
Number of variables	89
Total number of constraints	117
Number of constraints which are clauses	2
Number of constraints which are cardinality constraints (but not clauses)	104
Number of constraints which are nor clauses,nor cardinality constraints	11
Minimum length of a constraint	1
Maximum length of a constraint	47
Trace number 15059

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc18 THE 2005-04-21 02:59:12 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18499 boxname=wulflinc18 idbench=1423 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  99657262afbbfce7034a3ec6b29d9b3b  /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-13-7-lseu.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-13-7-lseu.opb /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-13-7-lseu.opb
IDLAUNCH: 18499
/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:        555248 kB
Buffers:         34496 kB
Cached:         413984 kB
SwapCached:        388 kB
Active:         145748 kB
Inactive:       305192 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        554996 kB
SwapTotal:     2097892 kB
SwapFree:      2096996 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6224 kB
Slab:            22848 kB
Committed_AS:    63816 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 03:08:29 (client local time) WITH STATUS 30 IN 556.593 SECONDS
stats: 18499 0 556.593 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 ---[  28]---> BDD-cost:    3
c ---[  27]---> BDD-cost:    7
c ---[  26]---> BDD-cost:    5
c ---[  24]---> BDD-cost:    3
c ---[  23]---> BDD-cost:    5
c ---[  22]---> BDD-cost:   11
c ---[  21]---> BDD-cost:    3
c ---[  20]---> BDD-cost:    7
c ---[  19]---> BDD-cost:    3
c ---[  18]---> BDD-cost:    7
c ---[  17]---> BDD-cost:    5
c ---[  16]---> BDD-cost:    7
c ---[  15]---> BDD-cost:    5
c ---[  14]---> BDD-cost:    3
c ---[  12]---> BDD-cost:    7
c ---[   9]---> Sorter-cost: 3170     Base: 5 2 2 3
c ---[   8]---> BDD-cost:   28
c ---[   7]---> BDD-cost:  202
c ---[   6]---> Sorter-cost: 1878     Base: 5 2 2 3
c ---[   4]---> Sorter-cost: 1741     Base: 5 2 2 2
c ---[   2]---> BDD-cost:   16
c ---[   0]---> BDD-cost:   32
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   18435    44047 |    6145       0        0     nan |  0.000 % |
c |       100 |   17905    42845 |    6759      87     1211    13.9 |  2.884 % |
c ==============================================================================
c [1mFound solution: 3706[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:12454     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       238 |   49551   117001 |   16517     217     3482    16.0 |  2.884 % |
c ==============================================================================
c [1mFound solution: 3646[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 |       322 |   50292   118812 |   16764     301     4848    16.1 |  2.884 % |
c ==============================================================================
c [1mFound solution: 3509[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 |       389 |   49541   117225 |   16513     356     5415    15.2 |  2.884 % |
c |       489 |   49541   117225 |   18164     456     6128    13.4 |  4.010 % |
c |       639 |   49028   116047 |   19980     599     8404    14.0 |  4.983 % |
c |       864 |   47046   111493 |   21978     748    10596    14.2 |  8.371 % |
c ==============================================================================
c [1mFound solution: 3497[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 |      1033 |   47013   111438 |   15671     914    12466    13.6 |  8.371 % |
c |      1133 |   46631   110560 |   17238    1005    13120    13.1 |  9.417 % |
c |      1283 |   46421   110076 |   18961    1146    14257    12.4 |  9.807 % |
c ==============================================================================
c [1mFound solution: 3098[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 |      1478 |   46086   109357 |   15362    1325    16765    12.7 |  9.807 % |
c |      1578 |   46086   109357 |   16898    1425    18802    13.2 | 10.963 % |
c |      1731 |   45911   108953 |   18588    1567    20057    12.8 | 11.269 % |
c |      1958 |   45819   108740 |   20446    1790    23204    13.0 | 11.427 % |
c ==============================================================================
c [1mFound solution: 2760[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 |      2074 |   46420   110213 |   15473    1906    24721    13.0 | 11.427 % |
c |      2174 |   46383   110128 |   17020    2002    26364    13.2 | 11.469 % |
c ==============================================================================
c [1mFound solution: 2738[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 |      2216 |   46631   110736 |   15543    2044    26963    13.2 | 11.469 % |
c |      2316 |   45992   109273 |   17097    2135    27675    13.0 | 12.554 % |
c |      2466 |   45746   108704 |   18807    2268    30775    13.6 | 13.012 % |
c ==============================================================================
c [1mFound solution: 2729[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 |      2652 |   45753   108721 |   15251    2454    45903    18.7 | 13.012 % |
c |      2753 |   45753   108721 |   16776    2555    47971    18.8 | 13.016 % |
c |      2903 |   45753   108721 |   18453    2705    50116    18.5 | 13.016 % |
c ==============================================================================
c [1mFound solution: 2598[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 |      2968 |   45963   109251 |   15321    2768    51198    18.5 | 13.016 % |
c |      3074 |   45963   109251 |   16853    2874    52424    18.2 | 13.060 % |
c |      3224 |   43854   104373 |   18538    2962    52992    17.9 | 16.849 % |
c |      3449 |   43002   102400 |   20392    3159    55173    17.5 | 18.280 % |
c |      3786 |   42006   100079 |   22431    3436    57494    16.7 | 20.114 % |
c |      4294 |   41967    99989 |   24674    3943    93789    23.8 | 20.178 % |
c ==============================================================================
c [1mFound solution: 2514[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 |      4650 |   42115   100365 |   14038    4294    99198    23.1 | 20.178 % |
c |      4750 |   41935    99951 |   15441    4383   101783    23.2 | 20.563 % |
c |      4902 |   41867    99795 |   16985    4529   105912    23.4 | 20.684 % |
c |      5127 |   41867    99795 |   18684    4754   117824    24.8 | 20.684 % |
c ==============================================================================
c [1mFound solution: 2360[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 |      5168 |   41906    99898 |   13968    4795   120669    25.2 | 20.684 % |
c |      5268 |   41906    99898 |   15364    4895   121972    24.9 | 20.680 % |
c |      5418 |   41906    99898 |   16901    5045   124153    24.6 | 20.680 % |
c |      5645 |   41906    99898 |   18591    5272   127240    24.1 | 20.680 % |
c |      5982 |   41906    99898 |   20450    5609   155430    27.7 | 20.680 % |
c ==============================================================================
c [1mFound solution: 2290[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 |      6227 |   41871    99820 |   13957    5853   159241    27.2 | 20.680 % |
c |      6327 |   41760    99561 |   15352    5944   160678    27.0 | 20.974 % |
c |      6477 |   41760    99561 |   16887    6094   162940    26.7 | 20.974 % |
c |      6702 |   40960    97704 |   18576    6292   166141    26.4 | 22.399 % |
c |      7039 |   40592    96849 |   20434    6514   173432    26.6 | 23.077 % |
c |      7546 |   40564    96785 |   22477    7017   213730    30.5 | 23.123 % |
c ==============================================================================
c [1mFound solution: 2264[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 |      7669 |   40590    96855 |   13530    7140   216541    30.3 | 23.123 % |
c |      7773 |   40590    96855 |   14883    7244   222878    30.8 | 23.122 % |
c |      7924 |   40590    96855 |   16371    7395   225486    30.5 | 23.122 % |
c |      8152 |   40590    96855 |   18008    7623   234777    30.8 | 23.122 % |
c |      8490 |   40590    96855 |   19809    7961   259509    32.6 | 23.122 % |
c |      8996 |   40558    96784 |   21790    8465   276031    32.6 | 23.174 % |
c |      9756 |   40553    96769 |   23969    9224   340049    36.9 | 23.179 % |
c |     10895 |   40490    96623 |   26366   10358   371317    35.8 | 23.289 % |
c |     12603 |   40490    96623 |   29002   12066   463467    38.4 | 23.289 % |
c |     15166 |   40490    96623 |   31903   14629   564096    38.6 | 23.289 % |
c ==============================================================================
c [1mFound solution: 2230[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 |     15526 |   40497    96647 |   13499   14988   577028    38.5 | 23.289 % |
c |     15626 |   40422    96474 |   14848   15078   578713    38.4 | 23.459 % |
c |     15781 |   40422    96474 |   16333   15233   582575    38.2 | 23.459 % |
c |     16007 |   40422    96474 |   17967   15459   593362    38.4 | 23.459 % |
c ==============================================================================
c [1mFound solution: 2196[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 |     16073 |   40439    96517 |   13479   15525   594764    38.3 | 23.459 % |
c ==============================================================================
c [1mFound solution: 2111[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 |     16113 |   40450    96544 |   13483   15565   597462    38.4 | 23.459 % |
c |     16215 |   40359    96334 |   14831   15664   599951    38.3 | 23.619 % |
c |     16366 |   40278    96147 |   16314   15813   603495    38.2 | 23.768 % |
c |     16594 |   40278    96147 |   17945   16041   608473    37.9 | 23.768 % |
c |     16932 |   40278    96147 |   19740   16379   620046    37.9 | 23.768 % |
c ==============================================================================
c [1mFound solution: 1942[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 |     16974 |   40297    96194 |   13432   16421   621027    37.8 | 23.768 % |
c |     17074 |   40289    96176 |   14775   16520   623605    37.7 | 23.771 % |
c |     17224 |   40289    96176 |   16252   16670   627184    37.6 | 23.771 % |
c |     17449 |   40289    96176 |   17877   16895   636695    37.7 | 23.771 % |
c |     17786 |   40289    96176 |   19665   17232   653727    37.9 | 23.771 % |
c |     18294 |   40289    96176 |   21632   17740   679909    38.3 | 23.771 % |
c ==============================================================================
c [1mFound solution: 1926[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 |     18947 |   40294    96189 |   13431   18393   707372    38.5 | 23.771 % |
c |     19047 |   40294    96189 |   14774    9297   273510    29.4 | 23.774 % |
c |     19198 |   40294    96189 |   16251    9448   278106    29.4 | 23.774 % |
c |     19425 |   40294    96189 |   17876    9675   284263    29.4 | 23.774 % |
c |     19762 |   40243    96071 |   19664   10010   303905    30.4 | 23.872 % |
c |     20268 |   40243    96071 |   21630   10516   331768    31.5 | 23.872 % |
c |     21027 |   40243    96071 |   23793   11275   376456    33.4 | 23.872 % |
c ==============================================================================
c [1mFound solution: 1921[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 |     21537 |   39762    94949 |   13254   11781   397028    33.7 | 23.872 % |
c |     21637 |   39762    94949 |   14579   11881   401507    33.8 | 24.741 % |
c |     21787 |   39762    94949 |   16037   12031   406152    33.8 | 24.741 % |
c |     22013 |   39762    94949 |   17641   12257   417533    34.1 | 24.741 % |
c |     22352 |   39631    94647 |   19405   12589   427213    33.9 | 24.976 % |
c |     22858 |   39631    94647 |   21345   13095   454469    34.7 | 24.976 % |
c |     23617 |   39631    94647 |   23480   13854   490846    35.4 | 24.976 % |
c |     24756 |   39607    94592 |   25828   14992   560541    37.4 | 25.004 % |
c |     26466 |   39387    94074 |   28411   16688   596272    35.7 | 25.417 % |
c |     29029 |   39387    94074 |   31252   19251   683079    35.5 | 25.417 % |
c ==============================================================================
c [1mFound solution: 1902[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 |     29256 |   39399    94104 |   13133   19478   689031    35.4 | 25.417 % |
c |     29356 |   39399    94104 |   14446    9839   262130    26.6 | 25.417 % |
c |     29506 |   39399    94104 |   15890    9989   270317    27.1 | 25.417 % |
c |     29732 |   39399    94104 |   17480   10215   280380    27.4 | 25.417 % |
c |     30069 |   39399    94104 |   19228   10552   300846    28.5 | 25.417 % |
c ==============================================================================
c [1mFound solution: 1844[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 |     30155 |   39407    94124 |   13135   10638   304826    28.7 | 25.417 % |
c ==============================================================================
c [1mFound solution: 1785[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 |     30240 |   39415    94144 |   13138   10723   309696    28.9 | 25.417 % |
c |     30340 |   39410    94129 |   14451   10822   311047    28.7 | 25.425 % |
c |     30490 |   39405    94114 |   15896   10971   315606    28.8 | 25.431 % |
c |     30715 |   39405    94114 |   17486   11196   324462    29.0 | 25.431 % |
c ==============================================================================
c [1mFound solution: 1769[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 |     30873 |   39411    94130 |   13137   11354   332222    29.3 | 25.431 % |
c |     30975 |   39411    94130 |   14450   11456   335406    29.3 | 25.434 % |
c |     31125 |   39411    94130 |   15895   11606   339707    29.3 | 25.434 % |
c ==============================================================================
c [1mFound solution: 1764[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 |     31242 |   39426    94167 |   13142   11723   346819    29.6 | 25.434 % |
c |     31343 |   39416    94144 |   14456   11823   348053    29.4 | 25.444 % |
c |     31494 |   39416    94144 |   15901   11974   355845    29.7 | 25.444 % |
c |     31720 |   39416    94144 |   17492   12200   365729    30.0 | 25.444 % |
c |     32059 |   39390    94083 |   19241   12538   373153    29.8 | 25.478 % |
c |     32565 |   39310    93901 |   21165   13042   383802    29.4 | 25.610 % |
c ==============================================================================
c [1mFound solution: 1755[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 |     33157 |   39334    93967 |   13111   13634   400144    29.3 | 25.610 % |
c ==============================================================================
c [1mFound solution: 1748[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 |     33182 |   39345    93994 |   13115   13659   401624    29.4 | 25.610 % |
c |     33283 |   39345    93994 |   14426   13760   407300    29.6 | 25.610 % |
c ==============================================================================
c [1mFound solution: 1740[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 |     33304 |   39352    94011 |   13117   13781   408198    29.6 | 25.610 % |
c ==============================================================================
c [1mFound solution: 1739[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 |     33310 |   39363    94038 |   13121   13787   408364    29.6 | 25.610 % |
c |     33410 |   39363    94038 |   14433   13887   414977    29.9 | 25.611 % |
c ==============================================================================
c [1mFound solution: 1664[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 |     33432 |   39374    94065 |   13124   13909   415503    29.9 | 25.611 % |
c ==============================================================================
c [1mFound solution: 1582[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 |     33469 |   39403    94137 |   13134   13946   417045    29.9 | 25.611 % |
c ==============================================================================
c [1mFound solution: 1562[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 |     33475 |   39415    94167 |   13138   13952   417136    29.9 | 25.611 % |
c |     33575 |   39415    94167 |   14451   14052   421899    30.0 | 25.601 % |
c |     33726 |   39415    94167 |   15896   14203   424212    29.9 | 25.601 % |
c |     33952 |   39415    94167 |   17486   14429   426999    29.6 | 25.601 % |
c |     34290 |   39415    94167 |   19235   14767   450048    30.5 | 25.601 % |
c |     34797 |   39415    94167 |   21158   15274   458322    30.0 | 25.602 % |
c |     35560 |   39415    94167 |   23274   16037   471992    29.4 | 25.602 % |
c |     36699 |   39415    94167 |   25602   17176   539850    31.4 | 25.602 % |
c |     38407 |   39415    94167 |   28162   18884   625011    33.1 | 25.601 % |
c ==============================================================================
c [1mFound solution: 1550[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 |     38665 |   39426    94194 |   13142   19142   635918    33.2 | 25.601 % |
c |     38766 |   39426    94194 |   14456    9672   277825    28.7 | 25.601 % |
c ==============================================================================
c [1mFound solution: 1524[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 |     38874 |   39437    94221 |   13145    9780   284392    29.1 | 25.601 % |
c |     38975 |   39437    94221 |   14459    9881   286834    29.0 | 25.601 % |
c |     39125 |   39431    94207 |   15905   10030   289534    28.9 | 25.613 % |
c |     39350 |   39431    94207 |   17495   10255   292945    28.6 | 25.613 % |
c |     39687 |   39431    94207 |   19245   10592   298412    28.2 | 25.613 % |
c ==============================================================================
c [1mFound solution: 1486[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 |     40087 |   39442    94234 |   13147   10992   306353    27.9 | 25.613 % |
c |     40187 |   39442    94234 |   14461   11092   307643    27.7 | 25.612 % |
c |     40337 |   39442    94234 |   15907   11242   320119    28.5 | 25.612 % |
c |     40562 |   39442    94234 |   17498   11467   324070    28.3 | 25.612 % |
c |     40899 |   39442    94234 |   19248   11804   335319    28.4 | 25.612 % |
c |     41407 |   39432    94211 |   21173   12311   352466    28.6 | 25.630 % |
c |     42166 |   39432    94211 |   23290   13070   381728    29.2 | 25.630 % |
c |     43306 |   39432    94211 |   25619   14210   426455    30.0 | 25.630 % |
c |     45014 |   39432    94211 |   28181   15918   501051    31.5 | 25.630 % |
c ==============================================================================
c [1mFound solution: 1334[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 |     46447 |   39378    94086 |   13126   17349   562939    32.4 | 25.630 % |
c |     46547 |   39378    94086 |   14438   17449   566917    32.5 | 25.759 % |
c |     46697 |   39378    94086 |   15882   17599   570946    32.4 | 25.759 % |
c |     46922 |   39378    94086 |   17470   17824   578290    32.4 | 25.759 % |
c ==============================================================================
c [1mFound solution: 1321[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 |     47115 |   39392    94120 |   13130   18017   588067    32.6 | 25.759 % |
c |     47215 |   39392    94120 |   14443    9109   252611    27.7 | 25.758 % |
c ==============================================================================
c [1mFound solution: 1315[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 |     47304 |   39403    94147 |   13134    9198   257848    28.0 | 25.758 % |
c |     47406 |   39403    94147 |   14447    9300   261943    28.2 | 25.758 % |
c |     47556 |   39403    94147 |   15892    9450   267536    28.3 | 25.758 % |
c |     47781 |   39403    94147 |   17481    9675   277815    28.7 | 25.758 % |
c |     48118 |   39403    94147 |   19229   10012   295645    29.5 | 25.758 % |
c ==============================================================================
c [1mFound solution: 1299[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    1     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     48157 |   39422    94195 |   13140   10051   297693    29.6 | 25.758 % |
c |     48258 |   39422    94195 |   14454   10152   302634    29.8 | 25.753 % |
c |     48408 |   39422    94195 |   15899   10302   308843    30.0 | 25.753 % |
c |     48634 |   39422    94195 |   17489   10528   312444    29.7 | 25.753 % |
c ==============================================================================
c [1mFound solution: 1296[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 |     48724 |   39431    94218 |   13143   10618   314824    29.7 | 25.753 % |
c |     48824 |   39431    94218 |   14457   10718   317890    29.7 | 25.754 % |
c |     48974 |   39431    94218 |   15903   10868   321750    29.6 | 25.754 % |
c ==============================================================================
c [1mFound solution: 1262[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 |     49021 |   39442    94245 |   13147   10915   323492    29.6 | 25.754 % |
c |     49124 |   39442    94245 |   14461   11018   327931    29.8 | 25.754 % |
c ==============================================================================
c [1mFound solution: 1261[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 |     49225 |   39453    94272 |   13151   11119   331970    29.9 | 25.754 % |
c |     49325 |   39453    94272 |   14466   11219   335905    29.9 | 25.754 % |
c |     49476 |   39453    94272 |   15912   11370   342680    30.1 | 25.754 % |
c ==============================================================================
c [1mFound solution: 1257[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 |     49518 |   39461    94292 |   13153   11412   344998    30.2 | 25.754 % |
c |     49618 |   39461    94292 |   14468   11512   348163    30.2 | 25.755 % |
c |     49768 |   39461    94292 |   15915   11662   354188    30.4 | 25.755 % |
c |     49993 |   39461    94292 |   17506   11887   358707    30.2 | 25.755 % |
c |     50330 |   39461    94292 |   19257   12224   369811    30.3 | 25.755 % |
c |     50836 |   39461    94292 |   21183   12730   386469    30.4 | 25.755 % |
c |     51595 |   39372    94086 |   23301   13486   420790    31.2 | 25.909 % |
c |     52734 |   39325    93976 |   25631   14622   479410    32.8 | 26.000 % |
c |     54442 |   39325    93976 |   28194   16330   521112    31.9 | 26.000 % |
c ==============================================================================
c [1mFound solution: 1244[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 |     55336 |   39336    94003 |   13112   17224   554244    32.2 | 26.000 % |
c |     55436 |   39336    94003 |   14423   17324   558460    32.2 | 26.000 % |
c |     55587 |   39336    94003 |   15865   17475   560803    32.1 | 26.000 % |
c |     55812 |   39336    94003 |   17452   17700   569223    32.2 | 26.000 % |
c |     56150 |   39336    94003 |   19197   18038   586944    32.5 | 26.000 % |
c |     56656 |   39336    94003 |   21117   18544   611308    33.0 | 26.000 % |
c |     57415 |   39336    94003 |   23228   19303   650563    33.7 | 26.000 % |
c ==============================================================================
c [1mFound solution: 1234[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 |     57865 |   39347    94030 |   13115   19753   668644    33.9 | 26.000 % |
c |     57967 |   39347    94030 |   14426    9979   246565    24.7 | 26.000 % |
c |     58118 |   39347    94030 |   15869   10130   253341    25.0 | 26.000 % |
c |     58345 |   39333    93998 |   17456   10356   265262    25.6 | 26.023 % |
c ==============================================================================
c [1mFound solution: 1214[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 |     58368 |   39344    94025 |   13114   10379   265964    25.6 | 26.023 % |
c |     58468 |   39344    94025 |   14425   10479   270517    25.8 | 26.022 % |
c ==============================================================================
c [1mFound solution: 1194[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 |     58542 |   39351    94042 |   13117   10553   274457    26.0 | 26.022 % |
c |     58642 |   39351    94042 |   14428   10653   278093    26.1 | 26.024 % |
c |     58793 |   39351    94042 |   15871   10804   283567    26.2 | 26.024 % |
c |     59019 |   39351    94042 |   17458   11030   293283    26.6 | 26.024 % |
c |     59360 |   39351    94042 |   19204   11371   312033    27.4 | 26.024 % |
c ==============================================================================
c [1mFound solution: 1149[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 |     59469 |   39356    94055 |   13118   11480   317888    27.7 | 26.024 % |
c ==============================================================================
c [1mFound solution: 1145[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 |     59514 |   39364    94075 |   13121   11525   319355    27.7 | 26.024 % |
c |     59617 |   39360    94065 |   14433   11627   323503    27.8 | 26.033 % |
c |     59767 |   39360    94065 |   15876   11777   328091    27.9 | 26.033 % |
c |     59993 |   39360    94065 |   17464   12003   334351    27.9 | 26.033 % |
c |     60330 |   39360    94065 |   19210   12340   346546    28.1 | 26.033 % |
c |     60837 |   39360    94065 |   21131   12847   362634    28.2 | 26.033 % |
c |     61596 |   39360    94065 |   23244   13606   405134    29.8 | 26.033 % |
c |     62735 |   39360    94065 |   25569   14745   433845    29.4 | 26.033 % |
c |     64443 |   39360    94065 |   28126   16453   468750    28.5 | 26.033 % |
c ==============================================================================
c [1mFound solution: 1136[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 |     64884 |   39374    94099 |   13124   16894   485278    28.7 | 26.033 % |
c |     64984 |   39374    94099 |   14436   16994   488957    28.8 | 26.032 % |
c |     65138 |   39374    94099 |   15880   17148   495823    28.9 | 26.032 % |
c |     65364 |   39374    94099 |   17468   17374   504844    29.1 | 26.032 % |
c |     65701 |   39359    94059 |   19214   17710   515265    29.1 | 26.037 % |
c |     66208 |   39359    94059 |   21136   18217   533652    29.3 | 26.037 % |
c |     66967 |   39359    94059 |   23249   18976   559816    29.5 | 26.037 % |
c |     68108 |   39359    94059 |   25574   20117   617911    30.7 | 26.037 % |
c |     69817 |   39359    94059 |   28132   21826   694674    31.8 | 26.037 % |
c |     72379 |   39359    94059 |   30945   24388   790130    32.4 | 26.037 % |
c |     76223 |   39304    93929 |   34040   28231  1005758    35.6 | 26.157 % |
c |     81990 |   39212    93714 |   37444   33994  1262798    37.1 | 26.311 % |
c ==============================================================================
c [1mFound solution: 1128[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 |     88107 |   39211    93714 |   13070   40110  1508942    37.6 | 26.311 % |
c |     88207 |   39211    93714 |   14377    9622   245626    25.5 | 26.327 % |
c |     88357 |   39211    93714 |   15814    9772   252727    25.9 | 26.327 % |
c |     88582 |   39211    93714 |   17396    9997   261822    26.2 | 26.327 % |
c |     88919 |   39211    93714 |   19135   10334   276258    26.7 | 26.327 % |
c |     89425 |   39211    93714 |   21049   10840   303438    28.0 | 26.327 % |
c |     90184 |   39211    93714 |   23154   11599   332528    28.7 | 26.327 % |
c |     91325 |   39211    93714 |   25469   12740   389477    30.6 | 26.327 % |
c |     93033 |   39211    93714 |   28016   14448   493060    34.1 | 26.327 % |
c |     95596 |   39211    93714 |   30818   17011   598307    35.2 | 26.327 % |
c |     99440 |   39135    93537 |   33900   20854   738298    35.4 | 26.475 % |
c |    105208 |   39066    93379 |   37290   22403   929250    41.5 | 26.583 % |
c |    113858 |   38759    92675 |   41019   30435  1356310    44.6 | 27.095 % |
c ==============================================================================
c [1mFound solution: 1120[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 |    123278 |   38676    92482 |   12892   39850  1800761    45.2 | 27.095 % |
c |    123380 |   38676    92482 |   14181    9793   260212    26.6 | 27.250 % |
c |    123530 |   38676    92482 |   15599    9943   266093    26.8 | 27.250 % |
c |    123756 |   38676    92482 |   17159   10169   276812    27.2 | 27.250 % |
c |    124093 |   38676    92482 |   18875   10506   290388    27.6 | 27.251 % |
c |    124599 |   38137    91231 |   20762    9142   237989    26.0 | 28.138 % |
c |    125358 |   38137    91231 |   22838    9901   263034    26.6 | 28.137 % |
c ==============================================================================
c [1mOptimal solution: 1120[0m
s OPTIMUM FOUND
v C101_bit0 C102_bit0 -C103_bit0 -C104_bit0 -C105_bit0 -C108_bit0 -C111_bit0 -C112_bit0 -C113_bit0 C114_bit0 -C115_bit0 -C116_bit0 -C117_bit0 -C118_bit0 -C119_bit0 -C120_bit0 -C121_bit0 -C122_bit0 -C123_bit0 -C124_bit0 -C125_bit0 -C126_bit0 C127_bit0 -C128_bit0 -C129_bit0 -C130_bit0 -C131_bit0 -C132_bit0 -C133_bit0 -C134_bit0 C135_bit0 -C136_bit0 -C137_bit0 -C138_bit0 C139_bit0 -C140_bit0 -C141_bit0 -C142_bit0 C143_bit0 -C144_bit0 -C145_bit0 -C146_bit0 -C147_bit0 -C148_bit0 -C149_bit0 -C150_bit0 C151_bit0 -C152_bit0 C153_bit0 -C154_bit0 -C155_bit0 -C156_bit0 -C157_bit0 -C158_bit0 -C159_bit0 -C160_bit0 -C161_bit0 -C162_bit0 -C163_bit0 C164_bit0 -C165_bit0 C166_bit0 -C167_bit0 -C168_bit0 -C169_bit0 -C170_bit0 -C171_bit0 -C172_bit0 -C173_bit0 -C174_bit0 -C175_bit0 -C176_bit0 -C177_bit0 -C178_bit0 -C179_bit0 -C180_bit0 -C181_bit0 -C182_bit0 -C183_bit0 -C184_bit0 -C185_bit0 C186_bit0 -C187_bit0 -C188_bit0 -C189_bit0 -C106_bit0 C107_bit0 -C109_bit0 -C110_bit0
c _______________________________________________________________________________
c 
c restarts              : 231
c conflicts             : 125428         (225 /sec)
c decisions             : 192116         (345 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 556.228 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.85 0.97 0.92 2/55 15928
Raw data (stat): 15928 (runsolver) R 15927 20024 20023 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 541656523 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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.0001 s]
Raw data (loadavg): 0.87 0.97 0.92 2/55 15928
Raw data (stat): 15928 (minisat+) R 15927 20024 20023 0 -1 0 1830 0 0 0 993 5 0 0 25 0 1 0 541656523 10088448 1799 4294967295 134512640 134672761 3221224544 3221223680 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2463 1799 603 41 0 2422 0
vsize: 9852
[startup+20.0002 s]
Raw data (loadavg): 0.89 0.97 0.92 2/55 15928
Raw data (stat): 15928 (minisat+) R 15927 20024 20023 0 -1 0 1998 0 0 0 1992 6 0 0 25 0 1 0 541656523 10813440 1967 4294967295 134512640 134672761 3221224544 3221223648 134560160 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2640 1967 603 41 0 2599 0
vsize: 10560
[startup+30.0015 s]
Raw data (loadavg): 0.91 0.97 0.92 2/55 15928
Raw data (stat): 15928 (minisat+) R 15927 20024 20023 0 -1 0 2236 0 0 0 2991 7 0 0 25 0 1 0 541656523 11747328 2205 4294967295 134512640 134672761 3221224544 3221223680 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2868 2205 603 41 0 2827 0
vsize: 11472
[startup+40.0018 s]
Raw data (loadavg): 0.92 0.97 0.92 2/55 15928
Raw data (stat): 15928 (minisat+) R 15927 20024 20023 0 -1 0 2377 0 0 0 3989 8 0 0 25 0 1 0 541656523 12279808 2346 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2998 2346 603 41 0 2957 0
vsize: 11992
[startup+50.0021 s]
Raw data (loadavg): 0.93 0.97 0.92 2/55 15928
Raw data (stat): 15928 (minisat+) R 15927 20024 20023 0 -1 0 2506 0 0 0 4989 8 0 0 25 0 1 0 541656523 12910592 2475 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3152 2475 603 41 0 3111 0
vsize: 12608
[startup+60.0027 s]
Raw data (loadavg): 0.94 0.97 0.92 2/55 15981
Raw data (stat): 15928 (minisat+) R 15927 20024 20023 0 -1 0 2599 0 0 0 5974 23 0 0 25 0 1 0 541656523 13266944 2568 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3239 2568 603 41 0 3198 0
vsize: 12956
[startup+70.0032 s]
Raw data (loadavg): 0.95 0.97 0.92 2/55 15981
Raw data (stat): 15928 (minisat+) R 15927 20024 20023 0 -1 0 2599 0 0 0 6974 23 0 0 25 0 1 0 541656523 13266944 2568 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3239 2568 603 41 0 3198 0
vsize: 12956
[startup+80.0042 s]
Raw data (loadavg): 0.96 0.97 0.92 2/55 15981
Raw data (stat): 15928 (minisat+) R 15927 20024 20023 0 -1 0 2599 0 0 0 7973 23 0 0 25 0 1 0 541656523 13266944 2568 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3239 2568 603 41 0 3198 0
vsize: 12956
[startup+90.0046 s]
Raw data (loadavg): 0.96 0.97 0.92 2/55 15981
Raw data (stat): 15928 (minisat+) R 15927 20024 20023 0 -1 0 2599 0 0 0 8973 23 0 0 25 0 1 0 541656523 13266944 2568 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3239 2568 603 41 0 3198 0
vsize: 12956
[startup+100.005 s]
Raw data (loadavg): 0.97 0.97 0.92 2/55 15983
Raw data (stat): 15928 (minisat+) R 15927 20024 20023 0 -1 0 2638 0 0 0 9973 24 0 0 25 0 1 0 541656523 13398016 2607 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3271 2607 603 41 0 3230 0
vsize: 13084
[startup+110.006 s]
Raw data (loadavg): 0.97 0.97 0.92 2/55 15983
Raw data (stat): 15928 (minisat+) R 15927 20024 20023 0 -1 0 2638 0 0 0 10973 24 0 0 25 0 1 0 541656523 13398016 2607 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3271 2607 603 41 0 3230 0
vsize: 13084
[startup+120.006 s]
Raw data (loadavg): 0.98 0.97 0.92 2/55 15983
Raw data (stat): 15928 (minisat+) R 15927 20024 20023 0 -1 0 2638 0 0 0 11973 24 0 0 25 0 1 0 541656523 13398016 2607 4294967295 134512640 134672761 3221224544 3221223680 134560598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3271 2607 603 41 0 3230 0
vsize: 13084
[startup+130.008 s]
Raw data (loadavg): 0.98 0.97 0.92 2/55 15985
Raw data (stat): 15928 (minisat+) R 15927 20024 20023 0 -1 0 2638 0 0 0 12972 25 0 0 25 0 1 0 541656523 13398016 2607 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3271 2607 603 41 0 3230 0
vsize: 13084
[startup+140.009 s]
Raw data (loadavg): 0.98 0.97 0.92 2/55 15985
Raw data (stat): 15928 (minisat+) R 15927 20024 20023 0 -1 0 2646 0 0 0 13972 25 0 0 25 0 1 0 541656523 13398016 2615 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3271 2615 603 41 0 3230 0
vsize: 13084
[startup+150.009 s]
Raw data (loadavg): 0.98 0.97 0.92 2/55 15985
Raw data (stat): 15928 (minisat+) R 15927 20024 20023 0 -1 0 2646 0 0 0 14972 25 0 0 25 0 1 0 541656523 13398016 2615 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3271 2615 603 41 0 3230 0
vsize: 13084
[startup+160.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 15985
Raw data (stat): 15928 (minisat+) R 15927 20024 20023 0 -1 0 2646 0 0 0 15972 25 0 0 25 0 1 0 541656523 13398016 2615 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3271 2615 603 41 0 3230 0
vsize: 13084
[startup+170.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 15985
Raw data (stat): 15928 (minisat+) R 15927 20024 20023 0 -1 0 2649 0 0 0 16972 26 0 0 25 0 1 0 541656523 13398016 2618 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3271 2618 603 41 0 3230 0
vsize: 13084
[startup+180.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 15985
Raw data (stat): 15928 (minisat+) R 15927 20024 20023 0 -1 0 2650 0 0 0 17972 26 0 0 25 0 1 0 541656523 13398016 2619 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3271 2619 603 41 0 3230 0
vsize: 13084
[startup+190.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 15985
Raw data (stat): 15928 (minisat+) R 15927 20024 20023 0 -1 0 2650 0 0 0 18972 26 0 0 25 0 1 0 541656523 13398016 2619 4294967295 134512640 134672761 3221224544 3221223700 134561032 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3271 2619 603 41 0 3230 0
vsize: 13084
[startup+200.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 15985
Raw data (stat): 15928 (minisat+) R 15927 20024 20023 0 -1 0 2662 0 0 0 19972 26 0 0 25 0 1 0 541656523 13533184 2631 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3304 2631 603 41 0 3263 0
vsize: 13216
[startup+210.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 15985
Raw data (stat): 15928 (minisat+) R 15927 20024 20023 0 -1 0 2686 0 0 0 20971 27 0 0 25 0 1 0 541656523 13664256 2655 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3336 2655 603 41 0 3295 0
vsize: 13344
[startup+220.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 15985
Raw data (stat): 15928 (minisat+) R 15927 20024 20023 0 -1 0 2715 0 0 0 21971 27 0 0 25 0 1 0 541656523 13750272 2684 4294967295 134512640 134672761 3221224544 3221223728 134558687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3357 2684 603 41 0 3316 0
vsize: 13428
[startup+230.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 15985
Raw data (stat): 15928 (minisat+) R 15927 20024 20023 0 -1 0 2715 0 0 0 22971 27 0 0 25 0 1 0 541656523 13750272 2684 4294967295 134512640 134672761 3221224544 3221223680 134560608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3357 2684 603 41 0 3316 0
vsize: 13428
[startup+240.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 15985
Raw data (stat): 15928 (minisat+) R 15927 20024 20023 0 -1 0 2716 0 0 0 23971 27 0 0 25 0 1 0 541656523 13750272 2685 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3357 2685 603 41 0 3316 0
vsize: 13428
[startup+250.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 15985
Raw data (stat): 15928 (minisat+) R 15927 20024 20023 0 -1 0 2720 0 0 0 24971 27 0 0 25 0 1 0 541656523 13750272 2689 4294967295 134512640 134672761 3221224544 3221223712 134561400 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3357 2689 603 41 0 3316 0
vsize: 13428
[startup+260.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 15985
Raw data (stat): 15928 (minisat+) R 15927 20024 20023 0 -1 0 2722 0 0 0 25971 27 0 0 25 0 1 0 541656523 13750272 2691 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3357 2691 603 41 0 3316 0
vsize: 13428
[startup+270.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 15985
Raw data (stat): 15928 (minisat+) R 15927 20024 20023 0 -1 0 2805 0 0 0 26971 28 0 0 25 0 1 0 541656523 14147584 2774 4294967295 134512640 134672761 3221224544 3221223680 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3454 2774 603 41 0 3413 0
vsize: 13816
[startup+280.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 15985
Raw data (stat): 15928 (minisat+) R 15927 20024 20023 0 -1 0 2921 0 0 0 27970 29 0 0 25 0 1 0 541656523 14548992 2890 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3552 2890 603 41 0 3511 0
vsize: 14208
[startup+290.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 15985
Raw data (stat): 15928 (minisat+) R 15927 20024 20023 0 -1 0 3040 0 0 0 28970 30 0 0 25 0 1 0 541656523 15110144 3009 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3689 3009 603 41 0 3648 0
vsize: 14756
[startup+300.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 15985
Raw data (stat): 15928 (minisat+) R 15927 20024 20023 0 -1 0 3161 0 0 0 29969 30 0 0 25 0 1 0 541656523 15642624 3130 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3819 3130 603 41 0 3778 0
vsize: 15276
[startup+310.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 15985
Raw data (stat): 15928 (minisat+) R 15927 20024 20023 0 -1 0 3251 0 0 0 30969 30 0 0 25 0 1 0 541656523 15908864 3220 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3884 3220 603 41 0 3843 0
vsize: 15536
[startup+320.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 15985
Raw data (stat): 15928 (minisat+) R 15927 20024 20023 0 -1 0 3339 0 0 0 31969 30 0 0 25 0 1 0 541656523 16302080 3308 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3980 3308 603 41 0 3939 0
vsize: 15920
[startup+330.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 15985
Raw data (stat): 15928 (minisat+) R 15927 20024 20023 0 -1 0 3456 0 0 0 32969 31 0 0 25 0 1 0 541656523 16834560 3425 4294967295 134512640 134672761 3221224544 3221223712 134560806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4110 3425 603 41 0 4069 0
vsize: 16440
[startup+340.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 15985
Raw data (stat): 15928 (minisat+) R 15927 20024 20023 0 -1 0 3541 0 0 0 33969 31 0 0 25 0 1 0 541656523 17231872 3510 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4207 3510 603 41 0 4166 0
vsize: 16828
[startup+350.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 15985
Raw data (stat): 15928 (minisat+) R 15927 20024 20023 0 -1 0 3622 0 0 0 34969 32 0 0 25 0 1 0 541656523 17522688 3591 4294967295 134512640 134672761 3221224544 3221223712 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4278 3591 603 41 0 4237 0
vsize: 17112
[startup+360.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 15985
Raw data (stat): 15928 (minisat+) R 15927 20024 20023 0 -1 0 3725 0 0 0 35969 32 0 0 25 0 1 0 541656523 17977344 3694 4294967295 134512640 134672761 3221224544 3221223680 134560604 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4389 3694 603 41 0 4348 0
vsize: 17556
[startup+370.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 15985
Raw data (stat): 15928 (minisat+) R 15927 20024 20023 0 -1 0 3763 0 0 0 36968 32 0 0 25 0 1 0 541656523 18194432 3732 4294967295 134512640 134672761 3221224544 3221223744 134557876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4442 3732 603 41 0 4401 0
vsize: 17768
[startup+380.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 15985
Raw data (stat): 15928 (minisat+) R 15927 20024 20023 0 -1 0 3763 0 0 0 37969 32 0 0 25 0 1 0 541656523 18194432 3732 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4442 3732 603 41 0 4401 0
vsize: 17768
[startup+390.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 15985
Raw data (stat): 15928 (minisat+) R 15927 20024 20023 0 -1 0 3763 0 0 0 38969 32 0 0 25 0 1 0 541656523 18194432 3732 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4442 3732 603 41 0 4401 0
vsize: 17768
[startup+400.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 15987
Raw data (stat): 15928 (minisat+) R 15927 20024 20023 0 -1 0 3763 0 0 0 39969 32 0 0 25 0 1 0 541656523 18194432 3732 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4442 3732 603 41 0 4401 0
vsize: 17768
[startup+410.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 15989
Raw data (stat): 15928 (minisat+) R 15927 20024 20023 0 -1 0 3763 0 0 0 40969 32 0 0 25 0 1 0 541656523 18194432 3732 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4442 3732 603 41 0 4401 0
vsize: 17768
[startup+420.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 15989
Raw data (stat): 15928 (minisat+) R 15927 20024 20023 0 -1 0 3763 0 0 0 41969 32 0 0 25 0 1 0 541656523 18194432 3732 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4442 3732 603 41 0 4401 0
vsize: 17768
[startup+430.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 15989
Raw data (stat): 15928 (minisat+) R 15927 20024 20023 0 -1 0 3763 0 0 0 42969 32 0 0 25 0 1 0 541656523 18194432 3732 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4442 3732 603 41 0 4401 0
vsize: 17768
[startup+440.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 15989
Raw data (stat): 15928 (minisat+) R 15927 20024 20023 0 -1 0 3763 0 0 0 43969 32 0 0 25 0 1 0 541656523 18194432 3732 4294967295 134512640 134672761 3221224544 3221223648 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4442 3732 603 41 0 4401 0
vsize: 17768
[startup+450.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 15989
Raw data (stat): 15928 (minisat+) R 15927 20024 20023 0 -1 0 3764 0 0 0 44969 33 0 0 25 0 1 0 541656523 18194432 3733 4294967295 134512640 134672761 3221224544 3221223728 134559161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4442 3733 603 41 0 4401 0
vsize: 17768
[startup+460.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 15989
Raw data (stat): 15928 (minisat+) R 15927 20024 20023 0 -1 0 3764 0 0 0 45969 33 0 0 25 0 1 0 541656523 18194432 3733 4294967295 134512640 134672761 3221224544 3221223648 134559887 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4442 3733 603 41 0 4401 0
vsize: 17768
[startup+470.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 15989
Raw data (stat): 15928 (minisat+) R 15927 20024 20023 0 -1 0 3764 0 0 0 46969 33 0 0 25 0 1 0 541656523 18194432 3733 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4442 3733 603 41 0 4401 0
vsize: 17768
[startup+480.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 15989
Raw data (stat): 15928 (minisat+) R 15927 20024 20023 0 -1 0 3764 0 0 0 47970 33 0 0 25 0 1 0 541656523 18194432 3733 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4442 3733 603 41 0 4401 0
vsize: 17768
[startup+490.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 15989
Raw data (stat): 15928 (minisat+) R 15927 20024 20023 0 -1 0 3764 0 0 0 48970 33 0 0 25 0 1 0 541656523 18194432 3733 4294967295 134512640 134672761 3221224544 3221223680 134565048 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4442 3733 603 41 0 4401 0
vsize: 17768
[startup+500.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 15989
Raw data (stat): 15928 (minisat+) R 15927 20024 20023 0 -1 0 3765 0 0 0 49970 33 0 0 25 0 1 0 541656523 18194432 3734 4294967295 134512640 134672761 3221224544 3221223648 134559835 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4442 3734 603 41 0 4401 0
vsize: 17768
[startup+510.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 15989
Raw data (stat): 15928 (minisat+) R 15927 20024 20023 0 -1 0 3784 0 0 0 50970 33 0 0 25 0 1 0 541656523 18325504 3753 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4474 3753 603 41 0 4433 0
vsize: 17896
[startup+520.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 15989
Raw data (stat): 15928 (minisat+) R 15927 20024 20023 0 -1 0 3881 0 0 0 51970 33 0 0 25 0 1 0 541656523 18718720 3850 4294967295 134512640 134672761 3221224544 3221223680 134560622 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4570 3850 603 41 0 4529 0
vsize: 18280
[startup+530.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 15989
Raw data (stat): 15928 (minisat+) R 15927 20024 20023 0 -1 0 3969 0 0 0 52969 34 0 0 25 0 1 0 541656523 18980864 3938 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4634 3938 603 41 0 4593 0
vsize: 18536
[startup+540.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 15989
Raw data (stat): 15928 (minisat+) R 15927 20024 20023 0 -1 0 4064 0 0 0 53969 34 0 0 25 0 1 0 541656523 19451904 4033 4294967295 134512640 134672761 3221224544 3221223744 134557900 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4749 4033 603 41 0 4708 0
vsize: 18996
[startup+550.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 15989
Raw data (stat): 15928 (minisat+) R 15927 20024 20023 0 -1 0 4130 0 0 0 54969 35 0 0 25 0 1 0 541656523 19718144 4099 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4814 4099 603 41 0 4773 0
vsize: 19256
[startup+556.572 s]
Raw data (loadavg): 0.99 0.97 0.92 1/54 15989
Raw data (stat): 15928 (minisat+) R 15927 20024 20023 0 -1 0 4130 0 0 0 54969 35 0 0 25 0 1 0 541656523 19718144 4099 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4814 4099 603 41 0 4773 0
vsize: 0

Child status: 30
Real time (s): 556.571
CPU time (s): 556.593
CPU user time (s): 556.232
CPU system time (s): 0.360945
CPU usage (%): 100.004
Max. virtual memory (Kb): 19256
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	1120
#### END VERIFIER DATA ####