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/routing/normalized-s4-4-3-10pb.opb
MD5SUM	3da806c3498bf979a43344fcf1dd59e3
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	70
Optimality of the best value was proved	NO
Number of terms in the objective function	840
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	840
Number of bits of the sum of numbers in the objective function	10
Biggest number in a constraint	3
Number of bits of the biggest number in a constraint	2
Biggest sum of numbers in a constraint	840
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	840
Total number of constraints	2528
Number of constraints which are clauses	2504
Number of constraints which are cardinality constraints (but not clauses)	24
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	2
Maximum length of a constraint	35
Trace number 5506

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc2 THE 2005-04-14 00:31:13 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3996 boxname=wulflinc2 idbench=236 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  3da806c3498bf979a43344fcf1dd59e3  /oldhome/oroussel/tmp/wulflinc2/normalized-s4-4-3-10pb.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc2/normalized-s4-4-3-10pb.opb /oldhome/oroussel/tmp/wulflinc2/normalized-s4-4-3-10pb.opb
IDLAUNCH: 3996
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.191
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.191
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:        902768 kB
Buffers:         34392 kB
Cached:          76988 kB
SwapCached:          4 kB
Active:          56492 kB
Inactive:        57708 kB
HighTotal:      131008 kB
HighFree:        50260 kB
LowTotal:       903652 kB
LowFree:        852508 kB
SwapTotal:     2097136 kB
SwapFree:      2097132 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6916 kB
Slab:            12020 kB
Committed_AS:    71676 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 00:36:34 (client local time) WITH STATUS 30 IN 321.242 SECONDS
stats: 3996 0 321.242 30
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 2528 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ############################################################################################################################################
c   -- Clauses(.)/Splits(s): ................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[2510]---> BDD-cost:    1
c ---[2488]---> BDD-cost:    1
c ---[2462]---> BDD-cost:    1
c ---[2456]---> BDD-cost:    1
c ---[2420]---> BDD-cost:    1
c ---[2398]---> BDD-cost:    1
c ---[2392]---> BDD-cost:    1
c ---[2386]---> BDD-cost:    1
c ---[2368]---> BDD-cost:    1
c ---[2346]---> BDD-cost:    1
c ---[2320]---> BDD-cost:    1
c ---[2314]---> BDD-cost:    1
c ---[2300]---> BDD-cost:    1
c ---[2274]---> BDD-cost:    1
c ---[2252]---> BDD-cost:    1
c ---[2242]---> BDD-cost:    1
c ---[2205]---> BDD-cost:    1
c ---[2184]---> BDD-cost:    1
c ---[2178]---> BDD-cost:    1
c ---[2172]---> BDD-cost:    1
c ---[2162]---> BDD-cost:    1
c ---[2152]---> BDD-cost:    1
c ---[2102]---> BDD-cost:    1
c ---[2100]---> BDD-cost:    1
c ---[2067]---> BDD-cost:    1
c ---[2041]---> BDD-cost:    1
c ---[2039]---> BDD-cost:    1
c ---[2029]---> BDD-cost:    1
c ---[2019]---> BDD-cost:    1
c ---[2009]---> BDD-cost:    1
c ---[1959]---> BDD-cost:    1
c ---[1957]---> BDD-cost:    1
c ---[1951]---> BDD-cost:    1
c ---[1933]---> BDD-cost:    1
c ---[1895]---> BDD-cost:    1
c ---[1885]---> BDD-cost:    1
c ---[1883]---> BDD-cost:    1
c ---[1857]---> BDD-cost:    1
c ---[1839]---> BDD-cost:    1
c ---[1813]---> BDD-cost:    1
c ---[1764]---> BDD-cost:    1
c ---[1754]---> BDD-cost:    1
c ---[1744]---> BDD-cost:    1
c ---[1742]---> BDD-cost:    1
c ---[1728]---> BDD-cost:    1
c ---[1703]---> BDD-cost:    1
c ---[1681]---> BDD-cost:    1
c ---[1671]---> BDD-cost:    1
c ---[1665]---> BDD-cost:    1
c ---[1647]---> BDD-cost:    1
c ---[1609]---> BDD-cost:    1
c ---[1599]---> BDD-cost:    1
c ---[1585]---> BDD-cost:    1
c ---[1560]---> BDD-cost:    1
c ---[1538]---> BDD-cost:    1
c ---[1528]---> BDD-cost:    1
c ---[1526]---> BDD-cost:    1
c ---[1500]---> BDD-cost:    1
c ---[1482]---> BDD-cost:    1
c ---[1456]---> BDD-cost:    1
c ---[1407]---> BDD-cost:    1
c ---[1397]---> BDD-cost:    1
c ---[1387]---> BDD-cost:    1
c ---[1385]---> BDD-cost:    1
c ---[1367]---> BDD-cost:    1
c ---[1345]---> BDD-cost:    1
c ---[1319]---> BDD-cost:    1
c ---[1313]---> BDD-cost:    1
c ---[1280]---> BDD-cost:    1
c ---[1254]---> BDD-cost:    1
c ---[1252]---> BDD-cost:    1
c ---[1242]---> BDD-cost:    1
c ---[1189]---> BDD-cost:    1
c ---[1179]---> BDD-cost:    1
c ---[1173]---> BDD-cost:    1
c ---[1171]---> BDD-cost:    1
c ---[1157]---> BDD-cost:    1
c ---[1131]---> BDD-cost:    1
c ---[1109]---> BDD-cost:    1
c ---[1099]---> BDD-cost:    1
c ---[1097]---> BDD-cost:    1
c ---[1071]---> BDD-cost:    1
c ---[1053]---> BDD-cost:    1
c ---[1027]---> BDD-cost:    1
c ---[1013]---> BDD-cost:    1
c ---[ 987]---> BDD-cost:    1
c ---[ 965]---> BDD-cost:    1
c ---[ 955]---> BDD-cost:    1
c ---[ 938]---> BDD-cost:    1
c ---[ 916]---> BDD-cost:    1
c ---[ 890]---> BDD-cost:    1
c ---[ 884]---> BDD-cost:    1
c ---[ 882]---> BDD-cost:    1
c ---[ 856]---> BDD-cost:    1
c ---[ 838]---> BDD-cost:    1
c ---[ 812]---> BDD-cost:    1
c ---[ 763]---> BDD-cost:    1
c ---[ 753]---> BDD-cost:    1
c ---[ 743]---> BDD-cost:    1
c ---[ 741]---> BDD-cost:    1
c ---[ 739]---> BDD-cost:    1
c ---[ 713]---> BDD-cost:    1
c ---[ 695]---> BDD-cost:    1
c ---[ 669]---> BDD-cost:    1
c ---[ 667]---> BDD-cost:    1
c ---[ 641]---> BDD-cost:    1
c ---[ 623]---> BDD-cost:    1
c ---[ 597]---> BDD-cost:    1
c ---[ 579]---> BDD-cost:    1
c ---[ 557]---> BDD-cost:    1
c ---[ 531]---> BDD-cost:    1
c ---[ 525]---> BDD-cost:    1
c ---[ 515]---> BDD-cost:    1
c ---[ 505]---> BDD-cost:    1
c ---[ 455]---> BDD-cost:    1
c ---[ 453]---> BDD-cost:    1
c ---[ 447]---> BDD-cost:    1
c ---[ 430]---> BDD-cost:    1
c ---[ 392]---> BDD-cost:    1
c ---[ 382]---> BDD-cost:    1
c ---[ 364]---> BDD-cost:    1
c ---[ 342]---> BDD-cost:    1
c ---[ 316]---> BDD-cost:    1
c ---[ 310]---> BDD-cost:    1
c ---[ 308]---> BDD-cost:    1
c ---[ 282]---> BDD-cost:    1
c ---[ 264]---> BDD-cost:    1
c ---[ 238]---> BDD-cost:    1
c ---[ 185]---> BDD-cost:    1
c ---[ 175]---> BDD-cost:    1
c ---[ 169]---> BDD-cost:    1
c ---[ 167]---> BDD-cost:    1
c ---[ 153]---> BDD-cost:    1
c ---[ 127]---> BDD-cost:    1
c ---[ 105]---> BDD-cost:    1
c ---[  95]---> BDD-cost:    1
c ---[  85]---> BDD-cost:    1
c ---[  76]---> BDD-cost:    1
c ---[  26]---> BDD-cost:    1
c ---[  24]---> BDD-cost:    1
c ---[  23]---> BDD-cost:  127
c ---[  22]---> BDD-cost:  127
c ---[  21]---> BDD-cost:  127
c ---[  20]---> BDD-cost:  127
c ---[  19]---> BDD-cost:  127
c ---[  18]---> BDD-cost:  127
c ---[  17]---> BDD-cost:  127
c ---[  16]---> BDD-cost:  127
c ---[  15]---> BDD-cost:  127
c ---[  14]---> BDD-cost:  127
c ---[  13]---> BDD-cost:  127
c ---[  12]---> BDD-cost:  127
c ---[  11]---> BDD-cost:  127
c ---[  10]---> BDD-cost:  127
c ---[   9]---> BDD-cost:  127
c ---[   8]---> BDD-cost:  127
c ---[   7]---> BDD-cost:  127
c ---[   6]---> BDD-cost:  127
c ---[   5]---> BDD-cost:  127
c ---[   4]---> BDD-cost:  127
c ---[   3]---> BDD-cost:  127
c ---[   2]---> BDD-cost:  127
c ---[   1]---> BDD-cost:  127
c ---[   0]---> BDD-cost:  127
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   10760    31100 |    3227       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/3864          
c   -- var.elim.:  2000/3864          
c   -- var.elim.:  3000/3864          
c   -- var.elim.:  3864/3864          
c   -- var.elim.:  336/336          
c   -- subsuming                       
c   -- var.elim.:  216/216          
c   -- var.elim.:  264/264          
c   -- subsuming                       
c |         0 |   10616    30604 |      --       0       --      -- |     --   | -144/-144
c |         0 |   10616    30604 |    4246       0        0     nan |  0.000 % |
c |       100 |   10616    30604 |    4671     100     1811    18.1 |  4.222 % |
c |       251 |   10616    30604 |    5138     251     5315    21.2 |  4.222 % |
c |       478 |   10595    30539 |    5640     476    10709    22.5 |  4.377 % |
c |       815 |   10595    30539 |    6204     813    26961    33.2 |  4.377 % |
c |      1324 |   10595    30539 |    6825    1322    44768    33.9 |  4.377 % |
c |      2084 |   10595    30539 |    7507    2082    69876    33.6 |  4.377 % |
c |      3223 |   10595    30539 |    8258    3221   134511    41.8 |  4.377 % |
c |      4932 |   10583    30504 |    9074    4919   206922    42.1 |  4.480 % |
c |      7497 |   10583    30504 |    9981    7484   428143    57.2 |  4.480 % |
c ==============================================================================
c (current CPU-time: 4.36134 s)
c ==============================================================================
c [1mFound solution: 72[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:38806     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     11279 |   55009   134038 |   16502   11266   657482    58.4 |  4.480 % |
c   -- subsuming                       
c   -- var.elim.:  1000/29931          
c   -- var.elim.:  2000/29931          
c   -- var.elim.:  3000/29931          
c   -- var.elim.:  4000/29931          
c   -- var.elim.:  5000/29931          
c   -- var.elim.:  6000/29931          
c   -- var.elim.:  7000/29931          
c   -- var.elim.:  8000/29931          
c   -- var.elim.:  9000/29931          
c   -- var.elim.:  10000/29931          
c   -- var.elim.:  11000/29931          
c   -- var.elim.:  12000/29931          
c   -- var.elim.:  13000/29931          
c   -- var.elim.:  14000/29931          
c   -- var.elim.:  15000/29931          
c   -- var.elim.:  16000/29931          
c   -- var.elim.:  17000/29931          
c   -- var.elim.:  18000/29931          
c   -- var.elim.:  19000/29931          
c   -- var.elim.:  20000/29931          
c   -- var.elim.:  21000/29931          
c   -- var.elim.:  22000/29931          
c   -- var.elim.:  23000/29931          
c   -- var.elim.:  24000/29931          
c   -- var.elim.:  25000/29931          
c   -- var.elim.:  26000/29931          
c   -- var.elim.:  27000/29931          
c   -- var.elim.:  28000/29931          
c   -- var.elim.:  29000/29931          
c   -- var.elim.:  29931/29931          
c   -- var.elim.:  1000/14811          
c   -- var.elim.:  2000/14811          
c   -- var.elim.:  3000/14811          
c   -- var.elim.:  4000/14811          
c   -- var.elim.:  5000/14811          
c   -- var.elim.:  6000/14811          
c   -- var.elim.:  7000/14811          
c   -- var.elim.:  8000/14811          
c   -- var.elim.:  9000/14811          
c   -- var.elim.:  10000/14811          
c   -- var.elim.:  11000/14811          
c   -- var.elim.:  12000/14811          
c   -- var.elim.:  13000/14811          
c   -- var.elim.:  14000/14811          
c   -- var.elim.:  14811/14811          
c   -- var.elim.:  1000/3251          
c   -- var.elim.:  2000/3251          
c   -- var.elim.:  3000/3251          
c   -- var.elim.:  3251/3251          
c   -- var.elim.:  1000/6247          
c   -- var.elim.:  2000/6247          
c   -- var.elim.:  3000/6247          
c   -- var.elim.:  4000/6247          
c   -- var.elim.:  5000/6247          
c   -- var.elim.:  6000/6247          
c   -- var.elim.:  6247/6247          
c   -- var.elim.:  1000/2328          
c   -- var.elim.:  2000/2328          
c   -- var.elim.:  2328/2328          
c   -- var.elim.:  1000/1029          
c   -- var.elim.:  1029/1029          
c   -- subsuming                       
c   -- var.elim.:  1000/12836          
c   -- var.elim.:  2000/12836          
c   -- var.elim.:  3000/12836          
c   -- var.elim.:  4000/12836          
c   -- var.elim.:  5000/12836          
c   -- var.elim.:  6000/12836          
c   -- var.elim.:  7000/12836          
c   -- var.elim.:  8000/12836          
c   -- var.elim.:  9000/12836          
c   -- var.elim.:  10000/12836          
c   -- var.elim.:  11000/12836          
c   -- var.elim.:  12000/12836          
c   -- var.elim.:  12836/12836          
c   -- var.elim.:  1000/5897          
c   -- var.elim.:  2000/5897          
c   -- var.elim.:  3000/5897          
c   -- var.elim.:  4000/5897          
c   -- var.elim.:  5000/5897          
c   -- var.elim.:  5897/5897          
c   -- var.elim.:  1000/6229          
c   -- var.elim.:  2000/6229          
c   -- var.elim.:  3000/6229          
c   -- var.elim.:  4000/6229          
c   -- var.elim.:  5000/6229          
c   -- var.elim.:  6000/6229          
c   -- var.elim.:  6229/6229          
c   -- var.elim.:  1000/6840          
c   -- var.elim.:  2000/6840          
c   -- var.elim.:  3000/6840          
c   -- var.elim.:  4000/6840          
c   -- var.elim.:  5000/6840          
c   -- var.elim.:  6000/6840          
c   -- var.elim.:  6840/6840          
c   -- var.elim.:  1000/2248          
c   -- var.elim.:  2000/2248          
c   -- var.elim.:  2248/2248          
c   -- var.elim.:  883/883          
c   -- subsuming                       
c   -- var.elim.:  1000/7181          
c   -- var.elim.:  2000/7181          
c   -- var.elim.:  3000/7181          
c   -- var.elim.:  4000/7181          
c   -- var.elim.:  5000/7181          
c   -- var.elim.:  6000/7181          
c   -- var.elim.:  7000/7181          
c   -- var.elim.:  7181/7181          
c   -- var.elim.:  1000/5183          
c   -- var.elim.:  2000/5183          
c   -- var.elim.:  3000/5183          
c   -- var.elim.:  4000/5183          
c   -- var.elim.:  5000/5183          
c   -- var.elim.:  5183/5183          
c   -- var.elim.:  1000/4634          
c   -- var.elim.:  2000/4634          
c   -- var.elim.:  3000/4634          
c   -- var.elim.:  4000/4634          
c   -- var.elim.:  4634/4634          
c   -- var.elim.:  1000/3262          
c   -- var.elim.:  2000/3262          
c   -- var.elim.:  3000/3262          
c   -- var.elim.:  3262/3262          
c   -- subsuming                       
c   -- var.elim.:  1000/5400          
c   -- var.elim.:  2000/5400          
c   -- var.elim.:  3000/5400          
c   -- var.elim.:  4000/5400          
c   -- var.elim.:  5000/5400          
c   -- var.elim.:  5400/5400          
c   -- var.elim.:  1000/3229          
c   -- var.elim.:  2000/3229          
c   -- var.elim.:  3000/3229          
c   -- var.elim.:  3229/3229          
c   -- var.elim.:  1000/1030          
c   -- var.elim.:  1030/1030          
c   -- subsuming                       
c   -- var.elim.:  1000/2855          
c   -- var.elim.:  2000/2855          
c   -- var.elim.:  2855/2855          
c   -- var.elim.:  1000/1248          
c   -- var.elim.:  1248/1248          
c |     11279 |   38632   214914 |      --   11266       --      -- |     --   | -16366/80909
c |     11279 |   38632   214914 |   15452    8508   410211    48.2 |  4.480 % |
c |     11379 |   38632   214914 |   16998    8608   412431    47.9 |  1.097 % |
c |     11529 |   38632   214914 |   18697    8758   417949    47.7 |  1.097 % |
c |     11755 |   38632   214914 |   20567    8984   424275    47.2 |  1.097 % |
c |     12092 |   38551   214416 |   22577    8594   413203    48.1 |  1.180 % |
c |     12603 |   38551   214416 |   24834    9105   438722    48.2 |  1.180 % |
c |     13364 |   38489   214225 |   27274    9853   467044    47.4 |  1.292 % |
c |     14504 |   38489   214225 |   30001   10993   526154    47.9 |  1.292 % |
c |     16216 |   38414   213935 |   32937   12655   654668    51.7 |  1.404 % |
c |     18780 |   38343   213288 |   36164   14878   841581    56.6 |  1.434 % |
c |     22626 |   38251   210398 |   39685   18636  1128110    60.5 |  1.505 % |
c |     28397 |   37825   206754 |   43167   24350  1530858    62.9 |  1.971 % |
c |     37047 |   37305   204066 |   46831   32436  2130080    65.7 |  2.360 % |
c |     50021 |   36792   199835 |   50806   43077  2968732    68.9 |  2.791 % |
c ==============================================================================
c (current CPU-time: 162.491 s)
c ==============================================================================
c [1mFound solution: 70[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:32582     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     55273 |   73919   285718 |   22175   34371  2286076    66.5 |  2.791 % |
c   -- subsuming                       
c   -- var.elim.:  1000/32950          
c   -- var.elim.:  2000/32950          
c   -- var.elim.:  3000/32950          
c   -- var.elim.:  4000/32950          
c   -- var.elim.:  5000/32950          
c   -- var.elim.:  6000/32950          
c   -- var.elim.:  7000/32950          
c   -- var.elim.:  8000/32950          
c   -- var.elim.:  9000/32950          
c   -- var.elim.:  10000/32950          
c   -- var.elim.:  11000/32950          
c   -- var.elim.:  12000/32950          
c   -- var.elim.:  13000/32950          
c   -- var.elim.:  14000/32950          
c   -- var.elim.:  15000/32950          
c   -- var.elim.:  16000/32950          
c   -- var.elim.:  17000/32950          
c   -- var.elim.:  18000/32950          
c   -- var.elim.:  19000/32950          
c   -- var.elim.:  20000/32950          
c   -- var.elim.:  21000/32950          
c   -- var.elim.:  22000/32950          
c   -- var.elim.:  23000/32950          
c   -- var.elim.:  24000/32950          
c   -- var.elim.:  25000/32950          
c   -- var.elim.:  26000/32950          
c   -- var.elim.:  27000/32950          
c   -- var.elim.:  28000/32950          
c   -- var.elim.:  29000/32950          
c   -- var.elim.:  30000/32950          
c   -- var.elim.:  31000/32950          
c   -- var.elim.:  32000/32950          
c   -- var.elim.:  32950/32950          
c   -- var.elim.:  1000/17295          
c   -- var.elim.:  2000/17295          
c   -- var.elim.:  3000/17295          
c   -- var.elim.:  4000/17295          
c   -- var.elim.:  5000/17295          
c   -- var.elim.:  6000/17295          
c   -- var.elim.:  7000/17295          
c   -- var.elim.:  8000/17295          
c   -- var.elim.:  9000/17295          
c   -- var.elim.:  10000/17295          
c   -- var.elim.:  11000/17295          
c   -- var.elim.:  12000/17295          
c   -- var.elim.:  13000/17295          
c   -- var.elim.:  14000/17295          
c   -- var.elim.:  15000/17295          
c   -- var.elim.:  16000/17295          
c   -- var.elim.:  17000/17295          
c   -- var.elim.:  17295/17295          
c   -- var.elim.:  1000/10104          
c   -- var.elim.:  2000/10104          
c   -- var.elim.:  3000/10104          
c   -- var.elim.:  4000/10104          
c   -- var.elim.:  5000/10104          
c   -- var.elim.:  6000/10104          
c   -- var.elim.:  7000/10104          
c   -- var.elim.:  8000/10104          
c   -- var.elim.:  9000/10104          
c   -- var.elim.:  10000/10104          
c   -- var.elim.:  10104/10104          
c   -- var.elim.:  1000/10328          
c   -- var.elim.:  2000/10328          
c   -- var.elim.:  3000/10328          
c   -- var.elim.:  4000/10328          
c   -- var.elim.:  5000/10328          
c   -- var.elim.:  6000/10328          
c   -- var.elim.:  7000/10328          
c   -- var.elim.:  8000/10328          
c   -- var.elim.:  9000/10328          
c   -- var.elim.:  10000/10328          
c   -- var.elim.:  10328/10328          
c   -- var.elim.:  1000/6784          
c   -- var.elim.:  2000/6784          
c   -- var.elim.:  3000/6784          
c   -- var.elim.:  4000/6784          
c   -- var.elim.:  5000/6784          
c   -- var.elim.:  6000/6784          
c   -- var.elim.:  6784/6784          
c   -- var.elim.:  1000/3079          
c   -- var.elim.:  2000/3079          
c   -- var.elim.:  3000/3079          
c   -- var.elim.:  3079/3079          
c   -- var.elim.:  1000/2500          
c   -- var.elim.:  2000/2500          
c   -- var.elim.:  2500/2500          
c   -- subsuming                       
c   -- var.elim.:  1000/17450          
c   -- var.elim.:  2000/17450          
c   -- var.elim.:  3000/17450          
c   -- var.elim.:  4000/17450          
c   -- var.elim.:  5000/17450          
c   -- var.elim.:  6000/17450          
c   -- var.elim.:  7000/17450          
c   -- var.elim.:  8000/17450          
c   -- var.elim.:  9000/17450          
c   -- var.elim.:  10000/17450          
c   -- var.elim.:  11000/17450          
c   -- var.elim.:  12000/17450          
c   -- var.elim.:  13000/17450          
c   -- var.elim.:  14000/17450          
c   -- var.elim.:  15000/17450          
c   -- var.elim.:  16000/17450          
c   -- var.elim.:  17000/17450          
c   -- var.elim.:  17450/17450          
c   -- var.elim.:  1000/8873          
c   -- var.elim.:  2000/8873          
c   -- var.elim.:  3000/8873          
c   -- var.elim.:  4000/8873          
c   -- var.elim.:  5000/8873          
c   -- var.elim.:  6000/8873          
c   -- var.elim.:  7000/8873          
c   -- var.elim.:  8000/8873          
c   -- var.elim.:  8873/8873          
c   -- var.elim.:  1000/9697          
c   -- var.elim.:  2000/9697          
c   -- var.elim.:  3000/9697          
c   -- var.elim.:  4000/9697          
c   -- var.elim.:  5000/9697          
c   -- var.elim.:  6000/9697          
c   -- var.elim.:  7000/9697          
c   -- var.elim.:  8000/9697          
c   -- var.elim.:  9000/9697          
c   -- var.elim.:  9697/9697          
c   -- var.elim.:  1000/11664          
c   -- var.elim.:  2000/11664          
c   -- var.elim.:  3000/11664          
c   -- var.elim.:  4000/11664          
c   -- var.elim.:  5000/11664          
c   -- var.elim.:  6000/11664          
c   -- var.elim.:  7000/11664          
c   -- var.elim.:  8000/11664          
c   -- var.elim.:  9000/11664          
c   -- var.elim.:  10000/11664          
c   -- var.elim.:  11000/11664          
c   -- var.elim.:  11664/11664          
c   -- var.elim.:  1000/7693          
c   -- var.elim.:  2000/7693          
c   -- var.elim.:  3000/7693          
c   -- var.elim.:  4000/7693          
c   -- var.elim.:  5000/7693          
c   -- var.elim.:  6000/7693          
c   -- var.elim.:  7000/7693          
c   -- var.elim.:  7693/7693          
c   -- var.elim.:  1000/1605          
c   -- var.elim.:  1605/1605          
c   -- var.elim.:  58/58          
c   -- subsuming                       
c   -- var.elim.:  1000/12421          
c   -- var.elim.:  2000/12421          
c   -- var.elim.:  3000/12421          
c   -- var.elim.:  4000/12421          
c   -- var.elim.:  5000/12421          
c   -- var.elim.:  6000/12421          
c   -- var.elim.:  7000/12421          
c   -- var.elim.:  8000/12421          
c   -- var.elim.:  9000/12421          
c   -- var.elim.:  10000/12421          
c   -- var.elim.:  11000/12421          
c   -- var.elim.:  12000/12421          
c   -- var.elim.:  12421/12421          
c   -- var.elim.:  1000/4984          
c   -- var.elim.:  2000/4984          
c   -- var.elim.:  3000/4984          
c   -- var.elim.:  4000/4984          
c   -- var.elim.:  4984/4984          
c   -- var.elim.:  1000/3973          
c   -- var.elim.:  2000/3973          
c   -- var.elim.:  3000/3973          
c   -- var.elim.:  3973/3973          
c   -- var.elim.:  1000/4614          
c   -- var.elim.:  2000/4614          
c   -- var.elim.:  3000/4614          
c   -- var.elim.:  4000/4614          
c   -- var.elim.:  4614/4614          
c   -- var.elim.:  317/317          
c   -- subsuming                       
c   -- var.elim.:  1000/5742          
c   -- var.elim.:  2000/5742          
c   -- var.elim.:  3000/5742          
c   -- var.elim.:  4000/5742          
c   -- var.elim.:  5000/5742          
c   -- var.elim.:  5742/5742          
c   -- var.elim.:  1000/5039          
c   -- var.elim.:  2000/5039          
c   -- var.elim.:  3000/5039          
c   -- var.elim.:  4000/5039          
c   -- var.elim.:  5000/5039          
c   -- var.elim.:  5039/5039          
c   -- var.elim.:  1000/2523          
c   -- var.elim.:  2000/2523          
c   -- var.elim.:  2523/2523          
c   -- var.elim.:  914/914          
c   -- subsuming                       
c   -- var.elim.:  1000/5341          
c   -- var.elim.:  2000/5341          
c   -- var.elim.:  3000/5341          
c   -- var.elim.:  4000/5341          
c   -- var.elim.:  5000/5341          
c   -- var.elim.:  5341/5341          
c   -- var.elim.:  1000/3285          
c   -- var.elim.:  2000/3285          
c   -- var.elim.:  3000/3285          
c   -- var.elim.:  3285/3285          
c   -- subsuming                       
c   -- var.elim.:  1000/2756          
c   -- var.elim.:  2000/2756          
c   -- var.elim.:  2756/2756          
c |     55273 |   56633   341819 |      --   34371       --      -- |     --   | -17283/56108
c |     55273 |   56633   341819 |   22653   34371  2286076    66.5 |  2.791 % |
c |     55373 |   56603   341496 |   24905    3608   100012    27.7 |  2.188 % |
c |     55524 |   56603   341496 |   27395    3759   108855    29.0 |  2.188 % |
c |     55752 |   56559   340965 |   30112    3981   122190    30.7 |  2.196 % |
c |     56094 |   56559   340965 |   33123    4323   141629    32.8 |  2.196 % |
c |     56600 |   56484   340473 |   36387    4801   166158    34.6 |  2.250 % |
c |     57364 |   56459   340231 |   40008    5564   220583    39.6 |  2.289 % |
c |     58504 |   56375   339536 |   43943    6679   315788    47.3 |  2.412 % |
c ==============================================================================
c [1mOptimal solution: 70[0m
s OPTIMUM FOUND
v -v1 v2 v3 -v4 -v5 -v6 -v7 -v8 -v9 -v10 -v11 -v12 -v13 -v14 -v15 v16 -v17 -v18 -v19 -v20 -v21 -v22 -v23 -v24 -v25 -v26 -v27 -v28 -v29 -v30 -v31 v32 -v33 -v34 -v35 -v36 -v37 -v38 -v39 -v40 -v41 -v42 -v43 -v44 -v45 -v46 -v47 -v48 -v49 -v50 -v51 -v52 -v53 -v54 -v55 -v56 -v57 -v58 v59 v60 -v61 v62 -v63 -v64 -v65 v66 -v67 -v68 -v69 v70 -v71 -v72 -v73 -v74 -v75 -v76 -v77 -v78 -v79 -v80 v81 -v82 -v83 -v84 -v85 -v86 -v87 -v88 -v89 -v90 -v91 -v92 -v93 -v94 v95 -v96 -v97 -v98 -v99 -v100 v101 -v102 -v103 -v104 -v105 -v106 -v107 -v108 -v109 -v110 -v111 -v112 -v113 v114 -v115 -v116 -v117 -v118 -v119 -v120 -v121 -v122 -v123 -v124 -v125 -v126 -v127 -v128 -v129 -v130 -v131 -v132 -v133 -v134 -v135 -v136 -v137 -v138 -v139 v140 -v141 -v142 -v143 -v144 -v145 -v146 -v147 -v148 -v149 v150 -v151 -v152 -v153 -v154 -v155 -v156 -v157 -v158 -v159 -v160 -v161 -v162 v163 -v164 -v165 -v166 -v167 -v168 -v169 -v170 -v171 -v172 -v173 -v174 -v175 -v176 -v177 -v178 -v179 -v180 -v181 -v182 -v183 -v184 -v185 -v186 -v187 v188 -v189 -v190 -v191 -v192 v193 -v194 -v195 -v196 v197 v198 -v199 -v200 -v201 -v202 -v203 -v204 -v205 v206 -v207 -v208 -v209 -v210 -v211 v212 -v213 -v214 -v215 -v216 -v217 -v218 -v219 -v220 -v221 -v222 -v223 -v224 -v225 -v226 -v227 -v228 v229 -v230 -v231 -v232 v233 -v234 -v235 -v236 v237 -v238 -v239 -v240 -v241 -v242 -v243 -v244 -v245 v246 -v247 -v248 -v249 -v250 -v251 -v252 -v253 -v254 -v255 v256 -v257 -v258 -v259 -v260 -v261 -v262 -v263 -v264 -v265 -v266 -v267 -v268 v269 -v270 -v271 -v272 -v273 -v274 -v275 -v276 -v277 -v278 v279 -v280 -v281 -v282 -v283 -v284 -v285 -v286 -v287 -v288 -v289 -v290 -v291 -v292 -v293 -v294 -v295 -v296 v297 -v298 -v299 -v300 -v301 -v302 v303 -v304 -v305 -v306 v307 -v308 -v309 -v310 -v311 -v312 -v313 -v314 -v315 -v316 -v317 -v318 -v319 -v320 -v321 -v322 v323 -v324 -v325 -v326 -v327 -v328 -v329 -v330 -v331 -v332 -v333 v334 -v335 -v336 v337 -v338 -v339 -v340 -v341 -v342 -v343 -v344 -v345 -v346 -v347 -v348 -v349 -v350 -v351 -v352 -v353 -v354 -v355 -v356 -v357 -v358 -v359 -v360 -v361 -v362 -v363 -v364 -v365 -v366 -v367 -v368 -v369 -v370 -v371 v372 -v373 -v374 -v375 -v376 -v377 -v378 v379 -v380 -v381 -v382 v383 -v384 -v385 -v386 -v387 -v388 -v389 -v390 -v391 -v392 -v393 v394 -v395 -v396 -v397 -v398 -v399 -v400 -v401 -v402 -v403 -v404 -v405 -v406 -v407 -v408 v409 -v410 -v411 -v412 -v413 -v414 -v415 v416 -v417 -v418 -v419 -v420 -v421 v422 -v423 -v424 -v425 v426 -v427 -v428 -v429 -v430 -v431 -v432 -v433 -v434 -v435 v436 -v437 -v438 -v439 -v440 -v441 -v442 -v443 -v444 -v445 -v446 -v447 -v448 v449 -v450 -v451 -v452 v453 -v454 -v455 -v456 -v457 -v458 -v459 -v460 -v461 -v462 -v463 -v464 -v465 v466 v467 -v468 -v469 -v470 -v471 -v472 v473 -v474 -v475 -v476 v477 -v478 -v479 -v480 -v481 -v482 -v483 -v484 -v485 -v486 v487 v488 -v489 -v490 -v491 v492 -v493 -v494 -v495 -v496 -v497 -v498 -v499 -v500 -v501 -v502 v503 -v504 -v505 -v506 v507 -v508 -v509 -v510 -v511 -v512 -v513 -v514 -v515 -v516 -v517 -v518 -v519 v520 -v521 -v522 -v523 -v524 -v525 -v526 -v527 -v528 -v529 -v530 -v531 -v532 -v533 -v534 -v535 -v536 -v537 -v538 -v539 -v540 -v541 -v542 -v543 -v544 -v545 -v546 -v547 -v548 -v549 v550 -v551 -v552 -v553 -v554 -v555 -v556 -v557 -v558 -v559 -v560 -v561 -v562 -v563 -v564 -v565 -v566 -v567 -v568 -v569 -v570 -v571 -v572 -v573 -v574 -v575 v576 -v577 -v578 v579 -v580 -v581 -v582 -v583 -v584 -v585 -v586 -v587 -v588 -v589 -v590 v591 -v592 -v593 -v594 -v595 -v596 -v597 -v598 -v599 -v600 -v601 -v602 -v603 -v604 -v605 -v606 -v607 -v608 -v609 -v610 -v611 -v612 -v613 -v614 -v615 -v616 -v617 -v618 -v619 -v620 -v621 -v622 -v623 v624 -v625 -v626 -v627 -v628 -v629 -v630 -v631 -v632 -v633 -v634 -v635 -v636 -v637 -v638 -v639 -v640 -v641 -v642 -v643 -v644 -v645 -v646 -v647 v648 -v649 -v650 -v651 -v652 -v653 -v654 -v655 -v656 -v657 v658 -v659 -v660 -v661 -v662 -v663 -v664 -v665 -v666 -v667 -v668 -v669 -v670 -v671 -v672 -v673 -v674 -v675 -v676 -v677 -v678 -v679 -v680 -v681 -v682 -v683 -v684 v685 -v686 -v687 -v688 -v689 -v690 -v691 -v692 -v693 -v694 -v695 -v696 -v697 -v698 -v699 -v700 -v701 -v702 -v703 -v704 v705 -v706 -v707 -v708 -v709 -v710 -v711 -v712 -v713 -v714 -v715 -v716 -v717 -v718 -v719 -v720 -v721 v722 -v723 -v724 -v725 -v726 -v727 -v728 -v729 -v730 -v731 -v732 -v733 -v734 -v735 -v736 -v737 -v738 -v739 -v740 -v741 -v742 -v743 -v744 -v745 -v746 -v747 -v748 -v749 -v750 -v751 -v752 -v753 -v754 -v755 -v756 v757 -v758 -v759 -v760 -v761 -v762 -v763 -v764 -v765 -v766 -v767 -v768 -v769 -v770 -v771 v772 -v773 -v774 -v775 -v776 -v777 -v778 -v779 -v780 -v781 -v782 -v783 -v784 -v785 -v786 -v787 -v788 -v789 -v790 -v791 -v792 -v793 v794 -v795 -v796 -v797 -v798 -v799 -v800 -v801 -v802 -v803 -v804 -v805 -v806 -v807 -v808 -v809 -v810 -v811 -v812 -v813 -v814 -v815 -v816 -v817 -v818 -v819 v820 -v821 -v822 -v823 -v824 -v825 -v826 -v827 -v828 -v829 -v830 -v831 -v832 -v833 -v834 -v835 -v836 -v837 -v838 -v839 -v840
c _______________________________________________________________________________
c 
c restarts              : 32
c conflicts             : 60147          (188 /sec)
c decisions             : 129122         (403 /sec)
c propagations          : 14279950       (44567 /sec)
c inspects              : 95136306       (296917 /sec)
c CPU time              : 320.414 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.98 0.91 2/54 24080
Raw data (stat): 24080 (runsolver) R 24079 20937 20936 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 422069397 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.0003 s]
Raw data (loadavg): 0.94 0.98 0.91 2/54 24080
Raw data (stat): 24080 (minisat+) R 24079 20937 20936 0 -1 0 5656 0 0 0 978 20 0 0 25 0 1 0 422069397 27516928 5464 4294967295 134512640 134672761 3221224560 3221222864 134621829 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6718 5464 603 41 0 6677 0
vsize: 26872
[startup+20.0006 s]
Raw data (loadavg): 0.95 0.98 0.91 2/54 24080
Raw data (stat): 24080 (minisat+) R 24079 20937 20936 0 -1 0 5727 0 0 0 1977 21 0 0 25 0 1 0 422069397 27783168 5535 4294967295 134512640 134672761 3221224560 3221223008 134644032 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6783 5535 603 41 0 6742 0
vsize: 27132
[startup+30.0008 s]
Raw data (loadavg): 0.95 0.98 0.91 2/54 24080
Raw data (stat): 24080 (minisat+) R 24079 20937 20936 0 -1 0 5778 0 0 0 2975 24 0 0 25 0 1 0 422069397 28049408 5586 4294967295 134512640 134672761 3221224560 3221223008 134643565 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6848 5586 603 41 0 6807 0
vsize: 27392
[startup+40.0014 s]
Raw data (loadavg): 0.96 0.98 0.91 2/54 24080
Raw data (stat): 24080 (minisat+) R 24079 20937 20936 0 -1 0 5957 0 0 0 3973 25 0 0 25 0 1 0 422069397 29016064 5763 4294967295 134512640 134672761 3221224560 3221223056 134606420 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7084 5763 603 41 0 7043 0
vsize: 28336
[startup+50.0017 s]
Raw data (loadavg): 0.97 0.98 0.91 2/54 24080
Raw data (stat): 24080 (minisat+) R 24079 20937 20936 0 -1 0 5958 0 0 0 4973 25 0 0 25 0 1 0 422069397 29016064 5764 4294967295 134512640 134672761 3221224560 3221223104 134621086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7084 5764 603 41 0 7043 0
vsize: 28336
[startup+60.0017 s]
Raw data (loadavg): 0.97 0.98 0.91 2/54 24080
Raw data (stat): 24080 (minisat+) R 24079 20937 20936 0 -1 0 5958 0 0 0 5970 27 0 0 25 0 1 0 422069397 28049408 5617 4294967295 134512640 134672761 3221224560 3221223008 134643542 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6848 5617 603 41 0 6807 0
vsize: 27392
[startup+70.0024 s]
Raw data (loadavg): 0.97 0.98 0.91 2/54 24080
Raw data (stat): 24080 (minisat+) R 24079 20937 20936 0 -1 0 5958 0 0 0 6969 29 0 0 25 0 1 0 422069397 28049408 5617 4294967295 134512640 134672761 3221224560 3221223008 134643542 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6848 5617 603 41 0 6807 0
vsize: 27392
[startup+80.0028 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 24080
Raw data (stat): 24080 (minisat+) R 24079 20937 20936 0 -1 0 6066 0 0 0 7968 30 0 0 25 0 1 0 422069397 28049408 5617 4294967295 134512640 134672761 3221224560 3221223008 134643969 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6848 5617 603 41 0 6807 0
vsize: 27392
[startup+90.0028 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 24080
Raw data (stat): 24080 (minisat+) R 24079 20937 20936 0 -1 0 6066 0 0 0 8967 31 0 0 25 0 1 0 422069397 28049408 5617 4294967295 134512640 134672761 3221224560 3221223008 134643583 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6848 5617 603 41 0 6807 0
vsize: 27392
[startup+100.002 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 24080
Raw data (stat): 24080 (minisat+) R 24079 20937 20936 0 -1 0 6174 0 0 0 9967 32 0 0 25 0 1 0 422069397 28049408 5617 4294967295 134512640 134672761 3221224560 3221223008 134643539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6848 5617 603 41 0 6807 0
vsize: 27392
[startup+110.002 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 24080
Raw data (stat): 24080 (minisat+) R 24079 20937 20936 0 -1 0 6282 0 0 0 10967 32 0 0 25 0 1 0 422069397 28049408 5617 4294967295 134512640 134672761 3221224560 3221223744 134615671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6848 5617 603 41 0 6807 0
vsize: 27392
[startup+120.002 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 24080
Raw data (stat): 24080 (minisat+) R 24079 20937 20936 0 -1 0 7118 0 0 0 11964 35 0 0 25 0 1 0 422069397 31600640 6453 4294967295 134512640 134672761 3221224560 3221223704 134616347 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7715 6453 603 41 0 7674 0
vsize: 30860
[startup+130.002 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 24080
Raw data (stat): 24080 (minisat+) R 24079 20937 20936 0 -1 0 7794 0 0 0 12962 37 0 0 25 0 1 0 422069397 34242560 7129 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8360 7129 603 41 0 8319 0
vsize: 33440
[startup+140.002 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 24080
Raw data (stat): 24080 (minisat+) R 24079 20937 20936 0 -1 0 8373 0 0 0 13961 38 0 0 25 0 1 0 422069397 36749312 7708 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8972 7708 603 41 0 8931 0
vsize: 35888
[startup+150.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 24080
Raw data (stat): 24080 (minisat+) R 24079 20937 20936 0 -1 0 8732 0 0 0 14959 39 0 0 25 0 1 0 422069397 38326272 8067 4294967295 134512640 134672761 3221224560 3221223392 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9357 8067 603 41 0 9316 0
vsize: 37428
[startup+160.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 24080
Raw data (stat): 24080 (minisat+) R 24079 20937 20936 0 -1 0 9036 0 0 0 15958 41 0 0 25 0 1 0 422069397 39518208 8371 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9648 8371 603 41 0 9607 0
vsize: 38592
[startup+170.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 24080
Raw data (stat): 24080 (minisat+) R 24079 20937 20936 0 -1 0 11891 0 0 0 16941 57 0 0 25 0 1 0 422069397 46358528 10149 4294967295 134512640 134672761 3221224560 3221223008 134643583 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11318 10149 603 41 0 11277 0
vsize: 45272
[startup+180.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 24080
Raw data (stat): 24080 (minisat+) R 24079 20937 20936 0 -1 0 11960 0 0 0 17937 61 0 0 25 0 1 0 422069397 46665728 10185 4294967295 134512640 134672761 3221224560 3221223008 134643532 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11393 10185 603 41 0 11352 0
vsize: 45572
[startup+190.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 24080
Raw data (stat): 24080 (minisat+) R 24079 20937 20936 0 -1 0 11974 0 0 0 18934 64 0 0 25 0 1 0 422069397 46579712 10198 4294967295 134512640 134672761 3221224560 3221223008 134643954 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11372 10198 603 41 0 11331 0
vsize: 45488
[startup+200.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 24080
Raw data (stat): 24080 (minisat+) R 24079 20937 20936 0 -1 0 11980 0 0 0 19933 65 0 0 25 0 1 0 422069397 46579712 10204 4294967295 134512640 134672761 3221224560 3221223008 134643471 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11372 10204 603 41 0 11331 0
vsize: 45488
[startup+210.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 24080
Raw data (stat): 24080 (minisat+) R 24079 20937 20936 0 -1 0 12222 0 0 0 20932 66 0 0 25 0 1 0 422069397 48058368 10413 4294967295 134512640 134672761 3221224560 3221223024 134644266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11733 10413 603 41 0 11692 0
vsize: 46932
[startup+220.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 24080
Raw data (stat): 24080 (minisat+) R 24079 20937 20936 0 -1 0 12222 0 0 0 21932 66 0 0 25 0 1 0 422069397 48058368 10413 4294967295 134512640 134672761 3221224560 3221223104 134621107 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11733 10413 603 41 0 11692 0
vsize: 46932
[startup+230.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 24080
Raw data (stat): 24080 (minisat+) R 24079 20937 20936 0 -1 0 12257 0 0 0 22931 68 0 0 25 0 1 0 422069397 46673920 10260 4294967295 134512640 134672761 3221224560 3221223008 134643583 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11395 10260 603 41 0 11354 0
vsize: 45580
[startup+240.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 24080
Raw data (stat): 24080 (minisat+) R 24079 20937 20936 0 -1 0 12257 0 0 0 23928 71 0 0 25 0 1 0 422069397 46673920 10260 4294967295 134512640 134672761 3221224560 3221223008 134644016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11395 10260 603 41 0 11354 0
vsize: 45580
[startup+250.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 24080
Raw data (stat): 24080 (minisat+) R 24079 20937 20936 0 -1 0 12257 0 0 0 24927 72 0 0 25 0 1 0 422069397 46673920 10260 4294967295 134512640 134672761 3221224560 3221222780 1075350746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11395 10260 603 41 0 11354 0
vsize: 45580
[startup+260.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 24080
Raw data (stat): 24080 (minisat+) R 24079 20937 20936 0 -1 0 12403 0 0 0 25927 72 0 0 25 0 1 0 422069397 47722496 10406 4294967295 134512640 134672761 3221224560 3221223056 134607003 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11651 10406 603 41 0 11610 0
vsize: 46604
[startup+270.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 24080
Raw data (stat): 24080 (minisat+) R 24079 20937 20936 0 -1 0 12403 0 0 0 26927 72 0 0 25 0 1 0 422069397 47722496 10406 4294967295 134512640 134672761 3221224560 3221223104 134621211 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11651 10406 603 41 0 11610 0
vsize: 46604
[startup+280.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 24080
Raw data (stat): 24080 (minisat+) R 24079 20937 20936 0 -1 0 12403 0 0 0 27926 73 0 0 25 0 1 0 422069397 46673920 10260 4294967295 134512640 134672761 3221224560 3221223008 134643954 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11395 10260 603 41 0 11354 0
vsize: 45580
[startup+290.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 24080
Raw data (stat): 24080 (minisat+) R 24079 20937 20936 0 -1 0 12548 0 0 0 28926 74 0 0 25 0 1 0 422069397 47288320 10405 4294967295 134512640 134672761 3221224560 3221223104 134621095 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11545 10405 603 41 0 11504 0
vsize: 46180
[startup+300.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 24080
Raw data (stat): 24080 (minisat+) R 24079 20937 20936 0 -1 0 12548 0 0 0 29925 74 0 0 25 0 1 0 422069397 46673920 10260 4294967295 134512640 134672761 3221224560 3221223008 134643524 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11395 10260 603 41 0 11354 0
vsize: 45580
[startup+310.003 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 24080
Raw data (stat): 24080 (minisat+) R 24079 20937 20936 0 -1 0 12836 0 0 0 30924 75 0 0 25 0 1 0 422069397 47476736 10403 4294967295 134512640 134672761 3221224560 3221223104 134621104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11591 10403 603 41 0 11550 0
vsize: 46364
[startup+320.004 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 24080
Raw data (stat): 24080 (minisat+) R 24079 20937 20936 0 -1 0 12919 0 0 0 31924 76 0 0 25 0 1 0 422069397 46936064 10309 4294967295 134512640 134672761 3221224560 3221223684 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11459 10309 603 41 0 11418 0
vsize: 45836
[startup+321.242 s]
Raw data (loadavg): 0.99 0.98 0.91 1/53 24080
Raw data (stat): 24080 (minisat+) R 24079 20937 20936 0 -1 0 12919 0 0 0 31924 76 0 0 25 0 1 0 422069397 46936064 10309 4294967295 134512640 134672761 3221224560 3221223684 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11459 10309 603 41 0 11418 0
vsize: 0

Child status: 30
Real time (s): 321.241
CPU time (s): 321.242
CPU user time (s): 320.438
CPU system time (s): 0.803877
CPU usage (%): 100
Max. virtual memory (Kb): 46932
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	70
#### END VERIFIER DATA ####