PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:

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

General information on the benchmark

Name	normalized-opb/mps-v2-13-7/plato.asu.edu/pub/fctp/normalized-mps-v2-13-7-bk4x3.opb
MD5SUM	c2339539ffa69702e62053614fe34ce1
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	44800
Optimality of the best value was proved	NO
Number of terms in the objective function	252
Biggest coefficient in the objective function	2621440
Number of bits for the biggest coefficient in the objective function	22
Sum of the numbers in the objective function	35682270
Number of bits of the sum of numbers in the objective function	26
Biggest number in a constraint	2621440
Number of bits of the biggest number in a constraint	22
Biggest sum of numbers in a constraint	35682270
Number of bits of the biggest sum of numbers	26
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	24.1133
Number of variables	252
Total number of constraints	19
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	19
Minimum length of a constraint	21
Maximum length of a constraint	80

Trace number 17787

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc15 THE 2005-04-21 12:23:57 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18978 boxname=wulflinc15 idbench=1460 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  c2339539ffa69702e62053614fe34ce1  /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-13-7-bk4x3.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-13-7-bk4x3.opb /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-13-7-bk4x3.opb
IDLAUNCH: 18978
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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		: 450.999
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:        554056 kB
Buffers:         34500 kB
Cached:         424604 kB
SwapCached:        440 kB
Active:         154492 kB
Inactive:       306784 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        553804 kB
SwapTotal:     2097136 kB
SwapFree:      2095984 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5360 kB
Slab:            13736 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 12:24:26 (client local time) WITH STATUS 30 IN 28.8256 SECONDS
stats: 18978 0 28.8256 30
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 26 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #######
c   -- Clauses(.)/Splits(s): (none)
c ---[  24]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  22]---> Sorter-cost:  261     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  20]---> Sorter-cost:  275     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  18]---> Sorter-cost:  261     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  16]---> Sorter-cost:  455     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  14]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  12]---> Sorter-cost:  455     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  11]---> BDD-cost:   14
c ---[  10]---> BDD-cost:   14
c ---[   9]---> BDD-cost:   15
c ---[   8]---> BDD-cost:   15
c ---[   7]---> BDD-cost:   14
c ---[   6]---> BDD-cost:   15
c ---[   5]---> BDD-cost:   16
c ---[   4]---> BDD-cost:   16
c ---[   3]---> BDD-cost:   15
c ---[   2]---> BDD-cost:   16
c ---[   1]---> BDD-cost:   16
c ---[   0]---> BDD-cost:   15
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |    6276    14813 |    1882       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1968          
c   -- var.elim.:  1968/1968          
c   -- var.elim.:  1000/1039          
c   -- var.elim.:  1039/1039          
c   -- var.elim.:  37/37          
c   -- subsuming                       
c   -- var.elim.:  663/663          
c   -- var.elim.:  467/467          
c   -- subsuming                       
c   -- var.elim.:  140/140          
c |         0 |    4518    13172 |      --       0       --      -- |     --   | -1201/-234
c |         0 |    4518    13172 |    1807       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 0.345947 s)
c ==============================================================================
c [1mFound solution: 64786[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 6116     Base: 2 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |        28 |   18753    46404 |    5625      28      137     4.9 |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/5518          
c   -- var.elim.:  2000/5518          
c   -- var.elim.:  3000/5518          
c   -- var.elim.:  4000/5518          
c   -- var.elim.:  5000/5518          
c   -- var.elim.:  5518/5518          
c   -- var.elim.:  1000/3001          
c   -- var.elim.:  2000/3001          
c   -- var.elim.:  3000/3001          
c   -- var.elim.:  3001/3001          
c   -- var.elim.:  295/295          
c   -- var.elim.:  276/276          
c   -- subsuming                       
c   -- var.elim.:  673/673          
c   -- var.elim.:  357/357          
c   -- subsuming                       
c   -- var.elim.:  153/153          
c |        28 |   16833    52992 |      --      28       --      -- |     --   | -1920/6589
c |        28 |   16833    52992 |    6733      28      137     4.9 |  0.000 % |
c |       128 |   16833    52992 |    7406     128     4940    38.6 |  8.243 % |
c ==============================================================================
c (current CPU-time: 1.9617 s)
c ==============================================================================
c [1mFound solution: 52480[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   12     Base: 2 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       263 |   17664    55405 |    5299     263     7854    29.9 |  8.243 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1431          
c   -- var.elim.:  1431/1431          
c   -- var.elim.:  776/776          
c   -- var.elim.:  216/216          
c   -- var.elim.:  244/244          
c   -- subsuming                       
c   -- var.elim.:  452/452          
c   -- var.elim.:  108/108          
c   -- var.elim.:  9/9          
c |       263 |   16953    54182 |      --     263       --      -- |     --   | -711/-1222
c |       263 |   16953    54182 |    6781     263     7854    29.9 |  8.243 % |
c |       363 |   16953    54182 |    7459     363    19729    54.3 |  8.203 % |
c |       516 |   16953    54182 |    8205     516    28368    55.0 |  8.203 % |
c ==============================================================================
c (current CPU-time: 2.96655 s)
c ==============================================================================
c [1mFound solution: 50816[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       658 |   17040    54499 |    5111     658    35278    53.6 |  8.203 % |
c   -- subsuming                       
c   -- var.elim.:  230/230          
c   -- var.elim.:  170/170          
c |       658 |   16991    54687 |      --     658       --      -- |     --   | -49/189
c |       658 |   16991    54687 |    6796     658    35278    53.6 |  8.203 % |
c |       758 |   16991    54687 |    7476     758    39475    52.1 |  8.207 % |
c |       908 |   16991    54687 |    8223     908    46792    51.5 |  8.207 % |
c |      1134 |   16912    54097 |    9003    1131    57359    50.7 |  8.515 % |
c |      1476 |   16912    54097 |    9904    1473    81433    55.3 |  8.515 % |
c |      1982 |   16912    54097 |   10894    1979   121077    61.2 |  8.515 % |
c ==============================================================================
c (current CPU-time: 4.56731 s)
c ==============================================================================
c [1mFound solution: 50176[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      2195 |   16634    52727 |    4990    2170   131899    60.8 |  8.515 % |
c   -- subsuming                       
c   -- var.elim.:  753/753          
c   -- var.elim.:  209/209          
c   -- subsuming                       
c   -- var.elim.:  52/52          
c   -- var.elim.:  13/13          
c |      2195 |   16579    52795 |      --    2170       --      -- |     --   | -55/69
c |      2195 |   16579    52795 |    6631    1076    25523    23.7 |  8.515 % |
c |      2295 |   16579    52795 |    7294    1176    30588    26.0 |  9.944 % |
c |      2445 |   16579    52795 |    8024    1326    38420    29.0 |  9.944 % |
c |      2672 |   16579    52795 |    8826    1553    56589    36.4 |  9.943 % |
c |      3009 |   16579    52795 |    9709    1890    79898    42.3 |  9.943 % |
c ==============================================================================
c (current CPU-time: 5.58815 s)
c ==============================================================================
c [1mFound solution: 48640[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      3055 |   16605    52919 |    4981    1936    85263    44.0 |  9.943 % |
c   -- subsuming                       
c   -- var.elim.:  157/157          
c   -- var.elim.:  78/78          
c |      3055 |   16590    53056 |      --    1936       --      -- |     --   | -15/138
c |      3055 |   16590    53056 |    6636    1936    85263    44.0 |  9.943 % |
c |      3156 |   16590    53056 |    7299    2037    89276    43.8 |  9.963 % |
c |      3306 |   16590    53056 |    8029    2187    99568    45.5 |  9.962 % |
c |      3531 |   16590    53056 |    8832    2412   109566    45.4 |  9.962 % |
c |      3869 |   16590    53056 |    9715    2750   131593    47.9 |  9.962 % |
c |      4375 |   16513    52775 |   10637    3251   167538    51.5 | 10.224 % |
c ==============================================================================
c (current CPU-time: 7.51886 s)
c ==============================================================================
c [1mFound solution: 48384[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      4678 |   16540    52900 |    4961    3554   190461    53.6 | 10.224 % |
c   -- subsuming                       
c   -- var.elim.:  218/218          
c   -- var.elim.:  117/117          
c |      4678 |   16505    52928 |      --    3554       --      -- |     --   | -35/29
c |      4678 |   16505    52928 |    6602    2649    90592    34.2 | 10.224 % |
c |      4779 |   16505    52928 |    7262    2750    96025    34.9 | 10.263 % |
c |      4929 |   16505    52928 |    7988    2900   107122    36.9 | 10.263 % |
c |      5154 |   16505    52928 |    8787    3125   132547    42.4 | 10.263 % |
c ==============================================================================
c (current CPU-time: 8.25375 s)
c ==============================================================================
c [1mFound solution: 47488[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      5185 |   16537    53078 |    4961    3156   133919    42.4 | 10.263 % |
c   -- subsuming                       
c   -- var.elim.:  124/124          
c   -- var.elim.:  95/95          
c |      5185 |   16514    53123 |      --    3156       --      -- |     --   | -23/46
c |      5185 |   16514    53123 |    6605    3156   133919    42.4 | 10.263 % |
c |      5286 |   16514    53123 |    7266    3257   135396    41.6 | 10.281 % |
c |      5438 |   16514    53123 |    7992    3409   142619    41.8 | 10.282 % |
c |      5663 |   16514    53123 |    8792    3634   157369    43.3 | 10.281 % |
c |      6000 |   16505    53095 |    9665    3970   180966    45.6 | 10.305 % |
c |      6506 |   16505    53095 |   10632    4476   213674    47.7 | 10.305 % |
c |      7265 |   16505    53095 |   11695    5235   269918    51.6 | 10.305 % |
c ==============================================================================
c (current CPU-time: 10.8553 s)
c ==============================================================================
c [1mFound solution: 47480[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      7498 |   16573    53393 |    4971    5466   289545    53.0 | 10.305 % |
c   -- subsuming                       
c   -- var.elim.:  272/272          
c   -- var.elim.:  223/223          
c   -- var.elim.:  14/14          
c |      7498 |   16499    53464 |      --    5466       --      -- |     --   | -74/72
c |      7498 |   16499    53464 |    6599    4251   204916    48.2 | 10.305 % |
c |      7599 |   16499    53464 |    7259    4352   214240    49.2 | 10.403 % |
c |      7749 |   16499    53464 |    7985    4502   228185    50.7 | 10.403 % |
c |      7974 |   16499    53464 |    8784    4727   242593    51.3 | 10.403 % |
c |      8315 |   16499    53464 |    9662    5068   268942    53.1 | 10.403 % |
c |      8821 |   16499    53464 |   10628    5574   308089    55.3 | 10.404 % |
c |      9580 |   16437    53070 |   11647    6330   379501    60.0 | 10.642 % |
c |     10725 |   16293    51786 |   12700    7463   449759    60.3 | 11.310 % |
c |     12436 |   16293    51786 |   13970    9174   574362    62.6 | 11.310 % |
c |     15000 |   16285    51763 |   15359   11685   744918    63.7 | 11.334 % |
c ==============================================================================
c (current CPU-time: 24.1083 s)
c ==============================================================================
c [1mFound solution: 46576[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     16769 |   16530    52558 |    4958   13454   857262    63.7 | 11.334 % |
c   -- subsuming                       
c   -- var.elim.:  927/927          
c   -- var.elim.:  460/460          
c   -- var.elim.:  215/215          
c   -- var.elim.:  195/195          
c   -- var.elim.:  54/54          
c   -- subsuming                       
c   -- var.elim.:  262/262          
c   -- var.elim.:  168/168          
c |     16769 |   16243    52674 |      --   13454       --      -- |     --   | -286/119
c |     16769 |   16243    52674 |    6497    7667   292382    38.1 | 11.334 % |
c |     16871 |   16243    52674 |    7146    5214   181855    34.9 | 11.533 % |
c |     17021 |   16243    52674 |    7861    5364   193911    36.2 | 11.533 % |
c |     17248 |   16243    52674 |    8647    5591   206684    37.0 | 11.533 % |
c |     17585 |   16243    52674 |    9512    5928   234767    39.6 | 11.533 % |
c ==============================================================================
c (current CPU-time: 26.077 s)
c ==============================================================================
c [1mFound solution: 46080[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 2 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     17867 |   16268    52789 |    4880    6210   257127    41.4 | 11.533 % |
c   -- subsuming                       
c   -- var.elim.:  235/235          
c   -- var.elim.:  72/72          
c |     17867 |   16254    52756 |      --    6210       --      -- |     --   | -14/-32
c |     17867 |   16254    52756 |    6501    6210   257127    41.4 | 11.533 % |
c ==============================================================================
c (current CPU-time: 26.377 s)
c ==============================================================================
c [1mFound solution: 44800[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 2 2 2 2 2 2 2 2
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     17915 |   16276    52866 |    4882    6258   260891    41.7 | 11.533 % |
c   -- subsuming                       
c   -- var.elim.:  86/86          
c   -- var.elim.:  70/70          
c |     17915 |   16261    52898 |      --    6258       --      -- |     --   | -15/33
c |     17915 |   16261    52898 |    6504    6258   260891    41.7 | 11.533 % |
c |     18015 |   16261    52898 |    7154    6358   266026    41.8 | 11.570 % |
c |     18165 |   16261    52898 |    7870    6508   275480    42.3 | 11.570 % |
c |     18390 |   16261    52898 |    8657    6733   287025    42.6 | 11.570 % |
c |     18728 |   16261    52898 |    9523    7071   302645    42.8 | 11.570 % |
c |     19234 |   16261    52898 |   10475    7577   327757    43.3 | 11.570 % |
c ==============================================================================
c [1mOptimal solution: 44800[0m
s OPTIMUM FOUND
v -X0_bit_7 -X0_bit_6 -X0_bit_5 -X0_bit_4 -X0_bit_3 -X0_bit_2 -X0_bit_1 -X0_bit0 -X0_bit1 -X0_bit2 -X0_bit3 -X0_bit4 -X0_bit5 -X0_bit6 -X0_bit7 -X0_bit8 -X0_bit9 -X0_bit10 -X0_bit11 -X0_bit12 -X1_bit_7 -X1_bit_6 -X1_bit_5 -X1_bit_4 -X1_bit_3 -X1_bit_2 -X1_bit_1 -X1_bit0 -X1_bit1 -X1_bit2 -X1_bit3 -X1_bit4 -X1_bit5 -X1_bit6 -X1_bit7 -X1_bit8 -X1_bit9 -X1_bit10 -X1_bit11 -X1_bit12 -X2_bit_7 -X2_bit_6 -X2_bit_5 -X2_bit_4 -X2_bit_3 -X2_bit_2 -X2_bit_1 -X2_bit0 X2_bit1 -X2_bit2 X2_bit3 -X2_bit4 -X2_bit5 -X2_bit6 -X2_bit7 -X2_bit8 -X2_bit9 -X2_bit10 -X2_bit11 -X2_bit12 -X3_bit_7 -X3_bit_6 -X3_bit_5 -X3_bit_4 -X3_bit_3 -X3_bit_2 -X3_bit_1 -X3_bit0 -X3_bit1 -X3_bit2 -X3_bit3 -X3_bit4 -X3_bit5 -X3_bit6 -X3_bit7 -X3_bit8 -X3_bit9 -X3_bit10 -X3_bit11 -X3_bit12 -X4_bit_7 -X4_bit_6 -X4_bit_5 -X4_bit_4 -X4_bit_3 -X4_bit_2 -X4_bit_1 -X4_bit0 X4_bit1 X4_bit2 X4_bit3 X4_bit4 -X4_bit5 -X4_bit6 -X4_bit7 -X4_bit8 -X4_bit9 -X4_bit10 -X4_bit11 -X4_bit12 -X5_bit_7 -X5_bit_6 -X5_bit_5 -X5_bit_4 -X5_bit_3 -X5_bit_2 -X5_bit_1 -X5_bit0 -X5_bit1 -X5_bit2 -X5_bit3 -X5_bit4 -X5_bit5 -X5_bit6 -X5_bit7 -X5_bit8 -X5_bit9 -X5_bit10 -X5_bit11 -X5_bit12 -X6_bit_7 -X6_bit_6 -X6_bit_5 -X6_bit_4 -X6_bit_3 -X6_bit_2 -X6_bit_1 -X6_bit0 -X6_bit1 X6_bit2 -X6_bit3 X6_bit4 -X6_bit5 -X6_bit6 -X6_bit7 -X6_bit8 -X6_bit9 -X6_bit10 -X6_bit11 -X6_bit12 -X7_bit_7 -X7_bit_6 -X7_bit_5 -X7_bit_4 -X7_bit_3 -X7_bit_2 -X7_bit_1 -X7_bit0 -X7_bit1 X7_bit2 -X7_bit3 X7_bit4 -X7_bit5 -X7_bit6 -X7_bit7 -X7_bit8 -X7_bit9 -X7_bit10 -X7_bit11 -X7_bit12 -X8_bit_7 -X8_bit_6 -X8_bit_5 -X8_bit_4 -X8_bit_3 -X8_bit_2 -X8_bit_1 -X8_bit0 -X8_bit1 -X8_bit2 -X8_bit3 -X8_bit4 -X8_bit5 -X8_bit6 -X8_bit7 -X8_bit8 -X8_bit9 -X8_bit10 -X8_bit11 -X8_bit12 -X9_bit_7 -X9_bit_6 -X9_bit_5 -X9_bit_4 -X9_bit_3 -X9_bit_2 -X9_bit_1 -X9_bit0 -X9_bit1 -X9_bit2 -X9_bit3 -X9_bit4 -X9_bit5 -X9_bit6 -X9_bit7 -X9_bit8 -X9_bit9 -X9_bit10 -X9_bit11 -X9_bit12 -X10_bit_7 -X10_bit_6 -X10_bit_5 -X10_bit_4 -X10_bit_3 -X10_bit_2 -X10_bit_1 -X10_bit0 -X10_bit1 -X10_bit2 -X10_bit3 -X10_bit4 -X10_bit5 -X10_bit6 -X10_bit7 -X10_bit8 -X10_bit9 -X10_bit10 -X10_bit11 -X10_bit12 -X11_bit_7 -X11_bit_6 -X11_bit_5 -X11_bit_4 -X11_bit_3 -X11_bit_2 -X11_bit_1 -X11_bit0 -X11_bit1 X11_bit2 -X11_bit3 X11_bit4 -X11_bit5 -X11_bit6 -X11_bit7 -X11_bit8 -X11_bit9 -X11_bit10 -X11_bit11 -X11_bit12 -Y0_bit0 -Y1_bit0 Y2_bit0 -Y3_bit0 Y4_bit0 -Y5_bit0 Y6_bit0 Y7_bit0 -Y8_bit0 -Y9_bit0 -Y10_bit0 Y11_bit0
c _______________________________________________________________________________
c 
c restarts              : 56
c conflicts             : 19571          (684 /sec)
c decisions             : 31307          (1093 /sec)
c propagations          : 6780432        (236816 /sec)
c inspects              : 40674754       (1420622 /sec)
c CPU time              : 28.6316 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.94 0.93 2/54 7793
Raw data (stat): 7793 (runsolver) R 7792 29151 29150 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 486829264 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.0006 s]
Raw data (loadavg): 0.87 0.94 0.93 2/54 7793
Raw data (stat): 7793 (minisat+) R 7792 29151 29150 0 -1 0 3259 0 0 0 986 12 0 0 25 0 1 0 486829264 9154560 1696 4294967295 134512640 134672761 3221224544 3221223744 134610675 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2235 1696 603 41 0 2194 0
vsize: 8940
[startup+20.0016 s]
Raw data (loadavg): 0.89 0.94 0.93 2/54 7793
Raw data (stat): 7793 (minisat+) R 7792 29151 29150 0 -1 0 3888 0 0 0 1985 13 0 0 25 0 1 0 486829264 11329536 2225 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2766 2225 603 41 0 2725 0
vsize: 11064
[startup+28.8448 s]
Raw data (loadavg): 0.91 0.94 0.93 1/53 7793
Raw data (stat): 7793 (minisat+) R 7792 29151 29150 0 -1 0 3888 0 0 0 1985 13 0 0 25 0 1 0 486829264 11329536 2225 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2766 2225 603 41 0 2725 0
vsize: 0

Child status: 30
Real time (s): 28.8445
CPU time (s): 28.8256
CPU user time (s): 28.6356
CPU system time (s): 0.189971
CPU usage (%): 99.9346
Max. virtual memory (Kb): 11064
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	44800
#### END VERIFIER DATA ####