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 6967

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        714400 kB
Buffers:         38552 kB
Cached:         241064 kB
SwapCached:          0 kB
Active:          85360 kB
Inactive:       197064 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        714148 kB
SwapTotal:     2097892 kB
SwapFree:      2097892 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            32236 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 20:53:29 (client local time) WITH STATUS 30 IN 470.38 SECONDS
stats: 5031 0 470.38 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]---> Sorter-cost: 1747     Base: 5 2 2 2
c ---[   3]---> Sorter-cost: 1884     Base: 5 2 2 3
c ---[   1]---> Sorter-cost: 3158     Base: 5 2 2 3
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 |   18201    43518 |    6759      94      638     6.8 |  1.585 % |
c |       251 |   17685    42339 |    7435     234     2385    10.2 |  4.047 % |
c ==============================================================================
c [1mFound solution: 4335[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:12452     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       469 |   48819   115246 |   16273     445     3991     9.0 |  4.047 % |
c |       569 |   46888   110847 |   17900     520     4918     9.5 |  5.555 % |
c |       719 |   45556   107785 |   19690     623     5793     9.3 |  8.002 % |
c |       944 |   45539   107747 |   21659     847     8872    10.5 |  8.032 % |
c |      1281 |   45500   107658 |   23825    1183    12810    10.8 |  8.106 % |
c ==============================================================================
c [1mFound solution: 2637[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 |      1732 |   44188   104730 |   14729    1573    17315    11.0 |  8.106 % |
c |      1832 |   44188   104730 |   16201    1673    19109    11.4 | 11.828 % |
c |      1982 |   42228   100184 |   17822    1790    20351    11.4 | 15.529 % |
c |      2207 |   41947    99536 |   19604    1913    22010    11.5 | 16.049 % |
c |      2546 |   41707    98996 |   21564    2247    32594    14.5 | 16.436 % |
c ==============================================================================
c [1mFound solution: 2500[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 |      2694 |   42755   101542 |   14251    2395    38518    16.1 | 16.436 % |
c |      2794 |   42740   101509 |   15676    2494    40122    16.1 | 16.592 % |
c ==============================================================================
c [1mFound solution: 2497[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 |      2919 |   43137   102486 |   14379    2619    48812    18.6 | 16.592 % |
c |      3019 |   43035   102250 |   15816    2714    49643    18.3 | 16.863 % |
c |      3169 |   42146   100197 |   17398    2842    50664    17.8 | 18.468 % |
c ==============================================================================
c [1mFound solution: 2462[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 |      3245 |   41961    99805 |   13987    2873    51340    17.9 | 18.468 % |
c |      3345 |   41550    98867 |   15385    2938    51859    17.7 | 19.690 % |
c |      3496 |   40832    97203 |   16924    3052    52376    17.2 | 20.972 % |
c |      3721 |   40331    96044 |   18616    3230    53898    16.7 | 21.898 % |
c ==============================================================================
c [1mFound solution: 2413[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 |      3846 |   40198    95757 |   13399    3347    54850    16.4 | 21.898 % |
c |      3946 |   40136    95612 |   14738    3446    56152    16.3 | 22.558 % |
c ==============================================================================
c [1mFound solution: 2412[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 |      4070 |   40167    95693 |   13389    3570    62021    17.4 | 22.558 % |
c |      4170 |   40124    95594 |   14727    3666    63095    17.2 | 22.636 % |
c |      4320 |   40012    95340 |   16200    3783    63950    16.9 | 22.829 % |
c |      4545 |   39818    94887 |   17820    3982    70229    17.6 | 23.231 % |
c |      4883 |   39592    94359 |   19602    4310    74181    17.2 | 23.663 % |
c |      5390 |   39395    93907 |   21563    4811    91390    19.0 | 23.979 % |
c |      6149 |   39249    93569 |   23719    5556   108383    19.5 | 24.247 % |
c |      7288 |   39249    93569 |   26091    6695   153757    23.0 | 24.247 % |
c ==============================================================================
c [1mFound solution: 2393[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 |      7498 |   39266    93619 |   13088    6904   160320    23.2 | 24.247 % |
c |      7599 |   39179    93419 |   14396    7000   162679    23.2 | 24.406 % |
c |      7752 |   39084    93198 |   15836    7145   171254    24.0 | 24.593 % |
c |      7978 |   39084    93198 |   17420    7371   177002    24.0 | 24.593 % |
c |      8315 |   39079    93183 |   19162    7707   183921    23.9 | 24.599 % |
c |      8822 |   38970    92931 |   21078    8206   197860    24.1 | 24.786 % |
c ==============================================================================
c [1mFound solution: 2327[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 |      9235 |   38854    92675 |   12951    8615   203649    23.6 | 24.786 % |
c |      9335 |   38592    92065 |   14246    8702   205656    23.6 | 25.510 % |
c |      9485 |   38123    90971 |   15670    8795   206942    23.5 | 26.380 % |
c |      9712 |   38055    90814 |   17237    9015   209702    23.3 | 26.508 % |
c |     10049 |   37961    90596 |   18961    9345   214055    22.9 | 26.689 % |
c |     10555 |   37909    90476 |   20857    9846   234721    23.8 | 26.782 % |
c ==============================================================================
c [1mFound solution: 2323[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 |     11234 |   37920    90503 |   12640   10525   252461    24.0 | 26.782 % |
c |     11335 |   37860    90364 |   13904   10617   253804    23.9 | 26.904 % |
c ==============================================================================
c [1mFound solution: 2273[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 |     11456 |   38011    90743 |   12670   10736   255532    23.8 | 26.904 % |
c |     11556 |   37997    90709 |   13937   10833   257524    23.8 | 27.082 % |
c ==============================================================================
c [1mFound solution: 2245[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 |     11643 |   38005    90729 |   12668   10920   261497    23.9 | 27.082 % |
c |     11743 |   38005    90729 |   13934   11020   263248    23.9 | 27.083 % |
c |     11894 |   38005    90729 |   15328   11171   264977    23.7 | 27.083 % |
c |     12119 |   38001    90720 |   16861   11393   270958    23.8 | 27.089 % |
c |     12457 |   37987    90688 |   18547   11730   278330    23.7 | 27.112 % |
c |     12963 |   37748    90136 |   20401   12206   290051    23.8 | 27.530 % |
c |     13722 |   37690    90003 |   22442   12958   340543    26.3 | 27.640 % |
c ==============================================================================
c [1mFound solution: 2211[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 |     14401 |   37826    90352 |   12608   13619   372287    27.3 | 27.640 % |
c |     14502 |   37826    90352 |   13868   13720   374929    27.3 | 28.053 % |
c |     14652 |   37826    90352 |   15255   13870   378215    27.3 | 28.053 % |
c ==============================================================================
c [1mFound solution: 2188[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 |     14701 |   37836    90378 |   12612   13919   383202    27.5 | 28.053 % |
c |     14802 |   37836    90378 |   13873   14020   385504    27.5 | 28.054 % |
c |     14953 |   37836    90378 |   15260   14171   388450    27.4 | 28.054 % |
c |     15181 |   37836    90378 |   16786   14399   392570    27.3 | 28.054 % |
c |     15518 |   37836    90378 |   18465   14736   400209    27.2 | 28.054 % |
c |     16024 |   37836    90378 |   20311   15242   426004    27.9 | 28.054 % |
c |     16783 |   37836    90378 |   22342   16001   472314    29.5 | 28.054 % |
c |     17922 |   37836    90378 |   24577   17140   537425    31.4 | 28.054 % |
c ==============================================================================
c [1mFound solution: 2142[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 |     18825 |   37956    90670 |   12652   18043   573902    31.8 | 28.054 % |
c |     18926 |   37935    90622 |   13917    9122   304576    33.4 | 28.113 % |
c |     19078 |   37935    90622 |   15308    9274   315366    34.0 | 28.113 % |
c |     19303 |   37912    90570 |   16839    9498   324650    34.2 | 28.154 % |
c |     19640 |   37861    90451 |   18523    9832   344794    35.1 | 28.246 % |
c ==============================================================================
c [1mFound solution: 2072[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 |     19841 |   37876    90488 |   12625   10033   354316    35.3 | 28.246 % |
c |     19942 |   37861    90453 |   13887   10133   355591    35.1 | 28.266 % |
c |     20092 |   37861    90453 |   15276   10283   357891    34.8 | 28.266 % |
c |     20317 |   37861    90453 |   16803   10508   362139    34.5 | 28.266 % |
c |     20654 |   37851    90430 |   18484   10844   367724    33.9 | 28.283 % |
c |     21160 |   37836    90396 |   20332   11349   391506    34.5 | 28.312 % |
c |     21919 |   37832    90387 |   22365   12106   413805    34.2 | 28.317 % |
c |     23058 |   37824    90369 |   24602   13244   444050    33.5 | 28.323 % |
c |     24766 |   37796    90304 |   27062   14951   486399    32.5 | 28.375 % |
c ==============================================================================
c [1mFound solution: 2053[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 |     26301 |   37736    90179 |   12578   16479   546673    33.2 | 28.375 % |
c |     26401 |   37736    90179 |   13835   16579   552356    33.3 | 28.526 % |
c |     26551 |   37736    90179 |   15219   16729   555775    33.2 | 28.526 % |
c |     26776 |   37677    90046 |   16741   16950   561318    33.1 | 28.623 % |
c |     27113 |   37677    90046 |   18415   17287   569315    32.9 | 28.623 % |
c |     27619 |   37677    90046 |   20256   17793   584195    32.8 | 28.623 % |
c ==============================================================================
c [1mFound solution: 2020[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 |     27737 |   37690    90077 |   12563   17911   588845    32.9 | 28.623 % |
c |     27837 |   37690    90077 |   13819    9056   188392    20.8 | 28.621 % |
c |     27987 |   37681    90057 |   15201    9204   190967    20.7 | 28.638 % |
c |     28212 |   37681    90057 |   16721    9429   194507    20.6 | 28.638 % |
c |     28550 |   37681    90057 |   18393    9767   204660    21.0 | 28.638 % |
c ==============================================================================
c [1mFound solution: 1946[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 |     28977 |   37643    89971 |   12547   10193   235043    23.1 | 28.638 % |
c |     29079 |   37643    89971 |   13801   10295   237033    23.0 | 28.723 % |
c |     29229 |   37643    89971 |   15181   10445   239596    22.9 | 28.723 % |
c |     29456 |   37551    89757 |   16700   10668   244465    22.9 | 28.895 % |
c |     29794 |   37531    89710 |   18370   10998   251315    22.9 | 28.935 % |
c |     30300 |   37531    89710 |   20207   11504   266426    23.2 | 28.935 % |
c |     31060 |   37531    89710 |   22227   12264   290020    23.6 | 28.935 % |
c ==============================================================================
c [1mFound solution: 1936[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 |     31225 |   37541    89734 |   12513   12429   294955    23.7 | 28.935 % |
c |     31327 |   37541    89734 |   13764   12531   296272    23.6 | 28.934 % |
c |     31477 |   37541    89734 |   15140   12681   301193    23.8 | 28.934 % |
c ==============================================================================
c [1mFound solution: 1865[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 |     31600 |   37574    89816 |   12524   12804   309222    24.2 | 28.934 % |
c |     31700 |   37574    89816 |   13776   12904   313034    24.3 | 28.921 % |
c |     31852 |   37574    89816 |   15154   13056   318232    24.4 | 28.921 % |
c |     32079 |   37574    89816 |   16669   13283   327602    24.7 | 28.921 % |
c |     32418 |   37574    89816 |   18336   13622   334605    24.6 | 28.921 % |
c |     32927 |   37570    89806 |   20170   14130   357256    25.3 | 28.927 % |
c |     33686 |   37570    89806 |   22187   14889   388219    26.1 | 28.927 % |
c |     34825 |   37570    89806 |   24405   16028   418816    26.1 | 28.927 % |
c |     36535 |   37570    89806 |   26846   17738   509871    28.7 | 28.927 % |
c ==============================================================================
c [1mFound solution: 1857[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 |     37851 |   37579    89829 |   12526   19054   562570    29.5 | 28.927 % |
c ==============================================================================
c [1mFound solution: 1833[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 |     37865 |   37601    89889 |   12533    9541   257906    27.0 | 28.927 % |
c ==============================================================================
c [1mFound solution: 1826[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 |     37885 |   37612    89916 |   12537    9561   258311    27.0 | 28.927 % |
c |     37985 |   37612    89916 |   13790    9661   261299    27.0 | 28.926 % |
c ==============================================================================
c [1mFound solution: 1789[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 |     38021 |   37619    89933 |   12539    9697   263407    27.2 | 28.926 % |
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 |     38091 |   37637    89977 |   12545    9767   267365    27.4 | 28.926 % |
c |     38193 |   37628    89955 |   13799    9868   271541    27.5 | 28.928 % |
c ==============================================================================
c [1mFound solution: 1736[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 |     38249 |   37638    89979 |   12546    9924   273204    27.5 | 28.928 % |
c ==============================================================================
c [1mFound solution: 1580[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 |     38305 |   37660    90034 |   12553    9980   276480    27.7 | 28.928 % |
c |     38405 |   37660    90034 |   13808   10080   281470    27.9 | 28.920 % |
c |     38555 |   37660    90034 |   15189   10230   284343    27.8 | 28.920 % |
c |     38781 |   37660    90034 |   16708   10456   287318    27.5 | 28.920 % |
c |     39119 |   37552    89779 |   18378   10788   297322    27.6 | 29.126 % |
c ==============================================================================
c [1mFound solution: 1549[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 |     39336 |   37568    89819 |   12522   11005   311696    28.3 | 29.126 % |
c |     39437 |   37568    89819 |   13774   11106   314704    28.3 | 29.123 % |
c |     39587 |   37568    89819 |   15151   11256   317604    28.2 | 29.123 % |
c |     39812 |   37568    89819 |   16666   11481   323095    28.1 | 29.123 % |
c |     40149 |   37568    89819 |   18333   11818   336435    28.5 | 29.123 % |
c |     40655 |   37568    89819 |   20166   12324   351426    28.5 | 29.123 % |
c |     41414 |   37568    89819 |   22183   13083   373502    28.5 | 29.123 % |
c |     42553 |   37564    89809 |   24401   14221   424650    29.9 | 29.129 % |
c |     44261 |   37564    89809 |   26842   15929   482264    30.3 | 29.129 % |
c |     46827 |   37564    89809 |   29526   18495   586631    31.7 | 29.130 % |
c ==============================================================================
c [1mFound solution: 1531[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 |     49857 |   37405    89449 |   12468   17117   550878    32.2 | 29.130 % |
c |     49958 |   37405    89449 |   13714   17218   554384    32.2 | 29.352 % |
c |     50108 |   37405    89449 |   15086   17368   558782    32.2 | 29.352 % |
c ==============================================================================
c [1mFound solution: 1456[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 |     50155 |   37411    89465 |   12470   17415   562028    32.3 | 29.352 % |
c |     50255 |   37411    89465 |   13717   17515   564888    32.3 | 29.355 % |
c |     50405 |   37411    89465 |   15088   17665   567057    32.1 | 29.355 % |
c |     50632 |   37411    89465 |   16597   17892   570103    31.9 | 29.355 % |
c |     50969 |   37411    89465 |   18257   18229   575319    31.6 | 29.355 % |
c |     51476 |   37411    89465 |   20083   18736   590111    31.5 | 29.355 % |
c |     52236 |   37411    89465 |   22091   19496   626928    32.2 | 29.355 % |
c ==============================================================================
c [1mFound solution: 1448[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 |     52998 |   37422    89492 |   12474   20258   645295    31.9 | 29.355 % |
c ==============================================================================
c [1mFound solution: 1417[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 |     53041 |   37433    89519 |   12477   10172   231719    22.8 | 29.355 % |
c ==============================================================================
c [1mFound solution: 1415[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 |     53092 |   37440    89536 |   12480   10223   234949    23.0 | 29.355 % |
c |     53192 |   37440    89536 |   13728   10323   240979    23.3 | 29.354 % |
c |     53342 |   37430    89513 |   15100   10470   243304    23.2 | 29.359 % |
c |     53567 |   37430    89513 |   16610   10695   252547    23.6 | 29.359 % |
c |     53904 |   37430    89513 |   18271   11032   263696    23.9 | 29.359 % |
c |     54410 |   37430    89513 |   20099   11538   293519    25.4 | 29.359 % |
c ==============================================================================
c [1mFound solution: 1402[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 |     55093 |   37440    89537 |   12480   12221   322728    26.4 | 29.359 % |
c |     55193 |   37440    89537 |   13728   12321   326955    26.5 | 29.358 % |
c |     55345 |   37440    89537 |   15100   12473   332732    26.7 | 29.358 % |
c |     55570 |   37440    89537 |   16610   12698   345325    27.2 | 29.358 % |
c |     55909 |   37440    89537 |   18271   13037   368466    28.3 | 29.358 % |
c |     56416 |   37440    89537 |   20099   13544   397031    29.3 | 29.358 % |
c ==============================================================================
c [1mFound solution: 1388[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 |     57159 |   37450    89561 |   12483   14287   439614    30.8 | 29.358 % |
c |     57259 |   37450    89561 |   13731   14387   444279    30.9 | 29.357 % |
c |     57410 |   37450    89561 |   15104   14538   452447    31.1 | 29.357 % |
c |     57635 |   37450    89561 |   16614   14763   464342    31.5 | 29.357 % |
c ==============================================================================
c [1mFound solution: 1354[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 |     57948 |   37460    89585 |   12486   15076   479367    31.8 | 29.357 % |
c ==============================================================================
c [1mFound solution: 1333[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 |     57997 |   37470    89609 |   12490   15125   481973    31.9 | 29.357 % |
c |     58097 |   37470    89609 |   13739   15225   485346    31.9 | 29.355 % |
c |     58247 |   37470    89609 |   15112   15375   489398    31.8 | 29.355 % |
c |     58472 |   37470    89609 |   16624   15600   498108    31.9 | 29.355 % |
c |     58809 |   37470    89609 |   18286   15937   515650    32.4 | 29.355 % |
c ==============================================================================
c [1mFound solution: 1304[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 |     59057 |   37444    89551 |   12481   16179   526175    32.5 | 29.355 % |
c |     59159 |   37444    89551 |   13729   16281   532343    32.7 | 29.414 % |
c |     59310 |   37444    89551 |   15102   16432   539582    32.8 | 29.414 % |
c |     59536 |   37444    89551 |   16612   16658   552955    33.2 | 29.414 % |
c |     59874 |   37444    89551 |   18273   16996   560317    33.0 | 29.415 % |
c |     60380 |   37444    89551 |   20100   17502   573463    32.8 | 29.414 % |
c |     61139 |   37444    89551 |   22110   18261   613885    33.6 | 29.414 % |
c ==============================================================================
c [1mFound solution: 1270[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 |     61522 |   37473    89623 |   12491   18644   635510    34.1 | 29.414 % |
c |     61623 |   37473    89623 |   13740    9423   256079    27.2 | 29.404 % |
c |     61773 |   37473    89623 |   15114    9573   264098    27.6 | 29.403 % |
c |     62000 |   37473    89623 |   16625    9800   275081    28.1 | 29.403 % |
c |     62342 |   37473    89623 |   18288   10142   291825    28.8 | 29.404 % |
c |     62849 |   37473    89623 |   20116   10649   319048    30.0 | 29.403 % |
c ==============================================================================
c [1mFound solution: 1261[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 |     63004 |   37482    89646 |   12494   10804   326046    30.2 | 29.403 % |
c |     63104 |   37482    89646 |   13743   10904   331554    30.4 | 29.404 % |
c |     63255 |   37482    89646 |   15117   11055   337699    30.5 | 29.404 % |
c |     63481 |   37482    89646 |   16629   11281   348428    30.9 | 29.404 % |
c |     63818 |   37482    89646 |   18292   11618   360142    31.0 | 29.404 % |
c |     64325 |   37482    89646 |   20121   12125   377579    31.1 | 29.404 % |
c ==============================================================================
c [1mFound solution: 1246[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 |     64708 |   37486    89656 |   12495   12508   390625    31.2 | 29.404 % |
c |     64809 |   37486    89656 |   13744   12609   393814    31.2 | 29.406 % |
c ==============================================================================
c [1mFound solution: 1224[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 |     64890 |   37496    89680 |   12498   12690   397803    31.3 | 29.406 % |
c |     64990 |   37496    89680 |   13747   12790   400551    31.3 | 29.405 % |
c |     65141 |   37496    89680 |   15122   12941   404785    31.3 | 29.405 % |
c |     65368 |   37496    89680 |   16634   13168   413036    31.4 | 29.406 % |
c |     65706 |   37496    89680 |   18298   13506   425772    31.5 | 29.405 % |
c |     66212 |   37496    89680 |   20128   14012   447769    32.0 | 29.405 % |
c |     66971 |   37496    89680 |   22140   14771   483388    32.7 | 29.405 % |
c |     68110 |   37496    89680 |   24355   15910   537554    33.8 | 29.405 % |
c |     69819 |   37425    89516 |   26790   17617   619566    35.2 | 29.531 % |
c ==============================================================================
c [1mFound solution: 1182[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 |     71325 |   37431    89528 |   12477   19122   694604    36.3 | 29.531 % |
c |     71425 |   37431    89528 |   13724    9661   291389    30.2 | 29.535 % |
c |     71576 |   37431    89528 |   15097    9812   298729    30.4 | 29.535 % |
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 |     71607 |   37436    89541 |   12478    9843   300033    30.5 | 29.535 % |
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 |     71619 |   37444    89561 |   12481    9855   300805    30.5 | 29.535 % |
c |     71719 |   37444    89561 |   13729    9955   303578    30.5 | 29.538 % |
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 |     71837 |   37455    89588 |   12485   10073   309336    30.7 | 29.538 % |
c |     71943 |   37455    89588 |   13733   10179   311574    30.6 | 29.537 % |
c |     72094 |   37455    89588 |   15106   10330   314152    30.4 | 29.537 % |
c |     72324 |   37455    89588 |   16617   10560   320246    30.3 | 29.537 % |
c |     72661 |   37455    89588 |   18279   10897   326228    29.9 | 29.537 % |
c |     73167 |   37157    88885 |   20107   11390   336110    29.5 | 30.084 % |
c |     73927 |   37157    88885 |   22117   12150   358721    29.5 | 30.084 % |
c |     75066 |   37152    88870 |   24329   13288   395252    29.7 | 30.089 % |
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 |     76588 |   37159    88887 |   12386   14810   455560    30.8 | 30.089 % |
c |     76688 |   37159    88887 |   13624   14910   458734    30.8 | 30.090 % |
c |     76838 |   37159    88887 |   14987   15060   462324    30.7 | 30.090 % |
c |     77065 |   37159    88887 |   16485   15287   474129    31.0 | 30.090 % |
c |     77402 |   37159    88887 |   18134   15624   487986    31.2 | 30.090 % |
c |     77909 |   37159    88887 |   19947   16131   505203    31.3 | 30.090 % |
c |     78668 |   37159    88887 |   21942   16890   533130    31.6 | 30.090 % |
c |     79807 |   37147    88857 |   24136   18028   568857    31.6 | 30.096 % |
c |     81515 |   37147    88857 |   26550   19736   642976    32.6 | 30.096 % |
c |     84077 |   36433    87195 |   29205   16641   556860    33.5 | 31.228 % |
c |     87921 |   36433    87195 |   32126   20485   699646    34.2 | 31.228 % |
c |     93687 |   36410    87143 |   35338   26248   960502    36.6 | 31.268 % |
c |    102336 |   36410    87143 |   38872   34897  1252170    35.9 | 31.268 % |
c ==============================================================================
c [1mFound solution: 1120[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 7743     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    106907 |   48655   115612 |   16218   39468  1469614    37.2 | 31.268 % |
c |    107008 |   48655   115612 |   17839   18706   598414    32.0 | 30.570 % |
c |    107158 |   48650   115597 |   19623   18855   607145    32.2 | 30.574 % |
c |    107383 |   48650   115597 |   21586   19080   616250    32.3 | 30.574 % |
c |    107723 |   48650   115597 |   23744   19420   630726    32.5 | 30.574 % |
c |    108229 |   48650   115597 |   26119   19926   653105    32.8 | 30.574 % |
c |    108990 |   48650   115597 |   28731   20687   683860    33.1 | 30.574 % |
c |    110129 |   48650   115597 |   31604   21826   739555    33.9 | 30.574 % |
c |    111838 |   48634   115560 |   34764   23532   810991    34.5 | 30.595 % |
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              : 233
c conflicts             : 113896         (242 /sec)
c decisions             : 185123         (394 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 470.058 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.91 0.95 0.69 2/54 22828
Raw data (stat): 22828 (runsolver) R 22827 11931 11930 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 487573803 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.0004 s]
Raw data (loadavg): 0.93 0.95 0.69 2/54 22828
Raw data (stat): 22828 (minisat+) R 22827 11931 11930 0 -1 0 1772 0 0 0 995 3 0 0 25 0 1 0 487573803 9887744 1748 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2414 1748 603 41 0 2373 0
vsize: 9656
[startup+20.0007 s]
Raw data (loadavg): 0.94 0.95 0.69 2/54 22828
Raw data (stat): 22828 (minisat+) R 22827 11931 11930 0 -1 0 1901 0 0 0 1995 4 0 0 25 0 1 0 487573803 10420224 1877 4294967295 134512640 134672761 3221224576 3221223732 134561241 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2544 1877 603 41 0 2503 0
vsize: 10176
[startup+30.0009 s]
Raw data (loadavg): 0.95 0.96 0.70 2/54 22828
Raw data (stat): 22828 (minisat+) R 22827 11931 11930 0 -1 0 2035 0 0 0 2993 5 0 0 25 0 1 0 487573803 10964992 2011 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2677 2011 603 41 0 2636 0
vsize: 10708
[startup+40.0017 s]
Raw data (loadavg): 0.95 0.96 0.70 2/54 22828
Raw data (stat): 22828 (minisat+) R 22827 11931 11930 0 -1 0 2218 0 0 0 3992 6 0 0 25 0 1 0 487573803 11628544 2194 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2839 2194 603 41 0 2798 0
vsize: 11356
[startup+50.002 s]
Raw data (loadavg): 0.96 0.96 0.70 2/54 22828
Raw data (stat): 22828 (minisat+) R 22827 11931 11930 0 -1 0 2377 0 0 0 4992 6 0 0 25 0 1 0 487573803 12431360 2353 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3035 2353 603 41 0 2994 0
vsize: 12140
[startup+60.0023 s]
Raw data (loadavg): 0.97 0.96 0.71 2/54 22828
Raw data (stat): 22828 (minisat+) R 22827 11931 11930 0 -1 0 2413 0 0 0 5992 7 0 0 25 0 1 0 487573803 12513280 2389 4294967295 134512640 134672761 3221224576 3221223720 134560553 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3055 2389 603 41 0 3014 0
vsize: 12220
[startup+70.0031 s]
Raw data (loadavg): 0.97 0.96 0.71 2/54 22828
Raw data (stat): 22828 (minisat+) R 22827 11931 11930 0 -1 0 2413 0 0 0 6991 7 0 0 25 0 1 0 487573803 12513280 2389 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3055 2389 603 41 0 3014 0
vsize: 12220
[startup+80.0034 s]
Raw data (loadavg): 0.98 0.96 0.71 2/54 22828
Raw data (stat): 22828 (minisat+) R 22827 11931 11930 0 -1 0 2439 0 0 0 7991 8 0 0 25 0 1 0 487573803 12648448 2415 4294967295 134512640 134672761 3221224576 3221223776 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3088 2415 603 41 0 3047 0
vsize: 12352
[startup+90.0047 s]
Raw data (loadavg): 0.98 0.96 0.71 2/54 22828
Raw data (stat): 22828 (minisat+) R 22827 11931 11930 0 -1 0 2484 0 0 0 8990 9 0 0 25 0 1 0 487573803 12779520 2460 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3120 2460 603 41 0 3079 0
vsize: 12480
[startup+100.005 s]
Raw data (loadavg): 0.98 0.96 0.72 2/54 22828
Raw data (stat): 22828 (minisat+) R 22827 11931 11930 0 -1 0 2484 0 0 0 9989 9 0 0 25 0 1 0 487573803 12779520 2460 4294967295 134512640 134672761 3221224576 3221223712 134560585 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3120 2460 603 41 0 3079 0
vsize: 12480
[startup+110.006 s]
Raw data (loadavg): 0.98 0.96 0.72 2/54 22828
Raw data (stat): 22828 (minisat+) R 22827 11931 11930 0 -1 0 2484 0 0 0 10989 10 0 0 25 0 1 0 487573803 12779520 2460 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3120 2460 603 41 0 3079 0
vsize: 12480
[startup+120.006 s]
Raw data (loadavg): 0.99 0.96 0.72 2/54 22828
Raw data (stat): 22828 (minisat+) R 22827 11931 11930 0 -1 0 2485 0 0 0 11989 10 0 0 25 0 1 0 487573803 12779520 2461 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3120 2461 603 41 0 3079 0
vsize: 12480
[startup+130.006 s]
Raw data (loadavg): 0.99 0.97 0.73 2/54 22828
Raw data (stat): 22828 (minisat+) R 22827 11931 11930 0 -1 0 2491 0 0 0 12988 10 0 0 25 0 1 0 487573803 12779520 2467 4294967295 134512640 134672761 3221224576 3221223712 134560647 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3120 2467 603 41 0 3079 0
vsize: 12480
[startup+140.006 s]
Raw data (loadavg): 0.99 0.97 0.73 2/54 22828
Raw data (stat): 22828 (minisat+) R 22827 11931 11930 0 -1 0 2492 0 0 0 13988 11 0 0 25 0 1 0 487573803 12779520 2468 4294967295 134512640 134672761 3221224576 3221223760 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3120 2468 603 41 0 3079 0
vsize: 12480
[startup+150.007 s]
Raw data (loadavg): 0.99 0.97 0.73 2/54 22828
Raw data (stat): 22828 (minisat+) R 22827 11931 11930 0 -1 0 2511 0 0 0 14988 11 0 0 25 0 1 0 487573803 12910592 2487 4294967295 134512640 134672761 3221224576 3221223744 134560864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3152 2487 603 41 0 3111 0
vsize: 12608
[startup+160.007 s]
Raw data (loadavg): 0.99 0.97 0.73 2/54 22828
Raw data (stat): 22828 (minisat+) R 22827 11931 11930 0 -1 0 2536 0 0 0 15987 11 0 0 25 0 1 0 487573803 13041664 2512 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3184 2512 603 41 0 3143 0
vsize: 12736
[startup+170.008 s]
Raw data (loadavg): 0.99 0.97 0.73 2/54 22828
Raw data (stat): 22828 (minisat+) R 22827 11931 11930 0 -1 0 2548 0 0 0 16987 12 0 0 25 0 1 0 487573803 13041664 2524 4294967295 134512640 134672761 3221224576 3221223776 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3184 2524 603 41 0 3143 0
vsize: 12736
[startup+180.009 s]
Raw data (loadavg): 0.99 0.97 0.74 2/54 22828
Raw data (stat): 22828 (minisat+) R 22827 11931 11930 0 -1 0 2630 0 0 0 17987 12 0 0 25 0 1 0 487573803 13381632 2606 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3267 2606 603 41 0 3226 0
vsize: 13068
[startup+190.01 s]
Raw data (loadavg): 0.99 0.97 0.74 2/54 22828
Raw data (stat): 22828 (minisat+) R 22827 11931 11930 0 -1 0 2630 0 0 0 18986 13 0 0 25 0 1 0 487573803 13381632 2606 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3267 2606 603 41 0 3226 0
vsize: 13068
[startup+200.01 s]
Raw data (loadavg): 0.99 0.97 0.74 2/54 22828
Raw data (stat): 22828 (minisat+) R 22827 11931 11930 0 -1 0 2630 0 0 0 19986 14 0 0 25 0 1 0 487573803 13381632 2606 4294967295 134512640 134672761 3221224576 3221223744 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3267 2606 603 41 0 3226 0
vsize: 13068
[startup+210.01 s]
Raw data (loadavg): 0.99 0.97 0.74 2/54 22828
Raw data (stat): 22828 (minisat+) R 22827 11931 11930 0 -1 0 2630 0 0 0 20985 14 0 0 25 0 1 0 487573803 13381632 2606 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3267 2606 603 41 0 3226 0
vsize: 13068
[startup+220.011 s]
Raw data (loadavg): 0.99 0.97 0.74 2/54 22828
Raw data (stat): 22828 (minisat+) R 22827 11931 11930 0 -1 0 2638 0 0 0 21985 14 0 0 25 0 1 0 487573803 13381632 2614 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3267 2614 603 41 0 3226 0
vsize: 13068
[startup+230.01 s]
Raw data (loadavg): 0.99 0.97 0.75 2/54 22828
Raw data (stat): 22828 (minisat+) R 22827 11931 11930 0 -1 0 2638 0 0 0 22985 15 0 0 25 0 1 0 487573803 13381632 2614 4294967295 134512640 134672761 3221224576 3221223744 134560864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3267 2614 603 41 0 3226 0
vsize: 13068
[startup+240.012 s]
Raw data (loadavg): 0.99 0.97 0.75 2/54 22828
Raw data (stat): 22828 (minisat+) R 22827 11931 11930 0 -1 0 2638 0 0 0 23984 15 0 0 25 0 1 0 487573803 13381632 2614 4294967295 134512640 134672761 3221224576 3221223712 134560640 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3267 2614 603 41 0 3226 0
vsize: 13068
[startup+250.012 s]
Raw data (loadavg): 0.99 0.97 0.75 2/54 22828
Raw data (stat): 22828 (minisat+) R 22827 11931 11930 0 -1 0 2638 0 0 0 24984 16 0 0 25 0 1 0 487573803 13381632 2614 4294967295 134512640 134672761 3221224576 3221223680 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3267 2614 603 41 0 3226 0
vsize: 13068
[startup+260.012 s]
Raw data (loadavg): 0.99 0.97 0.75 2/54 22828
Raw data (stat): 22828 (minisat+) R 22827 11931 11930 0 -1 0 2729 0 0 0 25983 17 0 0 25 0 1 0 487573803 13774848 2705 4294967295 134512640 134672761 3221224576 3221223680 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3363 2705 603 41 0 3322 0
vsize: 13452
[startup+270.012 s]
Raw data (loadavg): 0.99 0.97 0.75 2/54 22828
Raw data (stat): 22828 (minisat+) R 22827 11931 11930 0 -1 0 2729 0 0 0 26983 17 0 0 25 0 1 0 487573803 13774848 2705 4294967295 134512640 134672761 3221224576 3221223760 134558899 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3363 2705 603 41 0 3322 0
vsize: 13452
[startup+280.013 s]
Raw data (loadavg): 0.99 0.97 0.76 2/54 22828
Raw data (stat): 22828 (minisat+) R 22827 11931 11930 0 -1 0 2729 0 0 0 27982 17 0 0 25 0 1 0 487573803 13774848 2705 4294967295 134512640 134672761 3221224576 3221223712 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3363 2705 603 41 0 3322 0
vsize: 13452
[startup+290.013 s]
Raw data (loadavg): 0.99 0.97 0.76 2/54 22828
Raw data (stat): 22828 (minisat+) R 22827 11931 11930 0 -1 0 2731 0 0 0 28982 18 0 0 25 0 1 0 487573803 13774848 2707 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3363 2707 603 41 0 3322 0
vsize: 13452
[startup+300.013 s]
Raw data (loadavg): 0.99 0.97 0.76 2/54 22828
Raw data (stat): 22828 (minisat+) R 22827 11931 11930 0 -1 0 2737 0 0 0 29982 18 0 0 25 0 1 0 487573803 13774848 2713 4294967295 134512640 134672761 3221224576 3221223680 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3363 2713 603 41 0 3322 0
vsize: 13452
[startup+310.013 s]
Raw data (loadavg): 0.99 0.97 0.76 2/54 22828
Raw data (stat): 22828 (minisat+) R 22827 11931 11930 0 -1 0 2745 0 0 0 30981 18 0 0 25 0 1 0 487573803 13910016 2721 4294967295 134512640 134672761 3221224576 3221223680 134560529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3396 2721 603 41 0 3355 0
vsize: 13584
[startup+320.014 s]
Raw data (loadavg): 0.99 0.97 0.76 2/54 22828
Raw data (stat): 22828 (minisat+) R 22827 11931 11930 0 -1 0 2775 0 0 0 31981 19 0 0 25 0 1 0 487573803 14045184 2751 4294967295 134512640 134672761 3221224576 3221223716 134560556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3429 2751 603 41 0 3388 0
vsize: 13716
[startup+330.014 s]
Raw data (loadavg): 0.99 0.97 0.77 2/54 22828
Raw data (stat): 22828 (minisat+) R 22827 11931 11930 0 -1 0 2781 0 0 0 32980 19 0 0 25 0 1 0 487573803 14045184 2757 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3429 2757 603 41 0 3388 0
vsize: 13716
[startup+340.015 s]
Raw data (loadavg): 0.99 0.97 0.77 2/54 22828
Raw data (stat): 22828 (minisat+) R 22827 11931 11930 0 -1 0 2801 0 0 0 33980 20 0 0 25 0 1 0 487573803 14045184 2777 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3429 2777 603 41 0 3388 0
vsize: 13716
[startup+350.015 s]
Raw data (loadavg): 0.99 0.97 0.77 2/54 22828
Raw data (stat): 22828 (minisat+) R 22827 11931 11930 0 -1 0 2904 0 0 0 34980 20 0 0 25 0 1 0 487573803 14573568 2880 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3558 2880 603 41 0 3517 0
vsize: 14232
[startup+360.015 s]
Raw data (loadavg): 0.99 0.97 0.77 2/54 22828
Raw data (stat): 22828 (minisat+) R 22827 11931 11930 0 -1 0 3032 0 0 0 35979 21 0 0 25 0 1 0 487573803 15106048 3008 4294967295 134512640 134672761 3221224576 3221223744 134561148 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3688 3008 603 41 0 3647 0
vsize: 14752
[startup+370.016 s]
Raw data (loadavg): 0.99 0.97 0.77 2/54 22828
Raw data (stat): 22828 (minisat+) R 22827 11931 11930 0 -1 0 3105 0 0 0 36978 22 0 0 25 0 1 0 487573803 15372288 3081 4294967295 134512640 134672761 3221224576 3221223776 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3753 3081 603 41 0 3712 0
vsize: 15012
[startup+380.016 s]
Raw data (loadavg): 0.99 0.97 0.78 2/54 22828
Raw data (stat): 22828 (minisat+) R 22827 11931 11930 0 -1 0 3194 0 0 0 37977 23 0 0 25 0 1 0 487573803 15699968 3170 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3833 3170 603 41 0 3792 0
vsize: 15332
[startup+390.018 s]
Raw data (loadavg): 0.99 0.97 0.78 2/54 22828
Raw data (stat): 22828 (minisat+) R 22827 11931 11930 0 -1 0 3286 0 0 0 38977 23 0 0 25 0 1 0 487573803 16093184 3262 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3929 3262 603 41 0 3888 0
vsize: 15716
[startup+400.018 s]
Raw data (loadavg): 0.99 0.97 0.78 2/54 22828
Raw data (stat): 22828 (minisat+) R 22827 11931 11930 0 -1 0 3367 0 0 0 39976 24 0 0 25 0 1 0 487573803 16621568 3343 4294967295 134512640 134672761 3221224576 3221223712 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4058 3343 603 41 0 4017 0
vsize: 16232
[startup+410.018 s]
Raw data (loadavg): 0.99 0.97 0.78 2/54 22828
Raw data (stat): 22828 (minisat+) R 22827 11931 11930 0 -1 0 3458 0 0 0 40975 25 0 0 25 0 1 0 487573803 16896000 3434 4294967295 134512640 134672761 3221224576 3221223680 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4125 3434 603 41 0 4084 0
vsize: 16500
[startup+420.018 s]
Raw data (loadavg): 0.99 0.97 0.78 2/54 22828
Raw data (stat): 22828 (minisat+) R 22827 11931 11930 0 -1 0 3545 0 0 0 41975 25 0 0 25 0 1 0 487573803 17289216 3521 4294967295 134512640 134672761 3221224576 3221223592 1075352943 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4221 3521 603 41 0 4180 0
vsize: 16884
[startup+430.019 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 22828
Raw data (stat): 22828 (minisat+) R 22827 11931 11930 0 -1 0 3677 0 0 0 42975 26 0 0 25 0 1 0 487573803 17813504 3653 4294967295 134512640 134672761 3221224576 3221223680 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4349 3653 603 41 0 4308 0
vsize: 17396
[startup+440.019 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 22828
Raw data (stat): 22828 (minisat+) R 22827 11931 11930 0 -1 0 4077 0 0 0 43973 28 0 0 25 0 1 0 487573803 18968576 4011 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4631 4011 603 41 0 4590 0
vsize: 18524
[startup+450.02 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 22828
Raw data (stat): 22828 (minisat+) R 22827 11931 11930 0 -1 0 4080 0 0 0 44972 28 0 0 25 0 1 0 487573803 18968576 4014 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4631 4014 603 41 0 4590 0
vsize: 18524
[startup+460.02 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 22828
Raw data (stat): 22828 (minisat+) R 22827 11931 11930 0 -1 0 4080 0 0 0 45972 29 0 0 25 0 1 0 487573803 18968576 4014 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4631 4014 603 41 0 4590 0
vsize: 18524
[startup+470.02 s]
Raw data (loadavg): 0.99 0.97 0.79 2/54 22828
Raw data (stat): 22828 (minisat+) R 22827 11931 11930 0 -1 0 4080 0 0 0 46971 30 0 0 25 0 1 0 487573803 18968576 4014 4294967295 134512640 134672761 3221224576 3221223728 134554629 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4631 4014 603 41 0 4590 0
vsize: 18524
[startup+470.383 s]
Raw data (loadavg): 0.99 0.97 0.79 1/53 22828
Raw data (stat): 22828 (minisat+) R 22827 11931 11930 0 -1 0 4080 0 0 0 46971 30 0 0 25 0 1 0 487573803 18968576 4014 4294967295 134512640 134672761 3221224576 3221223728 134554629 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4631 4014 603 41 0 4590 0
vsize: 0

Child status: 30
Real time (s): 470.382
CPU time (s): 470.38
CPU user time (s): 470.069
CPU system time (s): 0.311952
CPU usage (%): 99.9996
Max. virtual memory (Kb): 18524
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	1120
#### END VERIFIER DATA ####