PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-p0040.opb
MD5SUM	1c249519911563f3292efb34f4875b44
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	62027
Optimality of the best value was proved	NO
Number of terms in the objective function	40
Biggest coefficient in the objective function	8161
Number of bits for the biggest coefficient in the objective function	13
Sum of the numbers in the objective function	265332
Number of bits of the sum of numbers in the objective function	19
Biggest number in a constraint	8161
Number of bits of the biggest number in a constraint	13
Biggest sum of numbers in a constraint	265332
Number of bits of the biggest sum of numbers	19
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	0.276957
Number of variables	40
Total number of constraints	63
Number of constraints which are clauses	10
Number of constraints which are cardinality constraints (but not clauses)	50
Number of constraints which are nor clauses,nor cardinality constraints	3
Minimum length of a constraint	1
Maximum length of a constraint	10
Trace number 16883

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc13 THE 2005-04-21 09:19:46 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=12114 boxname=wulflinc13 idbench=932 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  1c249519911563f3292efb34f4875b44  /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-20-10-p0040.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-20-10-p0040.opb /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-20-10-p0040.opb
IDLAUNCH: 12114
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
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	: 2
cpu MHz		: 451.242
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:        599200 kB
Buffers:         34240 kB
Cached:         379092 kB
SwapCached:        176 kB
Active:         183944 kB
Inactive:       232124 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        598948 kB
SwapTotal:     2097136 kB
SwapFree:      2096860 kB
Dirty:              36 kB
Writeback:           0 kB
Mapped:           6812 kB
Slab:            13724 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 09:20:41 (client local time) WITH STATUS 30 IN 53.9548 SECONDS
stats: 12114 0 53.9548 30
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 23 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ##########
c   -- Clauses(.)/Splits(s): .
c ---[  21]---> BDD-cost:    5
c ---[  19]---> BDD-cost:    5
c ---[  17]---> BDD-cost:    5
c ---[  15]---> BDD-cost:    5
c ---[  13]---> BDD-cost:    5
c ---[  11]---> BDD-cost:    5
c ---[   9]---> BDD-cost:    5
c ---[   7]---> BDD-cost:    5
c ---[   5]---> BDD-cost:    5
c ---[   3]---> BDD-cost:    5
c ---[   2]---> BDD-cost:   17
c ---[   1]---> BDD-cost:   16
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |     186      521 |      55       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  111/111          
c   -- var.elim.:  67/67          
c   -- subsuming                       
c   -- var.elim.:  57/57          
c   -- var.elim.:  40/40          
c |         0 |      90      340 |      --       0       --      -- |     --   | -96/-145
c |         0 |      90      340 |      36       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 0.016997 s)
c ==============================================================================
c [1mFound solution: 66305[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 7885     Base: 3 3 3 3 3 3 7
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         1 |   19529    45834 |    5858       1       16    16.0 |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/6844          
c   -- var.elim.:  2000/6844          
c   -- var.elim.:  3000/6844          
c   -- var.elim.:  4000/6844          
c   -- var.elim.:  5000/6844          
c   -- var.elim.:  6000/6844          
c   -- var.elim.:  6844/6844          
c   -- var.elim.:  1000/3666          
c   -- var.elim.:  2000/3666          
c   -- var.elim.:  3000/3666          
c   -- var.elim.:  3666/3666          
c   -- var.elim.:  238/238          
c   -- var.elim.:  52/52          
c   -- subsuming                       
c   -- var.elim.:  564/564          
c   -- var.elim.:  200/200          
c   -- var.elim.:  20/20          
c   -- subsuming                       
c   -- var.elim.:  85/85          
c   -- var.elim.:  25/25          
c |         1 |   16975    52482 |      --       1       --      -- |     --   | -2554/6649
c |         1 |   16975    52482 |    6790       1       16    16.0 |  0.000 % |
c |       102 |   16975    52482 |    7469     102     1202    11.8 |  0.906 % |
c ==============================================================================
c (current CPU-time: 1.39979 s)
c ==============================================================================
c [1mFound solution: 64521[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   13     Base: 3 3 3 3 3 3 7
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       106 |   18088    55372 |    5426     106     1222    11.5 |  0.906 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1534          
c   -- var.elim.:  1534/1534          
c   -- var.elim.:  843/843          
c   -- var.elim.:  142/142          
c   -- subsuming                       
c   -- var.elim.:  247/247          
c   -- var.elim.:  110/110          
c |       106 |   17503    55496 |      --     106       --      -- |     --   | -585/125
c |       106 |   17503    55496 |    7001     106     1222    11.5 |  0.906 % |
c ==============================================================================
c (current CPU-time: 1.87372 s)
c ==============================================================================
c [1mFound solution: 64435[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 3 3 3 3 3 3 7
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       107 |   17647    55995 |    5294     107     1428    13.3 |  0.906 % |
c   -- subsuming                       
c   -- var.elim.:  365/365          
c   -- var.elim.:  229/229          
c |       107 |   17535    56004 |      --     107       --      -- |     --   | -112/10
c |       107 |   17535    56004 |    7014     107     1428    13.3 |  0.906 % |
c ==============================================================================
c (current CPU-time: 2.22266 s)
c ==============================================================================
c [1mFound solution: 64046[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 3 3 3 3 3 3 7
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       109 |   17939    57179 |    5381     109     1657    15.2 |  0.906 % |
c   -- subsuming                       
c   -- var.elim.:  726/726          
c   -- var.elim.:  440/440          
c   -- var.elim.:  111/111          
c   -- var.elim.:  78/78          
c   -- subsuming                       
c   -- var.elim.:  148/148          
c   -- var.elim.:  74/74          
c |       109 |   17669    57320 |      --     109       --      -- |     --   | -270/142
c |       109 |   17669    57320 |    7067     109     1657    15.2 |  0.906 % |
c ==============================================================================
c (current CPU-time: 2.67359 s)
c ==============================================================================
c [1mFound solution: 63960[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 3 3 3 3 3 3 7
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       120 |   17876    57991 |    5362     120     3224    26.9 |  0.906 % |
c   -- subsuming                       
c   -- var.elim.:  450/450          
c   -- var.elim.:  289/289          
c   -- var.elim.:  96/96          
c |       120 |   17718    58122 |      --     120       --      -- |     --   | -158/132
c |       120 |   17718    58122 |    7087     120     3224    26.9 |  0.906 % |
c |       220 |   17718    58122 |    7795     220     6889    31.3 |  0.965 % |
c |       372 |   17718    58122 |    8575     372    20097    54.0 |  0.965 % |
c |       598 |   17710    58082 |    9428     597    31241    52.3 |  0.991 % |
c |       935 |   17710    58082 |   10371     934    59132    63.3 |  0.991 % |
c |      1444 |   17710    58082 |   11408    1443   118185    81.9 |  0.991 % |
c ==============================================================================
c (current CPU-time: 4.88726 s)
c ==============================================================================
c [1mFound solution: 63955[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 3 3 3 3 3 3 7
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1565 |   17621    56897 |    5286    1562   127921    81.9 |  0.991 % |
c   -- subsuming                       
c   -- var.elim.:  694/694          
c   -- var.elim.:  529/529          
c   -- var.elim.:  115/115          
c   -- subsuming                       
c   -- var.elim.:  122/122          
c   -- var.elim.:  7/7          
c |      1565 |   17420    56820 |      --    1562       --      -- |     --   | -199/-72
c |      1565 |   17420    56820 |    6968    1354    76282    56.3 |  0.991 % |
c |      1665 |   17404    56767 |    7657    1453    85251    58.7 |  1.759 % |
c |      1817 |   17360    56603 |    8402    1604    99262    61.9 |  1.889 % |
c |      2043 |   17103    55559 |    9105    1828   122688    67.1 |  2.704 % |
c |      2381 |   17094    55516 |   10010    2164   157686    72.9 |  2.808 % |
c |      2888 |   17094    55516 |   11012    2671   191006    71.5 |  2.808 % |
c ==============================================================================
c (current CPU-time: 7.38288 s)
c ==============================================================================
c [1mFound solution: 63884[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 3 3 3 3 3 3 7
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      2985 |   17259    56094 |    5177    2768   204376    73.8 |  2.808 % |
c   -- subsuming                       
c   -- var.elim.:  780/780          
c   -- var.elim.:  527/527          
c   -- var.elim.:  137/137          
c   -- subsuming                       
c   -- var.elim.:  178/178          
c |      2985 |   17062    55950 |      --    2768       --      -- |     --   | -195/-139
c |      2985 |   17062    55950 |    6824    1519    26659    17.6 |  2.808 % |
c ==============================================================================
c (current CPU-time: 7.9088 s)
c ==============================================================================
c [1mFound solution: 63847[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 3 3 3 3 3 3 7
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      2995 |   17465    57134 |    5239    1529    27131    17.7 |  2.808 % |
c   -- subsuming                       
c   -- var.elim.:  707/707          
c   -- var.elim.:  437/437          
c   -- var.elim.:  161/161          
c   -- var.elim.:  24/24          
c   -- subsuming                       
c   -- var.elim.:  71/71          
c |      2995 |   17171    56840 |      --    1529       --      -- |     --   | -290/-283
c |      2995 |   17171    56840 |    6868    1529    27131    17.7 |  2.808 % |
c ==============================================================================
c (current CPU-time: 8.40672 s)
c ==============================================================================
c [1mFound solution: 63840[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   11     Base: 3 3 3 3 3 3 7
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      3041 |   17389    57560 |    5216    1575    30493    19.4 |  2.808 % |
c   -- subsuming                       
c   -- var.elim.:  476/476          
c   -- var.elim.:  314/314          
c   -- var.elim.:  143/143          
c   -- var.elim.:  19/19          
c |      3041 |   17209    57492 |      --    1575       --      -- |     --   | -180/-67
c |      3041 |   17209    57492 |    6883    1575    30493    19.4 |  2.808 % |
c |      3142 |   17209    57492 |    7571    1676    38082    22.7 |  3.035 % |
c |      3293 |   17209    57492 |    8329    1827    41916    22.9 |  3.035 % |
c |      3518 |   17209    57492 |    9162    2052    49509    24.1 |  3.035 % |
c |      3856 |   17209    57492 |   10078    2390    69373    29.0 |  3.035 % |
c |      4364 |   17205    57475 |   11083    2889   105398    36.5 |  3.087 % |
c ==============================================================================
c (current CPU-time: 11.0313 s)
c ==============================================================================
c [1mFound solution: 63593[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   11     Base: 3 3 3 3 3 3 7
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      4684 |   17393    58115 |    5217    3209   138271    43.1 |  3.087 % |
c   -- subsuming                       
c   -- var.elim.:  481/481          
c   -- var.elim.:  313/313          
c   -- var.elim.:  82/82          
c   -- var.elim.:  19/19          
c |      4684 |   17236    58114 |      --    3209       --      -- |     --   | -157/0
c |      4684 |   17236    58114 |    6894    3209   138271    43.1 |  3.087 % |
c |      4784 |   17170    57843 |    7554    3308   144054    43.5 |  3.267 % |
c |      4934 |   17170    57843 |    8310    3458   151702    43.9 |  3.268 % |
c |      5161 |   17142    57348 |    9126    3684   181270    49.2 |  3.320 % |
c ==============================================================================
c (current CPU-time: 12.5061 s)
c ==============================================================================
c [1mFound solution: 63503[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 3 3 3 3 3 3 7
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      5412 |   17359    58059 |    5207    3935   194413    49.4 |  3.320 % |
c   -- subsuming                       
c   -- var.elim.:  625/625          
c   -- var.elim.:  436/436          
c   -- var.elim.:  123/123          
c   -- var.elim.:  16/16          
c   -- subsuming                       
c   -- var.elim.:  71/71          
c |      5412 |   17159    58242 |      --    3935       --      -- |     --   | -198/188
c |      5412 |   17159    58242 |    6863    3686   139936    38.0 |  3.320 % |
c |      5512 |   17159    58242 |    7549    3786   146758    38.8 |  3.401 % |
c |      5664 |   17159    58242 |    8304    3938   170136    43.2 |  3.401 % |
c |      5890 |   17159    58242 |    9135    4164   179683    43.2 |  3.400 % |
c |      6228 |   17159    58242 |   10048    4502   197873    44.0 |  3.401 % |
c |      6734 |   17159    58242 |   11053    5008   263560    52.6 |  3.401 % |
c |      7493 |   17159    58242 |   12159    5767   357608    62.0 |  3.401 % |
c ==============================================================================
c (current CPU-time: 16.6805 s)
c ==============================================================================
c [1mFound solution: 63287[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 3 3 3 3 3 3 7
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      7771 |   17588    59483 |    5276    6045   390606    64.6 |  3.401 % |
c   -- subsuming                       
c   -- var.elim.:  751/751          
c   -- var.elim.:  458/458          
c   -- var.elim.:  147/147          
c   -- var.elim.:  126/126          
c   -- var.elim.:  19/19          
c   -- subsuming                       
c   -- var.elim.:  71/71          
c |      7771 |   17288    59695 |      --    6045       --      -- |     --   | -299/215
c |      7771 |   17288    59695 |    6915    6045   390606    64.6 |  3.401 % |
c |      7872 |   17076    57819 |    7513    6002   391768    65.3 |  3.973 % |
c |      8022 |   17076    57819 |    8264    6152   399588    65.0 |  3.974 % |
c |      8247 |   17004    57547 |    9052    6375   414619    65.0 |  4.181 % |
c ==============================================================================
c (current CPU-time: 18.6412 s)
c ==============================================================================
c [1mFound solution: 63103[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 3 3 3 3 3 3 7
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      8516 |   17165    58061 |    5149    6644   453626    68.3 |  4.181 % |
c   -- subsuming                       
c   -- var.elim.:  626/626          
c   -- var.elim.:  475/475          
c   -- var.elim.:  100/100          
c   -- subsuming                       
c   -- var.elim.:  86/86          
c |      8516 |   17002    59066 |      --    6644       --      -- |     --   | -163/1006
c |      8516 |   17002    59066 |    6800    5798   253225    43.7 |  4.181 % |
c |      8616 |   17002    59066 |    7480    5898   264592    44.9 |  4.299 % |
c |      8767 |   17002    59066 |    8228    6049   277224    45.8 |  4.298 % |
c |      8992 |   17002    59066 |    9051    6274   307783    49.1 |  4.299 % |
c ==============================================================================
c (current CPU-time: 20.4289 s)
c ==============================================================================
c [1mFound solution: 63067[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 3 3 3 3 3 3 7
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      9176 |   17225    59783 |    5167    6458   333638    51.7 |  4.299 % |
c   -- subsuming                       
c   -- var.elim.:  467/467          
c   -- var.elim.:  304/304          
c   -- var.elim.:  149/149          
c   -- var.elim.:  76/76          
c |      9176 |   17025    59586 |      --    6458       --      -- |     --   | -200/-196
c |      9176 |   17025    59586 |    6810    6458   333638    51.7 |  4.299 % |
c |      9279 |   16976    59321 |    7469    6559   344532    52.5 |  4.507 % |
c |      9431 |   16976    59321 |    8216    6711   355392    53.0 |  4.507 % |
c |      9658 |   16976    59321 |    9038    6938   374697    54.0 |  4.507 % |
c |      9995 |   16976    59321 |    9941    7275   418622    57.5 |  4.507 % |
c |     10505 |   16976    59321 |   10936    7785   473073    60.8 |  4.507 % |
c |     11267 |   16936    59106 |   12001    8546   559014    65.4 |  4.585 % |
c ==============================================================================
c (current CPU-time: 25.3771 s)
c ==============================================================================
c [1mFound solution: 62968[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 3 3 3 3 3 3 7
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     11675 |   17091    59621 |    5127    8954   610180    68.1 |  4.585 % |
c   -- subsuming                       
c   -- var.elim.:  617/617          
c   -- var.elim.:  384/384          
c   -- var.elim.:  58/58          
c   -- subsuming                       
c   -- var.elim.:  71/71          
c |     11675 |   16948    59422 |      --    8954       --      -- |     --   | -140/-192
c |     11675 |   16948    59422 |    6779    8191   508006    62.0 |  4.585 % |
c |     11776 |   16948    59422 |    7457    5562   397450    71.5 |  4.659 % |
c |     11926 |   16948    59422 |    8202    5712   425052    74.4 |  4.660 % |
c |     12152 |   16948    59422 |    9023    5938   458004    77.1 |  4.659 % |
c |     12489 |   16948    59422 |    9925    6275   504186    80.3 |  4.659 % |
c |     12995 |   16948    59422 |   10917    6781   577071    85.1 |  4.660 % |
c ==============================================================================
c (current CPU-time: 28.9616 s)
c ==============================================================================
c [1mFound solution: 62963[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 3 3 3 3 3 3 7
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     13264 |   17130    60059 |    5138    7050   618620    87.7 |  4.660 % |
c   -- subsuming                       
c   -- var.elim.:  439/439          
c   -- var.elim.:  301/301          
c   -- var.elim.:  98/98          
c   -- var.elim.:  95/95          
c |     13264 |   16969    59846 |      --    7050       --      -- |     --   | -161/-212
c |     13264 |   16969    59846 |    6787    7050   618620    87.7 |  4.660 % |
c |     13364 |   16969    59846 |    7466    4800   436221    90.9 |  4.683 % |
c ==============================================================================
c (current CPU-time: 29.8405 s)
c ==============================================================================
c [1mFound solution: 62917[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 3 3 3 3 3 3 7
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     13434 |   17112    60342 |    5133    4870   446204    91.6 |  4.683 % |
c   -- subsuming                       
c   -- var.elim.:  364/364          
c   -- var.elim.:  232/232          
c   -- var.elim.:  32/32          
c |     13434 |   16990    60137 |      --    4870       --      -- |     --   | -122/-204
c |     13434 |   16990    60137 |    6796    4870   446204    91.6 |  4.683 % |
c |     13535 |   16990    60137 |    7475    4971   463127    93.2 |  4.705 % |
c |     13685 |   16990    60137 |    8223    5121   478805    93.5 |  4.705 % |
c |     13910 |   16990    60137 |    9045    5346   507288    94.9 |  4.705 % |
c ==============================================================================
c (current CPU-time: 31.2942 s)
c ==============================================================================
c [1mFound solution: 62592[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 3 3 3 3 3 3 7
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     14025 |   17352    61162 |    5205    5461   528453    96.8 |  4.705 % |
c   -- subsuming                       
c   -- var.elim.:  625/625          
c   -- var.elim.:  373/373          
c   -- var.elim.:  121/121          
c |     14025 |   17078    60811 |      --    5461       --      -- |     --   | -272/-346
c |     14025 |   17078    60811 |    6831    5461   528453    96.8 |  4.705 % |
c |     14126 |   17078    60811 |    7514    5562   540452    97.2 |  4.785 % |
c |     14277 |   17078    60811 |    8265    5713   557942    97.7 |  4.785 % |
c ==============================================================================
c (current CPU-time: 32.4871 s)
c ==============================================================================
c [1mFound solution: 62549[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   11     Base: 3 3 3 3 3 3 7
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     14369 |   17303    61571 |    5190    5805   572161    98.6 |  4.785 % |
c   -- subsuming                       
c   -- var.elim.:  538/538          
c   -- var.elim.:  368/368          
c   -- var.elim.:  163/163          
c   -- var.elim.:  151/151          
c |     14369 |   17107    61964 |      --    5805       --      -- |     --   | -196/394
c |     14369 |   17107    61964 |    6842    5805   572161    98.6 |  4.785 % |
c |     14470 |   17051    61714 |    7502    5905   585432    99.1 |  4.965 % |
c ==============================================================================
c (current CPU-time: 33.4779 s)
c ==============================================================================
c [1mFound solution: 62514[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 3 3 3 3 3 3 7
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     14537 |   17230    62302 |    5168    5972   597243   100.0 |  4.965 % |
c   -- subsuming                       
c   -- var.elim.:  453/453          
c   -- var.elim.:  314/314          
c   -- var.elim.:  63/63          
c |     14537 |   17073    62205 |      --    5972       --      -- |     --   | -157/-96
c |     14537 |   17073    62205 |    6829    5483   459382    83.8 |  4.965 % |
c |     14639 |   17025    62030 |    7491    5584   473400    84.8 |  5.198 % |
c |     14792 |   17025    62030 |    8240    5737   490073    85.4 |  5.198 % |
c |     15018 |   17025    62030 |    9064    5963   521671    87.5 |  5.198 % |
c |     15357 |   16931    61658 |    9915    6298   554537    88.0 |  5.483 % |
c ==============================================================================
c (current CPU-time: 36.1785 s)
c ==============================================================================
c [1mFound solution: 62251[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 3 3 3 3 3 3 7
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     15669 |   17121    62289 |    5136    6610   604002    91.4 |  5.483 % |
c   -- subsuming                       
c   -- var.elim.:  530/530          
c   -- var.elim.:  335/335          
c   -- var.elim.:  88/88          
c   -- var.elim.:  66/66          
c |     15669 |   16948    62065 |      --    6610       --      -- |     --   | -173/-223
c |     15669 |   16948    62065 |    6779    5636   368223    65.3 |  5.483 % |
c |     15769 |   16948    62065 |    7457    5736   382989    66.8 |  5.513 % |
c |     15920 |   16948    62065 |    8202    5887   403697    68.6 |  5.513 % |
c |     16145 |   16948    62065 |    9023    6112   425874    69.7 |  5.513 % |
c |     16482 |   16948    62065 |    9925    6449   478940    74.3 |  5.513 % |
c |     16988 |   16948    62065 |   10917    6955   539449    77.6 |  5.512 % |
c ==============================================================================
c (current CPU-time: 40.5688 s)
c ==============================================================================
c [1mFound solution: 62180[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 3 3 3 3 3 3 7
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     17475 |   17106    62434 |    5131    7440   614033    82.5 |  5.512 % |
c   -- subsuming                       
c   -- var.elim.:  633/633          
c   -- var.elim.:  424/424          
c   -- var.elim.:  111/111          
c   -- var.elim.:  73/73          
c |     17475 |   16914    62293 |      --    7440       --      -- |     --   | -192/-140
c |     17475 |   16914    62293 |    6765    6963   487991    70.1 |  5.512 % |
c ==============================================================================
c (current CPU-time: 41.4077 s)
c ==============================================================================
c [1mFound solution: 62116[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 3 3 3 3 3 3 7
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     17534 |   17122    62948 |    5136    7022   494855    70.5 |  5.512 % |
c   -- subsuming                       
c   -- var.elim.:  431/431          
c   -- var.elim.:  275/275          
c   -- var.elim.:  108/108          
c |     17534 |   16941    62692 |      --    7022       --      -- |     --   | -181/-255
c |     17534 |   16941    62692 |    6776    7022   494855    70.5 |  5.512 % |
c |     17635 |   16941    62692 |    7454    4783   318064    66.5 |  5.772 % |
c |     17785 |   16853    62156 |    8156    4931   335077    68.0 |  6.005 % |
c |     18012 |   16762    61688 |    8924    5155   365806    71.0 |  6.292 % |
c |     18349 |   16762    61688 |    9816    5492   405110    73.8 |  6.289 % |
c |     18856 |   16687    61388 |   10749    5996   472812    78.9 |  6.548 % |
c ==============================================================================
c (current CPU-time: 44.6872 s)
c ==============================================================================
c [1mFound solution: 62113[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 3 3 3 3 3 3 7
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     18992 |   16861    61929 |    5058    6132   491839    80.2 |  6.548 % |
c   -- subsuming                       
c   -- var.elim.:  742/742          
c   -- var.elim.:  625/625          
c   -- var.elim.:  58/58          
c   -- subsuming                       
c   -- var.elim.:  287/287          
c |     18992 |   16683    61979 |      --    6132       --      -- |     --   | -178/51
c |     18992 |   16683    61979 |    6673    4327   140235    32.4 |  6.548 % |
c ==============================================================================
c (current CPU-time: 45.6531 s)
c ==============================================================================
c [1mFound solution: 62051[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   11     Base: 3 3 3 3 3 3 7
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     19072 |   16957    62836 |    5087    4407   152284    34.6 |  6.548 % |
c   -- subsuming                       
c   -- var.elim.:  549/549          
c   -- var.elim.:  354/354          
c   -- var.elim.:  186/186          
c   -- var.elim.:  55/55          
c |     19072 |   16714    62440 |      --    4407       --      -- |     --   | -242/-393
c |     19072 |   16714    62440 |    6685    4407   152284    34.6 |  6.548 % |
c |     19172 |   16714    62440 |    7354    4507   170780    37.9 |  6.659 % |
c |     19322 |   16714    62440 |    8089    4657   189407    40.7 |  6.653 % |
c |     19547 |   16714    62440 |    8898    4882   216354    44.3 |  6.653 % |
c |     19887 |   16664    62218 |    9759    5221   253784    48.6 |  6.783 % |
c |     20393 |   16612    61898 |   10701    5726   328010    57.3 |  6.887 % |
c |     21152 |   14274    48635 |   10114    3980   196498    49.4 | 14.787 % |
c ==============================================================================
c (current CPU-time: 50.6843 s)
c ==============================================================================
c [1mFound solution: 62030[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 3480     Base: 3 3 3 3 3 3 7
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     21687 |   17277    49074 |    5183    1023    25839    25.3 | 14.787 % |
c   -- subsuming                       
c   -- var.elim.:  1000/4939          
c   -- var.elim.:  2000/4939          
c   -- var.elim.:  3000/4939          
c   -- var.elim.:  4000/4939          
c   -- var.elim.:  4939/4939          
c   -- var.elim.:  1000/2882          
c   -- var.elim.:  2000/2882          
c   -- var.elim.:  2882/2882          
c   -- var.elim.:  701/701          
c   -- var.elim.:  542/542          
c   -- var.elim.:  141/141          
c   -- var.elim.:  62/62          
c   -- subsuming                       
c   -- var.elim.:  694/694          
c   -- var.elim.:  304/304          
c   -- var.elim.:  18/18          
c   -- var.elim.:  44/44          
c   -- subsuming                       
c   -- var.elim.:  158/158          
c   -- var.elim.:  97/97          
c   -- subsuming                       
c   -- var.elim.:  44/44          
c   -- var.elim.:  21/21          
c |     21687 |   14222    46907 |      --    1023       --      -- |     --   | -3002/-2038
c |     21687 |   14222    46907 |    5688    1023    25839    25.3 | 14.787 % |
c |     21787 |   14200    46814 |    6248     321     6168    19.2 | 34.322 % |
c ==============================================================================
c (current CPU-time: 52.324 s)
c ==============================================================================
c [1mFound solution: 62027[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   12     Base: 3 3 3 3 3 3 7
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     21846 |   14619    47938 |    4385     380    12054    31.7 | 34.322 % |
c   -- subsuming                       
c   -- var.elim.:  659/659          
c   -- var.elim.:  531/531          
c   -- var.elim.:  156/156          
c   -- var.elim.:  20/20          
c   -- subsuming                       
c   -- var.elim.:  205/205          
c   -- var.elim.:  103/103          
c |     21846 |   14338    47879 |      --     380       --      -- |     --   | -281/-58
c |     21846 |   14338    47879 |    5735     376    11496    30.6 | 34.322 % |
c |     21946 |   14338    47879 |    6308     476    17289    36.3 | 34.066 % |
c ==============================================================================
c [1mOptimal solution: 62027[0m
s OPTIMUM FOUND
v -C1001_bit0 C1002_bit0 -C1003_bit0 -C1004_bit0 -C1005_bit0 C1006_bit0 -C1007_bit0 -C1008_bit0 C1009_bit0 -C1010_bit0 -C1011_bit0 -C1012_bit0 -C1013_bit0 -C1014_bit0 C1015_bit0 -C1016_bit0 -C1017_bit0 C1018_bit0 -C1019_bit0 -C1020_bit0 -C1021_bit0 C1022_bit0 -C1023_bit0 -C1024_bit0 -C1025_bit0 C1026_bit0 -C1027_bit0 -C1028_bit0 C1029_bit0 -C1030_bit0 -C1031_bit0 -C1032_bit0 -C1033_bit0 C1034_bit0 -C1035_bit0 -C1036_bit0 -C1037_bit0 C1038_bit0 -C1039_bit0 -C1040_bit0
c _______________________________________________________________________________
c 
c restarts              : 99
c conflicts             : 22086          (414 /sec)
c decisions             : 37782          (708 /sec)
c propagations          : 9856680        (184714 /sec)
c inspects              : 56859221       (1065540 /sec)
c CPU time              : 53.3619 s
c _______________________________________________________________________________
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.85 0.96 0.91 2/54 2992
Raw data (stat): 2992 (runsolver) R 2991 30701 30700 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 485731726 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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.0001 s]
Raw data (loadavg): 0.87 0.96 0.91 2/54 2992
Raw data (stat): 2992 (minisat+) R 2991 30701 30700 0 -1 0 5993 0 0 0 980 18 0 0 25 0 1 0 485731726 9424896 1792 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2301 1792 603 41 0 2260 0
vsize: 9204
[startup+20.0007 s]
Raw data (loadavg): 0.89 0.96 0.91 2/54 2992
Raw data (stat): 2992 (minisat+) R 2991 30701 30700 0 -1 0 8602 0 0 0 1972 26 0 0 25 0 1 0 485731726 10776576 2134 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2631 2134 603 41 0 2590 0
vsize: 10524
[startup+30.0014 s]
Raw data (loadavg): 0.91 0.96 0.91 2/54 2992
Raw data (stat): 2992 (minisat+) R 2991 30701 30700 0 -1 0 10230 0 0 0 2967 32 0 0 25 0 1 0 485731726 12247040 2498 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2990 2498 603 41 0 2949 0
vsize: 11960
[startup+40.002 s]
Raw data (loadavg): 0.92 0.96 0.91 2/54 2992
Raw data (stat): 2992 (minisat+) R 2991 30701 30700 0 -1 0 13406 0 0 0 3955 44 0 0 25 0 1 0 485731726 12840960 2645 4294967295 134512640 134672761 3221224544 3221223688 134616123 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3135 2645 603 41 0 3094 0
vsize: 12540
[startup+50.0031 s]
Raw data (loadavg): 0.93 0.97 0.91 2/54 2992
Raw data (stat): 2992 (minisat+) R 2991 30701 30700 0 -1 0 15982 0 0 0 4946 53 0 0 25 0 1 0 485731726 12787712 2653 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3122 2653 603 41 0 3081 0
vsize: 12488
[startup+53.9632 s]
Raw data (loadavg): 0.93 0.97 0.91 1/53 2992
Raw data (stat): 2992 (minisat+) R 2991 30701 30700 0 -1 0 15982 0 0 0 4946 53 0 0 25 0 1 0 485731726 12787712 2653 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3122 2653 603 41 0 3081 0
vsize: 0

Child status: 30
Real time (s): 53.9629
CPU time (s): 53.9548
CPU user time (s): 53.3669
CPU system time (s): 0.58791
CPU usage (%): 99.985
Max. virtual memory (Kb): 12540
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	62027
#### END VERIFIER DATA ####