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/manquinho/primes-dimacs-cnf/normalized-ii32c3.opb
MD5SUM	00d830716ad6728e4af33fe898d69922
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	261
Optimality of the best value was proved	NO
Number of terms in the objective function	558
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	558
Number of bits of the sum of numbers in the objective function	10
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	558
Number of bits of the biggest sum of numbers	10
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.03284
Number of variables	558
Total number of constraints	3551
Number of constraints which are clauses	3551
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	2
Maximum length of a constraint	32
Trace number 5456

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc6 THE 2005-04-14 00:08:56 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3913 boxname=wulflinc6 idbench=153 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  00d830716ad6728e4af33fe898d69922  /oldhome/oroussel/tmp/wulflinc6/normalized-ii32c3.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc6/normalized-ii32c3.opb /oldhome/oroussel/tmp/wulflinc6/normalized-ii32c3.opb
IDLAUNCH: 3913
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.042
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.042
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:        909428 kB
Buffers:         35132 kB
Cached:          68372 kB
SwapCached:       2644 kB
Active:          52096 kB
Inactive:        56900 kB
HighTotal:      131008 kB
HighFree:        58772 kB
LowTotal:       903652 kB
LowFree:        850656 kB
SwapTotal:     2097136 kB
SwapFree:      2094492 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            10792 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 00:21:45 (client local time) WITH STATUS 30 IN 769.374 SECONDS
stats: 3913 0 769.374 30
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 3551 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ...............................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |    3551    18021 |    1065       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  558/558          
c |         0 |    3551    18021 |    1420       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 0.218966 s)
c ==============================================================================
c [1mFound solution: 272[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:25022     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |        10 |   32824    86535 |    9847      10      427    42.7 |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/19639          
c   -- var.elim.:  2000/19639          
c   -- var.elim.:  3000/19639          
c   -- var.elim.:  4000/19639          
c   -- var.elim.:  5000/19639          
c   -- var.elim.:  6000/19639          
c   -- var.elim.:  7000/19639          
c   -- var.elim.:  8000/19639          
c   -- var.elim.:  9000/19639          
c   -- var.elim.:  10000/19639          
c   -- var.elim.:  11000/19639          
c   -- var.elim.:  12000/19639          
c   -- var.elim.:  13000/19639          
c   -- var.elim.:  14000/19639          
c   -- var.elim.:  15000/19639          
c   -- var.elim.:  16000/19639          
c   -- var.elim.:  17000/19639          
c   -- var.elim.:  18000/19639          
c   -- var.elim.:  19000/19639          
c   -- var.elim.:  19639/19639          
c   -- var.elim.:  1000/9726          
c   -- var.elim.:  2000/9726          
c   -- var.elim.:  3000/9726          
c   -- var.elim.:  4000/9726          
c   -- var.elim.:  5000/9726          
c   -- var.elim.:  6000/9726          
c   -- var.elim.:  7000/9726          
c   -- var.elim.:  8000/9726          
c   -- var.elim.:  9000/9726          
c   -- var.elim.:  9726/9726          
c   -- var.elim.:  1000/5880          
c   -- var.elim.:  2000/5880          
c   -- var.elim.:  3000/5880          
c   -- var.elim.:  4000/5880          
c   -- var.elim.:  5000/5880          
c   -- var.elim.:  5880/5880          
c   -- var.elim.:  1000/4064          
c   -- var.elim.:  2000/4064          
c   -- var.elim.:  3000/4064          
c   -- var.elim.:  4000/4064          
c   -- var.elim.:  4064/4064          
c   -- var.elim.:  1000/3473          
c   -- var.elim.:  2000/3473          
c   -- var.elim.:  3000/3473          
c   -- var.elim.:  3473/3473          
c   -- var.elim.:  1000/2886          
c   -- var.elim.:  2000/2886          
c   -- var.elim.:  2886/2886          
c   -- var.elim.:  1000/2266          
c   -- var.elim.:  2000/2266          
c   -- var.elim.:  2266/2266          
c   -- var.elim.:  1000/1833          
c   -- var.elim.:  1833/1833          
c   -- var.elim.:  157/157          
c   -- subsuming                       
c   -- var.elim.:  1000/2923          
c   -- var.elim.:  2000/2923          
c   -- var.elim.:  2923/2923          
c   -- var.elim.:  27/27          
c |        10 |   11588    80009 |      --      10       --      -- |     --   | -21227/-6499
c |        10 |   11588    80009 |    4635      10      427    42.7 |  0.000 % |
c ==============================================================================
c (current CPU-time: 34.7317 s)
c ==============================================================================
c [1mFound solution: 265[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |        17 |   32696   131850 |    9808      17      726    42.7 |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/19172          
c   -- var.elim.:  2000/19172          
c   -- var.elim.:  3000/19172          
c   -- var.elim.:  4000/19172          
c   -- var.elim.:  5000/19172          
c   -- var.elim.:  6000/19172          
c   -- var.elim.:  7000/19172          
c   -- var.elim.:  8000/19172          
c   -- var.elim.:  9000/19172          
c   -- var.elim.:  10000/19172          
c   -- var.elim.:  11000/19172          
c   -- var.elim.:  12000/19172          
c   -- var.elim.:  13000/19172          
c   -- var.elim.:  14000/19172          
c   -- var.elim.:  15000/19172          
c   -- var.elim.:  16000/19172          
c   -- var.elim.:  17000/19172          
c   -- var.elim.:  18000/19172          
c   -- var.elim.:  19000/19172          
c   -- var.elim.:  19172/19172          
c   -- var.elim.:  1000/9306          
c   -- var.elim.:  2000/9306          
c   -- var.elim.:  3000/9306          
c   -- var.elim.:  4000/9306          
c   -- var.elim.:  5000/9306          
c   -- var.elim.:  6000/9306          
c   -- var.elim.:  7000/9306          
c   -- var.elim.:  8000/9306          
c   -- var.elim.:  9000/9306          
c   -- var.elim.:  9306/9306          
c   -- var.elim.:  1000/5917          
c   -- var.elim.:  2000/5917          
c   -- var.elim.:  3000/5917          
c   -- var.elim.:  4000/5917          
c   -- var.elim.:  5000/5917          
c   -- var.elim.:  5917/5917          
c   -- var.elim.:  1000/4580          
c   -- var.elim.:  2000/4580          
c   -- var.elim.:  3000/4580          
c   -- var.elim.:  4000/4580          
c   -- var.elim.:  4580/4580          
c   -- var.elim.:  1000/3883          
c   -- var.elim.:  2000/3883          
c   -- var.elim.:  3000/3883          
c   -- var.elim.:  3883/3883          
c   -- var.elim.:  1000/3417          
c   -- var.elim.:  2000/3417          
c   -- var.elim.:  3000/3417          
c   -- var.elim.:  3417/3417          
c   -- var.elim.:  1000/3219          
c   -- var.elim.:  2000/3219          
c   -- var.elim.:  3000/3219          
c   -- var.elim.:  3219/3219          
c   -- var.elim.:  1000/2336          
c   -- var.elim.:  2000/2336          
c   -- var.elim.:  2336/2336          
c   -- var.elim.:  295/295          
c   -- subsuming                       
c   -- var.elim.:  1000/1988          
c   -- var.elim.:  1988/1988          
c   -- var.elim.:  19/19          
c |        17 |   11777    92897 |      --      17       --      -- |     --   | -20919/-38952
c |        17 |   11777    92897 |    4710      17      726    42.7 |  0.000 % |
c |       118 |   11777    92897 |    5181     118     6935    58.8 |  0.250 % |
c |       269 |   11777    92897 |    5700     269    16936    63.0 |  0.250 % |
c |       494 |   11777    92897 |    6270     494    57776   117.0 |  0.250 % |
c |       831 |   11777    92897 |    6897     831   140407   169.0 |  0.250 % |
c |      1337 |   11777    92897 |    7586    1337   449904   336.5 |  0.250 % |
c ==============================================================================
c (current CPU-time: 77.2813 s)
c ==============================================================================
c [1mFound solution: 263[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1953 |   32177   143067 |    9653    1953   576252   295.1 |  0.250 % |
c   -- subsuming                       
c   -- var.elim.:  1000/18680          
c   -- var.elim.:  2000/18680          
c   -- var.elim.:  3000/18680          
c   -- var.elim.:  4000/18680          
c   -- var.elim.:  5000/18680          
c   -- var.elim.:  6000/18680          
c   -- var.elim.:  7000/18680          
c   -- var.elim.:  8000/18680          
c   -- var.elim.:  9000/18680          
c   -- var.elim.:  10000/18680          
c   -- var.elim.:  11000/18680          
c   -- var.elim.:  12000/18680          
c   -- var.elim.:  13000/18680          
c   -- var.elim.:  14000/18680          
c   -- var.elim.:  15000/18680          
c   -- var.elim.:  16000/18680          
c   -- var.elim.:  17000/18680          
c   -- var.elim.:  18000/18680          
c   -- var.elim.:  18680/18680          
c   -- var.elim.:  1000/9058          
c   -- var.elim.:  2000/9058          
c   -- var.elim.:  3000/9058          
c   -- var.elim.:  4000/9058          
c   -- var.elim.:  5000/9058          
c   -- var.elim.:  6000/9058          
c   -- var.elim.:  7000/9058          
c   -- var.elim.:  8000/9058          
c   -- var.elim.:  9000/9058          
c   -- var.elim.:  9058/9058          
c   -- var.elim.:  1000/5738          
c   -- var.elim.:  2000/5738          
c   -- var.elim.:  3000/5738          
c   -- var.elim.:  4000/5738          
c   -- var.elim.:  5000/5738          
c   -- var.elim.:  5738/5738          
c   -- var.elim.:  1000/4713          
c   -- var.elim.:  2000/4713          
c   -- var.elim.:  3000/4713          
c   -- var.elim.:  4000/4713          
c   -- var.elim.:  4713/4713          
c   -- var.elim.:  1000/3583          
c   -- var.elim.:  2000/3583          
c   -- var.elim.:  3000/3583          
c   -- var.elim.:  3583/3583          
c   -- var.elim.:  1000/3231          
c   -- var.elim.:  2000/3231          
c   -- var.elim.:  3000/3231          
c   -- var.elim.:  3231/3231          
c   -- var.elim.:  1000/3289          
c   -- var.elim.:  2000/3289          
c   -- var.elim.:  3000/3289          
c   -- var.elim.:  3289/3289          
c   -- var.elim.:  1000/3137          
c   -- var.elim.:  2000/3137          
c   -- var.elim.:  3000/3137          
c   -- var.elim.:  3137/3137          
c   -- var.elim.:  1000/1756          
c   -- var.elim.:  1756/1756          
c   -- subsuming                       
c   -- var.elim.:  1000/2498          
c   -- var.elim.:  2000/2498          
c   -- var.elim.:  2498/2498          
c |      1953 |   11856   100164 |      --    1953       --      -- |     --   | -20321/-42902
c |      1953 |   11856   100164 |    4742    1953   576252   295.1 |  0.250 % |
c |      2054 |   11856   100164 |    5216    2054   589562   287.0 |  0.271 % |
c |      2208 |   11856   100164 |    5738    2208   633045   286.7 |  0.271 % |
c |      2437 |   11843   100058 |    6305    2436   773330   317.5 |  0.339 % |
c |      2774 |   11843   100058 |    6935    2773  1085258   391.4 |  0.339 % |
c |      3281 |   11843   100058 |    7629    3280  1501394   457.7 |  0.339 % |
c |      4041 |   11815    99903 |    8372    4039  2170990   537.5 |  0.610 % |
c |      5185 |   11815    99903 |    9209    5183  3390257   654.1 |  0.610 % |
c ==============================================================================
c (current CPU-time: 143.702 s)
c ==============================================================================
c [1mFound solution: 262[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      5384 |   29947   144528 |    8984    5382  3558524   661.2 |  0.610 % |
c   -- subsuming                       
c   -- var.elim.:  1000/16993          
c   -- var.elim.:  2000/16993          
c   -- var.elim.:  3000/16993          
c   -- var.elim.:  4000/16993          
c   -- var.elim.:  5000/16993          
c   -- var.elim.:  6000/16993          
c   -- var.elim.:  7000/16993          
c   -- var.elim.:  8000/16993          
c   -- var.elim.:  9000/16993          
c   -- var.elim.:  10000/16993          
c   -- var.elim.:  11000/16993          
c   -- var.elim.:  12000/16993          
c   -- var.elim.:  13000/16993          
c   -- var.elim.:  14000/16993          
c   -- var.elim.:  15000/16993          
c   -- var.elim.:  16000/16993          
c   -- var.elim.:  16993/16993          
c   -- var.elim.:  1000/8130          
c   -- var.elim.:  2000/8130          
c   -- var.elim.:  3000/8130          
c   -- var.elim.:  4000/8130          
c   -- var.elim.:  5000/8130          
c   -- var.elim.:  6000/8130          
c   -- var.elim.:  7000/8130          
c   -- var.elim.:  8000/8130          
c   -- var.elim.:  8130/8130          
c   -- var.elim.:  1000/5413          
c   -- var.elim.:  2000/5413          
c   -- var.elim.:  3000/5413          
c   -- var.elim.:  4000/5413          
c   -- var.elim.:  5000/5413          
c   -- var.elim.:  5413/5413          
c   -- var.elim.:  1000/3557          
c   -- var.elim.:  2000/3557          
c   -- var.elim.:  3000/3557          
c   -- var.elim.:  3557/3557          
c   -- var.elim.:  1000/2764          
c   -- var.elim.:  2000/2764          
c   -- var.elim.:  2764/2764          
c   -- var.elim.:  1000/2302          
c   -- var.elim.:  2000/2302          
c   -- var.elim.:  2302/2302          
c   -- var.elim.:  927/927          
c   -- var.elim.:  393/393          
c   -- subsuming                       
c   -- var.elim.:  303/303          
c |      5384 |   11786    96013 |      --    5382       --      -- |     --   | -18140/-46909
c |      5384 |   11786    96013 |    4714    2578   269163   104.4 |  0.610 % |
c |      5486 |   11786    96013 |    5185    2680   348570   130.1 |  0.852 % |
c |      5636 |   11786    96013 |    5704    2830   480861   169.9 |  0.852 % |
c |      5863 |   11786    96013 |    6274    3057   652968   213.6 |  0.852 % |
c |      6201 |   11786    96013 |    6902    3395   913374   269.0 |  0.852 % |
c |      6708 |   11684    95173 |    7526    3898  1232742   316.2 |  1.815 % |
c |      7467 |   11660    94989 |    8262    4655  1726245   370.8 |  2.039 % |
c ==============================================================================
c (current CPU-time: 186.091 s)
c ==============================================================================
c [1mFound solution: 261[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      8020 |   31549   143789 |    9464    5208  2106403   404.5 |  2.039 % |
c   -- subsuming                       
c   -- var.elim.:  1000/18386          
c   -- var.elim.:  2000/18386          
c   -- var.elim.:  3000/18386          
c   -- var.elim.:  4000/18386          
c   -- var.elim.:  5000/18386          
c   -- var.elim.:  6000/18386          
c   -- var.elim.:  7000/18386          
c   -- var.elim.:  8000/18386          
c   -- var.elim.:  9000/18386          
c   -- var.elim.:  10000/18386          
c   -- var.elim.:  11000/18386          
c   -- var.elim.:  12000/18386          
c   -- var.elim.:  13000/18386          
c   -- var.elim.:  14000/18386          
c   -- var.elim.:  15000/18386          
c   -- var.elim.:  16000/18386          
c   -- var.elim.:  17000/18386          
c   -- var.elim.:  18000/18386          
c   -- var.elim.:  18386/18386          
c   -- var.elim.:  1000/8817          
c   -- var.elim.:  2000/8817          
c   -- var.elim.:  3000/8817          
c   -- var.elim.:  4000/8817          
c   -- var.elim.:  5000/8817          
c   -- var.elim.:  6000/8817          
c   -- var.elim.:  7000/8817          
c   -- var.elim.:  8000/8817          
c   -- var.elim.:  8817/8817          
c   -- var.elim.:  1000/5366          
c   -- var.elim.:  2000/5366          
c   -- var.elim.:  3000/5366          
c   -- var.elim.:  4000/5366          
c   -- var.elim.:  5000/5366          
c   -- var.elim.:  5366/5366          
c   -- var.elim.:  1000/4053          
c   -- var.elim.:  2000/4053          
c   -- var.elim.:  3000/4053          
c   -- var.elim.:  4000/4053          
c   -- var.elim.:  4053/4053          
c   -- var.elim.:  1000/3154          
c   -- var.elim.:  2000/3154          
c   -- var.elim.:  3000/3154          
c   -- var.elim.:  3154/3154          
c   -- var.elim.:  1000/2503          
c   -- var.elim.:  2000/2503          
c   -- var.elim.:  2503/2503          
c   -- var.elim.:  1000/1634          
c   -- var.elim.:  1634/1634          
c   -- var.elim.:  1000/1212          
c   -- var.elim.:  1212/1212          
c   -- var.elim.:  396/396          
c   -- subsuming                       
c   -- var.elim.:  886/886          
c |      8020 |   11708   100885 |      --    5208       --      -- |     --   | -19838/-42897
c |      8020 |   11708   100885 |    4683    3293   300622    91.3 |  2.039 % |
c |      8124 |   11708   100885 |    5151    3397   380127   111.9 |  2.596 % |
c |      8274 |   11693   100763 |    5659    3546   503380   142.0 |  2.730 % |
c |      8502 |   11693   100763 |    6225    3774   697563   184.8 |  2.730 % |
c |      8839 |   11693   100763 |    6847    4111   863653   210.1 |  2.730 % |
c |      9347 |   11671   100585 |    7518    4618  1075431   232.9 |  2.909 % |
c |     10107 |   11671   100585 |    8270    5378  1339586   249.1 |  2.909 % |
c |     11247 |   11642   100370 |    9074    6517  1954924   300.0 |  3.177 % |
c |     12955 |   11618   100171 |    9961    8224  3208914   390.2 |  3.401 % |
c |     15518 |   11507    99354 |   10853    7351  3876859   527.4 |  4.475 % |
c |     19363 |   11392    98453 |   11819   11192  7457121   666.3 |  5.616 % |
c |     25130 |   11392    98453 |   13001   12688  8947999   705.2 |  5.616 % |
c |     33780 |   11305    97839 |   14191   12095  7117603   588.5 |  6.467 % |
c |     46757 |   11134    96566 |   15375   14836  7935485   534.9 |  8.145 % |
c |     66220 |   10847    94162 |   16476   12598  6383363   506.7 | 11.032 % |
c |     95412 |   10058    86851 |   16805   17830 10135834   568.5 | 19.042 % |
c ==============================================================================
c [1mOptimal solution: 261[0m
s OPTIMUM FOUND
v 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 x89 -x90 x91 -x92 x93 -x94 x95 -x96 x97 -x98 x99 -x100 x101 -x102 x103 -x104 x105 -x106 x107 -x108 x109 -x110 x111 -x112 x113 -x114 x115 -x116 x117 -x118 x119 -x120 x121 -x122 x123 -x124 -x125 x126 x127 -x128 -x129 -x130 x131 -x132 -x133 x134 x135 -x136 x137 -x138 x139 -x140 x141 -x142 -x143 x144 x145 -x146 x147 -x148 -x149 -x150 x151 -x152 -x153 -x154 x155 -x156 x157 -x158 x159 -x160 x161 -x162 x163 -x164 x165 -x166 x167 -x168 x169 -x170 x171 -x172 x173 -x174 x175 -x176 x177 -x178 x179 -x180 x181 -x182 x183 -x184 x185 -x186 -x187 -x188 x189 -x190 -x191 x192 x193 -x194 -x195 -x196 x197 -x198 -x199 -x200 -x201 -x202 x203 -x204 -x205 -x206 x207 -x208 x209 -x210 -x211 -x212 x213 -x214 -x215 -x216 x217 -x218 -x219 -x220 -x221 -x222 x223 -x224 x225 -x226 -x227 -x228 -x229 -x230 x231 -x232 x233 -x234 x235 -x236 -x237 -x238 x239 -x240 x241 -x242 x243 -x244 x245 -x246 x247 -x248 x249 -x250 x251 -x252 -x253 x254 x255 -x256 x257 -x258 x259 -x260 -x261 x262 x263 -x264 -x265 x266 x267 -x268 x269 -x270 x271 -x272 x273 -x274 x275 -x276 x277 -x278 x279 -x280 x281 -x282 x283 -x284 x285 -x286 x287 -x288 x289 -x290 x291 -x292 x293 -x294 x295 -x296 x297 -x298 x299 -x300 x301 -x302 x303 -x304 x305 -x306 x307 -x308 x309 -x310 x311 -x312 -x313 x314 x315 -x316 x317 -x318 x319 -x320 x321 -x322 x323 -x324 -x325 x326 x327 -x328 -x329 x330 x331 -x332 -x333 -x334 x335 -x336 x337 -x338 x339 -x340 x341 -x342 x343 -x344 x345 -x346 x347 -x348 x349 -x350 -x351 -x352 x353 -x354 x355 -x356 x357 -x358 x359 -x360 x361 -x362 x363 -x364 x365 -x366 x367 -x368 x369 -x370 x371 -x372 x373 -x374 -x375 -x376 -x377 x378 x379 -x380 x381 -x382 x383 -x384 x385 -x386 -x387 x388 -x389 x390 x391 -x392 -x393 x394 -x395 x396 x397 -x398 -x399 x400 -x401 x402 x403 -x404 -x405 x406 -x407 x408 x409 -x410 -x411 x412 -x413 x414 x415 -x416 -x417 x418 -x419 x420 -x421 x422 -x423 x424 x425 -x426 -x427 x428 -x429 x430 x431 -x432 x433 -x434 -x435 x436 -x437 x438 x439 -x440 -x441 x442 -x443 x444 x445 -x446 -x447 x448 -x449 x450 x451 -x452 -x453 x454 -x455 x456 -x457 x458 -x459 x460 x461 -x462 x463 -x464 -x465 x466 -x467 x468 x469 -x470 -x471 x472 -x473 x474 x475 -x476 -x477 x478 -x479 x480 -x481 x482 x483 -x484 -x485 x486 x487 -x488 -x489 x490 -x491 x492 x493 -x494 -x495 x496 -x497 x498 x499 -x500 -x501 x502 -x503 x504 x505 -x506 -x507 x508 -x509 x510 x511 -x512 -x513 x514 -x515 x516 -x517 x518 x519 -x520 -x521 x522 x523 -x524 -x525 x526 -x527 x528 -x529 x530 -x531 x532 x533 -x534 x535 -x536 -x537 x538 -x539 x540 x541 -x542 -x543 x544 -x545 x546 -x547 x548 -x549 x550 x551 -x552 x553 -x554 -x555 x556 -x557 x558
c _______________________________________________________________________________
c 
c restarts              : 39
c conflicts             : 138549         (180 /sec)
c decisions             : 443608         (578 /sec)
c propagations          : 30802742       (40107 /sec)
c inspects              : 340639218      (443536 /sec)
c CPU time              : 768.007 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.93 0.97 0.91 2/54 792
Raw data (stat): 792 (runsolver) R 791 29653 29652 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 421933362 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0004 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 792
Raw data (stat): 792 (minisat+) R 791 29653 29652 0 -1 0 3230 0 0 0 986 12 0 0 25 0 1 0 421933362 15900672 3127 4294967295 134512640 134672761 3221224576 3221223024 134643548 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3882 3127 603 41 0 3841 0
vsize: 15528
[startup+20.0002 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 792
Raw data (stat): 792 (minisat+) R 791 29653 29652 0 -1 0 3300 0 0 0 1980 18 0 0 25 0 1 0 421933362 16302080 3197 4294967295 134512640 134672761 3221224576 3221222796 1075349796 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3980 3197 603 41 0 3939 0
vsize: 15920
[startup+30.0007 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 792
Raw data (stat): 792 (minisat+) R 791 29653 29652 0 -1 0 3300 0 0 0 2981 18 0 0 25 0 1 0 421933362 16302080 3197 4294967295 134512640 134672761 3221224576 3221223040 134644235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3980 3197 603 41 0 3939 0
vsize: 15920
[startup+40.0009 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 792
Raw data (stat): 792 (minisat+) R 791 29653 29652 0 -1 0 4564 0 0 0 3974 25 0 0 25 0 1 0 421933362 20996096 4086 4294967295 134512640 134672761 3221224576 3221223024 134644038 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5126 4086 603 41 0 5085 0
vsize: 20504
[startup+50.0007 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 792
Raw data (stat): 792 (minisat+) R 791 29653 29652 0 -1 0 4572 0 0 0 4971 28 0 0 25 0 1 0 421933362 21118976 4094 4294967295 134512640 134672761 3221224576 3221223024 134643474 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5156 4094 603 41 0 5115 0
vsize: 20624
[startup+60.0002 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 792
Raw data (stat): 792 (minisat+) R 791 29653 29652 0 -1 0 4572 0 0 0 5967 32 0 0 25 0 1 0 421933362 21118976 4094 4294967295 134512640 134672761 3221224576 3221223024 134643532 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5156 4094 603 41 0 5115 0
vsize: 20624
[startup+70.0003 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 792
Raw data (stat): 792 (minisat+) R 791 29653 29652 0 -1 0 4572 0 0 0 6968 32 0 0 25 0 1 0 421933362 20967424 4083 4294967295 134512640 134672761 3221224576 3221223120 134621041 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5119 4083 603 41 0 5078 0
vsize: 20476
[startup+80.0002 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 792
Raw data (stat): 792 (minisat+) R 791 29653 29652 0 -1 0 8272 0 0 0 7953 47 0 0 25 0 1 0 421933362 24883200 5294 4294967295 134512640 134672761 3221224576 3221223068 134642716 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6075 5294 603 41 0 6034 0
vsize: 24300
[startup+90.0031 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 792
Raw data (stat): 792 (minisat+) R 791 29653 29652 0 -1 0 8390 0 0 0 8949 50 0 0 25 0 1 0 421933362 25341952 5412 4294967295 134512640 134672761 3221224576 3221223024 134643959 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6187 5412 603 41 0 6146 0
vsize: 24748
[startup+100.003 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 792
Raw data (stat): 792 (minisat+) R 791 29653 29652 0 -1 0 8390 0 0 0 9946 54 0 0 25 0 1 0 421933362 25341952 5412 4294967295 134512640 134672761 3221224576 3221223024 134643577 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6187 5412 603 41 0 6146 0
vsize: 24748
[startup+110.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 792
Raw data (stat): 792 (minisat+) R 791 29653 29652 0 -1 0 8390 0 0 0 10944 56 0 0 25 0 1 0 421933362 25341952 5412 4294967295 134512640 134672761 3221224576 3221223024 134643996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6187 5412 603 41 0 6146 0
vsize: 24748
[startup+120.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 792
Raw data (stat): 792 (minisat+) R 791 29653 29652 0 -1 0 8390 0 0 0 11944 57 0 0 25 0 1 0 421933362 25341952 5412 4294967295 134512640 134672761 3221224576 3221223056 134541817 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6187 5412 603 41 0 6146 0
vsize: 24748
[startup+130.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 792
Raw data (stat): 792 (minisat+) R 791 29653 29652 0 -1 0 8423 0 0 0 12944 57 0 0 25 0 1 0 421933362 25341952 5413 4294967295 134512640 134672761 3221224576 3221223024 134643542 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6187 5413 603 41 0 6146 0
vsize: 24748
[startup+140.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 792
Raw data (stat): 792 (minisat+) R 791 29653 29652 0 -1 0 10292 0 0 0 13940 61 0 0 25 0 1 0 421933362 33013760 7282 4294967295 134512640 134672761 3221224576 3221223616 134603565 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8060 7282 603 41 0 8019 0
vsize: 32240
[startup+150.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 792
Raw data (stat): 792 (minisat+) R 791 29653 29652 0 -1 0 15135 0 0 0 14921 80 0 0 25 0 1 0 421933362 46870528 10876 4294967295 134512640 134672761 3221224576 3221223024 134644016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11443 10876 603 41 0 11402 0
vsize: 45772
[startup+160.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 792
Raw data (stat): 792 (minisat+) R 791 29653 29652 0 -1 0 15135 0 0 0 15920 81 0 0 25 0 1 0 421933362 46870528 10876 4294967295 134512640 134672761 3221224576 3221222784 1075730206 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11443 10876 603 41 0 11402 0
vsize: 45772
[startup+170.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 792
Raw data (stat): 792 (minisat+) R 791 29653 29652 0 -1 0 15135 0 0 0 16918 84 0 0 25 0 1 0 421933362 46870528 10876 4294967295 134512640 134672761 3221224576 3221223024 134643474 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11443 10876 603 41 0 11402 0
vsize: 45772
[startup+180.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 792
Raw data (stat): 792 (minisat+) R 791 29653 29652 0 -1 0 15136 0 0 0 17918 84 0 0 25 0 1 0 421933362 46870528 10877 4294967295 134512640 134672761 3221224576 3221223664 1074743872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11443 10877 603 41 0 11402 0
vsize: 45772
[startup+190.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 792
Raw data (stat): 792 (minisat+) R 791 29653 29652 0 -1 0 18937 0 0 0 18900 102 0 0 25 0 1 0 421933362 44630016 9387 4294967295 134512640 134672761 3221224576 3221223120 134621211 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10896 9387 603 41 0 10855 0
vsize: 43584
[startup+200.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 792
Raw data (stat): 792 (minisat+) R 791 29653 29652 0 -1 0 19002 0 0 0 19897 105 0 0 25 0 1 0 421933362 44625920 9386 4294967295 134512640 134672761 3221224576 3221223024 134643483 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10895 9386 603 41 0 10854 0
vsize: 43580
[startup+210.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 792
Raw data (stat): 792 (minisat+) R 791 29653 29652 0 -1 0 19002 0 0 0 20889 108 0 0 25 0 1 0 421933362 44625920 9386 4294967295 134512640 134672761 3221224576 3221223024 134643954 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10895 9386 603 41 0 10854 0
vsize: 43580
[startup+220.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 792
Raw data (stat): 792 (minisat+) R 791 29653 29652 0 -1 0 19002 0 0 0 21889 108 0 0 25 0 1 0 421933362 44625920 9386 4294967295 134512640 134672761 3221224576 3221223024 134643636 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10895 9386 603 41 0 10854 0
vsize: 43580
[startup+230.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 792
Raw data (stat): 792 (minisat+) R 791 29653 29652 0 -1 0 19002 0 0 0 22889 108 0 0 25 0 1 0 421933362 44625920 9386 4294967295 134512640 134672761 3221224576 3221223760 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10895 9386 603 41 0 10854 0
vsize: 43580
[startup+240.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 792
Raw data (stat): 792 (minisat+) R 791 29653 29652 0 -1 0 19003 0 0 0 23889 108 0 0 25 0 1 0 421933362 44625920 9387 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10895 9387 603 41 0 10854 0
vsize: 43580
[startup+250.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 792
Raw data (stat): 792 (minisat+) R 791 29653 29652 0 -1 0 20442 0 0 0 24886 112 0 0 25 0 1 0 421933362 50667520 10826 4294967295 134512640 134672761 3221224576 3221223672 134616317 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12370 10826 603 41 0 12329 0
vsize: 49480
[startup+260.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 792
Raw data (stat): 792 (minisat+) R 791 29653 29652 0 -1 0 21291 0 0 0 25885 113 0 0 25 0 1 0 421933362 54018048 11675 4294967295 134512640 134672761 3221224576 3221223616 134614205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13188 11675 603 41 0 13147 0
vsize: 52752
[startup+270.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 792
Raw data (stat): 792 (minisat+) R 791 29653 29652 0 -1 0 22792 0 0 0 26882 117 0 0 25 0 1 0 421933362 60170240 13176 4294967295 134512640 134672761 3221224576 3221223568 134565103 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14690 13176 603 41 0 14649 0
vsize: 58760
[startup+280.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 792
Raw data (stat): 792 (minisat+) R 791 29653 29652 0 -1 0 24580 0 0 0 27878 121 0 0 25 0 1 0 421933362 67588096 14964 4294967295 134512640 134672761 3221224576 3221223760 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16501 14964 603 41 0 16460 0
vsize: 66004
[startup+290.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 792
Raw data (stat): 792 (minisat+) R 791 29653 29652 0 -1 0 24730 0 0 0 28878 122 0 0 25 0 1 0 421933362 68116480 15114 4294967295 134512640 134672761 3221224576 3221223760 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16630 15114 603 41 0 16589 0
vsize: 66520
[startup+300.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 792
Raw data (stat): 792 (minisat+) R 791 29653 29652 0 -1 0 25016 0 0 0 29877 122 0 0 25 0 1 0 421933362 69283840 15400 4294967295 134512640 134672761 3221224576 3221223700 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16915 15400 603 41 0 16874 0
vsize: 67660
[startup+310.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 792
Raw data (stat): 792 (minisat+) R 791 29653 29652 0 -1 0 25673 0 0 0 30877 123 0 0 25 0 1 0 421933362 72028160 16057 4294967295 134512640 134672761 3221224576 3221223760 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17585 16057 603 41 0 17544 0
vsize: 70340
[startup+320.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 792
Raw data (stat): 792 (minisat+) R 791 29653 29652 0 -1 0 25673 0 0 0 31877 123 0 0 25 0 1 0 421933362 72028160 16057 4294967295 134512640 134672761 3221224576 3221223720 134616108 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17585 16057 603 41 0 17544 0
vsize: 70340
[startup+330.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 792
Raw data (stat): 792 (minisat+) R 791 29653 29652 0 -1 0 25673 0 0 0 32877 123 0 0 25 0 1 0 421933362 72028160 16057 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17585 16057 603 41 0 17544 0
vsize: 70340
[startup+340.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 792
Raw data (stat): 792 (minisat+) R 791 29653 29652 0 -1 0 25673 0 0 0 33878 123 0 0 25 0 1 0 421933362 72028160 16057 4294967295 134512640 134672761 3221224576 3221223760 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17585 16057 603 41 0 17544 0
vsize: 70340
[startup+350.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 792
Raw data (stat): 792 (minisat+) R 791 29653 29652 0 -1 0 25928 0 0 0 34877 124 0 0 25 0 1 0 421933362 73048064 16312 4294967295 134512640 134672761 3221224576 3221223568 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17834 16312 603 41 0 17793 0
vsize: 71336
[startup+360.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 792
Raw data (stat): 792 (minisat+) R 791 29653 29652 0 -1 0 25928 0 0 0 35878 124 0 0 25 0 1 0 421933362 73048064 16312 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17834 16312 603 41 0 17793 0
vsize: 71336
[startup+370.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 792
Raw data (stat): 792 (minisat+) R 791 29653 29652 0 -1 0 25928 0 0 0 36878 124 0 0 25 0 1 0 421933362 73048064 16312 4294967295 134512640 134672761 3221224576 3221223616 134612684 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17834 16312 603 41 0 17793 0
vsize: 71336
[startup+380.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 792
Raw data (stat): 792 (minisat+) R 791 29653 29652 0 -1 0 25928 0 0 0 37878 124 0 0 25 0 1 0 421933362 73048064 16312 4294967295 134512640 134672761 3221224576 3221223760 134615919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17834 16312 603 41 0 17793 0
vsize: 71336
[startup+390.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 792
Raw data (stat): 792 (minisat+) R 791 29653 29652 0 -1 0 25928 0 0 0 38879 124 0 0 25 0 1 0 421933362 73048064 16312 4294967295 134512640 134672761 3221224576 3221223700 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17834 16312 603 41 0 17793 0
vsize: 71336
[startup+400.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 792
Raw data (stat): 792 (minisat+) R 791 29653 29652 0 -1 0 25929 0 0 0 39879 124 0 0 25 0 1 0 421933362 72884224 16284 4294967295 134512640 134672761 3221224576 3221223760 134615919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17794 16284 603 41 0 17753 0
vsize: 71176
[startup+410.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 792
Raw data (stat): 792 (minisat+) R 791 29653 29652 0 -1 0 25929 0 0 0 40879 124 0 0 25 0 1 0 421933362 72884224 16284 4294967295 134512640 134672761 3221224576 3221223728 134616597 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17794 16284 603 41 0 17753 0
vsize: 71176
[startup+420.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 792
Raw data (stat): 792 (minisat+) R 791 29653 29652 0 -1 0 25929 0 0 0 41880 124 0 0 25 0 1 0 421933362 72884224 16284 4294967295 134512640 134672761 3221224576 3221223720 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17794 16284 603 41 0 17753 0
vsize: 71176
[startup+430.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 792
Raw data (stat): 792 (minisat+) R 791 29653 29652 0 -1 0 25930 0 0 0 42880 124 0 0 25 0 1 0 421933362 72884224 16285 4294967295 134512640 134672761 3221224576 3221223616 134612628 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17794 16285 603 41 0 17753 0
vsize: 71176
[startup+440.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 792
Raw data (stat): 792 (minisat+) R 791 29653 29652 0 -1 0 25930 0 0 0 43881 124 0 0 25 0 1 0 421933362 72884224 16285 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17794 16285 603 41 0 17753 0
vsize: 71176
[startup+450.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 792
Raw data (stat): 792 (minisat+) R 791 29653 29652 0 -1 0 25930 0 0 0 44881 124 0 0 25 0 1 0 421933362 72884224 16285 4294967295 134512640 134672761 3221224576 3221223672 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17794 16285 603 41 0 17753 0
vsize: 71176
[startup+460.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 792
Raw data (stat): 792 (minisat+) R 791 29653 29652 0 -1 0 25930 0 0 0 45881 124 0 0 25 0 1 0 421933362 72884224 16285 4294967295 134512640 134672761 3221224576 3221223616 134612783 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17794 16285 603 41 0 17753 0
vsize: 71176
[startup+470.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 792
Raw data (stat): 792 (minisat+) R 791 29653 29652 0 -1 0 25930 0 0 0 46882 124 0 0 25 0 1 0 421933362 72884224 16285 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17794 16285 603 41 0 17753 0
vsize: 71176
[startup+480.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 792
Raw data (stat): 792 (minisat+) R 791 29653 29652 0 -1 0 27306 0 0 0 47878 128 0 0 25 0 1 0 421933362 78573568 17661 4294967295 134512640 134672761 3221224576 3221223616 134612614 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19183 17661 603 41 0 19142 0
vsize: 76732
[startup+490.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 792
Raw data (stat): 792 (minisat+) R 791 29653 29652 0 -1 0 27306 0 0 0 48879 128 0 0 25 0 1 0 421933362 78573568 17661 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19183 17661 603 41 0 19142 0
vsize: 76732
[startup+500.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 792
Raw data (stat): 792 (minisat+) R 791 29653 29652 0 -1 0 27306 0 0 0 49879 128 0 0 25 0 1 0 421933362 78573568 17661 4294967295 134512640 134672761 3221224576 3221223760 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19183 17661 603 41 0 19142 0
vsize: 76732
[startup+510.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 792
Raw data (stat): 792 (minisat+) R 791 29653 29652 0 -1 0 27439 0 0 0 50879 128 0 0 25 0 1 0 421933362 79118336 17793 4294967295 134512640 134672761 3221224576 3221223760 134615579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19316 17793 603 41 0 19275 0
vsize: 77264
[startup+520.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 792
Raw data (stat): 792 (minisat+) R 791 29653 29652 0 -1 0 27439 0 0 0 51880 128 0 0 25 0 1 0 421933362 79118336 17793 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19316 17793 603 41 0 19275 0
vsize: 77264
[startup+530.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 792
Raw data (stat): 792 (minisat+) R 791 29653 29652 0 -1 0 27439 0 0 0 52880 128 0 0 25 0 1 0 421933362 79118336 17793 4294967295 134512640 134672761 3221224576 3221223720 134616347 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19316 17793 603 41 0 19275 0
vsize: 77264
[startup+540.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 792
Raw data (stat): 792 (minisat+) R 791 29653 29652 0 -1 0 27883 0 0 0 53880 129 0 0 25 0 1 0 421933362 80957440 18237 4294967295 134512640 134672761 3221224576 3221223616 134612783 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19765 18238 603 41 0 19724 0
vsize: 79060
[startup+550.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 792
Raw data (stat): 792 (minisat+) R 791 29653 29652 0 -1 0 28285 0 0 0 54879 129 0 0 25 0 1 0 421933362 82587648 18639 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20163 18639 603 41 0 20122 0
vsize: 80652
[startup+560.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 792
Raw data (stat): 792 (minisat+) R 791 29653 29652 0 -1 0 28285 0 0 0 55879 129 0 0 25 0 1 0 421933362 82587648 18639 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20163 18639 603 41 0 20122 0
vsize: 80652
[startup+570.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 792
Raw data (stat): 792 (minisat+) R 791 29653 29652 0 -1 0 28285 0 0 0 56880 129 0 0 25 0 1 0 421933362 82587648 18639 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20163 18639 603 41 0 20122 0
vsize: 80652
[startup+580.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 792
Raw data (stat): 792 (minisat+) R 791 29653 29652 0 -1 0 28285 0 0 0 57880 129 0 0 25 0 1 0 421933362 82587648 18639 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20163 18639 603 41 0 20122 0
vsize: 80652
[startup+590.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 792
Raw data (stat): 792 (minisat+) R 791 29653 29652 0 -1 0 28285 0 0 0 58880 129 0 0 25 0 1 0 421933362 82587648 18639 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20163 18639 603 41 0 20122 0
vsize: 80652
[startup+600.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 792
Raw data (stat): 792 (minisat+) R 791 29653 29652 0 -1 0 28285 0 0 0 59881 129 0 0 25 0 1 0 421933362 82587648 18639 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20163 18639 603 41 0 20122 0
vsize: 80652
[startup+610.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 792
Raw data (stat): 792 (minisat+) R 791 29653 29652 0 -1 0 28285 0 0 0 60881 129 0 0 25 0 1 0 421933362 82575360 18638 4294967295 134512640 134672761 3221224576 3221223616 134612684 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20160 18638 603 41 0 20119 0
vsize: 80640
[startup+620.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 792
Raw data (stat): 792 (minisat+) R 791 29653 29652 0 -1 0 28286 0 0 0 61881 129 0 0 25 0 1 0 421933362 82575360 18639 4294967295 134512640 134672761 3221224576 3221223760 134615788 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20160 18639 603 41 0 20119 0
vsize: 80640
[startup+630.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 792
Raw data (stat): 792 (minisat+) R 791 29653 29652 0 -1 0 28286 0 0 0 62882 129 0 0 25 0 1 0 421933362 82526208 18638 4294967295 134512640 134672761 3221224576 3221223672 134616350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20148 18638 603 41 0 20107 0
vsize: 80592
[startup+640.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 792
Raw data (stat): 792 (minisat+) R 791 29653 29652 0 -1 0 28286 0 0 0 63882 129 0 0 25 0 1 0 421933362 82526208 18638 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20148 18638 603 41 0 20107 0
vsize: 80592
[startup+650.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 792
Raw data (stat): 792 (minisat+) R 791 29653 29652 0 -1 0 28286 0 0 0 64882 129 0 0 25 0 1 0 421933362 82526208 18638 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20148 18638 603 41 0 20107 0
vsize: 80592
[startup+660.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 792
Raw data (stat): 792 (minisat+) R 791 29653 29652 0 -1 0 28286 0 0 0 65883 129 0 0 25 0 1 0 421933362 82526208 18638 4294967295 134512640 134672761 3221224576 3221223752 134615850 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20148 18638 603 41 0 20107 0
vsize: 80592
[startup+670.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 792
Raw data (stat): 792 (minisat+) R 791 29653 29652 0 -1 0 28286 0 0 0 66883 129 0 0 25 0 1 0 421933362 82526208 18638 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20148 18638 603 41 0 20107 0
vsize: 80592
[startup+680.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 792
Raw data (stat): 792 (minisat+) R 791 29653 29652 0 -1 0 28286 0 0 0 67883 129 0 0 25 0 1 0 421933362 82526208 18638 4294967295 134512640 134672761 3221224576 3221223760 134615807 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20148 18638 603 41 0 20107 0
vsize: 80592
[startup+690.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 792
Raw data (stat): 792 (minisat+) R 791 29653 29652 0 -1 0 28286 0 0 0 68884 129 0 0 25 0 1 0 421933362 82526208 18638 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20148 18638 603 41 0 20107 0
vsize: 80592
[startup+700.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 792
Raw data (stat): 792 (minisat+) R 791 29653 29652 0 -1 0 28286 0 0 0 69884 129 0 0 25 0 1 0 421933362 82522112 18637 4294967295 134512640 134672761 3221224576 3221223672 134616299 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20147 18637 603 41 0 20106 0
vsize: 80588
[startup+710.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 792
Raw data (stat): 792 (minisat+) R 791 29653 29652 0 -1 0 28286 0 0 0 70885 129 0 0 25 0 1 0 421933362 82522112 18637 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20147 18637 603 41 0 20106 0
vsize: 80588
[startup+720.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 792
Raw data (stat): 792 (minisat+) R 791 29653 29652 0 -1 0 28286 0 0 0 71885 129 0 0 25 0 1 0 421933362 82522112 18637 4294967295 134512640 134672761 3221224576 3221223616 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20147 18637 603 41 0 20106 0
vsize: 80588
[startup+730.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 792
Raw data (stat): 792 (minisat+) R 791 29653 29652 0 -1 0 28286 0 0 0 72885 130 0 0 25 0 1 0 421933362 82522112 18637 4294967295 134512640 134672761 3221224576 3221223760 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20147 18637 603 41 0 20106 0
vsize: 80588
[startup+740.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 792
Raw data (stat): 792 (minisat+) R 791 29653 29652 0 -1 0 28286 0 0 0 73885 130 0 0 25 0 1 0 421933362 82522112 18637 4294967295 134512640 134672761 3221224576 3221223616 134613769 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20147 18637 603 41 0 20106 0
vsize: 80588
[startup+750.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 792
Raw data (stat): 792 (minisat+) R 791 29653 29652 0 -1 0 28286 0 0 0 74886 130 0 0 25 0 1 0 421933362 82522112 18637 4294967295 134512640 134672761 3221224576 3221223760 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20147 18637 603 41 0 20106 0
vsize: 80588
[startup+760.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 792
Raw data (stat): 792 (minisat+) R 791 29653 29652 0 -1 0 28286 0 0 0 75886 130 0 0 25 0 1 0 421933362 82522112 18637 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20147 18637 603 41 0 20106 0
vsize: 80588
[startup+769.22 s]
Raw data (loadavg): 0.99 0.97 0.91 1/53 792
Raw data (stat): 792 (minisat+) R 791 29653 29652 0 -1 0 28286 0 0 0 75886 130 0 0 25 0 1 0 421933362 82522112 18637 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20147 18637 603 41 0 20106 0
vsize: 0

Child status: 30
Real time (s): 769.219
CPU time (s): 769.374
CPU user time (s): 768.015
CPU system time (s): 1.35879
CPU usage (%): 100.02
Max. virtual memory (Kb): 80652
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	261
#### END VERIFIER DATA ####