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 6913

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.050
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:        834632 kB
Buffers:         38488 kB
Cached:         141712 kB
SwapCached:          0 kB
Active:          81056 kB
Inactive:       101956 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        834380 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            11288 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 20:41:42 (client local time) WITH STATUS 30 IN 515.855 SECONDS
stats: 5023 0 515.855 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 |   16046    38074 |    5348       0        0     nan |  0.000 % |
c |       100 |   15635    37138 |    5882      84      320     3.8 |  2.411 % |
c ==============================================================================
c [1mFound solution: 4214[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 |       165 |   44577   104802 |   14859     126      495     3.9 |  2.411 % |
c |       265 |   44148   103822 |   16344     204     1226     6.0 |  2.633 % |
c |       416 |   42786   100729 |   17979     340     2419     7.1 |  4.977 % |
c ==============================================================================
c [1mFound solution: 4091[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 |       516 |   43053   101446 |   14351     436     4111     9.4 |  4.977 % |
c |       617 |   42937   101186 |   15786     533     4805     9.0 |  5.472 % |
c ==============================================================================
c [1mFound solution: 2600[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 |       640 |   43156   101738 |   14385     553     5096     9.2 |  5.472 % |
c ==============================================================================
c [1mFound solution: 2564[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 |       733 |   43234   101950 |   14411     640     6902    10.8 |  5.472 % |
c |       833 |   42467   100186 |   15852     705     8115    11.5 |  7.152 % |
c |       984 |   42275    99752 |   17437     854    11226    13.1 |  7.490 % |
c |      1209 |   41845    98792 |   19181    1068    14405    13.5 |  8.265 % |
c ==============================================================================
c [1mFound solution: 2366[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 |      1405 |   41854    98818 |   13951    1262    19196    15.2 |  8.265 % |
c |      1505 |   41819    98739 |   15346    1359    20565    15.1 |  8.375 % |
c |      1658 |   41819    98739 |   16880    1512    22650    15.0 |  8.375 % |
c |      1886 |   41819    98739 |   18568    1740    26014    15.0 |  8.375 % |
c ==============================================================================
c [1mFound solution: 2325[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 |      2148 |   41870    98883 |   13956    2001    37066    18.5 |  8.375 % |
c |      2248 |   41870    98883 |   15351    2101    38353    18.3 |  8.415 % |
c |      2398 |   41718    98530 |   16886    2237    41178    18.4 |  8.688 % |
c ==============================================================================
c [1mFound solution: 2113[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 |      2526 |   41859    98891 |   13953    2365    43488    18.4 |  8.688 % |
c |      2626 |   41859    98891 |   15348    2465    45485    18.5 |  8.664 % |
c |      2776 |   40589    95970 |   16883    2550    46881    18.4 | 10.901 % |
c |      3001 |   40500    95764 |   18571    2771    49031    17.7 | 11.062 % |
c ==============================================================================
c [1mFound solution: 2077[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 |      3040 |   40584    95973 |   13528    2810    49423    17.6 | 11.062 % |
c |      3140 |   40559    95916 |   14880    2909    50766    17.5 | 11.092 % |
c |      3290 |   40559    95916 |   16368    3059    56749    18.6 | 11.092 % |
c |      3515 |   40515    95820 |   18005    3281    61210    18.7 | 11.184 % |
c |      3852 |   40515    95820 |   19806    3618    65648    18.1 | 11.184 % |
c |      4358 |   40515    95820 |   21786    4124    88847    21.5 | 11.184 % |
c |      5117 |   40196    95082 |   23965    4861   105377    21.7 | 11.755 % |
c ==============================================================================
c [1mFound solution: 2039[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 |      5461 |   40281    95290 |   13427    5205   111999    21.5 | 11.755 % |
c |      5561 |   40281    95290 |   14769    5305   113810    21.5 | 11.737 % |
c |      5713 |   40281    95290 |   16246    5457   119781    21.9 | 11.737 % |
c |      5941 |   40138    94960 |   17871    5682   123620    21.8 | 12.002 % |
c |      6278 |   40056    94769 |   19658    6012   139893    23.3 | 12.145 % |
c |      6785 |   40056    94769 |   21624    6519   154678    23.7 | 12.145 % |
c |      7544 |   40056    94769 |   23786    7278   185023    25.4 | 12.145 % |
c ==============================================================================
c [1mFound solution: 2010[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 |      7994 |   40046    94775 |   13348    7727   201707    26.1 | 12.145 % |
c |      8094 |   40046    94775 |   14682    7827   203566    26.0 | 12.180 % |
c |      8247 |   40046    94775 |   16151    7980   207754    26.0 | 12.180 % |
c |      8472 |   40046    94775 |   17766    8205   218952    26.7 | 12.180 % |
c |      8811 |   39869    94368 |   19542    8543   242672    28.4 | 12.478 % |
c |      9317 |   39869    94368 |   21497    9049   265341    29.3 | 12.479 % |
c |     10079 |   39716    94014 |   23646    9808   297070    30.3 | 12.725 % |
c ==============================================================================
c [1mFound solution: 1959[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 |     10263 |   39721    94026 |   13240    9992   307859    30.8 | 12.725 % |
c |     10364 |   39721    94026 |   14564   10093   309197    30.6 | 12.729 % |
c |     10516 |   39721    94026 |   16020   10245   318608    31.1 | 12.729 % |
c |     10741 |   39642    93844 |   17622   10469   325530    31.1 | 12.855 % |
c |     11078 |   39642    93844 |   19384   10806   334232    30.9 | 12.855 % |
c |     11584 |   39642    93844 |   21323   11312   343314    30.3 | 12.855 % |
c |     12343 |   39642    93844 |   23455   12071   395208    32.7 | 12.855 % |
c ==============================================================================
c [1mFound solution: 1886[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 |     13200 |   39659    93888 |   13219   12928   450474    34.8 | 12.855 % |
c |     13303 |   39659    93888 |   14540   13031   452979    34.8 | 12.853 % |
c |     13454 |   38672    91602 |   15994   13170   458874    34.8 | 14.632 % |
c |     13679 |   38263    90657 |   17594   13381   465007    34.8 | 15.366 % |
c |     14018 |   38263    90657 |   19353   13720   474081    34.6 | 15.366 % |
c |     14524 |   38117    90317 |   21289   14212   486103    34.2 | 15.647 % |
c |     15284 |   38117    90317 |   23418   14972   516201    34.5 | 15.647 % |
c |     16423 |   38096    90271 |   25760   16110   576733    35.8 | 15.688 % |
c |     18132 |   38096    90271 |   28336   17819   637141    35.8 | 15.687 % |
c ==============================================================================
c [1mFound solution: 1856[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 |     19713 |   37961    89969 |   12653   19397   724840    37.4 | 15.687 % |
c |     19814 |   37961    89969 |   13918    9800   342591    35.0 | 15.953 % |
c |     19964 |   37961    89969 |   15310    9950   348722    35.0 | 15.953 % |
c |     20191 |   37961    89969 |   16841   10177   365079    35.9 | 15.953 % |
c |     20528 |   37757    89497 |   18525   10510   372889    35.5 | 16.320 % |
c |     21038 |   37757    89497 |   20377   11020   391939    35.6 | 16.320 % |
c |     21797 |   37757    89497 |   22415   11779   428095    36.3 | 16.320 % |
c |     22936 |   37757    89497 |   24657   12918   478718    37.1 | 16.320 % |
c |     24644 |   37739    89455 |   27122   14624   564886    38.6 | 16.354 % |
c |     27206 |   37739    89455 |   29835   17186   670859    39.0 | 16.356 % |
c ==============================================================================
c [1mFound solution: 1839[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 |     28163 |   37595    89142 |   12531   18140   701282    38.7 | 16.356 % |
c ==============================================================================
c [1mFound solution: 1664[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 |     28226 |   37603    89161 |   12534    9133   312313    34.2 | 16.356 % |
c |     28329 |   37381    88644 |   13787    9234   317012    34.3 | 17.034 % |
c |     28480 |   37342    88554 |   15166    9384   320198    34.1 | 17.108 % |
c |     28706 |   37342    88554 |   16682    9610   330983    34.4 | 17.108 % |
c |     29043 |   37319    88502 |   18351    9946   337229    33.9 | 17.148 % |
c |     29551 |   37253    88349 |   20186   10451   354605    33.9 | 17.263 % |
c |     30310 |   37253    88349 |   22204   11210   376924    33.6 | 17.263 % |
c |     31450 |   37176    88173 |   24425   12348   421282    34.1 | 17.395 % |
c ==============================================================================
c [1mFound solution: 1652[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 |     32430 |   37181    88185 |   12393   13328   478161    35.9 | 17.395 % |
c |     32531 |   37181    88185 |   13632   13429   481643    35.9 | 17.398 % |
c ==============================================================================
c [1mFound solution: 1651[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 |     32556 |   37188    88201 |   12396   13454   483056    35.9 | 17.398 % |
c |     32657 |   37188    88201 |   13635   13555   488293    36.0 | 17.399 % |
c ==============================================================================
c [1mFound solution: 1645[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 |     32681 |   37193    88212 |   12397   13579   489409    36.0 | 17.399 % |
c ==============================================================================
c [1mFound solution: 1641[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 |     32709 |   37199    88239 |   12399   13607   490510    36.0 | 17.399 % |
c ==============================================================================
c [1mFound solution: 1626[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 |     32722 |   37206    88255 |   12402   13620   491045    36.1 | 17.399 % |
c ==============================================================================
c [1mFound solution: 1572[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 |     32812 |   37222    88295 |   12407   13710   495909    36.2 | 17.399 % |
c |     32912 |   37222    88295 |   13647   13810   500499    36.2 | 17.401 % |
c |     33062 |   37222    88295 |   15012   13960   505960    36.2 | 17.401 % |
c |     33288 |   37222    88295 |   16513   14186   515084    36.3 | 17.401 % |
c ==============================================================================
c [1mFound solution: 1569[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 |     33417 |   37227    88310 |   12409   14315   523217    36.6 | 17.401 % |
c |     33523 |   37227    88310 |   13649   14421   526997    36.5 | 17.403 % |
c ==============================================================================
c [1mFound solution: 1561[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 |     33536 |   37233    88325 |   12411   14434   527364    36.5 | 17.403 % |
c |     33636 |   37233    88325 |   13652   14534   532924    36.7 | 17.405 % |
c |     33786 |   37233    88325 |   15017   14684   542227    36.9 | 17.405 % |
c ==============================================================================
c [1mFound solution: 1553[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 |     33951 |   37239    88340 |   12413   14849   553272    37.3 | 17.405 % |
c ==============================================================================
c [1mFound solution: 1538[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 |     34010 |   37245    88354 |   12415   14908   556476    37.3 | 17.405 % |
c ==============================================================================
c [1mFound solution: 1472[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 |     34072 |   37250    88365 |   12416   14970   558955    37.3 | 17.405 % |
c ==============================================================================
c [1mFound solution: 1456[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 |     34088 |   37256    88378 |   12418   14986   559491    37.3 | 17.405 % |
c ==============================================================================
c [1mFound solution: 1452[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 |     34119 |   37263    88397 |   12421   15017   560717    37.3 | 17.405 % |
c |     34223 |   37263    88397 |   13663   15121   564578    37.3 | 17.415 % |
c |     34374 |   37263    88397 |   15029   15272   566776    37.1 | 17.415 % |
c |     34600 |   37212    88281 |   16532   15497   570014    36.8 | 17.507 % |
c |     34937 |   37212    88281 |   18185   15834   579121    36.6 | 17.507 % |
c |     35443 |   37200    88253 |   20004   16339   598956    36.7 | 17.530 % |
c |     36204 |   37200    88253 |   22004   17100   610536    35.7 | 17.530 % |
c |     37345 |   37200    88253 |   24205   18241   664918    36.5 | 17.530 % |
c ==============================================================================
c [1mFound solution: 1447[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 |     37458 |   37206    88268 |   12402   18354   668483    36.4 | 17.530 % |
c |     37559 |   37206    88268 |   13642    9278   289999    31.3 | 17.531 % |
c |     37710 |   37206    88268 |   15006    9429   292072    31.0 | 17.531 % |
c |     37935 |   37206    88268 |   16507    9654   294931    30.6 | 17.532 % |
c ==============================================================================
c [1mFound solution: 1443[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 |     38158 |   37211    88295 |   12403    9877   303179    30.7 | 17.532 % |
c |     38258 |   37211    88295 |   13643    9977   306001    30.7 | 17.533 % |
c |     38410 |   37211    88295 |   15007   10129   311348    30.7 | 17.533 % |
c |     38635 |   37211    88295 |   16508   10354   318865    30.8 | 17.533 % |
c |     38972 |   37211    88295 |   18159   10691   334629    31.3 | 17.533 % |
c ==============================================================================
c [1mFound solution: 1416[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 |     39137 |   37214    88302 |   12404   10856   341941    31.5 | 17.533 % |
c |     39237 |   37214    88302 |   13644   10956   346578    31.6 | 17.537 % |
c ==============================================================================
c [1mFound solution: 1408[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 |     39385 |   37222    88321 |   12407   11104   354963    32.0 | 17.537 % |
c |     39486 |   37222    88321 |   13647   11205   359650    32.1 | 17.538 % |
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 |     39559 |   37228    88336 |   12409   11278   363189    32.2 | 17.538 % |
c |     39660 |   37228    88336 |   13649   11379   369106    32.4 | 17.539 % |
c |     39810 |   37228    88336 |   15014   11529   374970    32.5 | 17.539 % |
c ==============================================================================
c [1mFound solution: 1394[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 |     39904 |   37232    88346 |   12410   11623   382319    32.9 | 17.539 % |
c ==============================================================================
c [1mFound solution: 1377[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 |     39989 |   37235    88353 |   12411   11708   385879    33.0 | 17.539 % |
c ==============================================================================
c [1mFound solution: 1358[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 |     40014 |   37242    88369 |   12414   11733   386311    32.9 | 17.539 % |
c ==============================================================================
c [1mFound solution: 1338[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 |     40098 |   37247    88381 |   12415   11817   391980    33.2 | 17.539 % |
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 |     40114 |   37254    88397 |   12418   11833   393663    33.3 | 17.539 % |
c |     40215 |   37254    88397 |   13659   11934   398464    33.4 | 17.552 % |
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 |     40255 |   37261    88413 |   12420   11974   401118    33.5 | 17.552 % |
c |     40356 |   37261    88413 |   13662   12075   405622    33.6 | 17.553 % |
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 |     40457 |   37278    88469 |   12426   12176   409843    33.7 | 17.553 % |
c |     40557 |   37278    88469 |   13668   12276   414230    33.7 | 17.548 % |
c |     40708 |   37278    88469 |   15035   12427   421195    33.9 | 17.548 % |
c |     40935 |   37278    88469 |   16539   12654   429895    34.0 | 17.548 % |
c ==============================================================================
c [1mFound solution: 1260[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 |     41007 |   37282    88481 |   12427   12726   433324    34.1 | 17.548 % |
c |     41108 |   37282    88481 |   13669   12827   435629    34.0 | 17.551 % |
c |     41258 |   37282    88481 |   15036   12977   442812    34.1 | 17.551 % |
c |     41483 |   37282    88481 |   16540   13202   450647    34.1 | 17.551 % |
c |     41820 |   37282    88481 |   18194   13539   465424    34.4 | 17.551 % |
c ==============================================================================
c [1mFound solution: 1251[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 |     41958 |   37286    88491 |   12428   13677   472983    34.6 | 17.551 % |
c |     42058 |   37286    88491 |   13670   13777   475577    34.5 | 17.554 % |
c |     42209 |   37286    88491 |   15037   13928   480858    34.5 | 17.554 % |
c |     42434 |   37286    88491 |   16541   14153   489371    34.6 | 17.554 % |
c |     42771 |   37286    88491 |   18195   14490   504565    34.8 | 17.554 % |
c ==============================================================================
c [1mFound solution: 1236[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 |     43097 |   37290    88501 |   12430   14816   517926    35.0 | 17.554 % |
c |     43201 |   37290    88501 |   13673   14920   520576    34.9 | 17.556 % |
c |     43352 |   37290    88501 |   15040   15071   524544    34.8 | 17.556 % |
c |     43578 |   37290    88501 |   16544   15297   529541    34.6 | 17.556 % |
c |     43915 |   37249    88407 |   18198   15632   546898    35.0 | 17.630 % |
c |     44421 |   37249    88407 |   20018   16138   572561    35.5 | 17.630 % |
c |     45180 |   37249    88407 |   22020   16897   599477    35.5 | 17.630 % |
c |     46319 |   37249    88407 |   24222   18036   663826    36.8 | 17.630 % |
c |     48027 |   37159    88200 |   26644   19742   733345    37.1 | 17.784 % |
c ==============================================================================
c [1mFound solution: 1232[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 |     48159 |   37162    88207 |   12387   19874   739448    37.2 | 17.784 % |
c |     48261 |   37162    88207 |   13625   10039   311227    31.0 | 17.788 % |
c |     48411 |   37162    88207 |   14988   10189   320968    31.5 | 17.788 % |
c |     48636 |   37162    88207 |   16487   10414   330060    31.7 | 17.788 % |
c |     48976 |   37162    88207 |   18135   10754   347428    32.3 | 17.788 % |
c |     49482 |   37162    88207 |   19949   11260   374286    33.2 | 17.788 % |
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 |     49511 |   37168    88221 |   12389   11289   375722    33.3 | 17.788 % |
c |     49611 |   37168    88221 |   13627   11389   377638    33.2 | 17.790 % |
c |     49762 |   37168    88221 |   14990   11540   379388    32.9 | 17.790 % |
c |     49987 |   37168    88221 |   16489   11765   382453    32.5 | 17.790 % |
c |     50324 |   37168    88221 |   18138   12102   386606    31.9 | 17.790 % |
c |     50830 |   37095    88046 |   19952   12607   411468    32.6 | 17.926 % |
c |     51589 |   37095    88046 |   21947   13366   457483    34.2 | 17.926 % |
c ==============================================================================
c [1mFound solution: 1164[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 |     51730 |   37102    88062 |   12367   13507   463432    34.3 | 17.926 % |
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 |     51773 |   37106    88071 |   12368   13550   465084    34.3 | 17.926 % |
c ==============================================================================
c [1mFound solution: 1145[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 |     51800 |   37111    88082 |   12370   13577   466661    34.4 | 17.926 % |
c |     51901 |   37111    88082 |   13607   13678   470120    34.4 | 17.935 % |
c |     52053 |   37050    87942 |   14967   13829   473685    34.3 | 18.043 % |
c |     52280 |   36992    87807 |   16464   14054   482775    34.4 | 18.140 % |
c |     52617 |   36992    87807 |   18110   14391   494648    34.4 | 18.140 % |
c |     53123 |   36932    87669 |   19922   14896   514713    34.6 | 18.248 % |
c |     53883 |   36905    87606 |   21914   15654   548585    35.0 | 18.305 % |
c |     55023 |   36839    87452 |   24105   16790   597435    35.6 | 18.430 % |
c |     56732 |   36839    87452 |   26516   18499   683813    37.0 | 18.430 % |
c |     59294 |   36575    86839 |   29167   21056   779119    37.0 | 18.891 % |
c ==============================================================================
c [1mFound solution: 1143[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 |     62257 |   36529    86733 |   12176   24018   940108    39.1 | 18.891 % |
c |     62357 |   36529    86733 |   13393   12109   411396    34.0 | 18.968 % |
c |     62507 |   36529    86733 |   14732   12259   416196    34.0 | 18.968 % |
c |     62736 |   36529    86733 |   16206   12488   424299    34.0 | 18.968 % |
c |     63074 |   36525    86724 |   17826   12824   435716    34.0 | 18.973 % |
c |     63580 |   36525    86724 |   19609   13330   453755    34.0 | 18.973 % |
c |     64340 |   36525    86724 |   21570   14090   483252    34.3 | 18.973 % |
c |     65480 |   36525    86724 |   23727   15230   531010    34.9 | 18.973 % |
c ==============================================================================
c [1mFound solution: 1136[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 |     66364 |   36531    86739 |   12177   16114   566145    35.1 | 18.973 % |
c |     66465 |   36531    86739 |   13394    8158   210937    25.9 | 18.975 % |
c |     66617 |   36531    86739 |   14734    8310   214915    25.9 | 18.975 % |
c |     66845 |   36531    86739 |   16207    8538   226913    26.6 | 18.975 % |
c |     67185 |   36531    86739 |   17828    8878   240121    27.0 | 18.975 % |
c |     67691 |   36531    86739 |   19611    9384   254470    27.1 | 18.975 % |
c |     68450 |   36531    86739 |   21572   10143   285357    28.1 | 18.975 % |
c |     69589 |   36531    86739 |   23729   11282   325499    28.9 | 18.975 % |
c |     71298 |   36531    86739 |   26102   12991   388992    29.9 | 18.975 % |
c |     73862 |   36531    86739 |   28712   15555   499400    32.1 | 18.975 % |
c |     77706 |   36531    86739 |   31584   19399   641893    33.1 | 18.975 % |
c |     83473 |   36531    86739 |   34742   25166   851867    33.8 | 18.975 % |
c ==============================================================================
c [1mFound solution: 1128[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:10819     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     83855 |   48846   115593 |   16282    9881   252889    25.6 | 18.975 % |
c |     83955 |   48846   115593 |   17910    9981   256387    25.7 | 13.426 % |
c |     84108 |   48846   115593 |   19701   10134   262174    25.9 | 13.426 % |
c |     84335 |   48846   115593 |   21671   10361   273735    26.4 | 13.426 % |
c |     84674 |   48846   115593 |   23838   10700   287638    26.9 | 13.426 % |
c |     85180 |   48846   115593 |   26222   11206   302850    27.0 | 13.426 % |
c |     85939 |   48846   115593 |   28844   11965   328037    27.4 | 13.426 % |
c |     87080 |   48846   115593 |   31729   13106   363663    27.7 | 13.426 % |
c |     88789 |   48846   115593 |   34901   14815   448569    30.3 | 13.426 % |
c |     91351 |   48842   115584 |   38392   17376   574966    33.1 | 13.430 % |
c |     95195 |   48842   115584 |   42231   21220   715548    33.7 | 13.430 % |
c |    100962 |   48832   115561 |   46454   26986   948975    35.2 | 13.441 % |
c ==============================================================================
c [1mFound solution: 1120[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 |    102576 |   58954   139062 |   19651   28600   999476    34.9 | 13.441 % |
c |    102676 |   58954   139062 |   21616   14400   427455    29.7 | 16.672 % |
c |    102826 |   58954   139062 |   23777   14550   429765    29.5 | 16.672 % |
c |    103052 |   58954   139062 |   26155   14776   433516    29.3 | 16.672 % |
c |    103390 |   58314   137610 |   28771   14316   428116    29.9 | 17.465 % |
c |    103898 |   58250   137467 |   31648   14819   442265    29.8 | 17.541 % |
c |    104661 |   58250   137467 |   34812   15582   470141    30.2 | 17.541 % |
c |    105802 |   58250   137467 |   38294   16723   498243    29.8 | 17.541 % |
c |    107510 |   58250   137467 |   42123   18431   562484    30.5 | 17.541 % |
c |    110076 |   58250   137467 |   46336   20997   665926    31.7 | 17.541 % |
c |    113921 |   58250   137467 |   50969   24842   808229    32.5 | 17.541 % |
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              : 222
c conflicts             : 114741         (223 /sec)
c decisions             : 222002         (431 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 515.684 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.97 0.78 0.38 2/54 2048
Raw data (stat): 2048 (runsolver) R 2047 22932 22931 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 429284332 1052672 99 4294967295 134512640 135381576 3221224544 3221219788 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.0006 s]
Raw data (loadavg): 0.98 0.79 0.39 2/54 2048
Raw data (stat): 2048 (minisat+) R 2047 22932 22931 0 -1 0 1792 0 0 0 993 5 0 0 25 0 1 0 429284332 9891840 1760 4294967295 134512640 134672761 3221224640 3221223808 134560882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2415 1760 603 41 0 2374 0
vsize: 9660
[startup+20.0008 s]
Raw data (loadavg): 0.98 0.80 0.39 2/54 2048
Raw data (stat): 2048 (minisat+) R 2047 22932 22931 0 -1 0 1957 0 0 0 1992 6 0 0 25 0 1 0 429284332 10563584 1925 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2579 1925 603 41 0 2538 0
vsize: 10316
[startup+30.0011 s]
Raw data (loadavg): 0.98 0.80 0.40 2/54 2048
Raw data (stat): 2048 (minisat+) R 2047 22932 22931 0 -1 0 2132 0 0 0 2991 6 0 0 25 0 1 0 429284332 11378688 2100 4294967295 134512640 134672761 3221224640 3221223824 134559516 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2778 2100 603 41 0 2737 0
vsize: 11112
[startup+40.0004 s]
Raw data (loadavg): 1.06 0.83 0.41 2/54 2048
Raw data (stat): 2048 (minisat+) R 2047 22932 22931 0 -1 0 2308 0 0 0 3990 7 0 0 25 0 1 0 429284332 12046336 2276 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2941 2276 603 41 0 2900 0
vsize: 11764
[startup+50.0004 s]
Raw data (loadavg): 1.13 0.85 0.42 2/54 2048
Raw data (stat): 2048 (minisat+) R 2047 22932 22931 0 -1 0 2453 0 0 0 4990 8 0 0 25 0 1 0 429284332 12738560 2421 4294967295 134512640 134672761 3221224640 3221223744 134560370 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3110 2421 603 41 0 3069 0
vsize: 12440
[startup+60.001 s]
Raw data (loadavg): 1.11 0.85 0.43 2/54 2048
Raw data (stat): 2048 (minisat+) R 2047 22932 22931 0 -1 0 2588 0 0 0 5990 8 0 0 25 0 1 0 429284332 13266944 2556 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3239 2556 603 41 0 3198 0
vsize: 12956
[startup+70.0003 s]
Raw data (loadavg): 1.09 0.86 0.43 2/54 2048
Raw data (stat): 2048 (minisat+) R 2047 22932 22931 0 -1 0 2618 0 0 0 6988 9 0 0 25 0 1 0 429284332 13348864 2586 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3259 2586 603 41 0 3218 0
vsize: 13036
[startup+80.0012 s]
Raw data (loadavg): 1.08 0.86 0.44 2/54 2048
Raw data (stat): 2048 (minisat+) R 2047 22932 22931 0 -1 0 2618 0 0 0 7989 9 0 0 25 0 1 0 429284332 13348864 2586 4294967295 134512640 134672761 3221224640 3221223840 134557849 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3259 2586 603 41 0 3218 0
vsize: 13036
[startup+90.0009 s]
Raw data (loadavg): 1.06 0.86 0.45 2/54 2048
Raw data (stat): 2048 (minisat+) R 2047 22932 22931 0 -1 0 2653 0 0 0 8989 9 0 0 25 0 1 0 429284332 13484032 2621 4294967295 134512640 134672761 3221224640 3221223808 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3292 2621 603 41 0 3251 0
vsize: 13168
[startup+100 s]
Raw data (loadavg): 1.05 0.87 0.45 2/54 2048
Raw data (stat): 2048 (minisat+) R 2047 22932 22931 0 -1 0 2653 0 0 0 9989 9 0 0 25 0 1 0 429284332 13484032 2621 4294967295 134512640 134672761 3221224640 3221223808 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3292 2621 603 41 0 3251 0
vsize: 13168
[startup+110.001 s]
Raw data (loadavg): 1.05 0.87 0.46 2/54 2048
Raw data (stat): 2048 (minisat+) R 2047 22932 22931 0 -1 0 2653 0 0 0 10989 9 0 0 25 0 1 0 429284332 13484032 2621 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3292 2621 603 41 0 3251 0
vsize: 13168
[startup+120.002 s]
Raw data (loadavg): 1.04 0.88 0.46 2/54 2048
Raw data (stat): 2048 (minisat+) R 2047 22932 22931 0 -1 0 2655 0 0 0 11989 9 0 0 25 0 1 0 429284332 13484032 2623 4294967295 134512640 134672761 3221224640 3221223776 134560640 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3292 2623 603 41 0 3251 0
vsize: 13168
[startup+130.002 s]
Raw data (loadavg): 1.03 0.88 0.47 2/54 2048
Raw data (stat): 2048 (minisat+) R 2047 22932 22931 0 -1 0 2655 0 0 0 12989 9 0 0 25 0 1 0 429284332 13484032 2623 4294967295 134512640 134672761 3221224640 3221223776 134565098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3292 2623 603 41 0 3251 0
vsize: 13168
[startup+140.002 s]
Raw data (loadavg): 1.03 0.88 0.47 2/54 2048
Raw data (stat): 2048 (minisat+) R 2047 22932 22931 0 -1 0 2656 0 0 0 13989 9 0 0 25 0 1 0 429284332 13484032 2624 4294967295 134512640 134672761 3221224640 3221223776 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3292 2624 603 41 0 3251 0
vsize: 13168
[startup+150.002 s]
Raw data (loadavg): 1.02 0.89 0.48 2/54 2048
Raw data (stat): 2048 (minisat+) R 2047 22932 22931 0 -1 0 2656 0 0 0 14989 9 0 0 25 0 1 0 429284332 13484032 2624 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3292 2624 603 41 0 3251 0
vsize: 13168
[startup+160.002 s]
Raw data (loadavg): 1.02 0.89 0.48 2/54 2048
Raw data (stat): 2048 (minisat+) R 2047 22932 22931 0 -1 0 2656 0 0 0 15990 9 0 0 25 0 1 0 429284332 13484032 2624 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3292 2624 603 41 0 3251 0
vsize: 13168
[startup+170.002 s]
Raw data (loadavg): 1.02 0.89 0.49 2/54 2048
Raw data (stat): 2048 (minisat+) R 2047 22932 22931 0 -1 0 2711 0 0 0 16989 10 0 0 25 0 1 0 429284332 13746176 2679 4294967295 134512640 134672761 3221224640 3221223776 134560673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3356 2679 603 41 0 3315 0
vsize: 13424
[startup+180.003 s]
Raw data (loadavg): 1.01 0.90 0.49 2/54 2048
Raw data (stat): 2048 (minisat+) R 2047 22932 22931 0 -1 0 2783 0 0 0 17989 10 0 0 25 0 1 0 429284332 14012416 2751 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3421 2751 603 41 0 3380 0
vsize: 13684
[startup+190.003 s]
Raw data (loadavg): 1.01 0.90 0.50 2/54 2048
Raw data (stat): 2048 (minisat+) R 2047 22932 22931 0 -1 0 2783 0 0 0 18989 10 0 0 25 0 1 0 429284332 14012416 2751 4294967295 134512640 134672761 3221224640 3221223840 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3421 2751 603 41 0 3380 0
vsize: 13684
[startup+200.003 s]
Raw data (loadavg): 1.01 0.90 0.50 2/54 2048
Raw data (stat): 2048 (minisat+) R 2047 22932 22931 0 -1 0 2783 0 0 0 19989 10 0 0 25 0 1 0 429284332 14012416 2751 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3421 2751 603 41 0 3380 0
vsize: 13684
[startup+210.003 s]
Raw data (loadavg): 1.01 0.90 0.51 2/54 2048
Raw data (stat): 2048 (minisat+) R 2047 22932 22931 0 -1 0 2783 0 0 0 20990 10 0 0 25 0 1 0 429284332 14012416 2751 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3421 2751 603 41 0 3380 0
vsize: 13684
[startup+220.004 s]
Raw data (loadavg): 1.00 0.91 0.51 2/54 2048
Raw data (stat): 2048 (minisat+) R 2047 22932 22931 0 -1 0 2783 0 0 0 21990 10 0 0 25 0 1 0 429284332 14012416 2751 4294967295 134512640 134672761 3221224640 3221223808 134560842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3421 2751 603 41 0 3380 0
vsize: 13684
[startup+230.005 s]
Raw data (loadavg): 1.00 0.91 0.52 2/54 2048
Raw data (stat): 2048 (minisat+) R 2047 22932 22931 0 -1 0 2854 0 0 0 22990 11 0 0 25 0 1 0 429284332 14274560 2822 4294967295 134512640 134672761 3221224640 3221223744 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3485 2822 603 41 0 3444 0
vsize: 13940
[startup+240.004 s]
Raw data (loadavg): 1.00 0.91 0.52 2/54 2048
Raw data (stat): 2048 (minisat+) R 2047 22932 22931 0 -1 0 2975 0 0 0 23990 11 0 0 25 0 1 0 429284332 14827520 2943 4294967295 134512640 134672761 3221224640 3221223808 134561406 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3620 2943 603 41 0 3579 0
vsize: 14480
[startup+250.004 s]
Raw data (loadavg): 1.00 0.91 0.53 2/54 2048
Raw data (stat): 2048 (minisat+) R 2047 22932 22931 0 -1 0 3038 0 0 0 24990 11 0 0 25 0 1 0 429284332 15060992 3006 4294967295 134512640 134672761 3221224640 3221223744 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3677 3006 603 41 0 3636 0
vsize: 14708
[startup+260.005 s]
Raw data (loadavg): 1.00 0.92 0.53 2/54 2048
Raw data (stat): 2048 (minisat+) R 2047 22932 22931 0 -1 0 3040 0 0 0 25990 11 0 0 25 0 1 0 429284332 15060992 3008 4294967295 134512640 134672761 3221224640 3221223776 134560703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3677 3008 603 41 0 3636 0
vsize: 14708
[startup+270.004 s]
Raw data (loadavg): 1.00 0.92 0.54 2/54 2048
Raw data (stat): 2048 (minisat+) R 2047 22932 22931 0 -1 0 3048 0 0 0 26990 11 0 0 25 0 1 0 429284332 15060992 3016 4294967295 134512640 134672761 3221224640 3221223824 134559581 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3677 3016 603 41 0 3636 0
vsize: 14708
[startup+280.005 s]
Raw data (loadavg): 1.00 0.92 0.54 2/54 2048
Raw data (stat): 2048 (minisat+) R 2047 22932 22931 0 -1 0 3048 0 0 0 27990 11 0 0 25 0 1 0 429284332 15060992 3016 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3677 3016 603 41 0 3636 0
vsize: 14708
[startup+290.005 s]
Raw data (loadavg): 1.00 0.92 0.54 2/54 2048
Raw data (stat): 2048 (minisat+) R 2047 22932 22931 0 -1 0 3048 0 0 0 28991 11 0 0 25 0 1 0 429284332 15060992 3016 4294967295 134512640 134672761 3221224640 3221223792 134565153 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3677 3016 603 41 0 3636 0
vsize: 14708
[startup+300.005 s]
Raw data (loadavg): 1.00 0.92 0.55 2/54 2048
Raw data (stat): 2048 (minisat+) R 2047 22932 22931 0 -1 0 3048 0 0 0 29991 11 0 0 25 0 1 0 429284332 15060992 3016 4294967295 134512640 134672761 3221224640 3221223808 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3677 3016 603 41 0 3636 0
vsize: 14708
[startup+310.005 s]
Raw data (loadavg): 1.00 0.93 0.55 2/54 2048
Raw data (stat): 2048 (minisat+) R 2047 22932 22931 0 -1 0 3048 0 0 0 30991 11 0 0 25 0 1 0 429284332 15060992 3016 4294967295 134512640 134672761 3221224640 3221223804 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3677 3016 603 41 0 3636 0
vsize: 14708
[startup+320.005 s]
Raw data (loadavg): 1.00 0.93 0.56 2/54 2048
Raw data (stat): 2048 (minisat+) R 2047 22932 22931 0 -1 0 3050 0 0 0 31991 11 0 0 25 0 1 0 429284332 15060992 3018 4294967295 134512640 134672761 3221224640 3221223840 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3677 3018 603 41 0 3636 0
vsize: 14708
[startup+330.006 s]
Raw data (loadavg): 1.00 0.93 0.56 2/54 2048
Raw data (stat): 2048 (minisat+) R 2047 22932 22931 0 -1 0 3051 0 0 0 32991 11 0 0 25 0 1 0 429284332 15060992 3019 4294967295 134512640 134672761 3221224640 3221223808 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3677 3019 603 41 0 3636 0
vsize: 14708
[startup+340.006 s]
Raw data (loadavg): 1.00 0.93 0.56 2/54 2048
Raw data (stat): 2048 (minisat+) R 2047 22932 22931 0 -1 0 3074 0 0 0 33991 11 0 0 25 0 1 0 429284332 15208448 3042 4294967295 134512640 134672761 3221224640 3221223840 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3713 3042 603 41 0 3672 0
vsize: 14852
[startup+350.005 s]
Raw data (loadavg): 1.00 0.93 0.57 2/54 2048
Raw data (stat): 2048 (minisat+) R 2047 22932 22931 0 -1 0 3334 0 0 0 34991 12 0 0 25 0 1 0 429284332 15605760 3260 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3810 3260 603 41 0 3769 0
vsize: 15240
[startup+360.006 s]
Raw data (loadavg): 1.00 0.94 0.57 2/54 2048
Raw data (stat): 2048 (minisat+) R 2047 22932 22931 0 -1 0 3334 0 0 0 35991 12 0 0 25 0 1 0 429284332 15605760 3260 4294967295 134512640 134672761 3221224640 3221223744 134560370 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3810 3260 603 41 0 3769 0
vsize: 15240
[startup+370.005 s]
Raw data (loadavg): 1.00 0.94 0.58 2/54 2048
Raw data (stat): 2048 (minisat+) R 2047 22932 22931 0 -1 0 3334 0 0 0 36991 12 0 0 25 0 1 0 429284332 15605760 3260 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3810 3260 603 41 0 3769 0
vsize: 15240
[startup+380.005 s]
Raw data (loadavg): 1.00 0.94 0.58 2/54 2048
Raw data (stat): 2048 (minisat+) R 2047 22932 22931 0 -1 0 3334 0 0 0 37992 12 0 0 25 0 1 0 429284332 15605760 3260 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3810 3260 603 41 0 3769 0
vsize: 15240
[startup+390.006 s]
Raw data (loadavg): 1.00 0.94 0.58 2/54 2048
Raw data (stat): 2048 (minisat+) R 2047 22932 22931 0 -1 0 3407 0 0 0 38991 12 0 0 25 0 1 0 429284332 15867904 3333 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3874 3333 603 41 0 3833 0
vsize: 15496
[startup+400.005 s]
Raw data (loadavg): 1.00 0.94 0.59 2/54 2048
Raw data (stat): 2048 (minisat+) R 2047 22932 22931 0 -1 0 3495 0 0 0 39991 13 0 0 25 0 1 0 429284332 16269312 3421 4294967295 134512640 134672761 3221224640 3221223808 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3972 3421 603 41 0 3931 0
vsize: 15888
[startup+410.006 s]
Raw data (loadavg): 1.00 0.94 0.59 2/54 2048
Raw data (stat): 2048 (minisat+) R 2047 22932 22931 0 -1 0 3583 0 0 0 40991 13 0 0 25 0 1 0 429284332 16535552 3509 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4037 3509 603 41 0 3996 0
vsize: 16148
[startup+420.006 s]
Raw data (loadavg): 1.00 0.94 0.60 2/54 2048
Raw data (stat): 2048 (minisat+) R 2047 22932 22931 0 -1 0 3677 0 0 0 41991 13 0 0 25 0 1 0 429284332 16928768 3603 4294967295 134512640 134672761 3221224640 3221223824 134559548 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4133 3603 603 41 0 4092 0
vsize: 16532
[startup+430.006 s]
Raw data (loadavg): 1.00 0.95 0.60 2/54 2048
Raw data (stat): 2048 (minisat+) R 2047 22932 22931 0 -1 0 3762 0 0 0 42990 14 0 0 25 0 1 0 429284332 17326080 3688 4294967295 134512640 134672761 3221224640 3221223824 134558403 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4230 3688 603 41 0 4189 0
vsize: 16920
[startup+440.006 s]
Raw data (loadavg): 1.00 0.95 0.60 2/54 2048
Raw data (stat): 2048 (minisat+) R 2047 22932 22931 0 -1 0 3925 0 0 0 43990 14 0 0 25 0 1 0 429284332 17920000 3851 4294967295 134512640 134672761 3221224640 3221223840 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4375 3851 603 41 0 4334 0
vsize: 17500
[startup+450.006 s]
Raw data (loadavg): 1.00 0.95 0.61 2/54 2048
Raw data (stat): 2048 (minisat+) R 2047 22932 22931 0 -1 0 3930 0 0 0 44991 14 0 0 25 0 1 0 429284332 18059264 3856 4294967295 134512640 134672761 3221224640 3221223840 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4409 3856 603 41 0 4368 0
vsize: 17636
[startup+460.006 s]
Raw data (loadavg): 1.00 0.95 0.61 2/54 2048
Raw data (stat): 2048 (minisat+) R 2047 22932 22931 0 -1 0 3931 0 0 0 45991 14 0 0 25 0 1 0 429284332 18059264 3857 4294967295 134512640 134672761 3221224640 3221223780 134560556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4409 3857 603 41 0 4368 0
vsize: 17636
[startup+470.006 s]
Raw data (loadavg): 1.00 0.95 0.62 2/54 2048
Raw data (stat): 2048 (minisat+) R 2047 22932 22931 0 -1 0 3943 0 0 0 46991 14 0 0 25 0 1 0 429284332 18059264 3869 4294967295 134512640 134672761 3221224640 3221223840 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4409 3869 603 41 0 4368 0
vsize: 17636
[startup+480.007 s]
Raw data (loadavg): 1.00 0.95 0.62 2/54 2048
Raw data (stat): 2048 (minisat+) R 2047 22932 22931 0 -1 0 3943 0 0 0 47991 14 0 0 25 0 1 0 429284332 18059264 3869 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4409 3869 603 41 0 4368 0
vsize: 17636
[startup+490.007 s]
Raw data (loadavg): 1.00 0.95 0.62 2/54 2048
Raw data (stat): 2048 (minisat+) R 2047 22932 22931 0 -1 0 3943 0 0 0 48991 14 0 0 25 0 1 0 429284332 18059264 3869 4294967295 134512640 134672761 3221224640 3221223792 134565086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4409 3869 603 41 0 4368 0
vsize: 17636
[startup+500.007 s]
Raw data (loadavg): 1.00 0.95 0.63 2/54 2048
Raw data (stat): 2048 (minisat+) R 2047 22932 22931 0 -1 0 3945 0 0 0 49991 14 0 0 25 0 1 0 429284332 18059264 3871 4294967295 134512640 134672761 3221224640 3221223808 134561161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4409 3871 603 41 0 4368 0
vsize: 17636
[startup+510.007 s]
Raw data (loadavg): 1.00 0.95 0.63 2/54 2048
Raw data (stat): 2048 (minisat+) R 2047 22932 22931 0 -1 0 3977 0 0 0 50991 14 0 0 25 0 1 0 429284332 18206720 3903 4294967295 134512640 134672761 3221224640 3221223744 134559946 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4445 3903 603 41 0 4404 0
vsize: 17780
[startup+515.795 s]
Raw data (loadavg): 1.00 0.95 0.63 1/53 2048
Raw data (stat): 2048 (minisat+) R 2047 22932 22931 0 -1 0 3977 0 0 0 50991 14 0 0 25 0 1 0 429284332 18206720 3903 4294967295 134512640 134672761 3221224640 3221223744 134559946 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4445 3903 603 41 0 4404 0
vsize: 0

Child status: 30
Real time (s): 515.795
CPU time (s): 515.855
CPU user time (s): 515.697
CPU system time (s): 0.157975
CPU usage (%): 100.012
Max. virtual memory (Kb): 17780
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	1120
#### END VERIFIER DATA ####